MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rplogsumlem2 Unicode version

Theorem rplogsumlem2 22475
Description: Lemma for rplogsum 22517. Equation 9.2.14 of [Shapiro], p. 331. (Contributed by Mario Carneiro, 2-May-2016.)
Assertion
Ref Expression
rplogsumlem2
Distinct variable group:   ,

Proof of Theorem rplogsumlem2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 flid 11598 . . . . 5
21oveq2d 6077 . . . 4
32sumeq1d 13119 . . 3
4 fveq2 5661 . . . . . 6
5 eleq1 2482 . . . . . . 7
6 fveq2 5661 . . . . . . 7
75, 6ifbieq1d 3789 . . . . . 6
84, 7oveq12d 6079 . . . . 5
9 id 21 . . . . 5
108, 9oveq12d 6079 . . . 4
11 zre 10595 . . . 4
12 elfznn 11422 . . . . . . . . 9
1312adantl 456 . . . . . . . 8
14 vmacl 22197 . . . . . . . 8
1513, 14syl 16 . . . . . . 7
1613nnrpd 10971 . . . . . . . . 9
1716relogcld 21813 . . . . . . . 8
18 0re 9332 . . . . . . . 8
19 ifcl 3808 . . . . . . . 8
2017, 18, 19sylancl 647 . . . . . . 7
2115, 20resubcld 9722 . . . . . 6
2221, 13nndivred 10316 . . . . 5
2322recnd 9358 . . . 4
24 simprr 741 . . . . . . . 8
25 vmaprm 22196 . . . . . . . . . . . . 13
26 prmnn 13706 . . . . . . . . . . . . . . 15
2726nnred 10283 . . . . . . . . . . . . . 14
28 prmuz2 13721 . . . . . . . . . . . . . . 15
29 eluz2b2 10872 . . . . . . . . . . . . . . . 16
3029simprbi 454 . . . . . . . . . . . . . . 15
3128, 30syl 16 . . . . . . . . . . . . . 14
3227, 31rplogcld 21819 . . . . . . . . . . . . 13
3325, 32eqeltrd 2496 . . . . . . . . . . . 12
3433rpne0d 10977 . . . . . . . . . . 11
3534necon2bi 2636 . . . . . . . . . 10
3635ad2antll 713 . . . . . . . . 9
37 iffalse 3776 . . . . . . . . 9
3836, 37syl 16 . . . . . . . 8
3924, 38oveq12d 6079 . . . . . . 7
40 0m0e0 10377 . . . . . . 7
4139, 40syl6eq 2470 . . . . . 6
4241oveq1d 6076 . . . . 5
4312ad2antrl 712 . . . . . . . 8
4443nnrpd 10971 . . . . . . 7
4544rpcnne0d 10981 . . . . . 6
46 div0 9968 . . . . . 6
4745, 46syl 16 . . . . 5
4842, 47eqtrd 2454 . . . 4
4910, 11, 23, 48fsumvma2 22294 . . 3
503, 49eqtr3d 2456 . 2
51 fzfid 11736 . . . . 5
52 inss2 3548 . . . . . . . . . . . 12
53 simpr 451 . . . . . . . . . . . 12
5452, 53sseldi 3331 . . . . . . . . . . 11
55 prmnn 13706 . . . . . . . . . . 11
5654, 55syl 16 . . . . . . . . . 10
5756nnred 10283 . . . . . . . . 9
5811adantr 455 . . . . . . . . 9
59 zcn 10596 . . . . . . . . . . . 12
6059abscld 12863 . . . . . . . . . . 11
61 peano2re 9488 . . . . . . . . . . 11
6260, 61syl 16 . . . . . . . . . 10
6362adantr 455 . . . . . . . . 9
64 inss1 3547 . . . . . . . . . . . . 13
6564sseli 3329 . . . . . . . . . . . 12
66 elicc2 11305 . . . . . . . . . . . . 13
6718, 11, 66sylancr 648 . . . . . . . . . . . 12
6865, 67syl5ib 213 . . . . . . . . . . 11
6968imp 422 . . . . . . . . . 10
7069simp3d 987 . . . . . . . . 9
7159adantr 455 . . . . . . . . . . 11
7271abscld 12863 . . . . . . . . . 10
7358leabsd 12842 . . . . . . . . . 10
7472lep1d 10210 . . . . . . . . . 10
7558, 72, 63, 73, 74letrd 9474 . . . . . . . . 9
7657, 58, 63, 70, 75letrd 9474 . . . . . . . 8
77 prmuz2 13721 . . . . . . . . . 10
7854, 77syl 16 . . . . . . . . 9
79 nn0abscl 12742 . . . . . . . . . . . 12
80 nn0p1nn 10565 . . . . . . . . . . . 12
8179, 80syl 16 . . . . . . . . . . 11
8281nnzd 10691 . . . . . . . . . 10
8382adantr 455 . . . . . . . . 9
84 elfz5 11389 . . . . . . . . 9
8578, 83, 84syl2anc 646 . . . . . . . 8
8676, 85mpbird 226 . . . . . . 7
8786ex 427 . . . . . 6
8887ssrdv 3339 . . . . 5
89 ssfi 7492 . . . . 5
9051, 88, 89syl2anc 646 . . . 4
91 fzfid 11736 . . . . 5
92 simprl 740 . . . . . . . . . . 11
9352, 92sseldi 3331 . . . . . . . . . 10
94 elfznn 11422 . . . . . . . . . . 11
9594ad2antll 713 . . . . . . . . . 10
96 vmappw 22195 . . . . . . . . . 10
9793, 95, 96syl2anc 646 . . . . . . . . 9
9856adantrr 701 . . . . . . . . . . 11
9998nnrpd 10971 . . . . . . . . . 10
10099relogcld 21813 . . . . . . . . 9
10197, 100eqeltrd 2496 . . . . . . . 8
10295nnnn0d 10581 . . . . . . . . . . . 12
103 nnexpcl 11819 . . . . . . . . . . . 12
10498, 102, 103syl2anc 646 . . . . . . . . . . 11
105104nnrpd 10971 . . . . . . . . . 10
106105relogcld 21813 . . . . . . . . 9
107 ifcl 3808 . . . . . . . . 9
108106, 18, 107sylancl 647 . . . . . . . 8
109101, 108resubcld 9722 . . . . . . 7
110109, 104nndivred 10316 . . . . . 6
111110anassrs 633 . . . . 5
11291, 111fsumrecl 13152 . . . 4
11390, 112fsumrecl 13152 . . 3
11456nnrpd 10971 . . . . . 6
115114relogcld 21813 . . . . 5
116 uz2m1nn 10874 . . . . . . 7
11778, 116syl 16 . . . . . 6
11856, 117nnmulcld 10315 . . . . 5
119115, 118nndivred 10316 . . . 4
12090, 119fsumrecl 13152 . . 3
121 2re 10337 . . . 4
122121a1i 11 . . 3
12318a1i 11 . . . . . . . . . . . . 13
12456nngt0d 10311 . . . . . . . . . . . . 13
125123, 57, 58, 124, 70ltletrd 9477 . . . . . . . . . . . 12
12658, 125elrpd 10970 . . . . . . . . . . 11
127126relogcld 21813 . . . . . . . . . 10
128 eluz2b2 10872 . . . . . . . . . . . . . 14
129128simprbi 454 . . . . . . . . . . . . 13
13077, 129syl 16 . . . . . . . . . . . 12
13154, 130syl 16 . . . . . . . . . . 11
13257, 131rplogcld 21819 . . . . . . . . . 10
133127, 132rerpdivcld 10999 . . . . . . . . 9
134132rpcnd 10974 . . . . . . . . . . . 12
135134mulid2d 9350 . . . . . . . . . . 11
136114, 126logled 21817 . . . . . . . . . . . 12
13770, 136mpbid 204 . . . . . . . . . . 11
138135, 137eqbrtrd 4287 . . . . . . . . . 10
139 1re 9331 . . . . . . . . . . . 12
140139a1i 11 . . . . . . . . . . 11
141140, 127, 132lemuldivd 11017 . . . . . . . . . 10
142138, 141mpbid 204 . . . . . . . . 9
143 flge1nn 11608 . . . . . . . . 9
144133, 142, 143syl2anc 646 . . . . . . . 8
145 nnuz 10841 . . . . . . . 8
146144, 145syl6eleq 2512 . . . . . . 7
147110recnd 9358 . . . . . . . 8
148147anassrs 633 . . . . . . 7
149 oveq2 6069 . . . . . . . . . 10
150149fveq2d 5665 . . . . . . . . 9
151149eleq1d 2488 . . . . . . . . . 10
152149fveq2d 5665 . . . . . . . . . 10
153151, 152ifbieq1d 3789 . . . . . . . . 9
154150, 153oveq12d 6079 . . . . . . . 8
155154, 149oveq12d 6079 . . . . . . 7
156146, 148, 155fsum1p 13163 . . . . . 6
15756nncnd 10284 . . . . . . . . . . . . . 14
158157exp1d 11944 . . . . . . . . . . . . 13
159158fveq2d 5665 . . . . . . . . . . . 12
160 vmaprm 22196 . . . . . . . . . . . . 13
16154, 160syl 16 . . . . . . . . . . . 12
162159, 161eqtrd 2454 . . . . . . . . . . 11
163158, 54eqeltrd 2496 . . . . . . . . . . . . 13
164 iftrue 3774 . . . . . . . . . . . . 13
165163, 164syl 16 . . . . . . . . . . . 12
166158fveq2d 5665 . . . . . . . . . . . 12
167165, 166eqtrd 2454 . . . . . . . . . . 11
168162, 167oveq12d 6079 . . . . . . . . . 10
169134subidd 9653 . . . . . . . . . 10
170168, 169eqtrd 2454 . . . . . . . . 9
171170, 158oveq12d 6079 . . . . . . . 8
172114rpcnne0d 10981 . . . . . . . . 9
173 div0 9968 . . . . . . . . 9
174172, 173syl 16 . . . . . . . 8
175171, 174eqtrd 2454 . . . . . . 7
176 1p1e2 10381 . . . . . . . . . 10
177176oveq1i 6071 . . . . . . . . 9
178177a1i 11 . . . . . . . 8
179 elfzuz 11393 . . . . . . . . . . . . . 14
180 eluz2b2 10872 . . . . . . . . . . . . . . 15
181180simplbi 450 . . . . . . . . . . . . . 14
182179, 181syl 16 . . . . . . . . . . . . 13
183182, 177eleq2s 2514 . . . . . . . . . . . 12
18454, 183, 96syl2an 467 . . . . . . . . . . 11
18556adantr 455 . . . . . . . . . . . . . 14
186 nnq 10911 . . . . . . . . . . . . . 14
187185, 186syl 16 . . . . . . . . . . . . 13
188179, 177eleq2s 2514 . . . . . . . . . . . . . 14
189188adantl 456 . . . . . . . . . . . . 13
190 expnprm 13904 . . . . . . . . . . . . 13
191187, 189, 190syl2anc 646 . . . . . . . . . . . 12
192 iffalse 3776 . . . . . . . . . . . 12
193191, 192syl 16 . . . . . . . . . . 11
194184, 193oveq12d 6079 . . . . . . . . . 10
195134subid1d 9654 . . . . . . . . . . 11
196195adantr 455 . . . . . . . . . 10
197194, 196eqtrd 2454 . . . . . . . . 9
198197oveq1d 6076 . . . . . . . 8
199178, 198sumeq12dv 13124 . . . . . . 7
200175, 199oveq12d 6079 . . . . . 6
201 fzfid 11736 . . . . . . . . 9
202115adantr 455 . . . . . . . . . . 11
203 nnnn0 10532 . . . . . . . . . . . 12
20456, 203, 103syl2an 467 . . . . . . . . . . 11
205202, 204nndivred 10316 . . . . . . . . . 10
206182, 205sylan2 464 . . . . . . . . 9
207201, 206fsumrecl 13152 . . . . . . . 8
208207recnd 9358 . . . . . . 7
209208addid2d 9516 . . . . . 6
210156, 200, 2093eqtrd 2458 . . . . 5
211114rpreccld 10982 . . . . . . . . . . . 12
212133flcld 11589 . . . . . . . . . . . . 13
213212peano2zd 10695 . . . . . . . . . . . 12
214211, 213rpexpcld 11972