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

Theorem mertenslem2 13694
Description: Lemma for mertens 13695. (Contributed by Mario Carneiro, 28-Apr-2014.)
Hypotheses
Ref Expression
mertens.1
mertens.2
mertens.3
mertens.4
mertens.5
mertens.6
mertens.7
mertens.8
mertens.9
mertens.10
mertens.11
Assertion
Ref Expression
mertenslem2
Distinct variable groups:   , , , , , ,   , , , , , , ,   , , , , ,   , , , , ,   , , , , , , ,   , , , , , , ,   , , , ,   , , , , , ,   , , , , , ,   , , ,   , ,

Proof of Theorem mertenslem2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnuz 11145 . . 3
2 1zzd 10920 . . 3
3 mertens.9 . . . . 5
43rphalfcld 11297 . . . 4
5 nn0uz 11144 . . . . . 6
6 0zd 10901 . . . . . 6
7 eqidd 2458 . . . . . 6
8 mertens.2 . . . . . . 7
9 mertens.3 . . . . . . . 8
109abscld 13267 . . . . . . 7
118, 10eqeltrd 2545 . . . . . 6
12 mertens.7 . . . . . 6
135, 6, 7, 11, 12isumrecl 13580 . . . . 5
149absge0d 13275 . . . . . . 7
1514, 8breqtrrd 4478 . . . . . 6
165, 6, 7, 11, 12, 15isumge0 13581 . . . . 5
1713, 16ge0p1rpd 11311 . . . 4
184, 17rpdivcld 11302 . . 3
19 eqidd 2458 . . 3
20 mertens.4 . . . 4
21 mertens.5 . . . 4
22 mertens.8 . . . 4
235, 6, 20, 21, 22isumclim2 13573 . . 3
241, 2, 18, 19, 23climi2 13334 . 2
25 eluznn 11181 . . . . . . . 8
2620, 21eqeltrd 2545 . . . . . . . . . . . . 13
275, 6, 26serf 12135 . . . . . . . . . . . 12
28 nnnn0 10827 . . . . . . . . . . . 12
29 ffvelrn 6029 . . . . . . . . . . . 12
3027, 28, 29syl2an 477 . . . . . . . . . . 11
315, 6, 20, 21, 22isumcl 13576 . . . . . . . . . . . 12
3231adantr 465 . . . . . . . . . . 11
3330, 32abssubd 13284 . . . . . . . . . 10
34 eqid 2457 . . . . . . . . . . . . . 14
3528adantl 466 . . . . . . . . . . . . . . . 16
36 peano2nn0 10861 . . . . . . . . . . . . . . . 16
3735, 36syl 16 . . . . . . . . . . . . . . 15
3837nn0zd 10992 . . . . . . . . . . . . . 14
39 simpll 753 . . . . . . . . . . . . . . 15
40 eluznn0 11180 . . . . . . . . . . . . . . . 16
4137, 40sylan 471 . . . . . . . . . . . . . . 15
4239, 41, 20syl2anc 661 . . . . . . . . . . . . . 14
4339, 41, 21syl2anc 661 . . . . . . . . . . . . . 14
4422adantr 465 . . . . . . . . . . . . . . 15
4526adantlr 714 . . . . . . . . . . . . . . . 16
465, 37, 45iserex 13479 . . . . . . . . . . . . . . 15
4744, 46mpbid 210 . . . . . . . . . . . . . 14
4834, 38, 42, 43, 47isumcl 13576 . . . . . . . . . . . . 13
4930, 48pncan2d 9956 . . . . . . . . . . . 12
5020adantlr 714 . . . . . . . . . . . . . . 15
5121adantlr 714 . . . . . . . . . . . . . . 15
525, 34, 37, 50, 51, 44isumsplit 13652 . . . . . . . . . . . . . 14
53 nncn 10569 . . . . . . . . . . . . . . . . . . . 20
5453adantl 466 . . . . . . . . . . . . . . . . . . 19
55 ax-1cn 9571 . . . . . . . . . . . . . . . . . . 19
56 pncan 9849 . . . . . . . . . . . . . . . . . . 19
5754, 55, 56sylancl 662 . . . . . . . . . . . . . . . . . 18
5857oveq2d 6312 . . . . . . . . . . . . . . . . 17
5958sumeq1d 13523 . . . . . . . . . . . . . . . 16
60 simpl 457 . . . . . . . . . . . . . . . . . 18
61 elfznn0 11800 . . . . . . . . . . . . . . . . . 18
6260, 61, 20syl2an 477 . . . . . . . . . . . . . . . . 17
6335, 5syl6eleq 2555 . . . . . . . . . . . . . . . . 17
6460, 61, 21syl2an 477 . . . . . . . . . . . . . . . . 17
6562, 63, 64fsumser 13552 . . . . . . . . . . . . . . . 16
6659, 65eqtrd 2498 . . . . . . . . . . . . . . 15
6766oveq1d 6311 . . . . . . . . . . . . . 14
6852, 67eqtrd 2498 . . . . . . . . . . . . 13
6968oveq1d 6311 . . . . . . . . . . . 12
7042sumeq2dv 13525 . . . . . . . . . . . 12
7149, 69, 703eqtr4d 2508 . . . . . . . . . . 11
7271fveq2d 5875 . . . . . . . . . 10
7333, 72eqtrd 2498 . . . . . . . . 9
7473breq1d 4462 . . . . . . . 8
7525, 74sylan2 474 . . . . . . 7
7675anassrs 648 . . . . . 6
7776ralbidva 2893 . . . . 5
78 oveq1 6303 . . . . . . . . . 10
7978fveq2d 5875 . . . . . . . . 9
8079sumeq1d 13523 . . . . . . . 8
8180fveq2d 5875 . . . . . . 7
8281breq1d 4462 . . . . . 6
8382cbvralv 3084 . . . . 5
8477, 83syl6bb 261 . . . 4
85 mertens.11 . . . . . 6
86 0zd 10901 . . . . . . . . 9
874adantr 465 . . . . . . . . . . 11
8885simplbi 460 . . . . . . . . . . . . 13
8988adantl 466 . . . . . . . . . . . 12
9089nnrpd 11284 . . . . . . . . . . 11
9187, 90rpdivcld 11302 . . . . . . . . . 10
92 mertens.10 . . . . . . . . . . . . 13
93 eqid 2457 . . . . . . . . . . . . . . . . . 18
94 elfznn0 11800 . . . . . . . . . . . . . . . . . . . . 21
9594adantl 466 . . . . . . . . . . . . . . . . . . . 20
96 peano2nn0 10861 . . . . . . . . . . . . . . . . . . . 20
9795, 96syl 16 . . . . . . . . . . . . . . . . . . 19
9897nn0zd 10992 . . . . . . . . . . . . . . . . . 18
99 eqidd 2458 . . . . . . . . . . . . . . . . . 18
100 simplll 759 . . . . . . . . . . . . . . . . . . 19
101 eluznn0 11180 . . . . . . . . . . . . . . . . . . . 20
10297, 101sylan 471 . . . . . . . . . . . . . . . . . . 19
103100, 102, 26syl2anc 661 . . . . . . . . . . . . . . . . . 18
10422ad2antrr 725 . . . . . . . . . . . . . . . . . . 19
105 simpll 753 . . . . . . . . . . . . . . . . . . . . 21
106105, 26sylan 471 . . . . . . . . . . . . . . . . . . . 20
1075, 97, 106iserex 13479 . . . . . . . . . . . . . . . . . . 19
108104, 107mpbid 210 . . . . . . . . . . . . . . . . . 18
10993, 98, 99, 103, 108isumcl 13576 . . . . . . . . . . . . . . . . 17
110109abscld 13267 . . . . . . . . . . . . . . . 16
111 eleq1a 2540 . . . . . . . . . . . . . . . 16
112110, 111syl 16 . . . . . . . . . . . . . . 15
113112rexlimdva 2949 . . . . . . . . . . . . . 14
114113abssdv 3573 . . . . . . . . . . . . 13
11592, 114syl5eqss 3547 . . . . . . . . . . . 12
116 fzfid 12083 . . . . . . . . . . . . . . 15
117 abrexfi 7840 . . . . . . . . . . . . . . 15
118116, 117syl 16 . . . . . . . . . . . . . 14
11992, 118syl5eqel 2549 . . . . . . . . . . . . 13
120 nnm1nn0 10862 . . . . . . . . . . . . . . . . . . 19
12189, 120syl 16 . . . . . . . . . . . . . . . . . 18
122121, 5syl6eleq 2555 . . . . . . . . . . . . . . . . 17
123 eluzfz1 11722 . . . . . . . . . . . . . . . . 17
124122, 123syl 16 . . . . . . . . . . . . . . . 16
125 nnnn0 10827 . . . . . . . . . . . . . . . . . . . . 21
126125, 20sylan2 474 . . . . . . . . . . . . . . . . . . . 20
127126sumeq2dv 13525 . . . . . . . . . . . . . . . . . . 19
128127adantr 465 . . . . . . . . . . . . . . . . . 18
129128fveq2d 5875 . . . . . . . . . . . . . . . . 17
130129eqcomd 2465 . . . . . . . . . . . . . . . 16
131 oveq1 6303 . . . . . . . . . . . . . . . . . . . . . . 23
132 0p1e1 10672 . . . . . . . . . . . . . . . . . . . . . . 23
133131, 132syl6eq 2514 . . . . . . . . . . . . . . . . . . . . . 22
134133fveq2d 5875 . . . . . . . . . . . . . . . . . . . . 21
135134, 1syl6eqr 2516 . . . . . . . . . . . . . . . . . . . 20
136135sumeq1d 13523 . . . . . . . . . . . . . . . . . . 19
137136fveq2d 5875 . . . . . . . . . . . . . . . . . 18
138137eqeq2d 2471 . . . . . . . . . . . . . . . . 17
139138rspcev 3210 . . . . . . . . . . . . . . . 16
140124, 130, 139syl2anc 661 . . . . . . . . . . . . . . 15
141 fvex 5881 . . . . . . . . . . . . . . . 16
142 eqeq1 2461 . . . . . . . . . . . . . . . . 17
143142rexbidv 2968 . . . . . . . . . . . . . . . 16
144141, 143, 92elab2 3249 . . . . . . . . . . . . . . 15
145140, 144sylibr 212 . . . . . . . . . . . . . 14
146 ne0i 3790 . . . . . . . . . . . . . 14
147145, 146syl 16 . . . . . . . . . . . . 13
148 ltso 9686 . . . . . . . . . . . . . 14
149 fisupcl 7948 . . . . . . . . . . . . . 14
150148, 149mpan 670 . . . . . . . . . . . . 13
151119, 147, 115, 150syl3anc 1228 . . . . . . . . . . . 12
152115, 151sseldd 3504 . . . . . . . . . . 11
153 0red 9618 . . . . . . . . . . . 12
154125, 21sylan2 474 . . . . . . . . . . . . . . 15
155 1nn0 10836 . . . . . . . . . . . . . . . . . 18
156155a1i 11 . . . . . . . . . . . . . . . . 17
1575, 156, 26iserex 13479 . . . . . . . . . . . . . . . 16
15822, 157mpbid 210 . . . . . . . . . . . . . . 15
1591, 2, 126, 154, 158isumcl 13576 . . . . . . . . . . . . . 14
160159adantr 465 . . . . . . . . . . . . 13
161160abscld 13267 . . . . . . . . . . . 12
162160absge0d 13275 . . . . . . . . . . . 12
163 fimaxre2 10516 . . . . . . . . . . . . . . 15
164115, 119, 163syl2anc 661 . . . . . . . . . . . . . 14
165115, 147, 1643jca 1176 . . . . . . . . . . . . 13
166 suprub 10529 . . . . . . . . . . . . 13
167165, 145, 166syl2anc 661 . . . . . . . . . . . 12
168153, 161, 152, 162, 167letrd 9760 . . . . . . . . . . 11
169152, 168ge0p1rpd 11311 . . . . . . . . . 10
17091, 169rpdivcld 11302 . . . . . . . . 9
171 fveq2 5871 . . . . . . . . . . 11
172 eqid 2457 . . . . . . . . . . 11
173 fvex 5881 . . . . . . . . . . 11
174171, 172, 173fvmpt 5956 . . . . . . . . . 10
175174adantl 466 . . . . . . . . 9
176 nn0ex 10826 . . . . . . . . . . . . 13
177176mptex 6143 . . . . . . . . . . . 12
178177a1i 11 . . . . . . . . . . 11
179 elnn0uz 11147 . . . . . . . . . . . . . 14
180 fveq2 5871 . . . . . . . . . . . . . . . 16
181 fvex 5881 . . . . . . . . . . . . . . . 16
182180, 172, 181fvmpt 5956 . . . . . . . . . . . . . . 15
183182adantl 466 . . . . . . . . . . . . . 14
184179, 183sylan2br 476 . . . . . . . . . . . . 13
1856, 184seqfeq 12132 . . . . . . . . . . . 12
186185, 12eqeltrd 2545 . . . . . . . . . . 11
187183, 8eqtrd 2498 . . . . . . . . . . . . 13
188187, 10eqeltrd 2545 . . . . . . . . . . . 12
189188recnd 9643 . . . . . . . . . . 11
1905, 6, 178, 186, 189serf0 13503 . . . . . . . . . 10
191190adantr 465 . . . . . . . . 9
1925, 86, 170, 175, 191climi0 13335 . . . . . . . 8
193 simplll 759 . . . . . . . . . . . . . 14
194 eluznn0 11180 . . . . . . . . . . . . . . 15
195194adantll 713 . . . . . . . . . . . . . 14
19611, 15absidd 13254 . . . . . . . . . . . . . . . 16
197196ralrimiva 2871 . . . . . . . . . . . . . . 15
198 fveq2 5871 . . . . . . . . . . . . . . . . . 18
199198fveq2d 5875 . . . . . . . . . . . . . . . . 17
200199, 198eqeq12d 2479 . . . . . . . . . . . . . . . 16
201200rspccva 3209 . . . . . . . . . . . . . . 15
202197, 201sylan 471 . . . . . . . . . . . . . 14
203193, 195, 202syl2anc 661 . . . . . . . . . . . . 13
204203breq1d 4462 . . . . . . . . . . . 12
205204ralbidva 2893 . . . . . . . . . . 11
206171breq1d 4462 . . . . . . . . . . . 12
207206cbvralv 3084 . . . . . . . . . . 11
208205, 207syl6bbr 263 . . . . . . . . . 10
209 simpll 753 . . . . . . . . . . . . 13