Proof of Theorem 0.999...OLD
Step | Hyp | Ref
| Expression |
1 | | 10reOLD 10986 |
. . . . . . 7
⊢ 10 ∈
ℝ |
2 | 1 | recni 9931 |
. . . . . 6
⊢ 10 ∈
ℂ |
3 | | nnnn0 11176 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) |
4 | | expcl 12740 |
. . . . . 6
⊢ ((10
∈ ℂ ∧ 𝑘
∈ ℕ0) → (10↑𝑘) ∈ ℂ) |
5 | 2, 3, 4 | sylancr 694 |
. . . . 5
⊢ (𝑘 ∈ ℕ →
(10↑𝑘) ∈
ℂ) |
6 | 2 | a1i 11 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → 10 ∈
ℂ) |
7 | | 10posOLD 11000 |
. . . . . . . 8
⊢ 0 <
10 |
8 | 1, 7 | gt0ne0ii 10443 |
. . . . . . 7
⊢ 10 ≠
0 |
9 | 8 | a1i 11 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → 10 ≠
0) |
10 | | nnz 11276 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℤ) |
11 | 6, 9, 10 | expne0d 12876 |
. . . . 5
⊢ (𝑘 ∈ ℕ →
(10↑𝑘) ≠
0) |
12 | | 9cn 10985 |
. . . . . 6
⊢ 9 ∈
ℂ |
13 | | divrec 10580 |
. . . . . 6
⊢ ((9
∈ ℂ ∧ (10↑𝑘) ∈ ℂ ∧ (10↑𝑘) ≠ 0) → (9 /
(10↑𝑘)) = (9 ·
(1 / (10↑𝑘)))) |
14 | 12, 13 | mp3an1 1403 |
. . . . 5
⊢
(((10↑𝑘) ∈
ℂ ∧ (10↑𝑘)
≠ 0) → (9 / (10↑𝑘)) = (9 · (1 / (10↑𝑘)))) |
15 | 5, 11, 14 | syl2anc 691 |
. . . 4
⊢ (𝑘 ∈ ℕ → (9 /
(10↑𝑘)) = (9 ·
(1 / (10↑𝑘)))) |
16 | 6, 9, 10 | exprecd 12878 |
. . . . 5
⊢ (𝑘 ∈ ℕ → ((1 /
10)↑𝑘) = (1 /
(10↑𝑘))) |
17 | 16 | oveq2d 6565 |
. . . 4
⊢ (𝑘 ∈ ℕ → (9
· ((1 / 10)↑𝑘))
= (9 · (1 / (10↑𝑘)))) |
18 | 15, 17 | eqtr4d 2647 |
. . 3
⊢ (𝑘 ∈ ℕ → (9 /
(10↑𝑘)) = (9 ·
((1 / 10)↑𝑘))) |
19 | 18 | sumeq2i 14277 |
. 2
⊢
Σ𝑘 ∈
ℕ (9 / (10↑𝑘)) =
Σ𝑘 ∈ ℕ (9
· ((1 / 10)↑𝑘)) |
20 | 1, 8 | rereccli 10669 |
. . . . 5
⊢ (1 / 10)
∈ ℝ |
21 | 20 | recni 9931 |
. . . 4
⊢ (1 / 10)
∈ ℂ |
22 | | 0re 9919 |
. . . . . . 7
⊢ 0 ∈
ℝ |
23 | 1, 7 | recgt0ii 10808 |
. . . . . . 7
⊢ 0 < (1
/ 10) |
24 | 22, 20, 23 | ltleii 10039 |
. . . . . 6
⊢ 0 ≤ (1
/ 10) |
25 | 20 | absidi 13965 |
. . . . . 6
⊢ (0 ≤
(1 / 10) → (abs‘(1 / 10)) = (1 / 10)) |
26 | 24, 25 | ax-mp 5 |
. . . . 5
⊢
(abs‘(1 / 10)) = (1 / 10) |
27 | | 1lt10OLD 11115 |
. . . . . 6
⊢ 1 <
10 |
28 | | recgt1 10798 |
. . . . . . 7
⊢ ((10
∈ ℝ ∧ 0 < 10) → (1 < 10 ↔ (1 / 10) <
1)) |
29 | 1, 7, 28 | mp2an 704 |
. . . . . 6
⊢ (1 <
10 ↔ (1 / 10) < 1) |
30 | 27, 29 | mpbi 219 |
. . . . 5
⊢ (1 / 10)
< 1 |
31 | 26, 30 | eqbrtri 4604 |
. . . 4
⊢
(abs‘(1 / 10)) < 1 |
32 | | geoisum1c 14450 |
. . . 4
⊢ ((9
∈ ℂ ∧ (1 / 10) ∈ ℂ ∧ (abs‘(1 / 10)) < 1)
→ Σ𝑘 ∈
ℕ (9 · ((1 / 10)↑𝑘)) = ((9 · (1 / 10)) / (1 − (1 /
10)))) |
33 | 12, 21, 31, 32 | mp3an 1416 |
. . 3
⊢
Σ𝑘 ∈
ℕ (9 · ((1 / 10)↑𝑘)) = ((9 · (1 / 10)) / (1 − (1 /
10))) |
34 | 12, 2, 8 | divreci 10649 |
. . . 4
⊢ (9 / 10)
= (9 · (1 / 10)) |
35 | 12, 2, 8 | divcan2i 10647 |
. . . . . 6
⊢ (10
· (9 / 10)) = 9 |
36 | | ax-1cn 9873 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
37 | 2, 36, 21 | subdii 10358 |
. . . . . . 7
⊢ (10
· (1 − (1 / 10))) = ((10 · 1) − (10 · (1 /
10))) |
38 | 2 | mulid1i 9921 |
. . . . . . . 8
⊢ (10
· 1) = 10 |
39 | 2, 8 | recidi 10635 |
. . . . . . . 8
⊢ (10
· (1 / 10)) = 1 |
40 | 38, 39 | oveq12i 6561 |
. . . . . . 7
⊢ ((10
· 1) − (10 · (1 / 10))) = (10 − 1) |
41 | 36, 12 | addcomi 10106 |
. . . . . . . . 9
⊢ (1 + 9) =
(9 + 1) |
42 | | df-10OLD 10964 |
. . . . . . . . 9
⊢ 10 = (9 +
1) |
43 | 41, 42 | eqtr4i 2635 |
. . . . . . . 8
⊢ (1 + 9) =
10 |
44 | 2, 36, 12, 43 | subaddrii 10249 |
. . . . . . 7
⊢ (10
− 1) = 9 |
45 | 37, 40, 44 | 3eqtrri 2637 |
. . . . . 6
⊢ 9 = (10
· (1 − (1 / 10))) |
46 | 35, 45 | eqtri 2632 |
. . . . 5
⊢ (10
· (9 / 10)) = (10 · (1 − (1 / 10))) |
47 | | 9re 10984 |
. . . . . . . 8
⊢ 9 ∈
ℝ |
48 | 47, 1, 8 | redivcli 10671 |
. . . . . . 7
⊢ (9 / 10)
∈ ℝ |
49 | 48 | recni 9931 |
. . . . . 6
⊢ (9 / 10)
∈ ℂ |
50 | 36, 21 | subcli 10236 |
. . . . . 6
⊢ (1
− (1 / 10)) ∈ ℂ |
51 | 49, 50, 2, 8 | mulcani 10545 |
. . . . 5
⊢ ((10
· (9 / 10)) = (10 · (1 − (1 / 10))) ↔ (9 / 10) = (1
− (1 / 10))) |
52 | 46, 51 | mpbi 219 |
. . . 4
⊢ (9 / 10)
= (1 − (1 / 10)) |
53 | 34, 52 | oveq12i 6561 |
. . 3
⊢ ((9 / 10)
/ (9 / 10)) = ((9 · (1 / 10)) / (1 − (1 / 10))) |
54 | | 9pos 10999 |
. . . . . 6
⊢ 0 <
9 |
55 | 47, 1, 54, 7 | divgt0ii 10820 |
. . . . 5
⊢ 0 < (9
/ 10) |
56 | 48, 55 | gt0ne0ii 10443 |
. . . 4
⊢ (9 / 10)
≠ 0 |
57 | 49, 56 | dividi 10637 |
. . 3
⊢ ((9 / 10)
/ (9 / 10)) = 1 |
58 | 33, 53, 57 | 3eqtr2i 2638 |
. 2
⊢
Σ𝑘 ∈
ℕ (9 · ((1 / 10)↑𝑘)) = 1 |
59 | 19, 58 | eqtri 2632 |
1
⊢
Σ𝑘 ∈
ℕ (9 / (10↑𝑘)) =
1 |