Alphabeta Math
Session-authored (Fable 5 assisted)
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.

29 results · all verified · 24 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 5 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Construction of the Real Numbers via Cauchy Sequences

1 · Prerequisites

2 · Summary

Objective. This page constructs the real number field R\mathbb{R} via Cauchy sequences, starting from the fundamental definitions of the integers and the rational numbers, and proves that R\mathbb{R} is a totally ordered, complete field. The natural numbers N\mathbb{N}, with their arithmetic and order, are the assumed starting point.

Layer 1: from N\mathbb{N} to Z\mathbb{Z}. Subtraction fails in N\mathbb{N}. The integers are defined as equivalence classes of pairs (a,b)(a,b) of naturals, where (a,b)(a,b) encodes the formal difference aba - b (The integers as equivalence classes of pairs of naturals), with arithmetic defined on representatives (Arithmetic on the integers). The result is a commutative ring (The integers form a commutative ring): a set with an addition and a multiplication, both associative and commutative, where multiplication distributes over addition, addition has an identity 00 and an inverse for every element, and multiplication has an identity 11. The integers also carry a total order, defined on representatives by (a,b)(c,d)(a,b) \le (c,d) exactly when a+db+ca + d \le b + c: any two integers are comparable, and the order is compatible with addition and with multiplication by nonnegative elements, so Z\mathbb{Z} is a totally ordered commutative ring.

Layer 2: from Z\mathbb{Z} to Q\mathbb{Q}. Division fails in Z\mathbb{Z}. The rationals are equivalence classes of pairs of integers with nonzero second component, encoding formal quotients a/ba/b. The result is a field: a commutative ring in which every nonzero element has a multiplicative inverse. The total order extends from Z\mathbb{Z}: any two rationals remain comparable, and the order stays compatible with the arithmetic; a field equipped with such an order is a totally ordered field.

Layer 3: from Q\mathbb{Q} to R\mathbb{R}. Limits fail in Q\mathbb{Q}: sequences such as 1,1.4,1.41,1.414,1, 1.4, 1.41, 1.414, \dots cluster ever more tightly yet converge to no rational. A Cauchy sequence is one whose terms eventually stay within any prescribed distance of one another (Cauchy sequence of rationals). The reals are equivalence classes of Cauchy sequences of rationals, two sequences being identified when their difference is a null sequence (Null sequence). Arithmetic passes to the quotient, the null sequences form a maximal ideal so that R\mathbb{R} is a field, and the order extends from Q\mathbb{Q}.

Destination. R\mathbb{R} is a totally ordered field that is complete: every Cauchy sequence of reals converges to a real. Completeness is the payoff of the construction, and the construction cannot be iterated to gain anything further: The reals are complete already gives every Cauchy sequence of reals a real limit.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-07-24Open item page →

The integers as equivalence classes of pairs of naturals

Definition

On the set N×N\mathbb{N} \times \mathbb{N} of pairs of natural numbers, define

(a,b)(c,d)    a+d=b+c.(a,b) \sim (c,d) \iff a + d = b + c.

This is an equivalence relation (The integer-defining relation is an equivalence relation ). The integers are the quotient

Z:=(N×N)/,\mathbb{Z} := (\mathbb{N} \times \mathbb{N}) / \sim,

and we write [(a,b)][(a,b)] for the equivalence class of (a,b)(a,b).

Remarks

  • The pair (a,b)(a,b) encodes the formal difference aba - b; the defining relation a+d=b+ca + d = b + c is the equation "ab=cda - b = c - d" restated using only addition, which is all N\mathbb{N} has.
  • N\mathbb{N} and its arithmetic (commutativity, associativity, distributivity, cancellation of addition, the order) are taken as given background throughout this construction.
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

The integer-defining relation is an equivalence relation

Statement

The relation (a,b)(c,d)    a+d=b+c(a,b) \sim (c,d) \iff a + d = b + c on N×N\mathbb{N} \times \mathbb{N} (The integers as equivalence classes of pairs of naturals) is an equivalence relation.

Facts & Assumptions

Given: The relation (a,b)(c,d)    a+d=b+c(a,b) \sim (c,d) \iff a + d = b + c on N×N\mathbb{N} \times \mathbb{N}.

[A1]

Addition on N\mathbb{N} is commutative and associative.

[A2]

Cancellation in N\mathbb{N}: if x+z=y+zx + z = y + z then x=yx = y.

Proof

technique · direct
1.1

Reflexivity: for any (a,b)(a,b) we have a+b=b+aa + b = b + a, so (a,b)(a,b)(a,b) \sim (a,b).

A1
1.2

Symmetry: suppose (a,b)(c,d)(a,b) \sim (c,d), i.e. a+d=b+ca + d = b + c. Then c+b=d+ac + b = d + a, which is the defining equation for (c,d)(a,b)(c,d) \sim (a,b).

A1
1.3

Suppose (a,b)(c,d)(a,b) \sim (c,d) and (c,d)(e,f)(c,d) \sim (e,f), i.e. a+d=b+ca + d = b + c and c+f=d+ec + f = d + e.

given
2.1

Adding the two equations: (a+d)+(c+f)=(b+c)+(d+e)(a + d) + (c + f) = (b + c) + (d + e).

step 1.3algebra
3.1

Regrouping both sides: (a+f)+(c+d)=(b+e)+(c+d)(a + f) + (c + d) = (b + e) + (c + d).

step 2.1A1
4.1

Cancelling (c+d)(c + d): a+f=b+ea + f = b + e, so (a,b)(e,f)(a,b) \sim (e,f); the relation is transitive.

step 3.1A2
5.1

The relation is reflexive, symmetric, and transitive, hence an equivalence relation.

step 1.1step 1.2step 4.1
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-07-24Open item page →

Arithmetic on the integers

Definition

On Z\mathbb{Z} (The integers as equivalence classes of pairs of naturals) define, on representatives,

[(a,b)]+[(c,d)]:=[(a+c,  b+d)],[(a,b)] + [(c,d)] := [(a+c,\; b+d)], [(a,b)][(c,d)]:=[(ac+bd,  ad+bc)],[(a,b)] \cdot [(c,d)] := [(ac+bd,\; ad+bc)], [(a,b)]:=[(b,a)],0:=[(0,0)],1:=[(1,0)].-[(a,b)] := [(b,a)], \qquad 0 := [(0,0)], \qquad 1 := [(1,0)].

These do not depend on the chosen representatives (Integer addition and negation are well defined , Integer multiplication is well defined ).

Remarks

  • The product formula is forced by the intended meaning: if (a,b)(a,b) stands for aba-b and (c,d)(c,d) for cdc-d, then (ab)(cd)=(ac+bd)(ad+bc)(a-b)(c-d) = (ac+bd) - (ad+bc).
  • Negation swaps the components: (ab)=ba-(a-b) = b-a.
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

Integer addition and negation are well defined

Statement

The operations [(a,b)]+[(c,d)]=[(a+c,b+d)][(a,b)] + [(c,d)] = [(a+c, b+d)] and [(a,b)]=[(b,a)]-[(a,b)] = [(b,a)] on Z\mathbb{Z} (Arithmetic on the integers) are independent of the chosen representatives.

Facts & Assumptions

Given: Pairs with (a,b)(a,b)(a,b) \sim (a',b') and (c,d)(c,d)(c,d) \sim (c',d') in the sense of The integers as equivalence classes of pairs of naturals.

[A1]

Addition on N\mathbb{N} is commutative and associative.

Proof

technique · direct
1.1

By hypothesis a+b=b+aa + b' = b + a'.

given
1.2

By hypothesis c+d=d+cc + d' = d + c'.

given
2.1

Adding the two equations: (a+b)+(c+d)=(b+a)+(d+c)(a + b') + (c + d') = (b + a') + (d + c').

step 1.1step 1.2algebra
2.2

Commuting the equation of step 1.1: b+a=a+bb + a' = a + b', which is the defining equation for (b,a)(b,a)(b,a) \sim (b',a'); negation is well defined.

step 1.1A1
3.1

Regrouping both sides: (a+c)+(b+d)=(b+d)+(a+c)(a+c) + (b'+d') = (b+d) + (a'+c'), which is the defining equation for (a+c,b+d)(a+c,b+d)(a+c,\, b+d) \sim (a'+c',\, b'+d'); addition is well defined.

step 2.1A1
4.1

Both operations are independent of representatives.

step 3.1step 2.2
LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

Integer multiplication is well defined

Statement

The operation [(a,b)][(c,d)]=[(ac+bd,ad+bc)][(a,b)] \cdot [(c,d)] = [(ac+bd,\, ad+bc)] on Z\mathbb{Z} (Arithmetic on the integers) is independent of the chosen representatives.

Facts & Assumptions

Given: Pairs with (a,b)(a,b)(a,b) \sim (a',b') and (c,d)(c,d)(c,d) \sim (c',d') in the sense of The integers as equivalence classes of pairs of naturals.

[A1]

Addition on N\mathbb{N} is commutative and associative.

[A2]

Multiplication on N\mathbb{N} is commutative.

[A3]

Distributivity in N\mathbb{N}: x(y+z)=xy+xzx(y+z) = xy + xz.

Proof

technique · direct
1.1

By hypothesis a+b=b+aa + b' = b + a'; write ss for this common value.

given
1.2

Regrouping and factoring: (ac+bd)+(ad+bc)=c(a+b)+d(b+a)(ac+bd) + (a'd+b'c) = c(a+b') + d(b+a').

A1A2A3
1.3

Regrouping and factoring: (ad+bc)+(ac+bd)=d(a+b)+c(b+a)(ad+bc) + (a'c+b'd) = d(a+b') + c(b+a').

A1A2A3
2.1

By step 1.1 both right-hand sides equal cs+dscs + ds, so (ac+bd)+(ad+bc)=(ad+bc)+(ac+bd)(ac+bd) + (a'd+b'c) = (ad+bc) + (a'c+b'd).

step 1.1step 1.2step 1.3
3.1

That equation is precisely the defining relation (ac+bd,ad+bc)(ac+bd,ad+bc)(ac+bd,\, ad+bc) \sim (a'c+b'd,\, a'd+b'c): the product class is unchanged when the first factor's representative changes.

step 2.1
4.1

