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\in \mathbb{N}}\left(\frac{9}{{10}^k}\right)=1$$

Proof

Step	Hyp	Ref	Expression
1		9cn	$$⊢9\in ℂ$$
2		10re	$$⊢10\in ℝ$$
3	2	recni	$$⊢10\in ℂ$$
4		nnnn0	$$⊢k\in \mathbb{N}\to k\in {\mathbb{N}}_0$$
5		expcl	$$⊢\left(10\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to {10}^k\in ℂ$$
6	3 4 5	sylancr	$$⊢k\in \mathbb{N}\to {10}^k\in ℂ$$
7	3	a1i	$$⊢k\in \mathbb{N}\to 10\in ℂ$$
8		10pos	$$⊢0<10$$
9	2 8	gt0ne0ii	$$⊢10\ne 0$$
10	9	a1i	$$⊢k\in \mathbb{N}\to 10\ne 0$$
11		nnz	$$⊢k\in \mathbb{N}\to k\in \mathbb{Z}$$
12	7 10 11	expne0d	$$⊢k\in \mathbb{N}\to {10}^k\ne 0$$
13		divrec	$$⊢\left(9\in ℂ\wedge {10}^k\in ℂ\wedge {10}^k\ne 0\right)\to \frac{9}{{10}^k}=9\left(\frac{1}{{10}^k}\right)$$
14	1 6 12 13	mp3an2i	$$⊢k\in \mathbb{N}\to \frac{9}{{10}^k}=9\left(\frac{1}{{10}^k}\right)$$
15	7 10 11	exprecd	$$⊢k\in \mathbb{N}\to {\left(\frac{1}{10}\right)}^k=\frac{1}{{10}^k}$$
16	15	oveq2d	$$⊢k\in \mathbb{N}\to 9{\left(\frac{1}{10}\right)}^k=9\left(\frac{1}{{10}^k}\right)$$
17	14 16	eqtr4d	$$⊢k\in \mathbb{N}\to \frac{9}{{10}^k}=9{\left(\frac{1}{10}\right)}^k$$
18	17	sumeq2i	$$⊢\sum _{k\in \mathbb{N}}\left(\frac{9}{{10}^k}\right)=\sum _{k\in \mathbb{N}}9{\left(\frac{1}{10}\right)}^k$$
19	2 9	rereccli	$$⊢\frac{1}{10}\in ℝ$$
20	19	recni	$$⊢\frac{1}{10}\in ℂ$$
21		0re	$$⊢0\in ℝ$$
22	2 8	recgt0ii	$$⊢0<\frac{1}{10}$$
23	21 19 22	ltleii	$$⊢0\le \frac{1}{10}$$
24	19	absidi	$$⊢0\le \frac{1}{10}\to \left|\frac{1}{10}\right|=\frac{1}{10}$$
25	23 24	ax-mp	$$⊢\left|\frac{1}{10}\right|=\frac{1}{10}$$
26		1lt10	$$⊢1<10$$
27		recgt1	$$⊢\left(10\in ℝ\wedge 0<10\right)\to \left(1<10\leftrightarrow \frac{1}{10}<1\right)$$
28	2 8 27	mp2an	$$⊢1<10\leftrightarrow \frac{1}{10}<1$$
29	26 28	mpbi	$$⊢\frac{1}{10}<1$$
30	25 29	eqbrtri	$$⊢\left|\frac{1}{10}\right|<1$$
31		geoisum1c	$$⊢\left(9\in ℂ\wedge \frac{1}{10}\in ℂ\wedge \left|\frac{1}{10}\right|<1\right)\to \sum _{k\in \mathbb{N}}9{\left(\frac{1}{10}\right)}^k=\frac{9\left(\frac{1}{10}\right)}{1-\left(\frac{1}{10}\right)}$$
32	1 20 30 31	mp3an	$$⊢\sum _{k\in \mathbb{N}}9{\left(\frac{1}{10}\right)}^k=\frac{9\left(\frac{1}{10}\right)}{1-\left(\frac{1}{10}\right)}$$
33	1 3 9	divreci	$$⊢\frac{9}{10}=9\left(\frac{1}{10}\right)$$
34	1 3 9	divcan2i	$$⊢10\left(\frac{9}{10}\right)=9$$
35		ax-1cn	$$⊢1\in ℂ$$
36	3 35 20	subdii	$$⊢10\left(1-\left(\frac{1}{10}\right)\right)=10\cdot 1-10\left(\frac{1}{10}\right)$$
37	3	mulid1i	$$⊢10\cdot 1=10$$
38	3 9	recidi	$$⊢10\left(\frac{1}{10}\right)=1$$
39	37 38	oveq12i	$$⊢10\cdot 1-10\left(\frac{1}{10}\right)=10-1$$
40		10m1e9	$$⊢10-1=9$$
41	36 39 40	3eqtrri	$$⊢9=10\left(1-\left(\frac{1}{10}\right)\right)$$
42	34 41	eqtri	$$⊢10\left(\frac{9}{10}\right)=10\left(1-\left(\frac{1}{10}\right)\right)$$
43		9re	$$⊢9\in ℝ$$
44	43 2 9	redivcli	$$⊢\frac{9}{10}\in ℝ$$
45	44	recni	$$⊢\frac{9}{10}\in ℂ$$
46	35 20	subcli	$$⊢1-\left(\frac{1}{10}\right)\in ℂ$$
47	45 46 3 9	mulcani	$$⊢10\left(\frac{9}{10}\right)=10\left(1-\left(\frac{1}{10}\right)\right)\leftrightarrow \frac{9}{10}=1-\left(\frac{1}{10}\right)$$
48	42 47	mpbi	$$⊢\frac{9}{10}=1-\left(\frac{1}{10}\right)$$
49	33 48	oveq12i	$$⊢\frac{\frac{9}{10}}{\frac{9}{10}}=\frac{9\left(\frac{1}{10}\right)}{1-\left(\frac{1}{10}\right)}$$
50		9pos	$$⊢0<9$$
51	43 2 50 8	divgt0ii	$$⊢0<\frac{9}{10}$$
52	44 51	gt0ne0ii	$$⊢\frac{9}{10}\ne 0$$
53	45 52	dividi	$$⊢\frac{\frac{9}{10}}{\frac{9}{10}}=1$$
54	32 49 53	3eqtr2i	$$⊢\sum _{k\in \mathbb{N}}9{\left(\frac{1}{10}\right)}^k=1$$
55	18 54	eqtri	$$⊢\sum _{k\in \mathbb{N}}\left(\frac{9}{{10}^k}\right)=1$$