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

Theorem rplogsumlem2 23134
Description: Lemma for rplogsum 23176. 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 11802 . . . . 5
21oveq2d 6238 . . . 4
32sumeq1d 13336 . . 3
4 fveq2 5813 . . . . . 6
5 eleq1 2526 . . . . . . 7
6 fveq2 5813 . . . . . . 7
75, 6ifbieq1d 3928 . . . . . 6
84, 7oveq12d 6240 . . . . 5
9 id 22 . . . . 5
108, 9oveq12d 6240 . . . 4
11 zre 10788 . . . 4
12 elfznn 11623 . . . . . . . . 9
1312adantl 466 . . . . . . . 8
14 vmacl 22856 . . . . . . . 8
1513, 14syl 16 . . . . . . 7
1613nnrpd 11165 . . . . . . . . 9
1716relogcld 22472 . . . . . . . 8
18 0re 9523 . . . . . . . 8
19 ifcl 3947 . . . . . . . 8
2017, 18, 19sylancl 662 . . . . . . 7
2115, 20resubcld 9913 . . . . . 6
2221, 13nndivred 10508 . . . . 5
2322recnd 9549 . . . 4
24 simprr 756 . . . . . . . 8
25 vmaprm 22855 . . . . . . . . . . . . 13
26 prmnn 13924 . . . . . . . . . . . . . . 15
2726nnred 10475 . . . . . . . . . . . . . 14
28 prmuz2 13939 . . . . . . . . . . . . . . 15
29 eluz2b2 11066 . . . . . . . . . . . . . . . 16
3029simprbi 464 . . . . . . . . . . . . . . 15
3128, 30syl 16 . . . . . . . . . . . . . 14
3227, 31rplogcld 22478 . . . . . . . . . . . . 13
3325, 32eqeltrd 2542 . . . . . . . . . . . 12
3433rpne0d 11171 . . . . . . . . . . 11
3534necon2bi 2690 . . . . . . . . . 10
3635ad2antll 728 . . . . . . . . 9
37 iffalse 3914 . . . . . . . . 9
3836, 37syl 16 . . . . . . . 8
3924, 38oveq12d 6240 . . . . . . 7
40 0m0e0 10569 . . . . . . 7
4139, 40syl6eq 2511 . . . . . 6
4241oveq1d 6237 . . . . 5
4312ad2antrl 727 . . . . . . . 8
4443nnrpd 11165 . . . . . . 7
4544rpcnne0d 11175 . . . . . 6
46 div0 10159 . . . . . 6
4745, 46syl 16 . . . . 5
4842, 47eqtrd 2495 . . . 4
4910, 11, 23, 48fsumvma2 22953 . . 3
503, 49eqtr3d 2497 . 2
51 fzfid 11940 . . . . 5
52 inss2 3685 . . . . . . . . . . . 12
53 simpr 461 . . . . . . . . . . . 12
5452, 53sseldi 3468 . . . . . . . . . . 11
55 prmnn 13924 . . . . . . . . . . 11
5654, 55syl 16 . . . . . . . . . 10
5756nnred 10475 . . . . . . . . 9
5811adantr 465 . . . . . . . . 9
59 zcn 10789 . . . . . . . . . . . 12
6059abscld 13080 . . . . . . . . . . 11
61 peano2re 9679 . . . . . . . . . . 11
6260, 61syl 16 . . . . . . . . . 10
6362adantr 465 . . . . . . . . 9
64 inss1 3684 . . . . . . . . . . . . 13
6564sseli 3466 . . . . . . . . . . . 12
66 elicc2 11499 . . . . . . . . . . . . 13
6718, 11, 66sylancr 663 . . . . . . . . . . . 12
6865, 67syl5ib 219 . . . . . . . . . . 11
6968imp 429 . . . . . . . . . 10
7069simp3d 1002 . . . . . . . . 9
7159adantr 465 . . . . . . . . . . 11
7271abscld 13080 . . . . . . . . . 10
7358leabsd 13059 . . . . . . . . . 10
7472lep1d 10401 . . . . . . . . . 10
7558, 72, 63, 73, 74letrd 9665 . . . . . . . . 9
7657, 58, 63, 70, 75letrd 9665 . . . . . . . 8
77 prmuz2 13939 . . . . . . . . . 10
7854, 77syl 16 . . . . . . . . 9
79 nn0abscl 12959 . . . . . . . . . . . 12
80 nn0p1nn 10757 . . . . . . . . . . . 12
8179, 80syl 16 . . . . . . . . . . 11
8281nnzd 10884 . . . . . . . . . 10
8382adantr 465 . . . . . . . . 9
84 elfz5 11590 . . . . . . . . 9
8578, 83, 84syl2anc 661 . . . . . . . 8
8676, 85mpbird 232 . . . . . . 7
8786ex 434 . . . . . 6
8887ssrdv 3476 . . . . 5
89 ssfi 7668 . . . . 5
9051, 88, 89syl2anc 661 . . . 4
91 fzfid 11940 . . . . 5
92 simprl 755 . . . . . . . . . . 11
9352, 92sseldi 3468 . . . . . . . . . 10
94 elfznn 11623 . . . . . . . . . . 11
9594ad2antll 728 . . . . . . . . . 10
96 vmappw 22854 . . . . . . . . . 10
9793, 95, 96syl2anc 661 . . . . . . . . 9
9856adantrr 716 . . . . . . . . . . 11
9998nnrpd 11165 . . . . . . . . . 10
10099relogcld 22472 . . . . . . . . 9
10197, 100eqeltrd 2542 . . . . . . . 8
10295nnnn0d 10774 . . . . . . . . . . . 12
103 nnexpcl 12035 . . . . . . . . . . . 12
10498, 102, 103syl2anc 661 . . . . . . . . . . 11
105104nnrpd 11165 . . . . . . . . . 10
106105relogcld 22472 . . . . . . . . 9
107 ifcl 3947 . . . . . . . . 9
108106, 18, 107sylancl 662 . . . . . . . 8
109101, 108resubcld 9913 . . . . . . 7
110109, 104nndivred 10508 . . . . . 6
111110anassrs 648 . . . . 5
11291, 111fsumrecl 13369 . . . 4
11390, 112fsumrecl 13369 . . 3
11456nnrpd 11165 . . . . . 6
115114relogcld 22472 . . . . 5
116 uz2m1nn 11068 . . . . . . 7
11778, 116syl 16 . . . . . 6
11856, 117nnmulcld 10507 . . . . 5
119115, 118nndivred 10508 . . . 4
12090, 119fsumrecl 13369 . . 3
121 2re 10529 . . . 4
122121a1i 11 . . 3
12318a1i 11 . . . . . . . . . . . . 13
12456nngt0d 10503 . . . . . . . . . . . . 13
125123, 57, 58, 124, 70ltletrd 9668 . . . . . . . . . . . 12
12658, 125elrpd 11164 . . . . . . . . . . 11
127126relogcld 22472 . . . . . . . . . 10
128 eluz2b2 11066 . . . . . . . . . . . . . 14
129128simprbi 464 . . . . . . . . . . . . 13
13077, 129syl 16 . . . . . . . . . . . 12
13154, 130syl 16 . . . . . . . . . . 11
13257, 131rplogcld 22478 . . . . . . . . . 10
133127, 132rerpdivcld 11193 . . . . . . . . 9
134132rpcnd 11168 . . . . . . . . . . . 12
135134mulid2d 9541 . . . . . . . . . . 11
136114, 126logled 22476 . . . . . . . . . . . 12
13770, 136mpbid 210 . . . . . . . . . . 11
138135, 137eqbrtrd 4429 . . . . . . . . . 10
139 1re 9522 . . . . . . . . . . . 12
140139a1i 11 . . . . . . . . . . 11
141140, 127, 132lemuldivd 11211 . . . . . . . . . 10
142138, 141mpbid 210 . . . . . . . . 9
143 flge1nn 11812 . . . . . . . . 9
144133, 142, 143syl2anc 661 . . . . . . . 8
145 nnuz 11035 . . . . . . . 8
146144, 145syl6eleq 2552 . . . . . . 7
147110recnd 9549 . . . . . . . 8
148147anassrs 648 . . . . . . 7
149 oveq2 6230 . . . . . . . . . 10
150149fveq2d 5817 . . . . . . . . 9
151149eleq1d 2523 . . . . . . . . . 10
152149fveq2d 5817 . . . . . . . . . 10
153151, 152ifbieq1d 3928 . . . . . . . . 9
154150, 153oveq12d 6240 . . . . . . . 8
155154, 149oveq12d 6240 . . . . . . 7
156146, 148, 155fsum1p 13380 . . . . . 6
15756nncnd 10476 . . . . . . . . . . . . . 14
158157exp1d 12160 . . . . . . . . . . . . 13
159158fveq2d 5817 . . . . . . . . . . . 12
160 vmaprm 22855 . . . . . . . . . . . . 13
16154, 160syl 16 . . . . . . . . . . . 12
162159, 161eqtrd 2495 . . . . . . . . . . 11
163158, 54eqeltrd 2542 . . . . . . . . . . . . 13
164 iftrue 3911 . . . . . . . . . . . . 13
165163, 164syl 16 . . . . . . . . . . . 12
166158fveq2d 5817 . . . . . . . . . . . 12
167165, 166eqtrd 2495 . . . . . . . . . . 11
168162, 167oveq12d 6240 . . . . . . . . . 10
169134subidd 9844 . . . . . . . . . 10
170168, 169eqtrd 2495 . . . . . . . . 9
171170, 158oveq12d 6240 . . . . . . . 8
172114rpcnne0d 11175 . . . . . . . . 9
173 div0 10159 . . . . . . . . 9
174172, 173syl 16 . . . . . . . 8
175171, 174eqtrd 2495 . . . . . . 7
176 1p1e2 10573 . . . . . . . . . 10
177176oveq1i 6232 . . . . . . . . 9
178177a1i 11 . . . . . . . 8
179 elfzuz 11594 . . . . . . . . . . . . . 14
180 eluz2b2 11066 . . . . . . . . . . . . . . 15
181180simplbi 460 . . . . . . . . . . . . . 14
182179, 181syl 16 . . . . . . . . . . . . 13
183182, 177eleq2s 2562 . . . . . . . . . . . 12
18454, 183, 96syl2an 477 . . . . . . . . . . 11
18556adantr 465 . . . . . . . . . . . . . 14
186 nnq 11105 . . . . . . . . . . . . . 14
187185, 186syl 16 . . . . . . . . . . . . 13
188179, 177eleq2s 2562 . . . . . . . . . . . . . 14
189188adantl 466 . . . . . . . . . . . . 13
190 expnprm 14122 . . . . . . . . . . . . 13
191187, 189, 190syl2anc 661 . . . . . . . . . . . 12
192 iffalse 3914 . . . . . . . . . . . 12
193191, 192syl 16 . . . . . . . . . . 11
194184, 193oveq12d 6240 . . . . . . . . . 10
195134subid1d 9845 . . . . . . . . . . 11
196195adantr 465 . . . . . . . . . 10
197194, 196eqtrd 2495 . . . . . . . . 9
198197oveq1d 6237 . . . . . . . 8
199178, 198sumeq12dv 13341 . . . . . . 7
200175, 199oveq12d 6240 . . . . . 6
201 fzfid 11940 . . . . . . . . 9
202115adantr 465 . . . . . . . . . . 11
203 nnnn0 10724 . . . . . . . . . . . 12
20456, 203, 103syl2an 477 . . . . . . . . . . 11
205202, 204nndivred 10508 . . . . . . . . . 10
206182, 205sylan2 474 . . . . . . . . 9
207201, 206fsumrecl 13369 . . . . . . . 8
208207recnd 9549 . . . . . . 7
209208addid2d 9707 . . . . . 6
210156, 200, 2093eqtrd 2499 . . . . 5
211114rpreccld 11176 . . . . . . . . . . . 12
212133flcld 11793 . . . . . . . . . . . . 13
213212peano2zd 10888 . . . . . . . . . . . 12
214211, 213rpexpcld 12188