The product formula is symmetric in its two arguments: swapping (a,b)(c,d)(a,b) \leftrightarrow (c,d) sends (ac+bd,ad+bc)(ac+bd,\, ad+bc) to (ca+db,cb+da)(ca+db,\, cb+da), the same pair. Hence, by the argument of steps 1.1–3.1 applied to the second factor, the product class is also unchanged when (c,d)(c,d) is replaced by (c,d)(c',d').

step 3.1A1A2
5.1

Replacing first (a,b)(a,b) by (a,b)(a',b') and then (c,d)(c,d) by (c,d)(c',d'): [(a,b)][(c,d)]=[(a,b)][(c,d)]=[(a,b)][(c,d)][(a,b)] \cdot [(c,d)] = [(a',b')] \cdot [(c,d)] = [(a',b')] \cdot [(c',d')]; multiplication is well defined.

step 3.1step 4.1
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)Open item page →

The integers form a commutative ring

Statement

(Z,+,,0,1)(\mathbb{Z}, +, \cdot, 0, 1) with the operations of Arithmetic on the integers is a commutative ring with multiplicative identity, in which every element has the additive inverse [(a,b)]=[(b,a)]-[(a,b)] = [(b,a)].

Facts & Assumptions

Given: Z\mathbb{Z} with the operations of Arithmetic on the integers.

[L1]

Addition on N\mathbb{N} is commutative and associative, with zero as a two-sided identity (Addition is commutative, Addition is associative, Left identity for addition).

[L2]

Multiplication on N\mathbb{N} is commutative and associative, distributes over addition, and has the usual zero and identity laws (Multiplication is commutative, Multiplication is associative, Distributivity and the successor law for multiplication, Zero and one under multiplication).

[L3]

The integer operations are independent of representatives (Integer addition and negation are well defined, Integer multiplication is well defined).

Proof

technique · direct
1.1

By [L3], each axiom may be verified on arbitrary fixed representatives (a,b),(c,d),(e,f)(a,b), (c,d), (e,f).

L3suffices
1.2

Associativity of ++: ((a,b)+(c,d))+(e,f)((a,b)+(c,d))+(e,f) and (a,b)+((c,d)+(e,f))(a,b)+((c,d)+(e,f)) both equal (a+c+e,  b+d+f)(a+c+e,\; b+d+f).

L1
1.3

Commutativity of ++: (a+c,b+d)=(c+a,d+b)(a+c,\, b+d) = (c+a,\, d+b).

L1
1.4

Additive identity: (a,b)+(0,0)=(a+0,b+0)=(a,b)(a,b) + (0,0) = (a+0,\, b+0) = (a,b).

L1
1.5

Additive inverses: (a,b)+(b,a)=(a+b,b+a)(0,0)(a,b) + (b,a) = (a+b,\, b+a) \sim (0,0), since (a+b)+0=(b+a)+0(a+b) + 0 = (b+a) + 0.

L1
1.6

Commutativity of \cdot: swapping (a,b)(c,d)(a,b) \leftrightarrow (c,d) sends (ac+bd,ad+bc)(ac+bd,\, ad+bc) to (ca+db,cb+da)(ca+db,\, cb+da), the same pair.

L1L2
1.7

Multiplicative identity: (a,b)(1,0)=(a1+b0,  a0+b1)=(a,b)(a,b) \cdot (1,0) = (a \cdot 1 + b \cdot 0,\; a \cdot 0 + b \cdot 1) = (a,b).

L1L2
1.8

Associativity of \cdot: expanding, both ((a,b)(c,d))(e,f)((a,b)(c,d))(e,f) and (a,b)((c,d)(e,f))(a,b)((c,d)(e,f)) equal (ace+adf+bcf+bde,  acf+ade+bce+bdf)(ace+adf+bcf+bde,\; acf+ade+bce+bdf).

L1L2
1.9

Distributivity: (a,b)((c,d)+(e,f))=(a(c+e)+b(d+f),  a(d+f)+b(c+e))=(ac+bd,ad+bc)+(ae+bf,af+be)=(a,b)(c,d)+(a,b)(e,f)(a,b) \cdot ((c,d)+(e,f)) = (a(c+e)+b(d+f),\; a(d+f)+b(c+e)) = (ac+bd,\, ad+bc) + (ae+bf,\, af+be) = (a,b)(c,d) + (a,b)(e,f).

L1L2
2.1

Steps 1.2–1.9 verify all axioms: (Z,+,,0,1)(\mathbb{Z}, +, \cdot, 0, 1) is a commutative ring with identity and additive inverses.

step 1.1step 1.2step 1.3step 1.4step 1.5step 1.6step 1.7step 1.8step 1.9
DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-07-24Open item page →

Order on the integers

Definition

For integers x=[(a,b)]x = [(a,b)] and y=[(c,d)]y = [(c,d)] (The integers as equivalence classes of pairs of naturals) define

xy    a+db+cin N.x \le y \iff a + d \le b + c \quad \text{in } \mathbb{N}.

Write x<yx < y when xyx \le y and xyx \ne y. An integer xx is positive when 0<x0 < x; on representatives, 0<[(a,b)]0 < [(a,b)] exactly when b<ab < a.

Remarks

  • The defining inequality is "abcda - b \le c - d" restated without subtraction.
  • Well-definedness, totality, and compatibility with the arithmetic are proved in The integers form a totally ordered ring .
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)Open item page →

The integers form a totally ordered ring

Statement

The relation of Order on the integers is well defined and is a total order on Z\mathbb{Z}; it is compatible with addition (xyx \le y implies x+zy+zx + z \le y + z) and positives are closed under multiplication (0<x0 < x and 0<y0 < y imply 0<xy0 < xy). Thus Z\mathbb{Z} is a totally ordered commutative ring.

Facts & Assumptions

Given: Integers x=[(a,b)]x = [(a,b)], y=[(c,d)]y = [(c,d)], z=[(e,f)]z = [(e,f)] with the operations of Arithmetic on the integers.

[L1]

Addition on N\mathbb{N} is commutative and associative (Addition is commutative, Addition is associative).

[L2]

The order on N\mathbb{N} is total, antisymmetric, and transitive (\le is a linear order on N\mathbb{N}).

[L3]

Natural order is translation-invariant: xy    x+zy+zx\le y\iff x+z\le y+z (Order is compatible with addition).

[L4]

By the definition of natural order, xyx\le y exactly when y=x+ky=x+k for some natural kk; if x<yx<y, such a gap is nonzero (Order on the natural numbers).

[L5]

Natural multiplication is commutative and associative, distributes over addition, and has the usual zero and identity laws; multiplication by a nonzero natural preserves strict order (Multiplication is commutative, Multiplication is associative, Distributivity and the successor law for multiplication, Zero and one under multiplication, Order is compatible with multiplication).

[L6]

The integer operations make Z\mathbb{Z} a commutative ring with multiplicative identity (The integers form a commutative ring).

Proof

technique · direct
1.1

Suppose (a,b)(a,b)(a,b) \sim (a',b') and (c,d)(c,d)(c,d) \sim (c',d'), i.e. a+b=b+aa + b' = b + a' and c+d=d+cc + d' = d + c'.

given
1.2

Suppose a+db+ca + d \le b + c.

given
1.3

Totality: in N\mathbb{N} either a+db+ca + d \le b + c or b+ca+db + c \le a + d, so xyx \le y or yxy \le x.

L2
1.4

Antisymmetry: xyx \le y and yxy \le x give a+db+ca + d \le b + c and b+ca+db + c \le a + d, hence a+d=b+ca + d = b + c, which is x=yx = y as classes.

L2
1.5

Transitivity: from a+db+ca + d \le b + c and c+fd+ec + f \le d + e, adding gives (a+d)+(c+f)(b+c)+(d+e)(a+d)+(c+f) \le (b+c)+(d+e); regrouping, (a+f)+(c+d)(b+e)+(c+d)(a+f)+(c+d) \le (b+e)+(c+d); cancelling, a+fb+ea + f \le b + e, i.e. xzx \le z.

L1L2L3
1.6

Compatibility with addition: x+zy+zx + z \le y + z reads (a+e)+(d+f)(b+f)+(c+e)(a+e)+(d+f) \le (b+f)+(c+e), which regroups to (a+d)+(e+f)(b+c)+(e+f)(a+d) + (e+f) \le (b+c) + (e+f), equivalent to a+db+ca + d \le b + c, i.e. xyx \le y.

L1L3
1.7

Suppose 0<x0 < x and 0<y0 < y, i.e. b<ab < a and d<cd < c.

given
2.1

Adding (a+d)(a'+d'): (a+d)+(a+d)(b+c)+(a+d)(a+d) + (a'+d') \le (b+c) + (a'+d').

step 1.2L3
2.2

Regrouping with the equations of step 1.1: (b+c)+(a+d)=(b+a)+(c+d)=(a+b)+(d+c)=(a+d)+(b+c)(b+c) + (a'+d') = (b+a') + (c+d') = (a+b') + (d+c') = (a+d) + (b'+c').

step 1.1L1
2.3

Write a=b+ka = b + k and c=d+mc = d + m with nonzero naturals k,mk,m.

step 1.7L4
3.1

So (a+d)+(a+d)(a+d)+(b+c)(a+d) + (a'+d') \le (a+d) + (b'+c'); cancelling (a+d)(a+d) gives a+db+ca'+d'\le b'+c'. Applying the same argument with primed and unprimed representatives exchanged proves the converse implication, so the relation is independent of representatives.

step 1.1step 2.1step 2.2L3
3.2

Expanding both components of xy=[(ac+bd,ad+bc)]xy = [(ac+bd,\, ad+bc)]: ac+bd=(b+k)(d+m)+bd=(bd+bm+kd+bd)+kmac + bd = (b+k)(d+m) + bd = (bd + bm + kd + bd) + km and ad+bc=(b+k)d+b(d+m)=bd+kd+bd+bmad + bc = (b+k)d + b(d+m) = bd + kd + bd + bm, so ac+bd=(ad+bc)+kmac + bd = (ad + bc) + km.

step 2.3L1L5
4.1

Since k,mk,m are nonzero, 0<k0<k and 0<m0<m by [L4]. Hence [L5] gives 0=0m<km0=0\cdot m<km, and step 3.2 yields ad+bc<ac+bdad+bc<ac+bd, which is 0<xy0<xy.

