HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem 0.999... 9531
Description: The recurring decimal 0.999..., which is defined as the infinite sum 0.9 + 0.09 + 0.009 + ... i.e. , 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...

Proof of Theorem 0.999...
StepHypRef Expression
1 10re 7879 . . . . . . 7
21recni 7194 . . . . . 6
3 nnnn0 7990 . . . . . 6
4 expcl 8757 . . . . . 6
52, 3, 4sylancr 638 . . . . 5
62a1i 10 . . . . . 6
7 10pos 7890 . . . . . . . 8
81, 7gt0ne0ii 7489 . . . . . . 7
98a1i 10 . . . . . 6
10 nnz 8048 . . . . . 6
11 expne0i 8767 . . . . . 6
126, 9, 10, 11syl3anc 1141 . . . . 5
13 9re 7878 . . . . . . 7
1413recni 7194 . . . . . 6
15 divrec 7606 . . . . . 6
1614, 15mp3an1 1223 . . . . 5
175, 12, 16syl2anc 636 . . . 4
18 exprec 8776 . . . . . 6
196, 9, 10, 18syl3anc 1141 . . . . 5
2019oveq2d 4957 . . . 4
2117, 20eqtr4d 1952 . . 3
2221sumeq2i 9388 . 2
231, 8rereccli 7665 . . . 4
2423recni 7194 . . 3
25 0re 7214 . . . . . 6
261, 7recgt0ii 7680 . . . . . 6
2725, 23, 26ltleii 7279 . . . . 5
2823absidi 9161 . . . . 5
2927, 28ax-mp 8 . . . 4
30 1lt10 7957 . . . . 5
31 recgt1 7757 . . . . . 6
321, 7, 31mp2an 647 . . . . 5
3330, 32mpbi 196 . . . 4
3429, 33eqbrtri 3377 . . 3
35 geoisum1c 9530 . . 3
3614, 24, 34, 35mp3an 1236 . 2
3714, 2, 8divreci 7604 . . . 4
3814, 2, 8divcan2i 7589 . . . . . 6
39 ax-1cn 7162 . . . . . . . 8
402, 39, 24subdii 7416 . . . . . . 7
412mulid1i 7207 . . . . . . . 8
422, 8recidi 7600 . . . . . . . 8
4341, 42oveq12i 4954 . . . . . . 7
4439, 14addcomi 7328 . . . . . . . . 9
45 df-10 7868 . . . . . . . . 9
4644, 45eqtr4i 1940 . . . . . . . 8
472, 39, 14, 46subaddrii 7368 . . . . . . 7
4840, 43, 473eqtrri 1942 . . . . . 6
4938, 48eqtri 1937 . . . . 5
5013, 1, 8redivcli 7662 . . . . . . 7
5150recni 7194 . . . . . 6
5239, 24subcli 7360 . . . . . 6
5351, 52, 2, 8mulcani 7562 . . . . 5
5449, 53mpbi 196 . . . 4
5537, 54oveq12i 4954 . . 3
56 9pos 7889 . . . . . 6
5713, 1, 56, 7divgt0ii 7722 . . . . 5
5850, 57gt0ne0ii 7489 . . . 4
5951, 58dividi 7630 . . 3
6055, 59eqtr3i 1939 . 2
6122, 36, 603eqtri 1941 1
Colors of variables: wff set class
Syntax hints:   wb 173   wceq 1413   wcel 1415   wne 2034   class class class wbr 3358  cfv 4007  (class class class)co 4944  cc 7105  cr 7106  cc0 7107  c1 7108   caddc 7110   cmul 7112   cle 7215   clt 7219   cmin 7330   cdiv 7332  cn 7333  cn0 7334  cz 7335  c9 7858  c10 7859  cexp 8740  cabs 9077  csu 9374
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1330  ax-6 1331  ax-7 1332  ax-gen 1333  ax-8 1417  ax-10 1418  ax-11 1419  ax-12 1420  ax-13 1421  ax-14 1422  ax-17 1429  ax-9 1444  ax-4 1450  ax-16 1628  ax-15 1791  ax-ext 1899  ax-rep 3444  ax-sep 3454  ax-nul 3463  ax-pow 3499  ax-pr 3523  ax-un 3797  ax-inf2 6154  ax-resscn 7161  ax-1cn 7162  ax-icn 7163  ax-addcl 7164  ax-addrcl 7165  ax-mulcl 7166  ax-mulrcl 7167  ax-mulcom 7168  ax-addass 7169  ax-mulass 7170  ax-distr 7171  ax-i2m1 7172  ax-1ne0 7173  ax-1rid 7174  ax-rnegex 7175  ax-rrecex 7176  ax-cnre 7177  ax-pre-lttri 7178  ax-pre-lttrn 7179  ax-pre-ltadd 7180  ax-pre-mulgt0 7181  ax-pre-sup 7182
This theorem depends on definitions:  df-bi 174  df-or 357  df-an 358  df-3or 899  df-3an 900  df-tru 1308  df-ex 1335  df-sb 1590  df-eu 1817  df-mo 1818  df-clab 1905  df-cleq 1910  df-clel 1913  df-ne 2036  df-nel 2037  df-ral 2129  df-rex 2130  df-reu 2131  df-rab 2132  df-v 2324  df-sbc 2491  df-csb 2573  df-dif 2635  df-un 2637  df-in 2639  df-ss 2641  df-pss 2643  df-nul 2899  df-if 3004  df-pw 3062  df-sn 3079  df-pr 3080  df-tp 3081  df-op 3082  df-uni 3214  df-int 3248  df-iun 3286  df-br 3359  df-opab 3413  df-tr 3428  df-eprel 3608  df-id 3611  df-po 3616  df-so 3630  df-fr 3650  df-we 3666  df-ord 3682  df-on 3683  df-lim 3684  df-suc 3685  df-om 3962  df-xp 4009  df-rel 4010  df-cnv 4011  df-co 4012  df-dm 4013  df-rn 4014  df-res 4015  df-ima 4016  df-fun 4017  df-fn 4018  df-f 4019  df-f1 4020  df-fo 4021  df-f1o 4022  df-fv 4023  df-iso 4024  df-ov 4946  df-oprab 4947  df-mpt 5106  df-mpt2 5107  df-1st 5231  df-2nd 5232  df-iota 5336  df-rdg 5424  df-1o 5461  df-er 5598  df-map 5690  df-pm 5691  df-en 5750  df-dom 5751  df-sdom 5752  df-fin 5753  df-riota 5896  df-sup 6075  df-card 6318  df-pnf 7220  df-mnf 7221  df-xr 7222  df-ltxr 7223  df-le 7224  df-sub 7349  df-neg 7351  df-div 7575  df-n 7814  df-2 7860  df-3 7861  df-4 7862  df-5 7863  df-6 7864  df-7 7865  df-8 7866  df-9 7867  df-10 7868  df-n0 7984  df-z 8029  df-uz 8149  df-q 8231  df-rp 8356  df-fz 8501  df-fl 8595  df-seq 8688  df-exp 8741  df-hash 8920  df-cj 8984  df-re 8985  df-im 8986  df-sqr 9078  df-abs 9079  df-clim 9249  df-rlim 9250  df-sum 9375
Copyright terms: Public domain