Nearby theorems
|
|
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
| Mirrors > Home > MPE Home > Th. List > rplogsumlem1 | Structured version Unicode version | |
| Description: Lemma for rplogsum 24352. (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 11797 |
. . . . . . . 8
 | |
| 3 | eluz2nn 11198 |
. . . . . . . 8
| |
| 4 | 2, 3 | syl 17 |
. . . . . . 7
|
| 5 | 4 | adantl 467 |
. . . . . 6
![/\](wedge.gif "/\"){kind=small}
|
| 6 | 5 | nnrpd 11340 |
. . . . 5
 |
| 7 | 6 | relogcld 23559 |
. . . 4
 |
| 8 | 2 | adantl 467 |
. . . . . 6
|
| 9 | uz2m1nn 11234 |
. . . . . 6
| |
| 10 | 8, 9 | syl 17 |
. . . . 5
|
| 11 | 5, 10 | nnmulcld 10658 |
. . . 4
|
| 12 | 7, 11 | nndivred 10659 |
. . 3
|
| 13 | 1, 12 | fsumrecl 13788 |
. 2
|
| 14 | 2re 10680 |
. . . . 5
| |
| 15 | 10 | nnrpd 11340 |
. . . . . 6
|
| 16 | 15 | rpsqrtcld 13462 |
. . . . 5
 |
| 17 | rerpdivcl 11331 |
. . . . 5
| |
| 18 | 14, 16, 17 | sylancr 667 |
. . . 4
|
| 19 | 6 | rpsqrtcld 13462 |
. . . . 5
|
| 20 | rerpdivcl 11331 |
. . . . 5
| |
| 21 | 14, 19, 20 | sylancr 667 |
. . . 4
|
| 22 | 18, 21 | resubcld 10048 |
. . 3
|
| 23 | 1, 22 | fsumrecl 13788 |
. 2
|
| 24 | 14 | a1i 11 |
. 2
|
| 25 | 16 | rpred 11342 |
. . . . 5
|
| 26 | 5 | nnred 10625 |
. . . . . . 7
|
| 27 | peano2rem 9942 |
. . . . . . . 8
| |
| 28 | 26, 27 | syl 17 |
. . . . . . 7
|
| 29 | 26, 28 | remulcld 9672 |
. . . . . 6
|
| 30 | 29, 22 | remulcld 9672 |
. . . . 5
|
| 31 | 5 | nncnd 10626 |
. . . . . . . 8
 |
| 32 | ax-1cn 9598 |
. . . . . . . 8
| |
| 33 | npcan 9885 |
. . . . . . . 8
  | |
| 34 | 31, 32, 33 | sylancl 666 |
. . . . . . 7
|
| 35 | 34 | fveq2d 5882 |
. . . . . 6
|
| 36 | 15 | rpge0d 11346 |
. . . . . . 7
 |
| 37 | loglesqrt 23685 |
. . . . . . 7
| |
| 38 | 28, 36, 37 | syl2anc 665 |
. . . . . 6
|
| 39 | 35, 38 | eqbrtrrd 4443 |
. . . . 5
|
| 40 | 19 | rpred 11342 |
. . . . . . . . . . 11
|
| 41 | 40, 25 | readdcld 9671 |
. . . . . . . . . 10
|
| 42 | remulcl 9625 |
. . . . . . . . . . 11
| |
| 43 | 40, 14, 42 | sylancl 666 |
. . . . . . . . . 10
|
| 44 | 40, 25 | resubcld 10048 |
. . . . . . . . . 10
|
| 45 | 26 | lem1d 10541 |
. . . . . . . . . . . 12
|
| 46 | 6 | rpge0d 11346 |
. . . . . . . . . . . . 13
|
| 47 | 28, 36, 26, 46 | sqrtled 13477 |
. . . . . . . . . . . 12
|
| 48 | 45, 47 | mpbid 213 |
. . . . . . . . . . 11
|
| 49 | 40, 25 | subge0d 10204 |
. . . . . . . . . . 11
|
| 50 | 48, 49 | mpbird 235 |
. . . . . . . . . 10
|
| 51 | 25, 40, 40, 48 | leadd2dd 10229 |
. . . . . . . . . . 11
|
| 52 | 19 | rpcnd 11344 |
. . . . . . . . . . . 12
|
| 53 | 52 | times2d 10857 |
. . . . . . . . . . 11
|
| 54 | 51, 53 | breqtrrd 4447 |
. . . . . . . . . 10
|
| 55 | 41, 43, 44, 50, 54 | lemul1ad 10547 |
. . . . . . . . 9
|
| 56 | 31 | sqsqrtd 13489 |
. . . . . . . . . . 11
 |
| 57 | subcl 9875 |
. . . . . . . . . . . . 13
| |
| 58 | 31, 32, 57 | sylancl 666 |
. . . . . . . . . . . 12
|
| 59 | 58 | sqsqrtd 13489 |
. . . . . . . . . . 11
|
| 60 | 56, 59 | oveq12d 6320 |
. . . . . . . . . 10
|
| 61 | 16 | rpcnd 11344 |
. . . . . . . . . . 11
|
| 62 | subsq 12382 |
. . . . . . . . . . 11
| |
| 63 | 52, 61, 62 | syl2anc 665 |
. . . . . . . . . 10
|
| 64 | nncan 9904 |
. . . . . . . . . . 11
| |
| 65 | 31, 32, 64 | sylancl 666 |
. . . . . . . . . 10
|
| 66 | 60, 63, 65 | 3eqtr3d 2471 |
. . . . . . . . 9
|
| 67 | 2cn 10681 |
. . . . . . . . . . 11
| |
| 68 | 67 | a1i 11 |
. . . . . . . . . 10
|
| 69 | 44 | recnd 9670 |
. . . . . . . . . 10
|
| 70 | 52, 68, 69 | mulassd 9667 |
. . . . . . . . 9
|
| 71 | 55, 66, 70 | 3brtr3d 4450 |
. . . . . . . 8
|
| 72 | 1red 9659 |
. . . . . . . . 9
| |
| 73 | remulcl 9625 |
. . . . . . . . . . 11
| |
| 74 | 14, 44, 73 | sylancr 667 |
. . . . . . . . . 10
|
| 75 | 40, 74 | remulcld 9672 |
. . . . . . . . 9
|
| 76 | 72, 75, 16 | lemul1d 11382 |
. . . . . . . 8
|
| 77 | 71, 76 | mpbid 213 |
. . . . . . 7
|
| 78 | 61 | mulid2d 9662 |
. . . . . . 7
|
| 79 | 74 | recnd 9670 |
. . . . . . . 8
|
| 80 | 52, 79, 61 | mul32d 9844 |
. . . . . . 7
|
| 81 | 77, 78, 80 | 3brtr3d 4450 |
. . . . . 6
|
| 82 | remsqsqrt 13309 |
. . . . . . . . . . 11
| |
| 83 | 26, 46, 82 | syl2anc 665 |
. . . . . . . . . 10
|
| 84 | remsqsqrt 13309 |
. . . . . . . . . . 11
| |
| 85 | 28, 36, 84 | syl2anc 665 |
. . . . . . . . . 10
|
| 86 | 83, 85 | oveq12d 6320 |
. . . . . . . . 9
|
| 87 | 52, 52, 61, 61 | mul4d 9846 |
. . . . . . . . 9
|
| 88 | 86, 87 | eqtr3d 2465 |
. . . . . . . 8
|
| 89 | 16 | rpcnne0d 11351 |
. . . . . . . . . 10
 |
| 90 | 19 | rpcnne0d 11351 |
. . . . . . . . . 10
|
| 91 | divsubdiv 10324 |
. . . . . . . . . 10
| |
| 92 | 68, 68, 89, 90, 91 | syl22anc 1265 |
. . . . . . . . 9
|
| 93 | 68, 52, 61 | subdid 10075 |
. . . . . . . . . 10
|
| 94 | 52, 61 | mulcomd 9665 |
. . . . . . . . . 10
|
| 95 | 93, 94 | oveq12d 6320 |
. . . . . . . . 9
|
| 96 | 92, 95 | eqtr4d 2466 |
. . . . . . . 8
|
| 97 | 88, 96 | oveq12d 6320 |
. . . . . . 7
|
| 98 | 52, 61 | mulcld 9664 |
. . . . . . . 8
|
| 99 | 19, 16 | rpmulcld 11358 |
. . . . . . . . . 10
|
| 100 | 74, 99 | rerpdivcld 11370 |
. . . . . . . . 9
|
| 101 | 100 | recnd 9670 |
. . . . . . . 8
|
| 102 | 98, 98, 101 | mulassd 9667 |
. . . . . . 7
|
| 103 | 99 | rpne0d 11347 |
. . . . . . . . 9
|
| 104 | 79, 98, 103 | divcan2d 10386 |
. . . . . . . 8
|
| 105 | 104 | oveq2d 6318 |
. . . . . . 7
|
| 106 | 97, 102, 105 | 3eqtrd 2467 |
. . . . . 6
|
| 107 | 81, 106 | breqtrrd 4447 |
. . . . 5
|
| 108 | 7, 25, 30, 39, 107 | letrd 9793 |
. . . 4
|
| 109 | 11 | nngt0d 10654 |
. . . . 5
 |
| 110 | ledivmul 10482 |
. . . . 5
| |
| 111 | 7, 22, 29, 109, 110 | syl112anc 1268 |
. . . 4
|
| 112 | 108, 111 | mpbird 235 |
. . 3
|
| 113 | 1, 12, 22, 112 | fsumle 13847 |
. 2
|
| 114 | oveq1 6309 |
. . . . . . 7
| |
| 115 | 114 | fveq2d 5882 |
. . . . . 6
|
| 116 | 115 | oveq2d 6318 |
. . . . 5
|
| 117 | oveq1 6309 |
. . . . . . 7
| |
| 118 | 117 | fveq2d 5882 |
. . . . . 6
|
| 119 | 118 | oveq2d 6318 |
. . . . 5
|
| 120 | oveq1 6309 |
. . . . . . . . . 10
| |
| 121 | 2m1e1 10725 |
. . . . . . . . . 10
| |
| 122 | 120, 121 | syl6eq 2479 |
. . . . . . . . 9
|
| 123 | 122 | fveq2d 5882 |
. . . . . . . 8
|
| 124 | sqrt1 13324 |
. . . . . . . 8
| |
| 125 | 123, 124 | syl6eq 2479 |
. . . . . . 7
|
| 126 | 125 | oveq2d 6318 |
. . . . . 6
|
| 127 | 67 | div1i 10336 |
. . . . . 6
|
| 128 | 126, 127 | syl6eq 2479 |
. . . . 5
|
| 129 | oveq1 6309 |
. . . . . . 7
| |
| 130 | 129 | fveq2d 5882 |
. . . . . 6
|
| 131 | 130 | oveq2d 6318 |
. . . . 5
|
| 132 | nnz 10960 |
. . . . 5
 | |
| 133 | eluzp1p1 11185 |
. . . . . . 7
| |
| 134 | nnuz 11195 |
. . . . . . 7
| |
| 135 | 133, 134 | eleq2s 2530 |
. . . . . 6
|
| 136 | df-2 10669 |
. . . . . . 7
| |
| 137 | 136 | fveq2i 5881 |
. . . . . 6
|
| 138 | 135, 137 | syl6eleqr 2521 |
. . . . 5
|
| 139 | elfzuz 11797 |
. . . . . . . . . . 11
| |
| 140 | uz2m1nn 11234 |
. . . . . . . . . . 11
| |
| 141 | 139, 140 | syl 17 |
. . . . . . . . . 10
|
| 142 | 141 | adantl 467 |
. . . . . . . . 9
|
| 143 | 142 | nnrpd 11340 |
. . . . . . . 8
|
| 144 | 143 | rpsqrtcld 13462 |
. . . . . . 7
|
| 145 | rerpdivcl 11331 |
. . . . . . 7
| |
| 146 | 14, 144, 145 | sylancr 667 |
. . . . . 6
|
| 147 | 146 | recnd 9670 |
. . . . 5
|
| 148 | 116, 119, 128, 131, 132, 138, 147 | telfsum 13852 |
. . . 4
|
| 149 | pncan 9882 |
. . . . . . . . 9
| |
| 150 | 31, 32, 149 | sylancl 666 |
. . . . . . . 8
|
| 151 | 150 | fveq2d 5882 |
. . . . . . 7
|
| 152 | 151 | oveq2d 6318 |
. . . . . 6
|
| 153 | 152 | oveq2d 6318 |
. . . . 5
|
| 154 | 153 | sumeq2dv 13757 |
. . . 4
|
| 155 | nncn 10618 |
. . . . . . . 8
| |
| 156 | pncan 9882 |
. . . . . . . 8
| |
| 157 | 155, 32, 156 | sylancl 666 |
. . . . . . 7
|
| 158 | 157 | fveq2d 5882 |
. . . . . 6
|
| 159 | 158 | oveq2d 6318 |
. . . . 5
|
| 160 | 159 | oveq2d 6318 |
. . . 4
|
| 161 | 148, 154, 160 | 3eqtr3d 2471 |
. . 3
|
| 162 | 2rp 11308 |
. . . . . 6
| |
| 163 | nnrp 11312 |
. . . . . . 7
| |
| 164 | 163 | rpsqrtcld 13462 |
. . . . . 6
|
| 165 | rpdivcl 11326 |
. . . . . 6
| |
| 166 | 162, 164, 165 | sylancr 667 |
. . . . 5
|
| 167 | 166 | rpge0d 11346 |
. . . 4
|
| 168 | 166 | rpred 11342 |
. . . . 5
|
| 169 | subge02 10131 |
. . . . 5
| |
| 170 | 14, 168, 169 | sylancr 667 |
. . . 4
|
| 171 | 167, 170 | mpbid 213 |
. . 3
|
| 172 | 161, 171 | eqbrtrd 4441 |
. 2
|
| 173 | 13, 23, 24, 113, 172 | letrd 9793 |
1
|
| Colors of variables: wff setvar class |
| Syntax hints: wi 4
wb 187 wa 370 wceq 1437 wcel 1868 wne 2618 class class class wbr 4420
cfv 5598
(class class class)co 6302 cc 9538 cr 9539 cc0 9540 c1 9541 caddc 9543 cmul 9545 clt 9676 cle 9677 cmin 9861 cdiv 10270 cn 10610 c2 10660 cuz 11160 crp 11303 cfz 11785 cexp 12272 csqrt 13285 csu 13740 clog 23491 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1748 ax-6 1794 ax-7 1839 ax-8 1870 ax-9 1872 ax-10 1887 ax-11 1892 ax-12 1905 ax-13 2053 ax-ext 2400 ax-rep 4533 ax-sep 4543 ax-nul 4552 ax-pow 4599 ax-pr 4657 ax-un 6594 ax-inf2 8149 ax-cnex 9596 ax-resscn 9597 ax-1cn 9598 ax-icn 9599 ax-addcl 9600 ax-addrcl 9601 ax-mulcl 9602 ax-mulrcl 9603 ax-mulcom 9604 ax-addass 9605 ax-mulass 9606 ax-distr 9607 ax-i2m1 9608 ax-1ne0 9609 ax-1rid 9610 ax-rnegex 9611 ax-rrecex 9612 ax-cnre 9613 ax-pre-lttri 9614 ax-pre-lttrn 9615 ax-pre-ltadd 9616 ax-pre-mulgt0 9617 ax-pre-sup 9618 ax-addf 9619 ax-mulf 9620 |
| This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-fal 1443 df-ex 1660 df-nf 1664 df-sb 1787 df-eu 2269 df-mo 2270 df-clab 2408 df-cleq 2414 df-clel 2417 df-nfc 2572 df-ne 2620 df-nel 2621 df-ral 2780 df-rex 2781 df-reu 2782 df-rmo 2783 df-rab 2784 df-v 3083 df-sbc 3300 df-csb 3396 df-dif 3439 df-un 3441 df-in 3443 df-ss 3450 df-pss 3452 df-nul 3762 df-if 3910 df-pw 3981 df-sn 3997 df-pr 3999 df-tp 4001 df-op 4003 df-uni 4217 df-int 4253 df-iun 4298 df-iin 4299 df-br 4421 df-opab 4480 df-mpt 4481 df-tr 4516 df-eprel 4761 df-id 4765 df-po 4771 df-so 4772 df-fr 4809 df-se 4810 df-we 4811 df-xp 4856 df-rel 4857 df-cnv 4858 df-co 4859 df-dm 4860 df-rn 4861 df-res 4862 df-ima 4863 df-pred 5396 df-ord 5442 df-on 5443 df-lim 5444 df-suc 5445 df-iota 5562 df-fun 5600 df-fn 5601 df-f 5602 df-f1 5603 df-fo 5604 df-f1o 5605 df-fv 5606 df-isom 5607 df-riota 6264 df-ov 6305 df-oprab 6306 df-mpt2 6307 df-of 6542 df-om 6704 df-1st 6804 df-2nd 6805 df-supp 6923 df-wrecs 7033 df-recs 7095 df-rdg 7133 df-1o 7187 df-2o 7188 df-oadd 7191 df-er 7368 df-map 7479 df-pm 7480 df-ixp 7528 df-en 7575 df-dom 7576 df-sdom 7577 df-fin 7578 df-fsupp 7887 df-fi 7928 df-sup 7959 df-inf 7960 df-oi 8028 df-card 8375 df-cda 8599 df-pnf 9678 df-mnf 9679 df-xr 9680 df-ltxr 9681 df-le 9682 df-sub 9863 df-neg 9864 df-div 10271 df-nn 10611 df-2 10669 df-3 10670 df-4 10671 df-5 10672 df-6 10673 df-7 10674 df-8 10675 df-9 10676 df-10 10677 df-n0 10871 df-z 10939 df-dec 11053 df-uz 11161 df-q 11266 df-rp 11304 df-xneg 11410 df-xadd 11411 df-xmul 11412 df-ioo 11640 df-ioc 11641 df-ico 11642 df-icc 11643 df-fz 11786 df-fzo 11917 df-fl 12028 df-mod 12097 df-seq 12214 df-exp 12273 df-fac 12460 df-bc 12488 df-hash 12516 df-shft 13119 df-cj 13151 df-re 13152 df-im 13153 df-sqrt 13287 df-abs 13288 df-limsup 13514 df-clim 13540 df-rlim 13541 df-sum 13741 df-ef 14109 df-sin 14111 df-cos 14112 df-tan 14113 df-pi 14114 df-struct 15111 df-ndx 15112 df-slot 15113 df-base 15114 df-sets 15115 df-ress 15116 df-plusg 15191 df-mulr 15192 df-starv 15193 df-sca 15194 df-vsca 15195 df-ip 15196 df-tset 15197 df-ple 15198 df-ds 15200 df-unif 15201 df-hom 15202 df-cco 15203 df-rest 15309 df-topn 15310 df-0g 15328 df-gsum 15329 df-topgen 15330 df-pt 15331 df-prds 15334 df-xrs 15388 df-qtop 15394 df-imas 15395 df-xps 15398 df-mre 15480 df-mrc 15481 df-acs 15483 df-mgm 16476 df-sgrp 16515 df-mnd 16525 df-submnd 16571 df-mulg 16664 df-cntz 16959 df-cmn 17420 df-psmet 18950 df-xmet 18951 df-met 18952 df-bl 18953 df-mopn 18954 df-fbas 18955 df-fg 18956 df-cnfld 18959 df-top 19908 df-bases 19909 df-topon 19910 df-topsp 19911 df-cld 20021 df-ntr 20022 df-cls 20023 df-nei 20101 df-lp 20139 df-perf 20140 df-cn 20230 df-cnp 20231 df-haus 20318 df-cmp 20389 df-tx 20564 df-hmeo 20757 df-fil 20848 df-fm 20940 df-flim 20941 df-flf 20942 df-xms 21322 df-ms 21323 df-tms 21324 df-cncf 21897 df-limc 22808 df-dv 22809 df-log 23493 df-cxp 23494 |
| This theorem is referenced by: rplogsumlem2 24310 |
| Copyright terms: Public domain | W3C validator |