step 2.3step 3.2L2L4L5
5.1

The order is well defined, total, compatible with addition, and positives are closed under multiplication; together with [L6], this makes Z\mathbb{Z} a totally ordered commutative ring.

step 3.1step 1.3step 1.4step 1.5step 1.6step 4.1L6
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

The integers have no zero divisors; multiplicative cancellation

Statement

If x,yZx, y \in \mathbb{Z} are nonzero then xy0xy \ne 0. Consequently, if xz=yzxz = yz and z0z \ne 0, then x=yx = y.

Facts & Assumptions

Given: Nonzero integers x,yx, y.

[L1]

Z\mathbb{Z} is a totally ordered ring; in particular trichotomy holds (each integer is negative, zero, or positive) and positives are closed under multiplication (The integers form a totally ordered ring).

[L2]

Ring arithmetic in Z\mathbb{Z}: (u)v=(uv)(-u)v = -(uv), (u)=u-(-u) = u, and distributivity (The integers form a commutative ring).

Proof

technique · cases
1.1

By trichotomy, each of xx and yy is positive or negative; split on the sign pattern.

L1cases-exhaustive
1.2

Case both positive: 0<xy0 < xy by closure of positives, so xy0xy \ne 0.

assume-case bothL1
1.3

Case exactly one negative, say y<0y < 0 (the other case is identical by commutativity): 0<y0 < -y, so 0<x(y)=(xy)0 < x(-y) = -(xy), hence xy<0xy < 0 and xy0xy \ne 0.

assume-case mixedL1L2
1.4

Case both negative: 0<x0 < -x and 0<y0 < -y, so 0<(x)(y)=xy0 < (-x)(-y) = xy, and xy0xy \ne 0.

assume-case negnegL1L2
2.1

In every case xy0xy \ne 0: the product of nonzero integers is nonzero.

step 1.2step 1.3step 1.4cases
3.1

Cancellation: if xz=yzxz = yz with z0z \ne 0, then (xy)z=xzyz=0(x-y)z = xz - yz = 0; were xy0x - y \ne 0, the product would be nonzero, so xy=0x - y = 0, i.e. x=yx = y.

step 2.1L2
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

The naturals embed in the integers

Statement

The map ι(n)=[(n,0)]\iota(n) = [(n,0)] is injective and preserves addition, multiplication, and order. Its image is exactly the set of nonnegative integers, so every x0x \ge 0 in Z\mathbb{Z} is ι(k)\iota(k) for a unique natural kk.

Facts & Assumptions

Given: The map ι:NZ\iota : \mathbb{N} \to \mathbb{Z}, ι(n)=[(n,0)]\iota(n) = [(n,0)].

[A1]

Arithmetic identities in N\mathbb{N}: x+0=xx + 0 = x, 0+x=x0 + x = x, x0=0x \cdot 0 = 0, 0x=00 \cdot x = 0, x1=xx \cdot 1 = x.

[A2]

The order on N\mathbb{N}, and: xyx \le y iff y=x+ky = x + k for some kk.

Proof

technique · direct
1.1

Injectivity: [(m,0)]=[(n,0)][(m,0)] = [(n,0)] means m+0=0+nm + 0 = 0 + n, i.e. m=nm = n.

A1
1.2

Addition: ι(m)+ι(n)=[(m+n,0+0)]=ι(m+n)\iota(m) + \iota(n) = [(m+n,\, 0+0)] = \iota(m+n).

A1
1.3

Multiplication: ι(m)ι(n)=[(mn+00,  m0+0n)]=ι(mn)\iota(m)\,\iota(n) = [(mn + 0 \cdot 0,\; m \cdot 0 + 0 \cdot n)] = \iota(mn).

A1
1.4

Order: ι(m)ι(n)\iota(m) \le \iota(n) reads m+00+nm + 0 \le 0 + n, i.e. mnm \le n.

A1A2
1.5

Image: if 0[(a,b)]0 \le [(a,b)] then bab \le a, so a=b+ka = b + k and (a,b)(k,0)(a,b) \sim (k,0), giving [(a,b)]=ι(k)[(a,b)] = \iota(k); conversely 0ι(k)0 \le \iota(k) for every kk.

A2algebra
2.1

ι\iota embeds N\mathbb{N} into Z\mathbb{Z}, preserving arithmetic and order, with image the nonnegative integers.

step 1.1step 1.2step 1.3step 1.4step 1.5
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-07-24Open item page →

The rationals as equivalence classes of pairs of integers

Definition

On the set of pairs (a,b)(a,b) with a,bZa, b \in \mathbb{Z} and b0b \ne 0, define

(a,b)(c,d)    ad=cbin Z.(a,b) \sim (c,d) \iff ad = cb \quad \text{in } \mathbb{Z}.

This is an equivalence relation (The rational-defining relation is an equivalence relation ). The rationals are the quotient Q\mathbb{Q}, and [(a,b)][(a,b)] is written a/ba/b.

Remarks

  • The pair (a,b)(a,b) encodes the formal quotient a/ba/b; the relation ad=cbad = cb is "a/b=c/da/b = c/d" cleared of denominators, using only the ring arithmetic of Z\mathbb{Z} (The integers form a commutative ring).
LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

The rational-defining relation is an equivalence relation

Statement

The relation (a,b)(c,d)    ad=cb(a,b) \sim (c,d) \iff ad = cb on pairs of integers with nonzero second component (The rationals as equivalence classes of pairs of integers) is an equivalence relation.

Facts & Assumptions

Given: Pairs (a,b),(c,d),(e,f)(a,b), (c,d), (e,f) of integers with b,d,f0b, d, f \ne 0.

[L1]

Z\mathbb{Z} is a commutative ring (The integers form a commutative ring).

[L2]

Multiplicative cancellation in Z\mathbb{Z}: ud=vdud = vd with d0d \ne 0 implies u=vu = v (The integers have no zero divisors; multiplicative cancellation).

Proof

technique · direct
1.1

Reflexivity: ab=baab = ba, so (a,b)(a,b)(a,b) \sim (a,b).

L1
1.2

Symmetry: if ad=cbad = cb then cb=adcb = ad, which is the defining equation for (c,d)(a,b)(c,d) \sim (a,b).

L1
1.3

Suppose (a,b)(c,d)(a,b) \sim (c,d) and (c,d)(e,f)(c,d) \sim (e,f), i.e. ad=cbad = cb and cf=edcf = ed.

given
2.1

Multiplying the first equation by ff and the second by bb: adf=cbfadf = cbf and cfb=edbcfb = edb.

step 1.3L1
3.1

Chaining: (af)d=adf=cbf=cfb=edb=(eb)d(af)d = adf = cbf = cfb = edb = (eb)d.

step 2.1L1
4.1

Cancelling the nonzero dd: af=ebaf = eb, so (a,b)(e,f)(a,b) \sim (e,f); the relation is transitive.

step 3.1L2
5.1

The relation is reflexive, symmetric, and transitive, hence an equivalence relation.

step 1.1step 1.2step 4.1
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-07-24Open item page →

Arithmetic on the rationals

Definition

On Q\mathbb{Q} (The rationals as equivalence classes of pairs of integers) define, on representatives,

[(a,b)]+[(c,d)]:=[(ad+cb,  bd)],[(a,b)][(c,d)]:=[(ac,  bd)],[(a,b)] + [(c,d)] := [(ad + cb,\; bd)], \qquad [(a,b)] \cdot [(c,d)] := [(ac,\; bd)], [(a,b)]:=[(a,b)],0:=[(0,1)],1:=[(1,1)],-[(a,b)] := [(-a, b)], \qquad 0 := [(0,1)], \qquad 1 := [(1,1)],

and, for [(a,b)]0[(a,b)] \ne 0 (equivalently a0a \ne 0), the inverse [(a,b)]1:=[(b,a)][(a,b)]^{-1} := [(b,a)].

Remarks

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

Rational arithmetic is well defined

Statement

Sum, product, and negation of Arithmetic on the rationals are independent of the chosen representatives.

Facts & Assumptions

Given: Pairs with (a,b)(a,b)(a,b) \sim (a',b') and (c,d)(c,d)(c,d) \sim (c',d') (The rationals as equivalence classes of pairs of integers), all second components nonzero.

[L1]

Z\mathbb{Z} is a commutative ring (The integers form a commutative ring).

Proof

technique · direct
1.1

By hypothesis ab=abab' = a'b and cd=cdcd' = c'd.

given
2.1

Product: (ac)(bd)=(ab)(cd)=(ab)(cd)=(ac)(bd)(ac)(b'd') = (ab')(cd') = (a'b)(c'd) = (a'c')(bd), so (ac,bd)(ac,bd)(ac,\, bd) \sim (a'c',\, b'd').

step 1.1L1
2.2

Sum: (ad+cb)(bd)=(ab)(dd)+(cd)(bb)=(ab)(dd)+(cd)(bb)=(ad+cb)(bd)(ad + cb)(b'd') = (ab')(dd') + (cd')(bb') = (a'b)(dd') + (c'd)(bb') = (a'd' + c'b')(bd), so (ad+cb,bd)(ad+cb,bd)(ad+cb,\, bd) \sim (a'd'+c'b',\, b'd').

step 1.1L1
2.3

Negation: from ab=abab' = a'b, (a)b=(a)b(-a)b' = (-a')b, so (a,b)(a,b)(-a, b) \sim (-a', b').

step 1.1L1
3.1

All three operations are independent of representatives.

step 2.1step 2.2step 2.3
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

The reciprocal on the rationals is well-defined

Statement

On Q{0}\mathbb{Q} \setminus \{0\} the reciprocal [(a,b)]1:=[(b,a)][(a,b)]^{-1} := [(b,a)] (Arithmetic on the rationals) is independent of the chosen representative: if (a,b)(a,b)(a,b) \sim (a',b') with a,a,b,b0a, a', b, b' \ne 0, then (b,a)(b,a)(b,a) \sim (b',a'). Hence the reciprocal is a well-defined function on Q{0}\mathbb{Q} \setminus \{0\}.

Facts & Assumptions

