Theorem 0.999... 8906

Description: The recurring decimal 0.999..., which is defined as the infinite sum 0.9 + 0.09 + 0.009 + ... i.e. 9 / 10^1 + 9 / 10^2 + 9 / 10^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.

Assertion

Ref	Expression
0.999...	|- sum_k e. NN (9 / (10^k)) = 1

Proof of Theorem 0.999...

Step	Hyp	Ref	Expression
1		nnnn0 7655	. . . 4 |- (k e. NN -> k e. NN0)
2		10re 7505	. . . . . . . 8 |- 10 e. RR
3	2	recni 6818	. . . . . . 7 |- 10 e. CC
4		expcl 8208	. . . . . . 7 |- ((10 e. CC /\ k e. NN0) -> (10^k) e. CC)
5	3, 4	mpan 677	. . . . . 6 |- (k e. NN0 -> (10^k) e. CC)
6		10pos 7515	. . . . . . . 8 |- 0 < 10
7	2, 6	gt0ne0ii 7143	. . . . . . 7 |- 10 =/= 0
8		expne0i 8214	. . . . . . 7 |- ((10 e. CC /\ 10 =/= 0 /\ k e. NN0) -> (10^k) =/= 0)
9	3, 7, 8	mp3an12 1456	. . . . . 6 |- (k e. NN0 -> (10^k) =/= 0)
10		9re 7504	. . . . . . . 8 |- 9 e. RR
11	10	recni 6818	. . . . . . 7 |- 9 e. CC
12		divrec 7253	. . . . . . 7 |- ((9 e. CC /\ (10^k) e. CC /\ (10^k) =/= 0) -> (9 / (10^k)) = (9 x. (1 / (10^k))))
13	11, 12	mp3an1 1453	. . . . . 6 |- (((10^k) e. CC /\ (10^k) =/= 0) -> (9 / (10^k)) = (9 x. (1 / (10^k))))
14	5, 9, 13	syl11anc 659	. . . . 5 |- (k e. NN0 -> (9 / (10^k)) = (9 x. (1 / (10^k))))
15		exprec 8221	. . . . . . 7 |- ((10 e. CC /\ 10 =/= 0 /\ k e. NN0) -> ((1 / 10)^k) = (1 / (10^k)))
16	3, 7, 15	mp3an12 1456	. . . . . 6 |- (k e. NN0 -> ((1 / 10)^k) = (1 / (10^k)))
17	16	opreq2d 4994	. . . . 5 |- (k e. NN0 -> (9 x. ((1 / 10)^k)) = (9 x. (1 / (10^k))))
18	14, 17	eqtr4d 2176	. . . 4 |- (k e. NN0 -> (9 / (10^k)) = (9 x. ((1 / 10)^k)))
19	1, 18	syl 13	. . 3 |- (k e. NN -> (9 / (10^k)) = (9 x. ((1 / 10)^k)))
20	19	sumeq2i 8644	. 2 |- sum_k e. NN (9 / (10^k)) = sum_k e. NN (9 x. ((1 / 10)^k))
21	2, 7	rereccli 7310	. . . 4 |- (1 / 10) e. RR
22	21	recni 6818	. . 3 |- (1 / 10) e. CC
23		0re 6840	. . . . . 6 |- 0 e. RR
24	2, 6	recgt0ii 7323	. . . . . 6 |- 0 < (1 / 10)
25	23, 21, 24	ltleii 6940	. . . . 5 |- 0 <_ (1 / 10)
26	21	absidi 8496	. . . . 5 |- (0 <_ (1 / 10) -> (abs` (1 / 10)) = (1 / 10))
27	25, 26	ax-mp 7	. . . 4 |- (abs` (1 / 10)) = (1 / 10)
28		9pos 7514	. . . . . . 7 |- 0 < 9
29		1re 6839	. . . . . . . 8 |- 1 e. RR
30		ltaddpos2 7174	. . . . . . . 8 |- ((9 e. RR /\ 1 e. RR) -> (0 < 9 <-> 1 < (9 + 1)))
31	10, 29, 30	mp2an 681	. . . . . . 7 |- (0 < 9 <-> 1 < (9 + 1))
32	28, 31	mpbi 272	. . . . . 6 |- 1 < (9 + 1)
33		df-10 7495	. . . . . 6 |- 10 = (9 + 1)
34	32, 33	breqtrri 3532	. . . . 5 |- 1 < 10
35		recgt1 7415	. . . . . 6 |- ((10 e. RR /\ 0 < 10) -> (1 < 10 <-> (1 / 10) < 1))
36	2, 6, 35	mp2an 681	. . . . 5 |- (1 < 10 <-> (1 / 10) < 1)
37	34, 36	mpbi 272	. . . 4 |- (1 / 10) < 1
38	27, 37	eqbrtri 3526	. . 3 |- (abs` (1 / 10)) < 1
39		geoisum1c 8905	. . 3 |- ((9 e. CC /\ (1 / 10) e. CC /\ (abs` (1 / 10)) < 1) -> sum_k e. NN (9 x. ((1 / 10)^k)) = ((9 x. (1 / 10)) / (1 - (1 / 10))))
40	11, 22, 38, 39	mp3an 1466	. 2 |- sum_k e. NN (9 x. ((1 / 10)^k)) = ((9 x. (1 / 10)) / (1 - (1 / 10)))
41	11, 3, 7	divreci 7251	. . . 4 |- (9 / 10) = (9 x. (1 / 10))
42	11, 3, 7	divcan2i 7236	. . . . . 6 |- (10 x. (9 / 10)) = 9
43		ax1cn 6787	. . . . . . . 8 |- 1 e. CC
44	3, 43, 22	subdii 7074	. . . . . . 7 |- (10 x. (1 - (1 / 10))) = ((10 x. 1) - (10 x. (1 / 10)))
45	3	mulid1i 6833	. . . . . . . 8 |- (10 x. 1) = 10
46	3, 7	recidi 7247	. . . . . . . 8 |- (10 x. (1 / 10)) = 1
47	45, 46	opreq12i 4991	. . . . . . 7 |- ((10 x. 1) - (10 x. (1 / 10))) = (10 - 1)
48	43, 11	addcomi 6987	. . . . . . . . 9 |- (1 + 9) = (9 + 1)
49	48, 33	eqtr4i 2164	. . . . . . . 8 |- (1 + 9) = 10
50	3, 43, 11, 49	subaddrii 7025	. . . . . . 7 |- (10 - 1) = 9
51	44, 47, 50	3eqtrri 2166	. . . . . 6 |- 9 = (10 x. (1 - (1 / 10)))
52	42, 51	eqtri 2161	. . . . 5 |- (10 x. (9 / 10)) = (10 x. (1 - (1 / 10)))
53	10, 2, 7	redivcli 7307	. . . . . . 7 |- (9 / 10) e. RR
54	53	recni 6818	. . . . . 6 |- (9 / 10) e. CC
55	43, 22	subcli 7019	. . . . . 6 |- (1 - (1 / 10)) e. CC
56	54, 55, 3, 7	mulcani 7210	. . . . 5 |- ((10 x. (9 / 10)) = (10 x. (1 - (1 / 10))) <-> (9 / 10) = (1 - (1 / 10)))
57	52, 56	mpbi 272	. . . 4 |- (9 / 10) = (1 - (1 / 10))
58	41, 57	opreq12i 4991	. . 3 |- ((9 / 10) / (9 / 10)) = ((9 x. (1 / 10)) / (1 - (1 / 10)))
59	10, 2, 28, 6	divgt0ii 7375	. . . . 5 |- 0 < (9 / 10)
60	53, 59	gt0ne0ii 7143	. . . 4 |- (9 / 10) =/= 0
61	54, 60	dividi 7277	. . 3 |- ((9 / 10) / (9 / 10)) = 1
62	58, 61	eqtr3i 2163	. 2 |- ((9 x. (1 / 10)) / (1 - (1 / 10))) = 1
63	20, 40, 62	3eqtri 2165	1 |- sum_k e. NN (9 / (10^k)) = 1

