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... 
|- sum_ k e. NN ( 9 / ( ; 1 0 ^ k ) ) = 1

Proof

Step Hyp Ref Expression
1 9cn 
 |-  9 e. CC
2 10re 
 |-  ; 1 0 e. RR
3 2 recni 
 |-  ; 1 0 e. CC
4 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
5 expcl 
 |-  ( ( ; 1 0 e. CC /\ k e. NN0 ) -> ( ; 1 0 ^ k ) e. CC )
6 3 4 5 sylancr 
 |-  ( k e. NN -> ( ; 1 0 ^ k ) e. CC )
7 3 a1i 
 |-  ( k e. NN -> ; 1 0 e. CC )
8 10pos 
 |-  0 < ; 1 0
9 2 8 gt0ne0ii 
 |-  ; 1 0 =/= 0
10 9 a1i 
 |-  ( k e. NN -> ; 1 0 =/= 0 )
11 nnz 
 |-  ( k e. NN -> k e. ZZ )
12 7 10 11 expne0d 
 |-  ( k e. NN -> ( ; 1 0 ^ k ) =/= 0 )
13 divrec 
 |-  ( ( 9 e. CC /\ ( ; 1 0 ^ k ) e. CC /\ ( ; 1 0 ^ k ) =/= 0 ) -> ( 9 / ( ; 1 0 ^ k ) ) = ( 9 x. ( 1 / ( ; 1 0 ^ k ) ) ) )
14 1 6 12 13 mp3an2i 
 |-  ( k e. NN -> ( 9 / ( ; 1 0 ^ k ) ) = ( 9 x. ( 1 / ( ; 1 0 ^ k ) ) ) )
15 7 10 11 exprecd 
 |-  ( k e. NN -> ( ( 1 / ; 1 0 ) ^ k ) = ( 1 / ( ; 1 0 ^ k ) ) )
16 15 oveq2d 
 |-  ( k e. NN -> ( 9 x. ( ( 1 / ; 1 0 ) ^ k ) ) = ( 9 x. ( 1 / ( ; 1 0 ^ k ) ) ) )
17 14 16 eqtr4d 
 |-  ( k e. NN -> ( 9 / ( ; 1 0 ^ k ) ) = ( 9 x. ( ( 1 / ; 1 0 ) ^ k ) ) )
18 17 sumeq2i 
 |-  sum_ k e. NN ( 9 / ( ; 1 0 ^ k ) ) = sum_ k e. NN ( 9 x. ( ( 1 / ; 1 0 ) ^ k ) )
19 2 9 rereccli 
 |-  ( 1 / ; 1 0 ) e. RR
20 19 recni 
 |-  ( 1 / ; 1 0 ) e. CC
21 0re 
 |-  0 e. RR
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 e. RR /\ 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 e. CC /\ ( 1 / ; 1 0 ) e. CC /\ ( abs ` ( 1 / ; 1 0 ) ) < 1 ) -> sum_ k e. NN ( 9 x. ( ( 1 / ; 1 0 ) ^ k ) ) = ( ( 9 x. ( 1 / ; 1 0 ) ) / ( 1 - ( 1 / ; 1 0 ) ) ) )
32 1 20 30 31 mp3an 
 |-  sum_ k e. NN ( 9 x. ( ( 1 / ; 1 0 ) ^ k ) ) = ( ( 9 x. ( 1 / ; 1 0 ) ) / ( 1 - ( 1 / ; 1 0 ) ) )
33 1 3 9 divreci 
 |-  ( 9 / ; 1 0 ) = ( 9 x. ( 1 / ; 1 0 ) )
34 1 3 9 divcan2i 
 |-  ( ; 1 0 x. ( 9 / ; 1 0 ) ) = 9
35 ax-1cn 
 |-  1 e. CC
36 3 35 20 subdii 
 |-  ( ; 1 0 x. ( 1 - ( 1 / ; 1 0 ) ) ) = ( ( ; 1 0 x. 1 ) - ( ; 1 0 x. ( 1 / ; 1 0 ) ) )
37 3 mulid1i 
 |-  ( ; 1 0 x. 1 ) = ; 1 0
38 3 9 recidi 
 |-  ( ; 1 0 x. ( 1 / ; 1 0 ) ) = 1
39 37 38 oveq12i 
 |-  ( ( ; 1 0 x. 1 ) - ( ; 1 0 x. ( 1 / ; 1 0 ) ) ) = ( ; 1 0 - 1 )
40 10m1e9 
 |-  ( ; 1 0 - 1 ) = 9
41 36 39 40 3eqtrri 
 |-  9 = ( ; 1 0 x. ( 1 - ( 1 / ; 1 0 ) ) )
42 34 41 eqtri 
 |-  ( ; 1 0 x. ( 9 / ; 1 0 ) ) = ( ; 1 0 x. ( 1 - ( 1 / ; 1 0 ) ) )
43 9re 
 |-  9 e. RR
44 43 2 9 redivcli 
 |-  ( 9 / ; 1 0 ) e. RR
45 44 recni 
 |-  ( 9 / ; 1 0 ) e. CC
46 35 20 subcli 
 |-  ( 1 - ( 1 / ; 1 0 ) ) e. CC
47 45 46 3 9 mulcani 
 |-  ( ( ; 1 0 x. ( 9 / ; 1 0 ) ) = ( ; 1 0 x. ( 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 x. ( 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 
 |-  sum_ k e. NN ( 9 x. ( ( 1 / ; 1 0 ) ^ k ) ) = 1
55 18 54 eqtri 
 |-  sum_ k e. NN ( 9 / ( ; 1 0 ^ k ) ) = 1