How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Inverses of positives are positive, and reciprocation reverses order
Statement
Let be an ordered field (Ordered field) with positive cone , and let .
- If then .
- If then .
Facts & Assumptions
Given: An ordered field with positive cone , and elements .
; ; and for exactly one of , holds (Ordered field).
Sign rules: a product of a positive and a negative is negative, a product of two positives is positive, and for one has (Sign rules for products and monotonicity of multiplication).
; in particular (The multiplicative identity is positive).
is closed under addition, so is transitive (Ordered field).
Proof
Assume , so and its inverse exists with ; moreover , since has as its inverse while is non-invertible ( by L3).
By trichotomy or ; if , then and give by the sign rules, i.e. , contradicting ; hence , i.e. , proving claim 1.
Assume ; then by transitivity, so by claim 1 both and , and the sign rules give .
Multiplying by the positive via the sign rules gives ; since and , this simplifies to .
Together with from step 3.1, we conclude , proving claim 2.
Depends on
Used by
- Every nondegenerate interval of ℝ is uncountable Corollary
- For every ε > 0 in a complete ordered field there is a natural n ≥ 1 with 1/n < ε Corollary
- Kummer with ζₖ = 1 recovers the ratio test Corollary
- Limit comparison for positive improper integrals Corollary
- Stolz-Cesaro, 0/0 form: if bₖ is strictly decreasing to 0, aₖ → 0, and the difference quotient converges, then aₖ/bₖ converges to the same value Corollary
- The a priori bound d(x^*, xₙ) ≤ qⁿ d(x₁,x₀)/(1-q) and the a posteriori bound d(x^*, xₙ₊₁) ≤ q d(xₙ₊₁,xₙ)/(1-q) Corollary
- The Cesaro matrix satisfies the Silverman-Toeplitz conditions, giving a second proof of the Cesaro mean theorem Corollary
- ∏_j ≥ 0 (1 + (-1)ʲ/√j+2) has partial products tending to 0 although ∑_j ≥ 0 (-1)ʲ/√j+2 converges Counterexample
- ∑ k^-1/2 diverges and ∑ k⁻² converges, and both have root limit exactly 1 Counterexample
- ⋂ₖ (-1/k, 1/k) = {0} is not open Counterexample
- 1/x² has no finite Cauchy principal value at zero Counterexample
- A summability matrix failing exactly one Silverman-Toeplitz condition and transforming a convergent sequence to a divergent one Counterexample
- aₖ = (-1)ᵏ, bₖ = k have aₖ/bₖ → 0 while the difference quotient oscillates, so Stolz-Cesaro has no converse Counterexample
- Continuous triangular spikes on [0,1] converge pointwise to zero but not uniformly when monotonicity is absent Counterexample
- Dini's theorem fails for discontinuous approximants: shrinking interval indicators decrease pointwise to zero but not uniformly Counterexample
- Dini's theorem fails on [0,∞): x/(ι(k+1)+x) decreases pointwise to zero but not uniformly Counterexample
- fₖ(x)=xᵏ⁺¹ converges pointwise but not uniformly on [0,1] Counterexample
- g(x,y) = xy/(x²+y²), extended by g(0,0)=0, is continuous in each variable separately and not continuous at the origin Counterexample
- In ℝ(t) the rationals are not dense: no rational lies strictly between 0 and 1/t Counterexample
- Null times divergent has no rule: xₖ = 1/k with yₖ = ck gives product limit c, and with yₖ = k² gives divergence Counterexample
- On (0,∞) the metrics |x-y| and |1/x - 1/y| have the same topology and are not uniformly equivalent Counterexample
- On (0,∞) the metrics |x-y| and |1/x - 1/y| share their topology and not their Cauchy sequences Counterexample
- On (0,1) the identity is bounded with no greatest value and x ↦ 1/x is continuous and unbounded, so the extreme value theorem needs compactness and not merely boundedness of the domain Counterexample
- On A = ([0,∞) × ℝ) ∪ (ℝ × {0}) the first projection is a quotient map, by the section x ↦ (x,0), and is neither open nor closed Counterexample
- On a closed interval of ℚ there is a continuous unbounded function, a bounded one with no maximum, and one without the intermediate value property Counterexample
- On ℕ with d(m,n) = 1 + 1/(m+n) for m ≠ n the sets {n, n+1, …} are nested, closed, bounded and complete with empty intersection Counterexample
- On ℝ the metrics |x-y| and min(|x-y|,1) are uniformly but not Lipschitz equivalent Counterexample
- On the positive integers the metrics |m-n| and |1/m - 1/n| both induce the discrete topology, and only the first is complete Counterexample
- Over ℚ there is a nonconstant differentiable function with identically zero derivative, so Rolle and the mean value theorem both fail Counterexample
- ℝ covered by its closed singletons: every restriction of the indicator of {0} is continuous and the map is not, so the closed pasting lemma needs finiteness Counterexample
- Refuted: a pointwise bounded family of continuous functions is equicontinuous. The spikes are bounded by 1 everywhere and are not equicontinuous at 0 Counterexample
- Refuted: C(X,Y) is closed in the topology of pointwise convergence. The ramps on [0,1] converge pointwise to a discontinuous limit Counterexample
- Refuted: convergence uniformly on every compact subset of ℝ implies uniform convergence. The maps x ↦ x/(n+1) separate the two Counterexample
- Shrinking rectangles converge pointwise to zero while every integral equals one Counterexample
- The Cauchy product of ∑_k ≥ 0 (-1)ᵏ/√k+1 with itself has |cₙ| ≥ 1 for every n, so it diverges Counterexample
- The cover {(1/k, 1)} of (0,1) has no finite subcover, so (0,1) is not compact Counterexample
- The cover of (0,1) by the intervals (1/(k+2), 1) has no Lebesgue number, so the Lebesgue number lemma needs compactness Counterexample
- The diagonal x ↦ (x,x,…) from ℝ into ℝ^ℕ is continuous for the product topology and not for the box topology Counterexample
- The double sequence (m+1)/(m+n+2) has unequal iterated limits Counterexample
- The hyperbola {(x,y) : xy = 1} is closed in ℝ² and its image under the first projection is ℝ ∖ {0}, which is not closed Counterexample
…and 172 more results.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 7 results over 5 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 1 (standard reference, not scraped)
- M. Spivak, Calculus, 4th ed., Ch. 1 (standard reference, not scraped)
- University of Innsbruck notes: Ordered fields (standard reference, not scraped)