Metamath Proof Explorer

Theorem 0.999...

Description: The recurring decimal 0.999..., which is defined as the infinite sum 0.9 + 0.09 + 0.009 + ... i.e. 9 / 1 0 ^ 1 + 9 / 1 0 ^ 2 + 9 / 1 0 ^ 3 + ... , is exactly equal to 1, according to ZF set theory. Interestingly, about 40% of the people responding to a poll at http://forum.physorg.com/index.php?showtopic=13177 disagree. (Contributed by NM, 2-Nov-2007) (Revised by AV, 8-Sep-2021)

Ref Expression
Assertion 0.999... Σ 𝑘 ∈ ℕ ( 9 / ( 1 0 ↑ 𝑘 ) ) = 1

Proof

Step Hyp Ref Expression
1 9cn ⊢ 9 ∈ ℂ
2 10re ⊢ 1 0 ∈ ℝ
3 2 recni ⊢ 1 0 ∈ ℂ
4 nnnn0 ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
5 expcl ⊢ ( ( 1 0 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 1 0 ↑ 𝑘 ) ∈ ℂ )
6 3 4 5 sylancr ⊢ ( 𝑘 ∈ ℕ → ( 1 0 ↑ 𝑘 ) ∈ ℂ )
7 3 a1i ⊢ ( 𝑘 ∈ ℕ → 1 0 ∈ ℂ )
8 10pos ⊢ 0 < 1 0
9 2 8 gt0ne0ii ⊢ 1 0 ≠ 0
10 9 a1i ⊢ ( 𝑘 ∈ ℕ → 1 0 ≠ 0 )
11 nnz ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℤ )
12 7 10 11 expne0d ⊢ ( 𝑘 ∈ ℕ → ( 1 0 ↑ 𝑘 ) ≠ 0 )
13 divrec ⊢ ( ( 9 ∈ ℂ ∧ ( 1 0 ↑ 𝑘 ) ∈ ℂ ∧ ( 1 0 ↑ 𝑘 ) ≠ 0 ) → ( 9 / ( 1 0 ↑ 𝑘 ) ) = ( 9 · ( 1 / ( 1 0 ↑ 𝑘 ) ) ) )
14 1 6 12 13 mp3an2i ⊢ ( 𝑘 ∈ ℕ → ( 9 / ( 1 0 ↑ 𝑘 ) ) = ( 9 · ( 1 / ( 1 0 ↑ 𝑘 ) ) ) )
15 7 10 11 exprecd ⊢ ( 𝑘 ∈ ℕ → ( ( 1 / 1 0 ) ↑ 𝑘 ) = ( 1 / ( 1 0 ↑ 𝑘 ) ) )
16 15 oveq2d ⊢ ( 𝑘 ∈ ℕ → ( 9 · ( ( 1 / 1 0 ) ↑ 𝑘 ) ) = ( 9 · ( 1 / ( 1 0 ↑ 𝑘 ) ) ) )
17 14 16 eqtr4d ⊢ ( 𝑘 ∈ ℕ → ( 9 / ( 1 0 ↑ 𝑘 ) ) = ( 9 · ( ( 1 / 1 0 ) ↑ 𝑘 ) ) )
18 17 sumeq2i ⊢ Σ 𝑘 ∈ ℕ ( 9 / ( 1 0 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ℕ ( 9 · ( ( 1 / 1 0 ) ↑ 𝑘 ) )
19 2 9 rereccli ⊢ ( 1 / 1 0 ) ∈ ℝ
20 19 recni ⊢ ( 1 / 1 0 ) ∈ ℂ
21 0re ⊢ 0 ∈ ℝ
22 2 8 recgt0ii ⊢ 0 < ( 1 / 1 0 )
23 21 19 22 ltleii ⊢ 0 ≤ ( 1 / 1 0 )
24 19 absidi ⊢ ( 0 ≤ ( 1 / 1 0 ) → ( abs ‘ ( 1 / 1 0 ) ) = ( 1 / 1 0 ) )
25 23 24 ax-mp ⊢ ( abs ‘ ( 1 / 1 0 ) ) = ( 1 / 1 0 )
26 1lt10 ⊢ 1 < 1 0
27 recgt1 ⊢ ( ( 1 0 ∈ ℝ ∧ 0 < 1 0 ) → ( 1 < 1 0 ↔ ( 1 / 1 0 ) < 1 ) )
28 2 8 27 mp2an ⊢ ( 1 < 1 0 ↔ ( 1 / 1 0 ) < 1 )
29 26 28 mpbi ⊢ ( 1 / 1 0 ) < 1
30 25 29 eqbrtri ⊢ ( abs ‘ ( 1 / 1 0 ) ) < 1
31 geoisum1c ⊢ ( ( 9 ∈ ℂ ∧ ( 1 / 1 0 ) ∈ ℂ ∧ ( abs ‘ ( 1 / 1 0 ) ) < 1 ) → Σ 𝑘 ∈ ℕ ( 9 · ( ( 1 / 1 0 ) ↑ 𝑘 ) ) = ( ( 9 · ( 1 / 1 0 ) ) / ( 1 − ( 1 / 1 0 ) ) ) )
32 1 20 30 31 mp3an ⊢ Σ 𝑘 ∈ ℕ ( 9 · ( ( 1 / 1 0 ) ↑ 𝑘 ) ) = ( ( 9 · ( 1 / 1 0 ) ) / ( 1 − ( 1 / 1 0 ) ) )
33 1 3 9 divreci ⊢ ( 9 / 1 0 ) = ( 9 · ( 1 / 1 0 ) )
34 1 3 9 divcan2i ⊢ ( 1 0 · ( 9 / 1 0 ) ) = 9
35 ax-1cn ⊢ 1 ∈ ℂ
36 3 35 20 subdii ⊢ ( 1 0 · ( 1 − ( 1 / 1 0 ) ) ) = ( ( 1 0 · 1 ) − ( 1 0 · ( 1 / 1 0 ) ) )
37 3 mulid1i ⊢ ( 1 0 · 1 ) = 1 0
38 3 9 recidi ⊢ ( 1 0 · ( 1 / 1 0 ) ) = 1
39 37 38 oveq12i ⊢ ( ( 1 0 · 1 ) − ( 1 0 · ( 1 / 1 0 ) ) ) = ( 1 0 − 1 )
40 10m1e9 ⊢ ( 1 0 − 1 ) = 9
41 36 39 40 3eqtrri ⊢ 9 = ( 1 0 · ( 1 − ( 1 / 1 0 ) ) )
42 34 41 eqtri ⊢ ( 1 0 · ( 9 / 1 0 ) ) = ( 1 0 · ( 1 − ( 1 / 1 0 ) ) )
43 9re ⊢ 9 ∈ ℝ
44 43 2 9 redivcli ⊢ ( 9 / 1 0 ) ∈ ℝ
45 44 recni ⊢ ( 9 / 1 0 ) ∈ ℂ
46 35 20 subcli ⊢ ( 1 − ( 1 / 1 0 ) ) ∈ ℂ
47 45 46 3 9 mulcani ⊢ ( ( 1 0 · ( 9 / 1 0 ) ) = ( 1 0 · ( 1 − ( 1 / 1 0 ) ) ) ↔ ( 9 / 1 0 ) = ( 1 − ( 1 / 1 0 ) ) )
48 42 47 mpbi ⊢ ( 9 / 1 0 ) = ( 1 − ( 1 / 1 0 ) )
49 33 48 oveq12i ⊢ ( ( 9 / 1 0 ) / ( 9 / 1 0 ) ) = ( ( 9 · ( 1 / 1 0 ) ) / ( 1 − ( 1 / 1 0 ) ) )
50 9pos ⊢ 0 < 9
51 43 2 50 8 divgt0ii ⊢ 0 < ( 9 / 1 0 )
52 44 51 gt0ne0ii ⊢ ( 9 / 1 0 ) ≠ 0
53 45 52 dividi ⊢ ( ( 9 / 1 0 ) / ( 9 / 1 0 ) ) = 1
54 32 49 53 3eqtr2i ⊢ Σ 𝑘 ∈ ℕ ( 9 · ( ( 1 / 1 0 ) ↑ 𝑘 ) ) = 1
55 18 54 eqtri ⊢ Σ 𝑘 ∈ ℕ ( 9 / ( 1 0 ↑ 𝑘 ) ) = 1