Given: Nonzero rationals represented by integer pairs (a,b)(a,b) and (a,b)(a',b') with a,a,b,b0a, a', b, b' \ne 0, where (x,y)(z,w)    xw=zy(x,y) \sim (z,w) \iff x w = z y in Z\mathbb{Z} (The rationals as equivalence classes of pairs of integers).

[L1]

Multiplication in Z\mathbb{Z} is commutative (The integers form a commutative ring).

Proof

technique · direct
1.1

By hypothesis (a,b)(a,b)(a,b) \sim (a',b'), that is ab=aba b' = a' b in Z\mathbb{Z}.

given
2.1

Commuting each product by [L1], ba=bab' a = b a', hence ba=bab a' = b' a.

step 1.1L1
3.1

The equation ba=bab a' = b' a is exactly the defining relation (b,a)(b,a)(b,a) \sim (b',a'), and since a,a0a, a' \ne 0 the pairs (b,a),(b,a)(b,a), (b',a') are legal rational representatives; therefore [(a,b)]1=[(b,a)]=[(b,a)]=[(a,b)]1[(a,b)]^{-1} = [(b,a)] = [(b',a')] = [(a',b')]^{-1}, so the reciprocal is well-defined on Q{0}\mathbb{Q} \setminus \{0\}.

step 2.1given
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

The rationals form a field

Statement

(Q,+,,0,1)(\mathbb{Q}, +, \cdot, 0, 1) with the operations of Arithmetic on the rationals is a field: a commutative ring with 101 \ne 0 in which every nonzero element has a multiplicative inverse.

Facts & Assumptions

Given: Rationals with representatives (a,b),(c,d),(e,f)(a,b), (c,d), (e,f), second components nonzero.

[L1]

The operations are independent of representatives (Rational arithmetic is well defined).

[L2]

Z\mathbb{Z} is a commutative ring in which 101 \ne 0 (The integers form a commutative ring; 101 \ne 0 because 101 \ne 0 in N\mathbb{N}).

[L3]

Z\mathbb{Z} has no zero divisors and admits cancellation (The integers have no zero divisors; multiplicative cancellation).

Proof

technique · direct
1.1

By [L1], each axiom may be verified on fixed representatives.

L1suffices
1.2

Associativity of ++: both ((a,b)+(c,d))+(e,f)((a,b)+(c,d))+(e,f) and (a,b)+((c,d)+(e,f))(a,b)+((c,d)+(e,f)) have representative (adf+cbf+ebd,  bdf)(adf + cbf + ebd,\; bdf).

L2
1.3

Commutativity of ++: (ad+cb,bd)(ad+cb,\, bd) and (cb+ad,db)(cb+ad,\, db) are equal pairs.

L2
1.4

Additive identity: (a,b)+(0,1)=(a1+0b,  b1)=(a,b)(a,b) + (0,1) = (a \cdot 1 + 0 \cdot b,\; b \cdot 1) = (a,b).

L2
1.5

Additive inverses: (a,b)+(a,b)=(abab,  b2)=(0,b2)(0,1)(a,b) + (-a,b) = (ab - ab,\; b^2) = (0, b^2) \sim (0,1).

L2
1.6

Associativity and commutativity of \cdot: ((ac)e,(bd)f)=(a(ce),b(df))((ac)e,\, (bd)f) = (a(ce),\, b(df)) and (ac,bd)=(ca,db)(ac,\, bd) = (ca,\, db).

L2
1.7

Multiplicative identity: (a,b)(1,1)=(a,b)(a,b)(1,1) = (a,b); and 101 \ne 0 since 11011 \cdot 1 \ne 0 \cdot 1.

L2
1.8

Distributivity: (a,b)((c,d)+(e,f))(a,b)\bigl((c,d)+(e,f)\bigr) has representative (a(cf+ed),  b(df))(a(cf+ed),\; b(df)), while (a,b)(c,d)+(a,b)(e,f)(a,b)(c,d) + (a,b)(e,f) has representative (acbf+aebd,  b2df)=(b(acf+aed),  b(bdf))(acbf + aebd,\; b^2 df) = (b(acf + aed),\; b(bdf)); cancelling the common nonzero factor bb these are equivalent.

L2L3
1.9

Inverses: [(a,b)]=0[(a,b)] = 0 iff a1=0ba \cdot 1 = 0 \cdot b iff a=0a = 0; for a0a \ne 0, (a,b)(b,a)=(ab,ba)(1,1)(a,b)(b,a) = (ab,\, ba) \sim (1,1).

L2
2.1

All field axioms hold: Q\mathbb{Q} is a field.

step 1.1step 1.2step 1.3step 1.4step 1.5step 1.6step 1.7step 1.8step 1.9
DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-07-24Open item page →

Order on the rationals

Definition

Every rational has a representative with positive denominator (if b<0b < 0 then (a,b)(a,b)(a,b) \sim (-a,-b) with b>0-b > 0, Every rational has a positive-denominator representative ). For representatives with b>0b > 0 and d>0d > 0 define

[(a,b)][(c,d)]    adcbin Z.[(a,b)] \le [(c,d)] \iff ad \le cb \quad \text{in } \mathbb{Z}.

A rational xx is positive when 0<x0 < x; on such representatives, 0<[(a,b)]0 < [(a,b)] exactly when 0<a0 < a.

Remarks

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

Every rational has a positive-denominator representative

Statement

Every rational has a representative (a,b)(a,b) with b>0b > 0: for a class [(a,b)][(a,b)] (where b0b \ne 0), if b>0b > 0 take (a,b)(a,b) itself, and if b<0b < 0 then (a,b)(a,b)(a,b) \sim (-a,-b) with b>0-b > 0. Consequently the order on Q\mathbb{Q} (Order on the rationals), which is stated on positive-denominator representatives, is defined on all of Q\mathbb{Q}.

Facts & Assumptions

Given: A rational represented by (a,b)(a,b) with a,bZa, b \in \mathbb{Z}, b0b \ne 0, and the relation (x,y)(z,w)    xw=zy(x,y) \sim (z,w) \iff x w = z y (The rationals as equivalence classes of pairs of integers).

[L1]

Trichotomy in Z\mathbb{Z}: each nonzero integer is either >0> 0 or <0< 0, and b<0b < 0 iff b>0-b > 0 (The integers form a totally ordered ring).

[L2]

In the commutative ring Z\mathbb{Z}, a(b)=(ab)=(a)ba(-b) = -(ab) = (-a)b (both products are the additive inverse of abab, by distributivity) (The integers form a commutative ring).

Proof

technique · direct
1.1

Since b0b \ne 0, by trichotomy [L1] either b>0b > 0 or b<0b < 0.

givenL1
2.1

If b>0b > 0, the representative (a,b)(a,b) already has positive denominator.

step 1.1
2.2

If b<0b < 0, then b>0-b > 0 by [L1], and a(b)=(a)ba(-b) = (-a)b by [L2] is exactly the defining relation (a,b)(a,b)(a,b) \sim (-a,-b); so (a,b)(-a,-b) represents the same class and has positive denominator b-b.

step 1.1L1L2
3.1

In either case the class has a representative with positive denominator; hence the order Order on the rationals, stated on such representatives, is defined for every rational.

step 2.1step 2.2
TheoremStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-02 (claude-opus-5)Open item page →

The rationals form a totally ordered field

Statement

The relation of Order on the rationals is well defined and makes the field Q\mathbb{Q} (The rationals form a field) a totally ordered field: the order is total, xyx \le y implies x+zy+zx + z \le y + z, and 0<x0 < x, 0<y0 < y imply 0<xy0 < xy.

Facts & Assumptions

Given: Rationals x=[(a,b)]x = [(a,b)], y=[(c,d)]y = [(c,d)], z=[(e,f)]z = [(e,f)] with b,d,f>0b, d, f > 0.

[L1]

Z\mathbb{Z} is a totally ordered commutative ring; positives are closed under products (The integers form a totally ordered ring).

Proof

technique · direct
1.1

Order-scaling in Z\mathbb{Z}: for p>0p > 0, if u<vu < v then 0<(vu)p0 < (v-u)p, so up<vpup < vp; conversely if upvpup \le vp and v<uv < u then vp<upvp < up, impossible; hence uvu \le v iff upvpup \le vp.

L1algebra
1.2

Suppose (a,b)(a,b)(a,b) \sim (a',b') and (c,d)(c,d)(c,d) \sim (c',d') with b,d>0b', d' > 0, i.e. ab=abab' = a'b and cd=cdcd' = c'd; suppose also adcbad \le cb.

given
1.3

Totality: adcbad \le cb or cbadcb \le ad in Z\mathbb{Z}, so xyx \le y or yxy \le x.

L1
1.4

Antisymmetry: adcbad \le cb and cbadcb \le ad give ad=cbad = cb, i.e. x=yx = y as classes.

L1
1.5

Positive products: if 0<x0 < x and 0<y0 < y then 0<a0 < a and 0<c0 < c, so xy=[(ac,bd)]xy = [(ac,\, bd)] has ac>0ac > 0 and bd>0bd > 0, hence 0<xy0 < xy.

L1
1.6

For transitivity, let z=[(e,f)]z = [(e,f)] with f>0f > 0 and suppose additionally yzy \le z, i.e. cfedcf \le ed.

given
2.1

Scaling the hypothesis adcbad \le cb by bd>0b'd' > 0: (ad)(bd)(cb)(bd)(ad)(b'd') \le (cb)(b'd').

step 1.1step 1.2L1
2.2

Rearranging both sides with ab=abab' = a'b and cd=cdcd' = c'd: (ad)(bd)=(ab)(dd)=(ab)(dd)=(ad)(bd)(ad)(b'd') = (ab')(dd') = (a'b)(dd') = (a'd')(bd) and (cb)(bd)=(cd)(bb)=(cd)(bb)=(cb)(bd)(cb)(b'd') = (cd')(bb') = (c'd)(bb') = (c'b')(bd).

step 1.2L1
2.3

Transitivity: from adcbad \le cb and cfedcf \le ed, scaling by f>0f > 0 and b>0b > 0 gives (af)d=(ad)f(cb)f=(cf)b(ed)b=(eb)d(af)d = (ad)f \le (cb)f = (cf)b \le (ed)b = (eb)d; cancelling d>0d > 0 via order-scaling, afebaf \le eb, i.e. xzx \le z.

