Nearby theorems
|
|
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > rplogsumlem1 | Structured version Visualization version Unicode version | ||
| Description: Lemma for rplogsum 24365. (Contributed by Mario Carneiro, 2-May-2016.) |
| Ref | Expression |
|---|---|
| rplogsumlem1 |
                 
|
,
is distinct from all other
variables.| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fzfid 12186 |
. . 3
 | |
| 2 | elfzuz 11796 |
. . . . . . . 8
 | |
| 3 | eluz2nn 11197 |
. . . . . . . 8
| |
| 4 | 2, 3 | syl 17 |
. . . . . . 7
|
| 5 | 4 | adantl 468 |
. . . . . 6
![/\](wedge.gif "/\"){kind=small}
|
| 6 | 5 | nnrpd 11339 |
. . . . 5
 |
| 7 | 6 | relogcld 23572 |
. . . 4
 |
| 8 | 2 | adantl 468 |
. . . . . 6
|
| 9 | uz2m1nn 11233 |
. . . . . 6
| |
| 10 | 8, 9 | syl 17 |
. . . . 5
|
| 11 | 5, 10 | nnmulcld 10657 |
. . . 4
|
| 12 | 7, 11 | nndivred 10658 |
. . 3
|
| 13 | 1, 12 | fsumrecl 13800 |
. 2
|
| 14 | 2re 10679 |
. . . . 5
| |
| 15 | 10 | nnrpd 11339 |
. . . . . 6
|
| 16 | 15 | rpsqrtcld 13473 |
. . . . 5
 |
| 17 | rerpdivcl 11330 |
. . . . 5
| |
| 18 | 14, 16, 17 | sylancr 669 |
. . . 4
|
| 19 | 6 | rpsqrtcld 13473 |
. . . . 5
|
| 20 | rerpdivcl 11330 |
. . . . 5
| |
| 21 | 14, 19, 20 | sylancr 669 |
. . . 4
|
| 22 | 18, 21 | resubcld 10047 |
. . 3
|
| 23 | 1, 22 | fsumrecl 13800 |
. 2
|
| 24 | 14 | a1i 11 |
. 2
|
| 25 | 16 | rpred 11341 |
. . . . 5
|
| 26 | 5 | nnred 10624 |
. . . . . . 7
|
| 27 | peano2rem 9941 |
. . . . . . . 8
| |
| 28 | 26, 27 | syl 17 |
. . . . . . 7
|
| 29 | 26, 28 | remulcld 9671 |
. . . . . 6
|
| 30 | 29, 22 | remulcld 9671 |
. . . . 5
|
| 31 | 5 | nncnd 10625 |
. . . . . . . 8
 |
| 32 | ax-1cn 9597 |
. . . . . . . 8
| |
| 33 | npcan 9884 |
. . . . . . . 8
  | |
| 34 | 31, 32, 33 | sylancl 668 |
. . . . . . 7
|
| 35 | 34 | fveq2d 5869 |
. . . . . 6
|
| 36 | 15 | rpge0d 11345 |
. . . . . . 7
 |
| 37 | loglesqrt 23698 |
. . . . . . 7
| |
| 38 | 28, 36, 37 | syl2anc 667 |
. . . . . 6
|
| 39 | 35, 38 | eqbrtrrd 4425 |
. . . . 5
|
| 40 | 19 | rpred 11341 |
. . . . . . . . . . 11
|
| 41 | 40, 25 | readdcld 9670 |
. . . . . . . . . 10
|
| 42 | remulcl 9624 |
. . . . . . . . . . 11
| |
| 43 | 40, 14, 42 | sylancl 668 |
. . . . . . . . . 10
|
| 44 | 40, 25 | resubcld 10047 |
. . . . . . . . . 10
|
| 45 | 26 | lem1d 10540 |
. . . . . . . . . . . 12
|
| 46 | 6 | rpge0d 11345 |
. . . . . . . . . . . . 13
|
| 47 | 28, 36, 26, 46 | sqrtled 13488 |
. . . . . . . . . . . 12
|
| 48 | 45, 47 | mpbid 214 |
. . . . . . . . . . 11
|
| 49 | 40, 25 | subge0d 10203 |
. . . . . . . . . . 11
|
| 50 | 48, 49 | mpbird 236 |
. . . . . . . . . 10
|
| 51 | 25, 40, 40, 48 | leadd2dd 10228 |
. . . . . . . . . . 11
|
| 52 | 19 | rpcnd 11343 |
. . . . . . . . . . . 12
|
| 53 | 52 | times2d 10856 |
. . . . . . . . . . 11
|
| 54 | 51, 53 | breqtrrd 4429 |
. . . . . . . . . 10
|
| 55 | 41, 43, 44, 50, 54 | lemul1ad 10546 |
. . . . . . . . 9
|
| 56 | 31 | sqsqrtd 13501 |
. . . . . . . . . . 11
 |
| 57 | subcl 9874 |
. . . . . . . . . . . . 13
| |
| 58 | 31, 32, 57 | sylancl 668 |
. . . . . . . . . . . 12
|
| 59 | 58 | sqsqrtd 13501 |
. . . . . . . . . . 11
|
| 60 | 56, 59 | oveq12d 6308 |
. . . . . . . . . 10
|
| 61 | 16 | rpcnd 11343 |
. . . . . . . . . . 11
|
| 62 | subsq 12382 |
. . . . . . . . . . 11
| |
| 63 | 52, 61, 62 | syl2anc 667 |
. . . . . . . . . 10
|
| 64 | nncan 9903 |
. . . . . . . . . . 11
| |
| 65 | 31, 32, 64 | sylancl 668 |
. . . . . . . . . 10
|
| 66 | 60, 63, 65 | 3eqtr3d 2493 |
. . . . . . . . 9
|
| 67 | 2cn 10680 |
. . . . . . . . . . 11
| |
| 68 | 67 | a1i 11 |
. . . . . . . . . 10
|
| 69 | 44 | recnd 9669 |
. . . . . . . . . 10
|
| 70 | 52, 68, 69 | mulassd 9666 |
. . . . . . . . 9
|
| 71 | 55, 66, 70 | 3brtr3d 4432 |
. . . . . . . 8
|
| 72 | 1red 9658 |
. . . . . . . . 9
| |
| 73 | remulcl 9624 |
. . . . . . . . . . 11
| |
| 74 | 14, 44, 73 | sylancr 669 |
. . . . . . . . . 10
|
| 75 | 40, 74 | remulcld 9671 |
. . . . . . . . 9
|
| 76 | 72, 75, 16 | lemul1d 11381 |
. . . . . . . 8
|
| 77 | 71, 76 | mpbid 214 |
. . . . . . 7
|
| 78 | 61 | mulid2d 9661 |
. . . . . . 7
|
| 79 | 74 | recnd 9669 |
. . . . . . . 8
|
| 80 | 52, 79, 61 | mul32d 9843 |
. . . . . . 7
|
| 81 | 77, 78, 80 | 3brtr3d 4432 |
. . . . . 6
|
| 82 | remsqsqrt 13320 |
. . . . . . . . . . 11
| |
| 83 | 26, 46, 82 | syl2anc 667 |
. . . . . . . . . 10
|
| 84 | remsqsqrt 13320 |
. . . . . . . . . . 11
| |
| 85 | 28, 36, 84 | syl2anc 667 |
. . . . . . . . . 10
|
| 86 | 83, 85 | oveq12d 6308 |
. . . . . . . . 9
|
| 87 | 52, 52, 61, 61 | mul4d 9845 |
. . . . . . . . 9
|
| 88 | 86, 87 | eqtr3d 2487 |
. . . . . . . 8
|
| 89 | 16 | rpcnne0d 11350 |
. . . . . . . . . 10
 |
| 90 | 19 | rpcnne0d 11350 |
. . . . . . . . . 10
|
| 91 | divsubdiv 10323 |
. . . . . . . . . 10
| |
| 92 | 68, 68, 89, 90, 91 | syl22anc 1269 |
. . . . . . . . 9
|
| 93 | 68, 52, 61 | subdid 10074 |
. . . . . . . . . 10
|
| 94 | 52, 61 | mulcomd 9664 |
. . . . . . . . . 10
|
| 95 | 93, 94 | oveq12d 6308 |
. . . . . . . . 9
|
| 96 | 92, 95 | eqtr4d 2488 |
. . . . . . . 8
|
| 97 | 88, 96 | oveq12d 6308 |
. . . . . . 7
|
| 98 | 52, 61 | mulcld 9663 |
. . . . . . . 8
|
| 99 | 19, 16 | rpmulcld 11357 |
. . . . . . . . . 10
|
| 100 | 74, 99 | rerpdivcld 11369 |
. . . . . . . . 9
|
| 101 | 100 | recnd 9669 |
. . . . . . . 8
|
| 102 | 98, 98, 101 | mulassd 9666 |
. . . . . . 7
|
| 103 | 99 | rpne0d 11346 |
. . . . . . . . 9
|
| 104 | 79, 98, 103 | divcan2d 10385 |
. . . . . . . 8
|
| 105 | 104 | oveq2d 6306 |
. . . . . . 7
|
| 106 | 97, 102, 105 | 3eqtrd 2489 |
. . . . . 6
|
| 107 | 81, 106 | breqtrrd 4429 |
. . . . 5
|
| 108 | 7, 25, 30, 39, 107 | letrd 9792 |
. . . 4
|
| 109 | 11 | nngt0d 10653 |
. . . . 5
 |
| 110 | ledivmul 10481 |
. . . . 5
| |
| 111 | 7, 22, 29, 109, 110 | syl112anc 1272 |
. . . 4
|
| 112 | 108, 111 | mpbird 236 |
. . 3
|
| 113 | 1, 12, 22, 112 | fsumle 13859 |
. 2
|
| 114 | oveq1 6297 |
. . . . . . 7
| |
| 115 | 114 | fveq2d 5869 |
. . . . . 6
|
| 116 | 115 | oveq2d 6306 |
. . . . 5
|
| 117 | oveq1 6297 |
. . . . . . 7
| |
| 118 | 117 | fveq2d 5869 |
. . . . . 6
|
| 119 | 118 | oveq2d 6306 |
. . . . 5
|
| 120 | oveq1 6297 |
. . . . . . . . . 10
| |
| 121 | 2m1e1 10724 |
. . . . . . . . . 10
| |
| 122 | 120, 121 | syl6eq 2501 |
. . . . . . . . 9
|
| 123 | 122 | fveq2d 5869 |
. . . . . . . 8
|
| 124 | sqrt1 13335 |
. . . . . . . 8
| |
| 125 | 123, 124 | syl6eq 2501 |
. . . . . . 7
|
| 126 | 125 | oveq2d 6306 |
. . . . . 6
|
| 127 | 67 | div1i 10335 |
. . . . . 6
|
| 128 | 126, 127 | syl6eq 2501 |
. . . . 5
|
| 129 | oveq1 6297 |
. . . . . . 7
| |
| 130 | 129 | fveq2d 5869 |
. . . . . 6
|
| 131 | 130 | oveq2d 6306 |
. . . . 5
|
| 132 | nnz 10959 |
. . . . 5
 | |
| 133 | eluzp1p1 11184 |
. . . . . . 7
| |
| 134 | nnuz 11194 |
. . . . . . 7
| |
| 135 | 133, 134 | eleq2s 2547 |
. . . . . 6
|
| 136 | df-2 10668 |
. . . . . . 7
| |
| 137 | 136 | fveq2i 5868 |
. . . . . 6
|
| 138 | 135, 137 | syl6eleqr 2540 |
. . . . 5
|
| 139 | elfzuz 11796 |
. . . . . . . . . . 11
| |
| 140 | uz2m1nn 11233 |
. . . . . . . . . . 11
| |
| 141 | 139, 140 | syl 17 |
. . . . . . . . . 10
|
| 142 | 141 | adantl 468 |
. . . . . . . . 9
|
| 143 | 142 | nnrpd 11339 |
. . . . . . . 8
|
| 144 | 143 | rpsqrtcld 13473 |
. . . . . . 7
|
| 145 | rerpdivcl 11330 |
. . . . . . 7
| |
| 146 | 14, 144, 145 | sylancr 669 |
. . . . . 6
|
| 147 | 146 | recnd 9669 |
. . . . 5
|
| 148 | 116, 119, 128, 131, 132, 138, 147 | telfsum 13864 |
. . . 4
|
| 149 | pncan 9881 |
. . . . . . . . 9
| |
| 150 | 31, 32, 149 | sylancl 668 |
. . . . . . . 8
|
| 151 | 150 | fveq2d 5869 |
. . . . . . 7
|
| 152 | 151 | oveq2d 6306 |
. . . . . 6
|
| 153 | 152 | oveq2d 6306 |
. . . . 5
|
| 154 | 153 | sumeq2dv 13769 |
. . . 4
|
| 155 | nncn 10617 |
. . . . . . . 8
| |
| 156 | pncan 9881 |
. . . . . . . 8
| |
| 157 | 155, 32, 156 | sylancl 668 |
. . . . . . 7
|
| 158 | 157 | fveq2d 5869 |
. . . . . 6
|
| 159 | 158 | oveq2d 6306 |
. . . . 5
|
| 160 | 159 | oveq2d 6306 |
. . . 4
|
| 161 | 148, 154, 160 | 3eqtr3d 2493 |
. . 3
|
| 162 | 2rp 11307 |
. . . . . 6
| |
| 163 | nnrp 11311 |
. . . . . . 7
| |
| 164 | 163 | rpsqrtcld 13473 |
. . . . . 6
|
| 165 | rpdivcl 11325 |
. . . . . 6
| |
| 166 | 162, 164, 165 | sylancr 669 |
. . . . 5
|
| 167 | 166 | rpge0d 11345 |
. . . 4
|
| 168 | 166 | rpred 11341 |
. . . . 5
|
| 169 | subge02 10130 |
. . . . 5
| |
| 170 | 14, 168, 169 | sylancr 669 |
. . . 4
|
| 171 | 167, 170 | mpbid 214 |
. . 3
|
| 172 | 161, 171 | eqbrtrd 4423 |
. 2
|
| 173 | 13, 23, 24, 113, 172 | letrd 9792 |
1
|
| Colors of variables: wff setvar class |
| Syntax hints: wi 4
wb 188 wa 371 wceq 1444 wcel 1887 wne 2622 class class class wbr 4402
cfv 5582
(class class class)co 6290 cc 9537 cr 9538 cc0 9539 c1 9540 caddc 9542 cmul 9544 clt 9675 cle 9676 cmin 9860 cdiv 10269 cn 10609 c2 10659 cuz 11159 crp 11302 cfz 11784 cexp 12272 csqrt 13296 csu 13752 clog 23504 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-rep 4515 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-inf2 8146 ax-cnex 9595 ax-resscn 9596 ax-1cn 9597 ax-icn 9598 ax-addcl 9599 ax-addrcl 9600 ax-mulcl 9601 ax-mulrcl 9602 ax-mulcom 9603 ax-addass 9604 ax-mulass 9605 ax-distr 9606 ax-i2m1 9607 ax-1ne0 9608 ax-1rid 9609 ax-rnegex 9610 ax-rrecex 9611 ax-cnre 9612 ax-pre-lttri 9613 ax-pre-lttrn 9614 ax-pre-ltadd 9615 ax-pre-mulgt0 9616 ax-pre-sup 9617 ax-addf 9618 ax-mulf 9619 |
| This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-fal 1450 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-reu 2744 df-rmo 2745 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-tp 3973 df-op 3975 df-uni 4199 df-int 4235 df-iun 4280 df-iin 4281 df-br 4403 df-opab 4462 df-mpt 4463 df-tr 4498 df-eprel 4745 df-id 4749 df-po 4755 df-so 4756 df-fr 4793 df-se 4794 df-we 4795 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-pred 5380 df-ord 5426 df-on 5427 df-lim 5428 df-suc 5429 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-isom 5591 df-riota 6252 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-of 6531 df-om 6693 df-1st 6793 df-2nd 6794 df-supp 6915 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-1o 7182 df-2o 7183 df-oadd 7186 df-er 7363 df-map 7474 df-pm 7475 df-ixp 7523 df-en 7570 df-dom 7571 df-sdom 7572 df-fin 7573 df-fsupp 7884 df-fi 7925 df-sup 7956 df-inf 7957 df-oi 8025 df-card 8373 df-cda 8598 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 df-sub 9862 df-neg 9863 df-div 10270 df-nn 10610 df-2 10668 df-3 10669 df-4 10670 df-5 10671 df-6 10672 df-7 10673 df-8 10674 df-9 10675 df-10 10676 df-n0 10870 df-z 10938 df-dec 11052 df-uz 11160 df-q 11265 df-rp 11303 df-xneg 11409 df-xadd 11410 df-xmul 11411 df-ioo 11639 df-ioc 11640 df-ico 11641 df-icc 11642 df-fz 11785 df-fzo 11916 df-fl 12028 df-mod 12097 df-seq 12214 df-exp 12273 df-fac 12460 df-bc 12488 df-hash 12516 df-shft 13130 df-cj 13162 df-re 13163 df-im 13164 df-sqrt 13298 df-abs 13299 df-limsup 13526 df-clim 13552 df-rlim 13553 df-sum 13753 df-ef 14121 df-sin 14123 df-cos 14124 df-tan 14125 df-pi 14126 df-struct 15123 df-ndx 15124 df-slot 15125 df-base 15126 df-sets 15127 df-ress 15128 df-plusg 15203 df-mulr 15204 df-starv 15205 df-sca 15206 df-vsca 15207 df-ip 15208 df-tset 15209 df-ple 15210 df-ds 15212 df-unif 15213 df-hom 15214 df-cco 15215 df-rest 15321 df-topn 15322 df-0g 15340 df-gsum 15341 df-topgen 15342 df-pt 15343 df-prds 15346 df-xrs 15400 df-qtop 15406 df-imas 15407 df-xps 15410 df-mre 15492 df-mrc 15493 df-acs 15495 df-mgm 16488 df-sgrp 16527 df-mnd 16537 df-submnd 16583 df-mulg 16676 df-cntz 16971 df-cmn 17432 df-psmet 18962 df-xmet 18963 df-met 18964 df-bl 18965 df-mopn 18966 df-fbas 18967 df-fg 18968 df-cnfld 18971 df-top 19921 df-bases 19922 df-topon 19923 df-topsp 19924 df-cld 20034 df-ntr 20035 df-cls 20036 df-nei 20114 df-lp 20152 df-perf 20153 df-cn 20243 df-cnp 20244 df-haus 20331 df-cmp 20402 df-tx 20577 df-hmeo 20770 df-fil 20861 df-fm 20953 df-flim 20954 df-flf 20955 df-xms 21335 df-ms 21336 df-tms 21337 df-cncf 21910 df-limc 22821 df-dv 22822 df-log 23506 df-cxp 23507 |
| This theorem is referenced by: rplogsumlem2 24323 |
| Copyright terms: Public domain | W3C validator |