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

Theorem mertenslem1 13693
Description: Lemma for mertens 13695. (Contributed by Mario Carneiro, 29-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
mertens.12
mertens.13
Assertion
Ref Expression
mertenslem1
Distinct variable groups:   , , , , , , ,   , , , , , , ,   , , , , ,   , , , , , ,   , , , , , , , ,   , , , , , , , ,   , , , ,   , , , , , , ,   , , , , , , , ,   , , ,

Proof of Theorem mertenslem1
StepHypRef Expression
1 mertens.12 . . . . . . 7
21simpld 459 . . . . . 6
3 mertens.11 . . . . . 6
42, 3sylib 196 . . . . 5
54simpld 459 . . . 4
65nnnn0d 10877 . . 3
71simprd 463 . . . 4
87simpld 459 . . 3
96, 8nn0addcld 10881 . 2
10 fzfid 12083 . . . . . 6
11 simpl 457 . . . . . . . 8
12 elfznn0 11800 . . . . . . . 8
13 mertens.3 . . . . . . . 8
1411, 12, 13syl2an 477 . . . . . . 7
15 eqid 2457 . . . . . . . 8
16 fznn0sub 11745 . . . . . . . . . . 11
1716adantl 466 . . . . . . . . . 10
18 peano2nn0 10861 . . . . . . . . . 10
1917, 18syl 16 . . . . . . . . 9
2019nn0zd 10992 . . . . . . . 8
21 simplll 759 . . . . . . . . 9
22 eluznn0 11180 . . . . . . . . . 10
2319, 22sylan 471 . . . . . . . . 9
24 mertens.4 . . . . . . . . 9
2521, 23, 24syl2anc 661 . . . . . . . 8
26 mertens.5 . . . . . . . . 9
2721, 23, 26syl2anc 661 . . . . . . . 8
28 mertens.8 . . . . . . . . . 10
2928ad2antrr 725 . . . . . . . . 9
30 nn0uz 11144 . . . . . . . . . 10
31 simpll 753 . . . . . . . . . . 11
3224, 26eqeltrd 2545 . . . . . . . . . . 11
3331, 32sylan 471 . . . . . . . . . 10
3430, 19, 33iserex 13479 . . . . . . . . 9
3529, 34mpbid 210 . . . . . . . 8
3615, 20, 25, 27, 35isumcl 13576 . . . . . . 7
3714, 36mulcld 9637 . . . . . 6
3810, 37fsumcl 13555 . . . . 5
3938abscld 13267 . . . 4
4037abscld 13267 . . . . 5
4110, 40fsumrecl 13556 . . . 4
42 mertens.9 . . . . . 6
4342rpred 11285 . . . . 5
4443adantr 465 . . . 4
4510, 37fsumabs 13615 . . . 4
46 fzfid 12083 . . . . . . 7
476adantr 465 . . . . . . . . . . . . 13
4847nn0ge0d 10880 . . . . . . . . . . . 12
49 eluzelz 11119 . . . . . . . . . . . . . . 15
5049adantl 466 . . . . . . . . . . . . . 14
5150zred 10994 . . . . . . . . . . . . 13
5247nn0red 10878 . . . . . . . . . . . . 13
5351, 52subge02d 10169 . . . . . . . . . . . 12
5448, 53mpbid 210 . . . . . . . . . . 11
5547, 30syl6eleq 2555 . . . . . . . . . . . . . . 15
565nnzd 10993 . . . . . . . . . . . . . . . . . 18
57 uzid 11124 . . . . . . . . . . . . . . . . . 18
5856, 57syl 16 . . . . . . . . . . . . . . . . 17
59 uzaddcl 11166 . . . . . . . . . . . . . . . . 17
6058, 8, 59syl2anc 661 . . . . . . . . . . . . . . . 16
61 eqid 2457 . . . . . . . . . . . . . . . . 17
6261uztrn2 11127 . . . . . . . . . . . . . . . 16
6360, 62sylan 471 . . . . . . . . . . . . . . 15
64 elfzuzb 11711 . . . . . . . . . . . . . . 15
6555, 63, 64sylanbrc 664 . . . . . . . . . . . . . 14
66 fznn0sub2 11810 . . . . . . . . . . . . . 14
6765, 66syl 16 . . . . . . . . . . . . 13
68 elfzelz 11717 . . . . . . . . . . . . 13
6967, 68syl 16 . . . . . . . . . . . 12
70 eluz 11123 . . . . . . . . . . . 12
7169, 50, 70syl2anc 661 . . . . . . . . . . 11
7254, 71mpbird 232 . . . . . . . . . 10
73 fzss2 11752 . . . . . . . . . 10
7472, 73syl 16 . . . . . . . . 9
7574sselda 3503 . . . . . . . 8
7613abscld 13267 . . . . . . . . . 10
7711, 12, 76syl2an 477 . . . . . . . . 9
7836abscld 13267 . . . . . . . . 9
7977, 78remulcld 9645 . . . . . . . 8
8075, 79syldan 470 . . . . . . 7
8146, 80fsumrecl 13556 . . . . . 6
82 fzfid 12083 . . . . . . 7
83 elfznn0 11800 . . . . . . . . . . . . 13
8467, 83syl 16 . . . . . . . . . . . 12
85 peano2nn0 10861 . . . . . . . . . . . 12
8684, 85syl 16 . . . . . . . . . . 11
8786, 30syl6eleq 2555 . . . . . . . . . 10
88 fzss1 11751 . . . . . . . . . 10
8987, 88syl 16 . . . . . . . . 9
9089sselda 3503 . . . . . . . 8
9190, 79syldan 470 . . . . . . 7
9282, 91fsumrecl 13556 . . . . . 6
9342rphalfcld 11297 . . . . . . . 8
9493rpred 11285 . . . . . . 7
9594adantr 465 . . . . . 6
96 elfznn0 11800 . . . . . . . . . . 11
9711, 96, 76syl2an 477 . . . . . . . . . 10
9846, 97fsumrecl 13556 . . . . . . . . 9
9998, 95remulcld 9645 . . . . . . . 8
100 0zd 10901 . . . . . . . . . . 11
101 eqidd 2458 . . . . . . . . . . 11
102 mertens.2 . . . . . . . . . . . 12
103102, 76eqeltrd 2545 . . . . . . . . . . 11
104 mertens.7 . . . . . . . . . . 11
10530, 100, 101, 103, 104isumrecl 13580 . . . . . . . . . 10
10613absge0d 13275 . . . . . . . . . . . 12
107106, 102breqtrrd 4478 . . . . . . . . . . 11
10830, 100, 101, 103, 104, 107isumge0 13581 . . . . . . . . . 10
109105, 108ge0p1rpd 11311 . . . . . . . . 9
110109adantr 465 . . . . . . . 8
11199, 110rerpdivcld 11312 . . . . . . 7
11293, 109rpdivcld 11302 . . . . . . . . . . . 12
113112rpred 11285 . . . . . . . . . . 11
114113ad2antrr 725 . . . . . . . . . 10
11597, 114remulcld 9645 . . . . . . . . 9
11675, 20syldan 470 . . . . . . . . . . . 12
117 simplll 759 . . . . . . . . . . . . 13
11875, 19syldan 470 . . . . . . . . . . . . . 14
119118, 22sylan 471 . . . . . . . . . . . . 13
120117, 119, 24syl2anc 661 . . . . . . . . . . . 12
121117, 119, 26syl2anc 661 . . . . . . . . . . . 12
12275, 35syldan 470 . . . . . . . . . . . 12
12315, 116, 120, 121, 122isumcl 13576 . . . . . . . . . . 11
124123abscld 13267 . . . . . . . . . 10
12576, 106jca 532 . . . . . . . . . . 11
12611, 96, 125syl2an 477 . . . . . . . . . 10
127120sumeq2dv 13525 . . . . . . . . . . . . 13
128127fveq2d 5875 . . . . . . . . . . . 12
129 elfzelz 11717 . . . . . . . . . . . . . . . . 17
130129adantl 466 . . . . . . . . . . . . . . . 16
131130zred 10994 . . . . . . . . . . . . . . 15
13249ad2antlr 726 . . . . . . . . . . . . . . . 16
133132zred 10994 . . . . . . . . . . . . . . 15
13456ad2antrr 725 . . . . . . . . . . . . . . . 16
135134zred 10994 . . . . . . . . . . . . . . 15
136 elfzle2 11719 . . . . . . . . . . . . . . . 16
137136adantl 466 . . . . . . . . . . . . . . 15
138131, 133, 135, 137lesubd 10181 . . . . . . . . . . . . . 14
139132, 130zsubcld 10999 . . . . . . . . . . . . . . 15
140 eluz 11123 . . . . . . . . . . . . . . 15
141134, 139, 140syl2anc 661 . . . . . . . . . . . . . 14
142138, 141mpbird 232 . . . . . . . . . . . . 13
1434simprd 463 . . . . . . . . . . . . . 14
144143ad2antrr 725 . . . . . . . . . . . . 13
145 oveq1 6303 . . . . . . . . . . . . . . . . . 18
146145fveq2d 5875 . . . . . . . . . . . . . . . . 17
147146sumeq1d 13523 . . . . . . . . . . . . . . . 16
148147fveq2d 5875 . . . . . . . . . . . . . . 15
149148breq1d 4462 . . . . . . . . . . . . . 14
150149rspcv 3206 . . . . . . . . . . . . 13
151142, 144, 150sylc 60 . . . . . . . . . . . 12
152128, 151eqbrtrrd 4474 . . . . . . . . . . 11
153124, 114, 152ltled 9754 . . . . . . . . . 10
154 lemul2a 10422 . . . . . . . . . 10
155124, 114, 126, 153, 154syl31anc 1231 . . . . . . . . 9
15646, 80, 115, 155fsumle 13613 . . . . . . . 8
15798recnd 9643 . . . . . . . . . 10
15893rpcnd 11287 . . . . . . . . . . 11
159158adantr 465 . . . . . . . . . 10
160 peano2re 9774 . . . . . . . . . . . . 13
161105, 160syl 16 . . . . . . . . . . . 12
162161recnd 9643 . . . . . . . . . . 11
163162adantr 465 . . . . . . . . . 10
164109rpne0d 11290 . . . . . . . . . . 11
165164adantr 465 . . . . . . . . . 10
166157, 159, 163, 165divassd 10380 . . . . . . . . 9
167 fveq2 5871 . . . . . . . . . . . . . . . . 17
168167cbvsumv 13518 . . . . . . . . . . . . . . . 16
169168oveq1i 6306 . . . . . . . . . . . . . . 15
170169oveq2i 6307 . . . . . . . . . . . . . 14
171170, 112syl5eqel 2549 . . . . . . . . . . . . 13
172171rpcnd 11287 . . . . . . . . . . . 12
173172adantr 465 . . . . . . . . . . 11
17476recnd 9643 . . . . . . . . . . . 12
17511, 96, 174syl2an 477 . . . . . . . . . . 11
17646, 173, 175fsummulc1 13600 . . . . . . . . . 10
177170oveq2i 6307 . . . . . . . . . 10
178170oveq2i 6307 . . . . . . . . . . . 12
179178a1i 11 . . . . . . . . . . 11
180179sumeq2i 13521 . . . . . . . . . 10
181176, 177, 1803eqtr3g 2521 . . . . . . . . 9