step 1.1step 1.2step 1.6L1
2.4

Compatibility with addition: x+zy+zx + z \le y + z reads (af+eb)(df)(cf+ed)(bf)(af+eb)(df) \le (cf+ed)(bf), which expands to (ad)f2+(eb)(df)(cb)f2+(ed)(bf)(ad)f^2 + (eb)(df) \le (cb)f^2 + (ed)(bf); the second terms are equal, so this is (ad)f2(cb)f2(ad)f^2 \le (cb)f^2, equivalent by order-scaling with f2>0f^2 > 0 to adcbad \le cb, i.e. xyx \le y.

step 1.1L1
3.1

Combining: (ad)(bd)(cb)(bd)(a'd')(bd) \le (c'b')(bd) with bd>0bd > 0, so adcba'd' \le c'b' by order-scaling: the order is independent of representatives.

step 2.1step 2.2step 1.1L1
4.1

The order is well defined, total, compatible with addition, and positives are closed under multiplication: Q\mathbb{Q} is a totally ordered field.

step 3.1step 1.3step 1.4step 2.3step 2.4step 1.5
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-02 (claude-opus-5)Open item page →

The integers embed in the rationals

Statement

The map j(k)=[(k,1)]j(k) = [(k,1)] is injective and preserves addition, multiplication, and order. Composing with The naturals embed in the integers embeds N\mathbb{N} in Q\mathbb{Q}; we write kk for j(k)j(k) throughout.

Facts & Assumptions

Given: The map j:ZQj : \mathbb{Z} \to \mathbb{Q}, j(k)=[(k,1)]j(k) = [(k,1)].

[L1]

Ring arithmetic in Z\mathbb{Z} (The integers form a commutative ring).

[L2]

The order on Q\mathbb{Q} (Order on the rationals), whose defining inequality is read in the order on Z\mathbb{Z} (Order on the integers).

[L3]

Equality in Q\mathbb{Q}: [(a,b)]=[(c,d)][(a,b)] = [(c,d)] iff ad=cbad = cb (The rationals as equivalence classes of pairs of integers).

Proof

technique · direct
1.1

Injectivity: (k,1)(m,1)(k,1) \sim (m,1) means k1=m1k \cdot 1 = m \cdot 1, i.e. k=mk = m.

L3L1
1.2

Addition: j(k)+j(m)=[(k1+m1,  1)]=j(k+m)j(k) + j(m) = [(k \cdot 1 + m \cdot 1,\; 1)] = j(k+m).

L1
1.3

Multiplication: j(k)j(m)=[(km,1)]=j(km)j(k)\,j(m) = [(km,\, 1)] = j(km).

L1
1.4

Order: denominators are 1>01 > 0, so j(k)j(m)j(k) \le j(m) reads k1m1k \cdot 1 \le m \cdot 1, i.e. kmk \le m.

L1L2
2.1

jj embeds Z\mathbb{Z} into Q\mathbb{Q}, preserving arithmetic and order.

step 1.1step 1.2step 1.3step 1.4
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

The rationals are Archimedean

Statement

For every rational xx there is a natural number nn with x<nx < n. Consequently, for every rational ε>0\varepsilon > 0 there is a natural n1n \ge 1 with 1/n<ε1/n < \varepsilon.

Facts & Assumptions

Given: A rational x=[(a,b)]x = [(a,b)] with b>0b > 0.

[L1]

The order and arithmetic of Q\mathbb{Q} (The rationals form a totally ordered field).

[L2]

Integer facts: positive integers are exactly ι(m)\iota(m) with m1m \ge 1 natural; nonnegative integers are the image of N\mathbb{N}; the embeddings preserve arithmetic and order (The naturals embed in the integers, The integers embed in the rationals, The integers form a totally ordered ring).

Proof

technique · direct
1.1

Since b>0b > 0, bb lies in the image of N\mathbb{N} and b1b \ge 1.

L2
1.2

If a0a \le 0 set k=0k = 0; otherwise aa is a positive integer, so a=ι(k)a = \iota(k) for some natural k1k \ge 1. In both cases aka \le k (as integers).

L2
2.1

Then a<k+1a < k + 1 and, since b1b \ge 1 and k+1>0k+1 > 0, also k+1(k+1)bk + 1 \le (k+1)b.

step 1.1step 1.2L2
3.1

Hence a<(k+1)ba < (k+1)b, and dividing by b>0b > 0 (order-scaling in the definition of the rational order), x=[(a,b)]<[((k+1)b,b)]=k+1=:nx = [(a,b)] < [( (k+1)b,\, b)] = k+1 =: n.

step 2.1L1
4.1

For rational ε>0\varepsilon > 0: apply the above to x=1/εx = 1/\varepsilon to get nn with 1/ε<n1/\varepsilon < n, hence 1/n<ε1/n < \varepsilon.

step 3.1L1
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

Absolute value and the triangle inequality

Statement

For xQx \in \mathbb{Q} set x=x|x| = x if x0x \ge 0 and x=x|x| = -x otherwise. Then xy=xy|xy| = |x|\,|y|, x+yx+y|x + y| \le |x| + |y|, and xyxy\bigl||x| - |y|\bigr| \le |x - y|.

The proof uses only the axioms of a totally ordered field, so it applies verbatim to any such field (in particular to R\mathbb{R} once constructed).

Facts & Assumptions

Given: Elements x,yx, y of the totally ordered field Q\mathbb{Q}.

[L1]

Ordered-field arithmetic: trichotomy, compatibility of the order with addition, products of positives are positive, (u)v=(uv)(-u)v = -(uv) (The rationals form a totally ordered field).

Proof

technique · cases
1.1

For every uu: uuu \le |u|, uu-u \le |u|, u0|u| \ge 0, and u=u|-u| = |u|, directly from the definition and trichotomy.

L1
1.2

Case xx and yy have the same sign (both 0\ge 0 or both <0< 0): xy0xy \ge 0 and xy=xyxy = |x||y| (for both negative, xy=(x)(y)xy = (-x)(-y)).

assume-case sameL1
1.3

Case x,yx, y have mixed signs, say x0>yx \ge 0 > y (the other order is identical): xy0xy \le 0, so xy=(xy)=x(y)=xy|xy| = -(xy) = x(-y) = |x||y|.

assume-case mixedL1
2.1

In all cases xy=xy|xy| = |x|\,|y|.

step 1.2step 1.3cases-exhaustive
2.2

Adding xxx \le |x| and yyy \le |y| gives x+yx+yx + y \le |x| + |y|; adding xx-x \le |x| and yy-y \le |y| gives (x+y)x+y-(x+y) \le |x| + |y|; since x+y|x+y| is one of ±(x+y)\pm(x+y), x+yx+y|x+y| \le |x| + |y|.

step 1.1L1
3.1

From x=(xy)+yx = (x - y) + y: xxy+y|x| \le |x-y| + |y|, so xyxy|x| - |y| \le |x-y|; symmetrically yxyx=xy|y| - |x| \le |y-x| = |x-y|; hence xyxy\bigl||x|-|y|\bigr| \le |x-y|.

step 2.2L1
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-07-24Open item page →

Cauchy sequence of rationals

Definition

A sequence (an)n1(a_n)_{n \ge 1} of rational numbers is a Cauchy sequence if for every rational ε>0\varepsilon > 0 there exists NNN \in \mathbb{N} such that

aman<εfor all m,nN.|a_m - a_n| < \varepsilon \qquad \text{for all } m, n \ge N.

Remarks

  • The quantifier ranges over rational ε\varepsilon only. This is deliberate: the definition is stated before the real numbers exist, which is exactly what allows the reals to be constructed from it.
  • Informally: the terms of the sequence eventually cluster arbitrarily tightly, without any reference to a limit value.
DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-07-24Open item page →

Null sequence

Definition

A sequence (an)n1(a_n)_{n \ge 1} of rational numbers is a null sequence if for every rational ε>0\varepsilon > 0 there exists NNN \in \mathbb{N} such that

an<εfor all nN.|a_n| < \varepsilon \qquad \text{for all } n \ge N.

Remarks

  • Equivalently: (an)(a_n) converges to 00 (with rational tolerances).
  • In the construction of R\mathbb{R}, two Cauchy sequences will be declared equivalent exactly when their difference is a null sequence; the null sequences are the "zero" of the construction.
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

Every Cauchy sequence of rationals is bounded

Statement

Every Cauchy sequence (an)n1(a_n)_{n \ge 1} of rational numbers (Cauchy sequence of rationals) is bounded: there exists a rational M0M \ge 0 such that anM|a_n| \le M for all n1n \ge 1.

Facts & Assumptions

Given: A Cauchy sequence (an)n1(a_n)_{n \ge 1} of rational numbers.

[A1]

For every rational ε>0\varepsilon > 0 there exists NNN \in \mathbb{N} with aman<ε|a_m - a_n| < \varepsilon for all m,nNm, n \ge N.

[L1]

Triangle inequality on Q\mathbb{Q}: xxy+y|x| \le |x - y| + |y| (Absolute value and the triangle inequality).

Proof

technique · direct
1.1

Apply [A1] with ε=1\varepsilon = 1: fix NNN \in \mathbb{N} such that aman<1|a_m - a_n| < 1 for all m,nNm, n \ge N.

A1
1.2

For every nNn \ge N: ananaN+aN|a_n| \le |a_n - a_N| + |a_N|.

L1
2.1

For every nNn \ge N: an<aN+1|a_n| < |a_N| + 1.

step 1.1step 1.2algebra
2.2

Define M=max{a1,a2,,aN1,aN+1}M = \max\{|a_1|, |a_2|, \dots, |a_{N-1}|, |a_N| + 1\}, a maximum of finitely many rationals, hence rational and 0\ge 0.

step 1.1choose
3.1

For every n<Nn < N: anM|a_n| \le M, since an|a_n| appears in the maximum.

step 2.2algebra
3.2

For every nNn \ge N: an<aN+1M|a_n| < |a_N| + 1 \le M.

step 2.1step 2.2algebra
4.1

For every n1n \ge 1: anM|a_n| \le M, so (an)(a_n) is bounded.

step 3.1step 3.2
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

Null sequences are Cauchy

Statement

