| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: The recurring decimal
0.999..., which is defined as the infinite sum 0.9 +
0.09 + 0.009 + ... i.e. |
| Ref | Expression |
|---|---|
| 0.999... |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nnnn0 7655 |
. . . 4
| |
| 2 | 10re 7505 |
. . . . . . . 8
| |
| 3 | 2 | recni 6818 |
. . . . . . 7
|
| 4 | expcl 8208 |
. . . . . . 7
| |
| 5 | 3, 4 | mpan 677 |
. . . . . 6
|
| 6 | 10pos 7515 |
. . . . . . . 8
| |
| 7 | 2, 6 | gt0ne0ii 7143 |
. . . . . . 7
|
| 8 | expne0i 8214 |
. . . . . . 7
| |
| 9 | 3, 7, 8 | mp3an12 1456 |
. . . . . 6
|
| 10 | 9re 7504 |
. . . . . . . 8
| |
| 11 | 10 | recni 6818 |
. . . . . . 7
|
| 12 | divrec 7253 |
. . . . . . 7
| |
| 13 | 11, 12 | mp3an1 1453 |
. . . . . 6
|
| 14 | 5, 9, 13 | syl11anc 659 |
. . . . 5
|
| 15 | exprec 8221 |
. . . . . . 7
| |
| 16 | 3, 7, 15 | mp3an12 1456 |
. . . . . 6
|
| 17 | 16 | opreq2d 4994 |
. . . . 5
|
| 18 | 14, 17 | eqtr4d 2176 |
. . . 4
|
| 19 | 1, 18 | syl 13 |
. . 3
|
| 20 | 19 | sumeq2i 8644 |
. 2
|
| 21 | 2, 7 | rereccli 7310 |
. . . 4
|
| 22 | 21 | recni 6818 |
. . 3
|
| 23 | 0re 6840 |
. . . . . 6
| |
| 24 | 2, 6 | recgt0ii 7323 |
. . . . . 6
|
| 25 | 23, 21, 24 | ltleii 6940 |
. . . . 5
|
| 26 | 21 | absidi 8496 |
. . . . 5
|
| 27 | 25, 26 | ax-mp 7 |
. . . 4
|
| 28 | 9pos 7514 |
. . . . . . 7
| |
| 29 | 1re 6839 |
. . . . . . . 8
| |
| 30 | ltaddpos2 7174 |
. . . . . . . 8
| |
| 31 | 10, 29, 30 | mp2an 681 |
. . . . . . 7
|
| 32 | 28, 31 | mpbi 272 |
. . . . . 6
|
| 33 | df-10 7495 |
. . . . . 6
| |
| 34 | 32, 33 | breqtrri 3532 |
. . . . 5
|
| 35 | recgt1 7415 |
. . . . . 6
| |
| 36 | 2, 6, 35 | mp2an 681 |
. . . . 5
|
| 37 | 34, 36 | mpbi 272 |
. . . 4
|
| 38 | 27, 37 | eqbrtri 3526 |
. . 3
|
| 39 | geoisum1c 8905 |
. . 3
| |
| 40 | 11, 22, 38, 39 | mp3an 1466 |
. 2
|
| 41 | 11, 3, 7 | divreci 7251 |
. . . 4
|
| 42 | 11, 3, 7 | divcan2i 7236 |
. . . . . 6
|
| 43 | ax1cn 6787 |
. . . . . . . 8
| |
| 44 | 3, 43, 22 | subdii 7074 |
. . . . . . 7
|
| 45 | 3 | mulid1i 6833 |
. . . . . . . 8
|
| 46 | 3, 7 | recidi 7247 |
. . . . . . . 8
|
| 47 | 45, 46 | opreq12i 4991 |
. . . . . . 7
|
| 48 | 43, 11 | addcomi 6987 |
. . . . . . . . 9
|
| 49 | 48, 33 | eqtr4i 2164 |
. . . . . . . 8
|
| 50 | 3, 43, 11, 49 | subaddrii 7025 |
. . . . . . 7
|
| 51 | 44, 47, 50 | 3eqtrri 2166 |
. . . . . 6
|
| 52 | 42, 51 | eqtri 2161 |
. . . . 5
|
| 53 | 10, 2, 7 | redivcli 7307 |
. . . . . . 7
|
| 54 | 53 | recni 6818 |
. . . . . 6
|
| 55 | 43, 22 | subcli 7019 |
. . . . . 6
|
| 56 | 54, 55, 3, 7 | mulcani 7210 |
. . . . 5
|
| 57 | 52, 56 | mpbi 272 |
. . . 4
|
| 58 | 41, 57 | opreq12i 4991 |
. . 3
|
| 59 | 10, 2, 28, 6 | divgt0ii 7375 |
. . . . 5
|
| 60 | 53, 59 | gt0ne0ii 7143 |
. . . 4
|
| 61 | 54, 60 | dividi 7277 |
. . 3
|
| 62 | 58, 61 | eqtr3i 2163 |
. 2
|
| 63 | 20, 40, 62 | 3eqtri 2165 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| 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 |