Main derivation
S01 · definition
Before
\mathbb{R}After
\{[(a_n)]\mid (a_n)\ \text{Cauchy in}\ \mathbb{Q}\},\ \iota(q)=[(q)_{n\ge1}]Conditions: none
Rule: equiv_def · Uses: G2, G3, mko_real_def
Leaf basis: equiv_def + cauchy_def + mko_real_def
By MKO assumption a1, work in the Cauchy-completion setting: a real number is an equivalence class of Cauchy sequences of rationals, and a rational q is embedded by ι as the class of its constant sequence (every term equal to q). A constant sequence is Cauchy, since |q−q|=0<ε for all m, n.
S02 · equivalent
Before
[(a_n)]=[(b_n)]
After
(a_n)\sim(b_n)
Conditions: (a_n),(b_n)\ \text{Cauchy}
Rule: thm_equiv_relation · Uses: S01, thm_equiv_relation
Leaf basis: thm_equiv_relation + def_unfold
∼ is an equivalence relation (cited as thm_equiv_relation), so the classes are well defined, and two classes are equal exactly when their representative sequences are equivalent. From now on, to prove two reals equal it suffices to prove the sequences equivalent, and to prove them different, that the sequences are not equivalent.
S03 · definition
Before
a_n=1-10^{-n}\ \ (n\ge1)After
a_1=\tfrac{9}{10},\ a_2=\tfrac{99}{100},\ a_3=\tfrac{999}{1000}Conditions: none
Rule: def_intro · Uses: G4
Leaf basis: def_intro + q_ordered_field + numeric_evaluation
Define a_n=1−10^{−n}. Every term is rational (10^{−n}=1/10^n with 10^n≠0). The first three terms are 9/10, 99/100, 999/1000 (N1 to N3), the finite decimals 0.9, 0.99, 0.999; in general a_n is the finite decimal with n nines after the point.
S04 · equivalent
Before
a_n-1
After
-10^{-n},\quad |a_n-1|=10^{-n}Conditions: none
Rule: q_ordered_field · Uses: S03, q_ordered_field
Leaf basis: q_ordered_field + add_inverse + numeric_evaluation
a_n−1=(1−10^{−n})−1=−10^{−n}. 10^n>0, so 10^{−n}=1/10^n>0 and |−10^{−n}|=10^{−n}. Example: a_3−1=999/1000−1=−1/1000 (N4).
S05 · implies
Before
n\ge 1\ \text{an integer}After
10^n>n
Conditions: n\ge 1
Rule: L_pow_ten · Uses: L_pow_ten
Leaf basis: L_pow_ten
Lemma L_pow_ten: for every integer n≥1, 10^n>n. It is proved by induction in S05.1 and S05.2. N8 checks n=1 to 40; that is a finite check only, not a proof; the proof is the induction.
S06 · implies
Before
\varepsilon\in\mathbb{Q},\ \varepsilon>0After
\exists N\ \forall n\ge N:\ 10^{-n}<\varepsilonConditions: \varepsilon>0
Rule: L_small · Uses: L_small
Leaf basis: L_small
Lemma L_small: every positive rational ε has an N with 10^{−n}<ε for n≥N. It is proved in S06.1 and S06.2. Only rational arithmetic and order are used, not the reals being constructed, which avoids circularity.
S07 · implies
Before
(a_n)_{n\ge1}After
(a_n)\ \text{is Cauchy}Conditions: none
Rule: cauchy_def · Uses: S04, S06, G2
Leaf basis: cauchy_def + q_ordered_field + forall_intro + exists_intro
Take any rational ε>0. Apply L_small to ε/2 (still a positive rational) to get N with 10^{−n}<ε/2 for n≥N. For m,n≥N: |a_m−a_n|=|(a_m−1)+(1−a_n)|≤|a_m−1|+|a_n−1|=10^{−m}+10^{−n}<ε/2+ε/2=ε (triangle inequality and S04). ε was arbitrary, so (a_n) is a Cauchy sequence.
S08 · implies
Before
(a_n),\ (1)_{n\ge1}After
(a_n)\sim(1)_{n\ge1}Conditions: none
Rule: equiv_def · Uses: S01, S04, S06, S07, G3
Leaf basis: equiv_def + forall_intro + exists_intro
Both sequences are Cauchy (S07 and S01). Take any rational ε>0; L_small gives N with |a_n−1|=10^{−n}<ε for n≥N (S04). ε was arbitrary, so by G3, (a_n) is equivalent to the constant sequence 1.
S09 · equivalent
Before
(a_n)\sim(1)_{n\ge1}After
[(a_n)]=\iota(1)
Conditions: none
Rule: thm_equiv_relation · Uses: S02, S08
Leaf basis: thm_equiv_relation + def_unfold
By S02, equivalence of sequences is exactly equality of classes, so [(a_n)]=[(1)_{n≥1}]=ι(1). That is, the real number determined by the whole sequence of truncations 0.9, 0.99, 0.999 and so on is exactly the embedding of the rational 1; the usual statement '0.9 with the digit 9 repeating indefinitely equals 1' is, in this construction, this equality.
S10 · implies
Before
p\neq q\ \text{in}\ \mathbb{Q}After
\iota(p)\neq\iota(q)
Conditions: none
Rule: contradiction · Uses: S02, G3, q_ordered_field
Leaf basis: contradiction + q_ordered_field + equiv_def
Let p≠q and δ=|p−q|>0 (a rational). If the constant sequences (p) and (q) were equivalent, taking ε=δ would give N with |p−q|<δ for n≥N, that is δ<δ, a contradiction. So the constant sequences are not equivalent, and by S02, ι(p)≠ι(q): ι is injective, and different rationals embed as different reals.
S11 · implies
Before
\tfrac{999}{1000}\neq 1After
\iota(\tfrac{999}{1000})\neq\iota(1)Conditions: none
Rule: forall_elim · Uses: S10, G4
Leaf basis: forall_elim + numeric_evaluation
999/1000≠1 (they differ by 1/1000, N12, N13), so by S10 the real ι(999/1000) denoted by the finite decimal 0.999 is not 1. What equals 1 is the class of the whole sequence of truncations (S09), not any single finite truncation; a finite truncation is only an approximation.
S12 · implies
Before
0.375
After
\tfrac{375}{1000}=\tfrac{3}{8},\quad \iota(\tfrac{3}{8})\in\mathbb{R}Conditions: none
Rule: mko_real_def · Uses: S01, G4
Leaf basis: mko_real_def + equiv_def + numeric_evaluation
The finite decimal 0.375=3/10+7/100+5/1000=375/1000=3/8 (N14, N15) is rational; in ℝ it is ι(3/8), the class of the constant sequence 3/8. A finite decimal is not a separate number system, and certainly not irrational.
S13 · implies
Before
\text{S07, S09, S10, S11, S12}After
[(a_n)]=\iota(1);\ \iota\ \text{injective};\ \iota(\tfrac{999}{1000})\neq\iota(1);\ 0.375=\tfrac{3}{8}Conditions: none
Rule: and_intro_elim · Uses: S07, S09, S10, S11, S12
Leaf basis: and_intro_elim
The truncation sequence (a_n) is Cauchy and equivalent to the constant sequence 1, so the real it determines is ι(1); ι is injective, so the single finite truncation 0.999 is not 1; and the finite decimal 0.375 is the embedding of the rational 3/8.
Substeps and lemmas
S05.1 · induction_base
Before
n=1
After
10^1=10>1
Conditions: none
Rule: nat_induction · Uses: q_ordered_field
Leaf basis: nat_induction + numeric_evaluation
Base case n=1: 10¹=10>1 (N5).
S05.2 · induction_step
Before
10^n>n\ \ (n\ge1)
After
10^{n+1}>n+1Conditions: n\ge 1
Rule: nat_induction · Uses: S05.1, q_ordered_field
Leaf basis: nat_induction + power_laws + q_ordered_field
Assume 10^n>n (n≥1). Then 10^{n+1}=10·10^n>10n (multiplying by the positive 10 preserves the inequality). Also 10n−(n+1)=9n−1 (N6 is an identity), and for n≥1, 9n−1≥9·1−1=8>0 (N7), so 10n>n+1. Together 10^{n+1}>n+1. By the induction principle (S05.1 and this step), 10^n>n for all n≥1, which proves Lemma L_pow_ten.
S06.1 · implies
Before
\varepsilon=\frac{p}{q}>0,\ p,q\in\mathbb{Z},\ q\neq0After
\varepsilon=\frac{r}{s},\ r,s\in\mathbb{Z},\ r\ge1,\ s\ge1Conditions: \varepsilon>0
Rule: frac_rules · Uses: q_ordered_field, pos_int_ge_one
Leaf basis: frac_rules + q_ordered_field + pos_int_ge_one + exists_elim
ε is rational, so ε=p/q with q≠0. If q<0, the fraction rule gives p/q=(−p)/(−q), so we may assume q>0. Then p=εq is a product of two positives, so p>0. Let r=p and s=q; both are positive integers, so r≥1 and s≥1.
S06.2 · implies
Before
N:=s,\ n\ge N
After
10^{-n}<\tfrac{1}{n}\le\tfrac{1}{s}\le\tfrac{r}{s}=\varepsilonConditions: n\ge s\ge 1; r\ge 1
Rule: q_ordered_field · Uses: S06.1, L_pow_ten
Leaf basis: q_ordered_field + L_pow_ten + exists_intro + forall_intro
Take N=s. For n≥s: by L_pow_ten, 10^n>n>0, and taking reciprocals of positives reverses the inequality, so 10^{−n}=1/10^n<1/n; n≥s>0 gives 1/n≤1/s; r≥1 and 1/s>0 give 1/s≤r/s=ε. Chaining, 10^{−n}<ε. Example: for ε=1/100, r=1 and s=100, and N=100 works (N9); the lemma needs some N, not the least one; for instance already 10^{−3}<1/100 at n=3 (N10). S06.1 and S06.2 together prove Lemma L_small.