Every null sequence (Null sequence) is a Cauchy sequence (Cauchy sequence of rationals).

Facts & Assumptions

Given: A null sequence (an)(a_n) and a rational ε>0\varepsilon > 0.

[A1]

Null: for every rational δ>0\delta > 0 there is NN with an<δ|a_n| < \delta for all nNn \ge N.

[A2]

Cauchy: for every rational δ>0\delta > 0 there is NN with aman<δ|a_m - a_n| < \delta for all m,nNm,n \ge N.

[L1]

Field arithmetic in Q\mathbb{Q}: ε/2>0\varepsilon/2 > 0 and ε/2+ε/2=ε\varepsilon/2 + \varepsilon/2 = \varepsilon (The rationals form a field, The rationals form a totally ordered field).

Proof

technique · direct
1.1

ε/2\varepsilon/2 is a positive rational.

L1
2.1

Fix NN with an<ε/2|a_n| < \varepsilon/2 for all nNn \ge N.

step 1.1A1
3.1

For m,nNm, n \ge N: amanam+an<ε/2+ε/2=ε|a_m - a_n| \le |a_m| + |a_n| < \varepsilon/2 + \varepsilon/2 = \varepsilon.

step 2.1L1L2
4.1

(an)(a_n) is Cauchy.

step 3.1A2
TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

Cauchy sequences form a commutative ring

Statement

The set C\mathcal{C} of Cauchy sequences of rationals, with termwise addition and multiplication and the constant sequences 00 and 11, is a commutative ring with identity.

Facts & Assumptions

Given: Cauchy sequences (an),(bn)(a_n), (b_n) and a rational ε>0\varepsilon > 0.

[A1]

Cauchy: for every rational δ>0\delta > 0 there is an index beyond which any two terms differ by less than δ\delta.

[L1]

Q\mathbb{Q} is a field; ring axioms hold termwise (The rationals form a field).

[L2]

Triangle inequality and uv=uv|uv| = |u||v| (Absolute value and the triangle inequality).

[L3]

Cauchy sequences are bounded (Every Cauchy sequence of rationals is bounded).

[L4]

Ordered-field arithmetic: ε/2\varepsilon/2, ε/(A+B)\varepsilon/(A+B) are positive rationals for A,B1A, B \ge 1 (The rationals form a totally ordered field).

Proof

technique · direct
1.1

Termwise, all ring axioms (associativity, commutativity, identities, inverses for ++, distributivity) hold in C\mathcal{C} because they hold in Q\mathbb{Q} at every index; the constant sequences 0,10, 1 are Cauchy. What needs proof is closure of C\mathcal{C} under ++, negation, and \cdot.

L1
1.2

Fix NaN_a with aman<ε/2|a_m - a_n| < \varepsilon/2 for m,nNam,n \ge N_a and NbN_b likewise for (bn)(b_n).

A1L4
1.3

Fix rational bounds A,B1A, B \ge 1 with anA|a_n| \le A and bnB|b_n| \le B for all nn.

L3
2.1

Sum: for m,nmax(Na,Nb)m,n \ge \max(N_a, N_b), (am+bm)(an+bn)aman+bmbn<ε|(a_m + b_m) - (a_n + b_n)| \le |a_m - a_n| + |b_m - b_n| < \varepsilon; so (an+bn)(a_n + b_n) is Cauchy. Negation likewise: (am)(an)=aman|(-a_m) - (-a_n)| = |a_m - a_n|.

step 1.2L2
2.2

Set δ=ε/(A+B)>0\delta = \varepsilon/(A+B) > 0 and fix Ma,MbM_a, M_b with aman<δ|a_m - a_n| < \delta for m,nMam,n \ge M_a and bmbn<δ|b_m - b_n| < \delta for m,nMbm,n \ge M_b.

step 1.3A1L4
3.1

Product: for m,nmax(Ma,Mb)m,n \ge \max(M_a, M_b), ambmanbn=am(bmbn)+bn(aman)Abmbn+Baman<(A+B)δ=ε|a_m b_m - a_n b_n| = |a_m(b_m - b_n) + b_n(a_m - a_n)| \le A|b_m - b_n| + B|a_m - a_n| < (A+B)\delta = \varepsilon; so (anbn)(a_n b_n) is Cauchy.

step 1.3step 2.2L2
4.1

C\mathcal{C} is closed under addition, negation, and multiplication, contains 00 and 11, and satisfies the ring axioms termwise: a commutative ring with identity.

step 1.1step 2.1step 3.1
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

Null sequences form an ideal

Statement

The set N\mathcal{N} of null sequences is an ideal of the ring C\mathcal{C} of Cauchy sequences (Cauchy sequences form a commutative ring): it is a subgroup under addition, and czNc \cdot z \in \mathcal{N} whenever cCc \in \mathcal{C} and zNz \in \mathcal{N}.

Facts & Assumptions

Given: Null sequences (zn),(wn)(z_n), (w_n), a Cauchy sequence (cn)(c_n), and a rational ε>0\varepsilon > 0.

[A1]

Null: beyond some index, zn|z_n| is smaller than any prescribed positive rational.

[L1]

Ordered-field arithmetic in Q\mathbb{Q} (The rationals form a totally ordered field).

[L2]

Triangle inequality and multiplicativity of |\cdot| (Absolute value and the triangle inequality).

[L3]

Cauchy sequences are bounded (Every Cauchy sequence of rationals is bounded).

[L4]

Null sequences are Cauchy, so NC\mathcal{N} \subseteq \mathcal{C} (Null sequences are Cauchy).

Proof

technique · direct
1.1

Fix Nz,NwN_z, N_w with zn<ε/2|z_n| < \varepsilon/2 for nNzn \ge N_z and wn<ε/2|w_n| < \varepsilon/2 for nNwn \ge N_w.

A1L1
1.2

Fix M0M \ge 0 with cnM|c_n| \le M ([L3]) and set B=max(M,1)1B = \max(M, 1) \ge 1, so cnB|c_n| \le B for all nn.

L3
2.1

Sum: for nmax(Nz,Nw)n \ge \max(N_z, N_w), zn+wnzn+wn<ε|z_n + w_n| \le |z_n| + |w_n| < \varepsilon; negation: zn=zn|-z_n| = |z_n|. So N\mathcal{N} is a subgroup under addition.

step 1.1L2
2.2

Fix NN with zn<ε/B|z_n| < \varepsilon/B for nNn \ge N.

step 1.2A1L1
3.1

Product: for nNn \ge N, cnzn=cnznBzn<ε|c_n z_n| = |c_n|\,|z_n| \le B\,|z_n| < \varepsilon; so (cnzn)(c_n z_n) is null.

step 1.2step 2.2L2
4.1

N\mathcal{N} is a nonempty additive subgroup of C\mathcal{C} absorbing multiplication by C\mathcal{C}: an ideal.

step 2.1step 3.1L4
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

A non-null Cauchy sequence is eventually bounded away from zero, with constant sign

Statement

If (an)(a_n) is Cauchy but not null, there are a rational δ>0\delta > 0 and an index N0N_0 such that an>δ|a_n| > \delta for all nN0n \ge N_0; moreover either an>δa_n > \delta for all nN0n \ge N_0, or an<δa_n < -\delta for all nN0n \ge N_0.

Facts & Assumptions

Given: A Cauchy sequence (an)(a_n) that is not null.

[A1]

Negation of null (Null sequence): there is a rational ε0>0\varepsilon_0 > 0 such that for every NN some nNn \ge N has anε0|a_n| \ge \varepsilon_0.

[L1]

Ordered-field arithmetic: ε0/3>0\varepsilon_0/3 > 0, ε0ε0/3>ε0/3\varepsilon_0 - \varepsilon_0/3 > \varepsilon_0/3 (The rationals form a totally ordered field).

[L2]

Triangle inequality, in the form uvvu|u| \ge |v| - |v - u| (Absolute value and the triangle inequality).

Proof

technique · direct
1.1

Fix ε0>0\varepsilon_0 > 0 witnessing that (an)(a_n) is not null.

A1
1.2

Fix N0N_0 with aman<ε0/3|a_m - a_n| < \varepsilon_0/3 for all m,nN0m, n \ge N_0.

A2L1
2.1

Pick n0N0n_0 \ge N_0 with an0ε0|a_{n_0}| \ge \varepsilon_0.

step 1.1step 1.2
3.1

For every nN0n \ge N_0: anan0an0an>ε0ε0/3>ε0/3=:δ|a_n| \ge |a_{n_0}| - |a_{n_0} - a_n| > \varepsilon_0 - \varepsilon_0/3 > \varepsilon_0/3 =: \delta; so an>δ|a_n| > \delta for all nN0n \ge N_0.

step 2.1step 1.2L2L1
4.1

Sign stability: if some am>δa_m > \delta and some an<δa_n < -\delta with m,nN0m, n \ge N_0, then aman>2δ=2ε0/3>ε0/3|a_m - a_n| > 2\delta = 2\varepsilon_0/3 > \varepsilon_0/3, impossible by step 1.2; so beyond N0N_0 all terms have one sign, and by step 3.1 either an>δa_n > \delta for all nN0n \ge N_0 or an<δa_n < -\delta for all nN0n \ge N_0.

step 3.1step 1.2L1
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

The null ideal is maximal

Statement

If (an)CN(a_n) \in \mathcal{C} \setminus \mathcal{N}, then the ideal of C\mathcal{C} generated by N\mathcal{N} and (an)(a_n) is all of C\mathcal{C}. Hence N\mathcal{N} is a maximal ideal.

Facts & Assumptions

Given: A Cauchy sequence (an)(a_n) that is not null.

[L1]

Away-from-zero: there are δ>0\delta > 0 and N0N_0 with an>δ|a_n| > \delta for all nN0n \ge N_0 (A non-null Cauchy sequence is eventually bounded away from zero, with constant sign).

[L2]

Triangle inequality and uv=uv|uv| = |u||v| (Absolute value and the triangle inequality).

[L3]

Cauchy definition and field arithmetic in Q\mathbb{Q}: εδ2>0\varepsilon\delta^2 > 0 for ε>0\varepsilon > 0 (The rationals form a totally ordered field).

[L4]

Null definition; a sequence that is 00 from some index on is null (Null sequence).

[L5]

