Nearby theorems
|
|
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
| Mirrors > Home > MPE Home > Th. List > rplogsumlem1 | Structured version Unicode version | |
| Description: Lemma for rplogsum 23913. (Contributed by Mario Carneiro, 2-May-2016.) |
| Ref | Expression |
|---|---|
| rplogsumlem1 |
                 
|
,
is distinct from all other
variables.| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fzfid 12068 |
. . 3
 | |
| 2 | elfzuz 11687 |
. . . . . . . 8
 | |
| 3 | eluz2nn 11120 |
. . . . . . . 8
| |
| 4 | 2, 3 | syl 16 |
. . . . . . 7
|
| 5 | 4 | adantl 464 |
. . . . . 6
![/\](wedge.gif "/\"){kind=small}
|
| 6 | 5 | nnrpd 11257 |
. . . . 5
 |
| 7 | 6 | relogcld 23179 |
. . . 4
 |
| 8 | 2 | adantl 464 |
. . . . . 6
|
| 9 | uz2m1nn 11157 |
. . . . . 6
| |
| 10 | 8, 9 | syl 16 |
. . . . 5
|
| 11 | 5, 10 | nnmulcld 10579 |
. . . 4
|
| 12 | 7, 11 | nndivred 10580 |
. . 3
|
| 13 | 1, 12 | fsumrecl 13641 |
. 2
|
| 14 | 2re 10601 |
. . . . 5
| |
| 15 | 10 | nnrpd 11257 |
. . . . . 6
|
| 16 | 15 | rpsqrtcld 13328 |
. . . . 5
 |
| 17 | rerpdivcl 11249 |
. . . . 5
| |
| 18 | 14, 16, 17 | sylancr 661 |
. . . 4
|
| 19 | 6 | rpsqrtcld 13328 |
. . . . 5
|
| 20 | rerpdivcl 11249 |
. . . . 5
| |
| 21 | 14, 19, 20 | sylancr 661 |
. . . 4
|
| 22 | 18, 21 | resubcld 9983 |
. . 3
|
| 23 | 1, 22 | fsumrecl 13641 |
. 2
|
| 24 | 14 | a1i 11 |
. 2
|
| 25 | 16 | rpred 11259 |
. . . . 5
|
| 26 | 5 | nnred 10546 |
. . . . . . 7
|
| 27 | peano2rem 9877 |
. . . . . . . 8
| |
| 28 | 26, 27 | syl 16 |
. . . . . . 7
|
| 29 | 26, 28 | remulcld 9613 |
. . . . . 6
|
| 30 | 29, 22 | remulcld 9613 |
. . . . 5
|
| 31 | 5 | nncnd 10547 |
. . . . . . . 8
 |
| 32 | ax-1cn 9539 |
. . . . . . . 8
| |
| 33 | npcan 9820 |
. . . . . . . 8
  | |
| 34 | 31, 32, 33 | sylancl 660 |
. . . . . . 7
|
| 35 | 34 | fveq2d 5852 |
. . . . . 6
|
| 36 | 15 | rpge0d 11263 |
. . . . . . 7
 |
| 37 | loglesqrt 23303 |
. . . . . . 7
| |
| 38 | 28, 36, 37 | syl2anc 659 |
. . . . . 6
|
| 39 | 35, 38 | eqbrtrrd 4461 |
. . . . 5
|
| 40 | 19 | rpred 11259 |
. . . . . . . . . . 11
|
| 41 | 40, 25 | readdcld 9612 |
. . . . . . . . . 10
|
| 42 | remulcl 9566 |
. . . . . . . . . . 11
| |
| 43 | 40, 14, 42 | sylancl 660 |
. . . . . . . . . 10
|
| 44 | 40, 25 | resubcld 9983 |
. . . . . . . . . 10
|
| 45 | 26 | lem1d 10474 |
. . . . . . . . . . . 12
|
| 46 | 6 | rpge0d 11263 |
. . . . . . . . . . . . 13
|
| 47 | 28, 36, 26, 46 | sqrtled 13343 |
. . . . . . . . . . . 12
|
| 48 | 45, 47 | mpbid 210 |
. . . . . . . . . . 11
|
| 49 | 40, 25 | subge0d 10138 |
. . . . . . . . . . 11
|
| 50 | 48, 49 | mpbird 232 |
. . . . . . . . . 10
|
| 51 | 25, 40, 40, 48 | leadd2dd 10163 |
. . . . . . . . . . 11
|
| 52 | 19 | rpcnd 11261 |
. . . . . . . . . . . 12
|
| 53 | 52 | times2d 10778 |
. . . . . . . . . . 11
|
| 54 | 51, 53 | breqtrrd 4465 |
. . . . . . . . . 10
|
| 55 | 41, 43, 44, 50, 54 | lemul1ad 10480 |
. . . . . . . . 9
|
| 56 | 31 | sqsqrtd 13355 |
. . . . . . . . . . 11
 |
| 57 | subcl 9810 |
. . . . . . . . . . . . 13
| |
| 58 | 31, 32, 57 | sylancl 660 |
. . . . . . . . . . . 12
|
| 59 | 58 | sqsqrtd 13355 |
. . . . . . . . . . 11
|
| 60 | 56, 59 | oveq12d 6288 |
. . . . . . . . . 10
|
| 61 | 16 | rpcnd 11261 |
. . . . . . . . . . 11
|
| 62 | subsq 12260 |
. . . . . . . . . . 11
| |
| 63 | 52, 61, 62 | syl2anc 659 |
. . . . . . . . . 10
|
| 64 | nncan 9839 |
. . . . . . . . . . 11
| |
| 65 | 31, 32, 64 | sylancl 660 |
. . . . . . . . . 10
|
| 66 | 60, 63, 65 | 3eqtr3d 2503 |
. . . . . . . . 9
|
| 67 | 2cn 10602 |
. . . . . . . . . . 11
| |
| 68 | 67 | a1i 11 |
. . . . . . . . . 10
|
| 69 | 44 | recnd 9611 |
. . . . . . . . . 10
|
| 70 | 52, 68, 69 | mulassd 9608 |
. . . . . . . . 9
|
| 71 | 55, 66, 70 | 3brtr3d 4468 |
. . . . . . . 8
|
| 72 | 1red 9600 |
. . . . . . . . 9
| |
| 73 | remulcl 9566 |
. . . . . . . . . . 11
| |
| 74 | 14, 44, 73 | sylancr 661 |
. . . . . . . . . 10
|
| 75 | 40, 74 | remulcld 9613 |
. . . . . . . . 9
|
| 76 | 72, 75, 16 | lemul1d 11298 |
. . . . . . . 8
|
| 77 | 71, 76 | mpbid 210 |
. . . . . . 7
|
| 78 | 61 | mulid2d 9603 |
. . . . . . 7
|
| 79 | 74 | recnd 9611 |
. . . . . . . 8
|
| 80 | 52, 79, 61 | mul32d 9779 |
. . . . . . 7
|
| 81 | 77, 78, 80 | 3brtr3d 4468 |
. . . . . 6
|
| 82 | remsqsqrt 13175 |
. . . . . . . . . . 11
| |
| 83 | 26, 46, 82 | syl2anc 659 |
. . . . . . . . . 10
|
| 84 | remsqsqrt 13175 |
. . . . . . . . . . 11
| |
| 85 | 28, 36, 84 | syl2anc 659 |
. . . . . . . . . 10
|
| 86 | 83, 85 | oveq12d 6288 |
. . . . . . . . 9
|
| 87 | 52, 52, 61, 61 | mul4d 9781 |
. . . . . . . . 9
|
| 88 | 86, 87 | eqtr3d 2497 |
. . . . . . . 8
|
| 89 | 16 | rpcnne0d 11268 |
. . . . . . . . . 10
 |
| 90 | 19 | rpcnne0d 11268 |
. . . . . . . . . 10
|
| 91 | divsubdiv 10256 |
. . . . . . . . . 10
| |
| 92 | 68, 68, 89, 90, 91 | syl22anc 1227 |
. . . . . . . . 9
|
| 93 | 68, 52, 61 | subdid 10008 |
. . . . . . . . . 10
|
| 94 | 52, 61 | mulcomd 9606 |
. . . . . . . . . 10
|
| 95 | 93, 94 | oveq12d 6288 |
. . . . . . . . 9
|
| 96 | 92, 95 | eqtr4d 2498 |
. . . . . . . 8
|
| 97 | 88, 96 | oveq12d 6288 |
. . . . . . 7
|
| 98 | 52, 61 | mulcld 9605 |
. . . . . . . 8
|
| 99 | 19, 16 | rpmulcld 11275 |
. . . . . . . . . 10
|
| 100 | 74, 99 | rerpdivcld 11286 |
. . . . . . . . 9
|
| 101 | 100 | recnd 9611 |
. . . . . . . 8
|
| 102 | 98, 98, 101 | mulassd 9608 |
. . . . . . 7
|
| 103 | 99 | rpne0d 11264 |
. . . . . . . . 9
|
| 104 | 79, 98, 103 | divcan2d 10318 |
. . . . . . . 8
|
| 105 | 104 | oveq2d 6286 |
. . . . . . 7
|
| 106 | 97, 102, 105 | 3eqtrd 2499 |
. . . . . 6
|
| 107 | 81, 106 | breqtrrd 4465 |
. . . . 5
|
| 108 | 7, 25, 30, 39, 107 | letrd 9728 |
. . . 4
|
| 109 | 11 | nngt0d 10575 |
. . . . 5
 |
| 110 | ledivmul 10414 |
. . . . 5
| |
| 111 | 7, 22, 29, 109, 110 | syl112anc 1230 |
. . . 4
|
| 112 | 108, 111 | mpbird 232 |
. . 3
|
| 113 | 1, 12, 22, 112 | fsumle 13698 |
. 2
|
| 114 | oveq1 6277 |
. . . . . . 7
| |
| 115 | 114 | fveq2d 5852 |
. . . . . 6
|
| 116 | 115 | oveq2d 6286 |
. . . . 5
|
| 117 | oveq1 6277 |
. . . . . . 7
| |
| 118 | 117 | fveq2d 5852 |
. . . . . 6
|
| 119 | 118 | oveq2d 6286 |
. . . . 5
|
| 120 | oveq1 6277 |
. . . . . . . . . 10
| |
| 121 | 2m1e1 10646 |
. . . . . . . . . 10
| |
| 122 | 120, 121 | syl6eq 2511 |
. . . . . . . . 9
|
| 123 | 122 | fveq2d 5852 |
. . . . . . . 8
|
| 124 | sqrt1 13190 |
. . . . . . . 8
| |
| 125 | 123, 124 | syl6eq 2511 |
. . . . . . 7
|
| 126 | 125 | oveq2d 6286 |
. . . . . 6
|
| 127 | 67 | div1i 10268 |
. . . . . 6
|
| 128 | 126, 127 | syl6eq 2511 |
. . . . 5
|
| 129 | oveq1 6277 |
. . . . . . 7
| |
| 130 | 129 | fveq2d 5852 |
. . . . . 6
|
| 131 | 130 | oveq2d 6286 |
. . . . 5
|
| 132 | nnz 10882 |
. . . . 5
 | |
| 133 | eluzp1p1 11107 |
. . . . . . 7
| |
| 134 | nnuz 11117 |
. . . . . . 7
| |
| 135 | 133, 134 | eleq2s 2562 |
. . . . . 6
|
| 136 | df-2 10590 |
. . . . . . 7
| |
| 137 | 136 | fveq2i 5851 |
. . . . . 6
|
| 138 | 135, 137 | syl6eleqr 2553 |
. . . . 5
|
| 139 | elfzuz 11687 |
. . . . . . . . . . 11
| |
| 140 | uz2m1nn 11157 |
. . . . . . . . . . 11
| |
| 141 | 139, 140 | syl 16 |
. . . . . . . . . 10
|
| 142 | 141 | adantl 464 |
. . . . . . . . 9
|
| 143 | 142 | nnrpd 11257 |
. . . . . . . 8
|
| 144 | 143 | rpsqrtcld 13328 |
. . . . . . 7
|
| 145 | rerpdivcl 11249 |
. . . . . . 7
| |
| 146 | 14, 144, 145 | sylancr 661 |
. . . . . 6
|
| 147 | 146 | recnd 9611 |
. . . . 5
|
| 148 | 116, 119, 128, 131, 132, 138, 147 | telfsum 13703 |
. . . 4
|
| 149 | pncan 9817 |
. . . . . . . . 9
| |
| 150 | 31, 32, 149 | sylancl 660 |
. . . . . . . 8
|
| 151 | 150 | fveq2d 5852 |
. . . . . . 7
|
| 152 | 151 | oveq2d 6286 |
. . . . . 6
|
| 153 | 152 | oveq2d 6286 |
. . . . 5
|
| 154 | 153 | sumeq2dv 13610 |
. . . 4
|
| 155 | nncn 10539 |
. . . . . . . 8
| |
| 156 | pncan 9817 |
. . . . . . . 8
| |
| 157 | 155, 32, 156 | sylancl 660 |
. . . . . . 7
|
| 158 | 157 | fveq2d 5852 |
. . . . . 6
|
| 159 | 158 | oveq2d 6286 |
. . . . 5
|
| 160 | 159 | oveq2d 6286 |
. . . 4
|
| 161 | 148, 154, 160 | 3eqtr3d 2503 |
. . 3
|
| 162 | 2rp 11226 |
. . . . . 6
| |
| 163 | nnrp 11230 |
. . . . . . 7
| |
| 164 | 163 | rpsqrtcld 13328 |
. . . . . 6
|
| 165 | rpdivcl 11244 |
. . . . . 6
| |
| 166 | 162, 164, 165 | sylancr 661 |
. . . . 5
|
| 167 | 166 | rpge0d 11263 |
. . . 4
|
| 168 | 166 | rpred 11259 |
. . . . 5
|
| 169 | subge02 10064 |
. . . . 5
| |
| 170 | 14, 168, 169 | sylancr 661 |
. . . 4
|
| 171 | 167, 170 | mpbid 210 |
. . 3
|
| 172 | 161, 171 | eqbrtrd 4459 |
. 2
|
| 173 | 13, 23, 24, 113, 172 | letrd 9728 |
1
|
| Colors of variables: wff setvar class |
| Syntax hints: wi 4
wb 184 wa 367 wceq 1398 wcel 1823 wne 2649 class class class wbr 4439
cfv 5570
(class class class)co 6270 cc 9479 cr 9480 cc0 9481 c1 9482 caddc 9484 cmul 9486 clt 9617 cle 9618 cmin 9796 cdiv 10202 cn 10531 c2 10581 cuz 11082 crp 11221 cfz 11675 cexp 12151 csqrt 13151 csu 13593 clog 23111 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1623 ax-4 1636 ax-5 1709 ax-6 1752 ax-7 1795 ax-8 1825 ax-9 1827 ax-10 1842 ax-11 1847 ax-12 1859 ax-13 2004 ax-ext 2432 ax-rep 4550 ax-sep 4560 ax-nul 4568 ax-pow 4615 ax-pr 4676 ax-un 6565 ax-inf2 8049 ax-cnex 9537 ax-resscn 9538 ax-1cn 9539 ax-icn 9540 ax-addcl 9541 ax-addrcl 9542 ax-mulcl 9543 ax-mulrcl 9544 ax-mulcom 9545 ax-addass 9546 ax-mulass 9547 ax-distr 9548 ax-i2m1 9549 ax-1ne0 9550 ax-1rid 9551 ax-rnegex 9552 ax-rrecex 9553 ax-cnre 9554 ax-pre-lttri 9555 ax-pre-lttrn 9556 ax-pre-ltadd 9557 ax-pre-mulgt0 9558 ax-pre-sup 9559 ax-addf 9560 ax-mulf 9561 |
| This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1401 df-fal 1404 df-ex 1618 df-nf 1622 df-sb 1745 df-eu 2288 df-mo 2289 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2651 df-nel 2652 df-ral 2809 df-rex 2810 df-reu 2811 df-rmo 2812 df-rab 2813 df-v 3108 df-sbc 3325 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-pss 3477 df-nul 3784 df-if 3930 df-pw 4001 df-sn 4017 df-pr 4019 df-tp 4021 df-op 4023 df-uni 4236 df-int 4272 df-iun 4317 df-iin 4318 df-br 4440 df-opab 4498 df-mpt 4499 df-tr 4533 df-eprel 4780 df-id 4784 df-po 4789 df-so 4790 df-fr 4827 df-se 4828 df-we 4829 df-ord 4870 df-on 4871 df-lim 4872 df-suc 4873 df-xp 4994 df-rel 4995 df-cnv 4996 df-co 4997 df-dm 4998 df-rn 4999 df-res 5000 df-ima 5001 df-iota 5534 df-fun 5572 df-fn 5573 df-f 5574 df-f1 5575 df-fo 5576 df-f1o 5577 df-fv 5578 df-isom 5579 df-riota 6232 df-ov 6273 df-oprab 6274 df-mpt2 6275 df-of 6513 df-om 6674 df-1st 6773 df-2nd 6774 df-supp 6892 df-recs 7034 df-rdg 7068 df-1o 7122 df-2o 7123 df-oadd 7126 df-er 7303 df-map 7414 df-pm 7415 df-ixp 7463 df-en 7510 df-dom 7511 df-sdom 7512 df-fin 7513 df-fsupp 7822 df-fi 7863 df-sup 7893 df-oi 7927 df-card 8311 df-cda 8539 df-pnf 9619 df-mnf 9620 df-xr 9621 df-ltxr 9622 df-le 9623 df-sub 9798 df-neg 9799 df-div 10203 df-nn 10532 df-2 10590 df-3 10591 df-4 10592 df-5 10593 df-6 10594 df-7 10595 df-8 10596 df-9 10597 df-10 10598 df-n0 10792 df-z 10861 df-dec 10977 df-uz 11083 df-q 11184 df-rp 11222 df-xneg 11321 df-xadd 11322 df-xmul 11323 df-ioo 11536 df-ioc 11537 df-ico 11538 df-icc 11539 df-fz 11676 df-fzo 11800 df-fl 11910 df-mod 11979 df-seq 12093 df-exp 12152 df-fac 12339 df-bc 12366 df-hash 12391 df-shft 12985 df-cj 13017 df-re 13018 df-im 13019 df-sqrt 13153 df-abs 13154 df-limsup 13379 df-clim 13396 df-rlim 13397 df-sum 13594 df-ef 13888 df-sin 13890 df-cos 13891 df-tan 13892 df-pi 13893 df-struct 14721 df-ndx 14722 df-slot 14723 df-base 14724 df-sets 14725 df-ress 14726 df-plusg 14800 df-mulr 14801 df-starv 14802 df-sca 14803 df-vsca 14804 df-ip 14805 df-tset 14806 df-ple 14807 df-ds 14809 df-unif 14810 df-hom 14811 df-cco 14812 df-rest 14915 df-topn 14916 df-0g 14934 df-gsum 14935 df-topgen 14936 df-pt 14937 df-prds 14940 df-xrs 14994 df-qtop 14999 df-imas 15000 df-xps 15002 df-mre 15078 df-mrc 15079 df-acs 15081 df-mgm 16074 df-sgrp 16113 df-mnd 16123 df-submnd 16169 df-mulg 16262 df-cntz 16557 df-cmn 17002 df-psmet 18609 df-xmet 18610 df-met 18611 df-bl 18612 df-mopn 18613 df-fbas 18614 df-fg 18615 df-cnfld 18619 df-top 19569 df-bases 19571 df-topon 19572 df-topsp 19573 df-cld 19690 df-ntr 19691 df-cls 19692 df-nei 19769 df-lp 19807 df-perf 19808 df-cn 19898 df-cnp 19899 df-haus 19986 df-cmp 20057 df-tx 20232 df-hmeo 20425 df-fil 20516 df-fm 20608 df-flim 20609 df-flf 20610 df-xms 20992 df-ms 20993 df-tms 20994 df-cncf 21551 df-limc 22439 df-dv 22440 df-log 23113 df-cxp 23114 |
| This theorem is referenced by: rplogsumlem2 23871 |
| Copyright terms: Public domain | W3C validator |