Syntax hints:   <-> wb 219   = wceq 1586   e. wcel 1588   =/= wne 2266   class class class wbr 3507  ` cfv 4131  (class class class)co 4981  CCcc 6750  RRcr 6751  0cc0 6752  1c1 6753   + caddc 6755   x. cmul 6757   <_ cle 6841   < clt 6845   - cmin 6989   / cdiv 6991  NNcn 6992  NN0cn0 6993  9c9 7485  10c10 7486  ^cexp 8195  abscabs 8384  sum_csu 8635

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1590  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-rep 3596  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929  ax-inf2 5964

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3or 1103  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-nel 2269  df-ral 2359  df-rex 2360  df-reu 2361  df-rab 2362  df-v 2540  df-sbc 2700  df-csb 2774  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-pss 2838  df-nul 3083  df-if 3181  df-pw 3229  df-sn 3242  df-pr 3243  df-tp 3245  df-op 3246  df-uni 3367  df-int 3401  df-iun 3438  df-br 3508  df-opab 3566  df-tr 3580  df-eprel 3744  df-id 3747  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-ord 3814  df-on 3815  df-lim 3816  df-suc 3817  df-om 4086  df-xp 4133  df-rel 4134  df-cnv 4135  df-co 4136  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fun 4141  df-fn 4142  df-f 4143  df-f1 4144  df-fo 4145  df-f1o 4146  df-fv 4147  df-opr 4983  df-oprab 4984  df-mpt 5099  df-1st 5126  df-2nd 5127  df-iota 5219  df-rdg 5304  df-1o 5344  df-oadd 5346  df-omul 5347  df-er 5479  df-ec 5481  df-qs 5484  df-en 5588  df-dom 5589  df-sdom 5590  df-undef 5725  df-riota 5729  df-sup 5888  df-ni 6518  df-pli 6519  df-mi 6520  df-lti 6521  df-plpq 6553  df-mpq 6554  df-enq 6555  df-nq 6556  df-plq 6557  df-mq 6558  df-rq 6559  df-ltq 6560  df-1q 6561  df-np 6604  df-1p 6605  df-plp 6606  df-mp 6607  df-ltp 6608  df-plpr 6682  df-mpr 6683  df-enr 6684  df-nr 6685  df-plr 6686  df-mr 6687  df-ltr 6688  df-0r 6689  df-1r 6690  df-m1r 6691  df-c 6758  df-0 6759  df-1 6760  df-i 6761  df-r 6762  df-plus 6763  df-mul 6764  df-lt 6765  df-pnf 6846  df-mnf 6847  df-xr 6848  df-ltxr 6849  df-le 6850  df-sub 7009  df-neg 7011  df-div 7223  df-n 7441  df-2 7487  df-3 7488  df-4 7489  df-5 7490  df-6 7491  df-7 7492  df-8 7493  df-9 7494  df-10 7495  df-n0 7649  df-z 7686  df-fl 7809  df-uz 7934  df-fz 7999  df-seq1 8094  df-shft 8129  df-seqz 8151  df-seq0 8152  df-exp 8196  df-sqr 8304  df-re 8385  df-im 8386  df-cj 8387  df-abs 8388  df-clim 8631  df-sum 8636

Copyright terms: Public domain