Ideal arithmetic in C\mathcal{C}: an ideal containing 11 is the whole ring (Cauchy sequences form a commutative ring, Null sequences form an ideal).

Proof

technique · direct
1.1

Fix δ>0\delta > 0 and N0N_0 with an>δ|a_n| > \delta for all nN0n \ge N_0; in particular an0a_n \ne 0 there.

L1
2.1

Define bn=1b_n = 1 for n<N0n < N_0 and bn=1/anb_n = 1/a_n for nN0n \ge N_0.

step 1.1choose
3.1

(bn)(b_n) is Cauchy: for m,nN0m, n \ge N_0, bmbn=anamaman<amanδ2|b_m - b_n| = \dfrac{|a_n - a_m|}{|a_m|\,|a_n|} < \dfrac{|a_m - a_n|}{\delta^2}; given ε>0\varepsilon > 0, choosing the Cauchy index of (an)(a_n) at εδ2\varepsilon\delta^2 makes this <ε< \varepsilon.

step 2.1step 1.1L2L3
3.2

For nN0n \ge N_0, anbn=1a_n b_n = 1, so the sequence (anbn1)(a_n b_n - 1) is 00 from N0N_0 on, hence null.

step 2.1L4
4.1

Therefore 1C=(an)(bn)((anbn)1)1_{\mathcal{C}} = (a_n)(b_n) - \bigl((a_n b_n) - 1\bigr) lies in the ideal generated by (an)(a_n) and N\mathcal{N}, so that ideal is all of C\mathcal{C}; any ideal strictly containing N\mathcal{N} contains a non-null element and thus equals C\mathcal{C}: N\mathcal{N} is maximal.

step 3.1step 3.2L5
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-07-24Open item page →

The real numbers

Definition

The real numbers are the quotient ring

R:=C/N\mathbb{R} := \mathcal{C} / \mathcal{N}

of the ring of Cauchy sequences (Cauchy sequences form a commutative ring) by the ideal of null sequences (Null sequences form an ideal). The class of (an)(a_n) is written [(an)][(a_n)]. Each rational qq maps to the class q^\hat q of the constant sequence (q,q,q,)(q, q, q, \dots).

Remarks

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

The reals form a field

Statement

R=C/N\mathbb{R} = \mathcal{C}/\mathcal{N} (The real numbers) is a field.

Facts & Assumptions

Given: Classes [(an)],[(bn)]R[(a_n)], [(b_n)] \in \mathbb{R}.

[L1]

N\mathcal{N} is an ideal of C\mathcal{C} (Null sequences form an ideal).

[L2]

C\mathcal{C} is a commutative ring with 11 (Cauchy sequences form a commutative ring).

[L3]

Maximality construction: for non-null (an)(a_n) there is Cauchy (bn)(b_n) with (anbn)1(a_n b_n) - 1 null (The null ideal is maximal).

[L4]

The constant sequence 11 is not a null sequence (its terms stay at 11), so N\mathcal{N} is a proper ideal and 1^0^\hat 1 \ne \hat 0 (Null sequence).

Proof

technique · direct
1.1

Operations on classes via representatives are well defined: for z,wNz, w \in \mathcal{N}, ((a+z)+(b+w))(a+b)=z+wN\bigl((a+z)+(b+w)\bigr) - (a+b) = z + w \in \mathcal{N} and (a+z)(b+w)ab=aw+zb+zwN(a+z)(b+w) - ab = aw + zb + zw \in \mathcal{N}, since ideals absorb products and sums.

L1L2
2.1

The ring axioms descend to the quotient because the operations are well defined and C\mathcal{C} is a ring, verified on representatives; 1^0^\hat 1 \ne \hat 0 since the constant sequence 11 is not null.

step 1.1L1L2L4
2.2

Inverses: a nonzero class has a non-null representative (an)(a_n); taking (bn)(b_n) from the maximality construction, (an)(bn)1N(a_n)(b_n) - 1 \in \mathcal{N}, so [(bn)][(b_n)] is a multiplicative inverse of [(an)][(a_n)].

step 1.1L3
3.1

R\mathbb{R} is a commutative ring with 101 \ne 0 in which every nonzero element is invertible: a field.

step 2.1step 2.2
DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-07-24Open item page →

Order on the reals

Definition

A real xx is positive when it has a representative (an)(a_n) together with a rational δ>0\delta > 0 and an index NN such that an>δa_n > \delta for all nNn \ge N. Define

xy    x=y   or   yx is positive,x \le y \iff x = y \;\text{ or }\; y - x \text{ is positive},

and x=x|x| = x if x0x \ge 0, x=x|x| = -x otherwise.

Remarks

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

The reals form a totally ordered field

Statement

The relation of Order on the reals is well defined and makes R\mathbb{R} (The reals form a field) a totally ordered field.

Facts & Assumptions

Given: Reals x,yx, y with representatives (an),(bn)(a_n), (b_n).

[L1]

A sequence (un)n1(u_n)_{n \ge 1} of rational numbers is null if, for every rational ε>0\varepsilon > 0, there is NNN \in \mathbb{N} such that un<ε|u_n| < \varepsilon for every nNn \ge N (Null sequence).

[L2]

Ordered-field arithmetic in Q\mathbb{Q}: δ/2>0\delta/2 > 0; sums and products of eventual lower bounds (The rationals form a totally ordered field).

[L3]

Dichotomy for non-null Cauchy sequences: eventually >δ> \delta or eventually <δ< -\delta (A non-null Cauchy sequence is eventually bounded away from zero, with constant sign).

[L4]

R\mathbb{R} is a field (The reals form a field).

[L5]

In R=C/N\mathbb{R} = \mathcal{C}/\mathcal{N}, x=0x = 0 iff a representative is null; so x0x \ne 0 iff every representative is non-null (The real numbers).

Proof

technique · direct
1.1

