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	mulridi	⊢ ( ; 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