Positivity is independent of the representative: if an>δa_n > \delta for nNn \ge N and (anan)(a'_n - a_n) is null, then beyond some NNN' \ge N also anan<δ/2|a'_n - a_n| < \delta/2, so an>δ/2a'_n > \delta/2: the defining property holds for (an)(a'_n) with δ/2\delta/2.

L1L2
1.2

Trichotomy: if x0x \ne 0, any representative is non-null, so by the dichotomy either an>δa_n > \delta eventually (xx positive) or an<δa_n < -\delta eventually (x-x positive); the two exclude each other, and exactly one of xx positive, x=0x = 0, x-x positive holds.

L1L3L5
1.3

Positives are closed under ++ and \cdot: from an>δa_n > \delta and bn>δb_n > \delta' eventually, an+bn>δ+δa_n + b_n > \delta + \delta' and anbn>δδa_n b_n > \delta\delta' eventually, with δ+δ,δδ>0\delta + \delta', \delta\delta' > 0.

L2
2.1

Consequently \le is a total order (trichotomy plus transitivity from closure under sums), compatible with addition (translation preserves the difference) and with multiplication by positives: R\mathbb{R} is a totally ordered field.

step 1.1step 1.2step 1.3L4
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-02 (claude-opus-5)Open item page →

The rationals embed densely in the reals

Statement

The map qq^q \mapsto \hat q (The real numbers) is an embedding of ordered fields. Every real is approximated by rationals: for xRx \in \mathbb{R} and rational ε>0\varepsilon > 0 there is qQq \in \mathbb{Q} with xq^<ε^|x - \hat q| < \hat\varepsilon. Consequently, strictly between any two reals lies a rational.

Facts & Assumptions

Given: A real x=[(an)]x = [(a_n)] and a rational ε>0\varepsilon > 0.

[L1]

The orders of Q\mathbb{Q} and R\mathbb{R}; ordered-field arithmetic (The rationals form a totally ordered field, The reals form a totally ordered field).

[L2]

Field arithmetic in Q\mathbb{Q}: ε/2,δ/4\varepsilon/2, \delta/4 are positive rationals, and every nonzero rational qq has a reciprocal 1/q1/q with q(1/q)=1q \cdot (1/q) = 1 (The rationals form a field).

[L3]

Cauchy definition (Cauchy sequence of rationals).

[L4]

Real positivity via eventual rational lower bounds (Order on the reals).

[L5]

R=C/N\mathbb{R} = \mathcal{C}/\mathcal{N} is a field (The reals form a field), and 0R=0^0_{\mathbb{R}} = \hat 0, 1R=1^1_{\mathbb{R}} = \hat 1 are the classes of the constant sequences (The real numbers). A multiplicative inverse there is unique: if ab=1R=acab = 1_{\mathbb{R}} = ac then b=b(ac)=(ba)c=cb = b(ac) = (ba)c = c.

Proof

technique · direct
1.1

Embedding: constant sequences are Cauchy; q^=r^\hat q = \hat r iff the constant qrq - r is null iff q=rq = r; operations match termwise; and q<rq < r gives the constant lower bound rq>0r - q > 0, so q^<r^\hat q < \hat r and order is preserved and reflected.

L1L4
1.2

Fix NN with aman<ε/2|a_m - a_n| < \varepsilon/2 for all m,nNm, n \ge N, and set q=aNq = a_N.

L3L2
2.1

The difference q^x\hat q - x has representative (aNan)(a_N - a_n) with aNan<ε/2|a_N - a_n| < \varepsilon/2 for nNn \ge N; hence both ε^(xq^)\hat\varepsilon - (x - \hat q) and ε^(q^x)\hat\varepsilon - (\hat q - x) have representatives eventually >ε/2> \varepsilon/2, so both are positive: xq^<ε^|x - \hat q| < \hat\varepsilon.

step 1.2L4L1
2.2

Inverses: let qq be a nonzero rational. Then q^0^=0R\hat q \ne \hat 0 = 0_{\mathbb{R}} by the injectivity of step 1.1, and 1/q1/q exists in Q\mathbb{Q} by [L2]; since the operations match termwise (step 1.1), q^1/q^=q(1/q)^=1^=1R\hat q \cdot \widehat{1/q} = \widehat{q \cdot (1/q)} = \hat 1 = 1_{\mathbb{R}}. Inverses in R\mathbb{R} are unique by [L5], so (q^)1=1/q^(\hat q)^{-1} = \widehat{1/q}: the embedding preserves reciprocals.

step 1.1L2L5
3.1

Density: let x<yx < y; pick δ>0\delta > 0 rational and NN with the representative of yxy - x eventually >δ> \delta; set ε=δ/4\varepsilon = \delta/4 and pick qq with xq^<ε^|x - \hat q| < \hat\varepsilon; then q=q+2εq' = q + 2\varepsilon satisfies q^xε^+2ε^=ε^>0\hat q' - x \ge -\hat\varepsilon + 2\hat\varepsilon = \hat\varepsilon > 0 and yq^δ^ε^2ε^=δ^/4>0y - \hat q' \ge \hat\delta - \hat\varepsilon - 2\hat\varepsilon = \hat\delta/4 > 0, so x<q^<yx < \hat q' < y.

step 2.1L4L1L2
4.1

The rationals embed as an ordered subfield — injectively, preserving the order in both directions, the ring operations, and reciprocals — and they approximate every real arbitrarily well and separate any two reals.

step 1.1step 2.2step 3.1
DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-07-24Open item page →

Limits and Cauchy sequences of reals

Definition

A sequence (xk)(x_k) of reals converges to xRx \in \mathbb{R} when for every rational ε>0\varepsilon > 0 there is KK with xkx<ε^|x_k - x| < \hat\varepsilon for all kKk \ge K. It is Cauchy when for every rational ε>0\varepsilon > 0 there is KK with xkxl<ε^|x_k - x_l| < \hat\varepsilon for all k,lKk, l \ge K.

Remarks

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

The reals are complete

Statement

Every Cauchy sequence of real numbers (Limits and Cauchy sequences of reals) converges to a real number. Together with The reals form a totally ordered field, this completes the construction: R\mathbb{R} is a complete totally ordered field.

Facts & Assumptions

Given: A Cauchy sequence (xk)k1(x_k)_{k \ge 1} of reals.

[L1]

Rational approximation: for any real zz and rational η>0\eta > 0 there is qq with zq^<η^|z - \hat q| < \hat\eta (The rationals embed densely in the reals).

[L2]

Archimedean property: for rational ε>0\varepsilon > 0 there is kk with 1/k<ε1/k < \varepsilon (The rationals are Archimedean).

[L3]

Cauchy definitions in Q\mathbb{Q} and R\mathbb{R} (Cauchy sequence of rationals, Limits and Cauchy sequences of reals).

[L4]

The embedding preserves and reflects order and arithmetic; triangle inequality in R\mathbb{R} (The rationals embed densely in the reals, The reals form a totally ordered field, Order on the reals).

[L5]

Reals are classes of rational Cauchy sequences (The real numbers).

Proof

technique · direct
1.1

For each k1k \ge 1 pick a rational qkq_k with xkq^k<1/k^|x_k - \hat q_k| < \widehat{1/k}.

L1choose
2.1

(qk)(q_k) is Cauchy in Q\mathbb{Q}: given rational ε>0\varepsilon > 0, pick k0k_0 with 1/k0<ε/31/k_0 < \varepsilon/3 and KK with xkxl<ε/3^|x_k - x_l| < \widehat{\varepsilon/3} for k,lKk, l \ge K; then for k,lmax(k0,K)k, l \ge \max(k_0, K), qkql^q^kxk+xkxl+xlq^l<1/k^+ε/3^+1/l^3ε/3^=ε^\widehat{|q_k - q_l|} \le |\hat q_k - x_k| + |x_k - x_l| + |x_l - \hat q_l| < \widehat{1/k} + \widehat{\varepsilon/3} + \widehat{1/l} \le 3\,\widehat{\varepsilon/3} = \hat\varepsilon, and the embedding reflects order, so qkql<ε|q_k - q_l| < \varepsilon.

step 1.1L2L3L4
3.1

Set x:=[(qk)]Rx := [(q_k)] \in \mathbb{R}, the class of this rational Cauchy sequence.

step 2.1L5
4.1

xkxx_k \to x: given rational ε>0\varepsilon > 0, pick k1k_1 with 1/k1<ε/31/k_1 < \varepsilon/3 and K2K_2 with qkql<ε/3|q_k - q_l| < \varepsilon/3 for k,lK2k, l \ge K_2; for kmax(k1,K2)k \ge \max(k_1, K_2), the difference q^kx\hat q_k - x has representative (qkql)l(q_k - q_l)_l, whose absolute values qkql|q_k - q_l| are eventually below ε/3\varepsilon/3, so q^kxε/3^|\hat q_k - x| \le \widehat{\varepsilon/3}, and xkxxkq^k+q^kx<1/k^+ε/3^2ε/3^<ε^|x_k - x| \le |x_k - \hat q_k| + |\hat q_k - x| < \widehat{1/k} + \widehat{\varepsilon/3} \le 2\,\widehat{\varepsilon/3} < \hat\varepsilon.

step 1.1step 2.1step 3.1L4
5.1

Every Cauchy sequence of reals converges in R\mathbb{R}: the reals are complete.

step 4.1

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

The sequence 1/n1/n is null

Example

The sequence (1/n)n1(1/n)_{n \ge 1} of rationals is a null sequence (Null sequence): its terms become smaller than any prescribed positive rational. It is the standard witness that "eventually arbitrarily small" is a nonvacuous notion, and the rate 1/k1/k used in the completeness proof.

Facts & Assumptions

Given: A rational ε>0\varepsilon > 0.

[L1]

Archimedean property (The rationals are Archimedean).

[L2]

Order arithmetic: 0<1/n1/N0 < 1/n \le 1/N for nN1n \ge N \ge 1 (The rationals form a totally ordered field).

[L3]

Null definition (Null sequence).

Verification

technique · direct
1.1

Pick a natural N1N \ge 1 with 1/N<ε1/N < \varepsilon.

L1
2.1

For every nNn \ge N: 0<1/n1/N<ε0 < 1/n \le 1/N < \varepsilon, so 1/n<ε|1/n| < \varepsilon.

step 1.1L2
3.1

(1/n)(1/n) is null.

step 2.1L3
False statementConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

FALSE: some rational number squares to 2

Statement

False claim: there exists xQx \in \mathbb{Q} with x2=2x^2 = 2.

Facts & Assumptions

Given: The rationals as quotients of integer pairs (The rationals as equivalence classes of pairs of integers).

[A1]

Every rational can be written a/ba/b in lowest terms, with a,ba, b not both even (cancel common factors of 22; the process terminates by well-ordering of N\mathbb{N}).

[A2]

Parity in Z\mathbb{Z}: if k2k^2 is even then kk is even (an odd k=2j+1k = 2j+1 has odd square 4j2+4j+14j^2 + 4j + 1).

Refutation

technique · contradiction
1.1

Assume, for contradiction, that some xQx \in \mathbb{Q} has x2=2x^2 = 2; write x=a/bx = a/b in lowest terms, a,ba, b not both even.

assume-contraA1
2.1

Clearing denominators: a2=2b2a^2 = 2b^2.

step 1.1algebra
3.1

a2a^2 is even, hence aa is even: a=2ca = 2c.

step 2.1A2
4.1

Substituting: 4c2=2b24c^2 = 2b^2, so b2=2c2b^2 = 2c^2 is even, hence bb is even.

step 3.1A2algebra
5.1

Both aa and bb are even, contradicting the lowest-terms choice of step 1.1; the assumption fails: no rational squares to 22.

step 4.1step 1.1discharge-contradiction
False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

FALSE: the rationals are complete

Statement

False claim: every Cauchy sequence of rationals converges to a rational (where (an)q(a_n) \to q means (anq)(a_n - q) is null).

This is precisely the defect the construction of R\mathbb{R} repairs.

Facts & Assumptions

Given: The decimal truncations of 2\sqrt 2, built below.

[A1]

In N\mathbb{N}: for each nn there is a largest natural kk with k22102nk^2 \le 2 \cdot 10^{2n} (only finitely many candidates, since k>210nk > 2 \cdot 10^n already fails); and n<10nn < 10^n.

[L2]

No rational squares to 22 (FALSE: some rational number squares to 2).

[L3]

A constant sequence is null only if the constant is 00; sums of null sequences are null; a Cauchy multiple of a null sequence is null (Null sequence, Null sequences form an ideal).

[L4]

Archimedean property, so 10n10^{-n} falls below any positive rational (The rationals are Archimedean).

Refutation

technique · direct
1.1

For each nn let knk_n be the largest natural with kn22102nk_n^2 \le 2 \cdot 10^{2n}, and set sn=kn/10ns_n = k_n / 10^n; then sn22<(sn+10n)2s_n^2 \le 2 < (s_n + 10^{-n})^2, and sn2s_n \le 2 (since kn22102n<(210n)2k_n^2 \le 2\cdot 10^{2n} < (2 \cdot 10^n)^2).

A1L1
2.1

(sn)(s_n) is Cauchy: for mnm \ge n, (10mnkn)22102m(10^{m-n} k_n)^2 \le 2 \cdot 10^{2m} gives 10mnknkm10^{m-n} k_n \le k_m, so snsms_n \le s_m; and sm22<(sn+10n)2s_m^2 \le 2 < (s_n + 10^{-n})^2 forces sm<sn+10ns_m < s_n + 10^{-n}; hence 0smsn<10n0 \le s_m - s_n < 10^{-n}, and 10n10^{-n} eventually falls below any ε>0\varepsilon > 0.

step 1.1L1L4
2.2

(sn22)(s_n^2 - 2) is null: 02sn2<(sn+10n)2sn2=10n(2sn+10n)510n0 \le 2 - s_n^2 < (s_n + 10^{-n})^2 - s_n^2 = 10^{-n}(2 s_n + 10^{-n}) \le 5 \cdot 10^{-n}.

step 1.1L1L4
3.1

If (sn)(s_n) converged to a rational qq, then (snq)(s_n - q) would be null; since (sn+q)(s_n + q) is Cauchy, (sn2q2)=(snq)(sn+q)(s_n^2 - q^2) = (s_n - q)(s_n + q) would be null; adding the null (2sn2)(2 - s_n^2), the constant 2q22 - q^2 would be null, forcing q2=2q^2 = 2.

step 2.1step 2.2L3L1
4.1

No rational squares to 22, so (sn)(s_n) is a Cauchy sequence of rationals with no rational limit: the claim is refuted.

step 3.1step 2.1L2

Sources