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

Theorem mertens 13695
 Description: Mertens' theorem. If A( ) is an absolutely convergent series and ( ) is convergent, then (sum_ e. A( ) sum_ e. ( ))= sum_ e. sum_ e.(0 )(A( ) ( )) (and this latter series is convergent). This latter sum is commonly known as the Cauchy product of the sequences. The proof follows the outline at http://en.wikipedia.org/wiki/Cauchy_product#Proof_of_Mertens.27_theorem. (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
Assertion
Ref Expression
mertens
Distinct variable groups:   ,   ,,   ,,   ,   ,,   ,   ,

Proof of Theorem mertens
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nn0uz 11144 . 2
2 0zd 10901 . 2
3 seqex 12109 . . 3
43a1i 11 . 2
5 mertens.6 . . . . 5
6 fzfid 12083 . . . . . 6
7 simpl 457 . . . . . . . 8
8 elfznn0 11800 . . . . . . . 8
9 mertens.3 . . . . . . . 8
107, 8, 9syl2an 477 . . . . . . 7
11 fznn0sub 11745 . . . . . . . . 9
1211adantl 466 . . . . . . . 8
13 mertens.4 . . . . . . . . . . . 12
14 mertens.5 . . . . . . . . . . . 12
1513, 14eqeltrd 2545 . . . . . . . . . . 11
1615ralrimiva 2871 . . . . . . . . . 10
17 fveq2 5871 . . . . . . . . . . . 12
1817eleq1d 2526 . . . . . . . . . . 11
1918cbvralv 3084 . . . . . . . . . 10
2016, 19sylib 196 . . . . . . . . 9
2120ad2antrr 725 . . . . . . . 8
22 fveq2 5871 . . . . . . . . . 10
2322eleq1d 2526 . . . . . . . . 9
2423rspcv 3206 . . . . . . . 8
2512, 21, 24sylc 60 . . . . . . 7
2610, 25mulcld 9637 . . . . . 6
276, 26fsumcl 13555 . . . . 5
285, 27eqeltrd 2545 . . . 4
291, 2, 28serf 12135 . . 3
3029ffvelrnda 6031 . 2
31 mertens.1 . . . . . 6
3231adantlr 714 . . . . 5
33 mertens.2 . . . . . 6
3433adantlr 714 . . . . 5
359adantlr 714 . . . . 5
3613adantlr 714 . . . . 5
3714adantlr 714 . . . . 5
385adantlr 714 . . . . 5
39 mertens.7 . . . . . 6
4039adantr 465 . . . . 5
41 mertens.8 . . . . . 6
4241adantr 465 . . . . 5
43 simpr 461 . . . . 5
44 fveq2 5871 . . . . . . . . . . . 12
4544cbvsumv 13518 . . . . . . . . . . 11
46 oveq1 6303 . . . . . . . . . . . . 13
4746fveq2d 5875 . . . . . . . . . . . 12
4847sumeq1d 13523 . . . . . . . . . . 11
4945, 48syl5eq 2510 . . . . . . . . . 10
5049fveq2d 5875 . . . . . . . . 9
5150eqeq2d 2471 . . . . . . . 8
5251cbvrexv 3085 . . . . . . 7
53 eqeq1 2461 . . . . . . . 8
5453rexbidv 2968 . . . . . . 7
5552, 54syl5bb 257 . . . . . 6
5655cbvabv 2600 . . . . 5
57 fveq2 5871 . . . . . . . . . . . 12
5857cbvsumv 13518 . . . . . . . . . . 11
5958oveq1i 6306 . . . . . . . . . 10
6059oveq2i 6307 . . . . . . . . 9
6160breq2i 4460 . . . . . . . 8
62 fveq2 5871 . . . . . . . . . . . 12
6362cbvsumv 13518 . . . . . . . . . . 11
64 oveq1 6303 . . . . . . . . . . . . 13
6564fveq2d 5875 . . . . . . . . . . . 12
6665sumeq1d 13523 . . . . . . . . . . 11
6763, 66syl5eq 2510 . . . . . . . . . 10
6867fveq2d 5875 . . . . . . . . 9
6968breq1d 4462 . . . . . . . 8
7061, 69syl5bb 257 . . . . . . 7
7170cbvralv 3084 . . . . . 6
7271anbi2i 694 . . . . 5
7332, 34, 35, 36, 37, 38, 40, 42, 43, 56, 72mertenslem2 13694 . . . 4
74 eluznn0 11180 . . . . . . . . 9
75 fzfid 12083 . . . . . . . . . . . . 13
76 simpll 753 . . . . . . . . . . . . . 14
77 elfznn0 11800 . . . . . . . . . . . . . . 15
7877adantl 466 . . . . . . . . . . . . . 14
791, 2, 13, 14, 41isumcl 13576 . . . . . . . . . . . . . . . 16
8079adantr 465 . . . . . . . . . . . . . . 15
8131, 9eqeltrd 2545 . . . . . . . . . . . . . . 15
8280, 81mulcld 9637 . . . . . . . . . . . . . 14
8376, 78, 82syl2anc 661 . . . . . . . . . . . . 13
84 fzfid 12083 . . . . . . . . . . . . . 14
85 simplll 759 . . . . . . . . . . . . . . . 16
8677ad2antlr 726 . . . . . . . . . . . . . . . 16
8785, 86, 9syl2anc 661 . . . . . . . . . . . . . . 15
88 elfznn0 11800 . . . . . . . . . . . . . . . . 17
8988adantl 466 . . . . . . . . . . . . . . . 16
9085, 89, 15syl2anc 661 . . . . . . . . . . . . . . 15
9187, 90mulcld 9637 . . . . . . . . . . . . . 14
9284, 91fsumcl 13555 . . . . . . . . . . . . 13
9375, 83, 92fsumsub 13603 . . . . . . . . . . . 12
9476, 78, 9syl2anc 661 . . . . . . . . . . . . . . 15
9579ad2antrr 725 . . . . . . . . . . . . . . 15
9684, 90fsumcl 13555 . . . . . . . . . . . . . . 15
9794, 95, 96subdid 10037 . . . . . . . . . . . . . 14
98 eqid 2457 . . . . . . . . . . . . . . . . . . 19
99 fznn0sub 11745 . . . . . . . . . . . . . . . . . . . . 21
10099adantl 466 . . . . . . . . . . . . . . . . . . . 20
101 peano2nn0 10861 . . . . . . . . . . . . . . . . . . . 20
102100, 101syl 16 . . . . . . . . . . . . . . . . . . 19
10376, 13sylan 471 . . . . . . . . . . . . . . . . . . 19
10476, 14sylan 471 . . . . . . . . . . . . . . . . . . 19
10541ad2antrr 725 . . . . . . . . . . . . . . . . . . 19
1061, 98, 102, 103, 104, 105isumsplit 13652 . . . . . . . . . . . . . . . . . 18
107100nn0cnd 10879 . . . . . . . . . . . . . . . . . . . . . . 23
108 ax-1cn 9571 . . . . . . . . . . . . . . . . . . . . . . 23
109 pncan 9849 . . . . . . . . . . . . . . . . . . . . . . 23
110107, 108, 109sylancl 662 . . . . . . . . . . . . . . . . . . . . . 22
111110oveq2d 6312 . . . . . . . . . . . . . . . . . . . . 21
112111sumeq1d 13523 . . . . . . . . . . . . . . . . . . . 20
11385, 89, 13syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21
114113sumeq2dv 13525 . . . . . . . . . . . . . . . . . . . 20
115112, 114eqtr4d 2501 . . . . . . . . . . . . . . . . . . 19
116115oveq1d 6311 . . . . . . . . . . . . . . . . . 18
117106, 116eqtrd 2498 . . . . . . . . . . . . . . . . 17
118117oveq1d 6311 . . . . . . . . . . . . . . . 16
119102nn0zd 10992 . . . . . . . . . . . . . . . . . 18
120 simplll 759 . . . . . . . . . . . . . . . . . . 19
121 eluznn0 11180 . . . . . . . . . . . . . . . . . . . 20
122102, 121sylan 471 . . . . . . . . . . . . . . . . . . 19
123120, 122, 13syl2anc 661 . . . . . . . . . . . . . . . . . 18
124120, 122, 14syl2anc 661 . . . . . . . . . . . . . . . . . 18
125103, 104eqeltrd 2545 . . . . . . . . . . . . . . . . . . . 20
1261, 102, 125iserex 13479 . . . . . . . . . . . . . . . . . . 19
127105, 126mpbid 210 . . . . . . . . . . . . . . . . . 18
12898, 119, 123, 124, 127isumcl 13576 . . . . . . . . . . . . . . . . 17
12996, 128pncan2d 9956 . . . . . . . . . . . . . . . 16
130118, 129eqtrd 2498 . . . . . . . . . . . . . . 15
131130oveq2d 6312 . . . . . . . . . . . . . 14
1329, 80mulcomd 9638 . . . . . . . . . . . . . . . . 17
13331oveq2d 6312 . . . . . . . . . . . . . . . . 17
134132, 133eqtr4d 2501 . . . . . . . . . . . . . . . 16
13576, 78, 134syl2anc 661 . . . . . . . . . . . . . . 15
13684, 94, 90fsummulc2 13599 . . . . . . . . . . . . . . 15
137135, 136oveq12d 6314 . . . . . . . . . . . . . 14
13897, 131, 1373eqtr3rd 2507 . . . . . . . . . . . . 13
139138sumeq2dv 13525 . . . . . . . . . . . 12
140 fveq2 5871 . . . . . . . . . . . . . . . . 17
141140oveq2d 6312 . . . . . . . . . . . . . . . 16
142 eqid 2457 . . . . . . . . . . . . . . . 16
143 ovex 6324 . . . . . . . . . . . . . . . 16
144141, 142, 143fvmpt 5956 . . . . . . . . . . . . . . 15
14578, 144syl 16 . . . . . . . . . . . . . 14
146 simpr 461 . . . . . . . . . . . . . . 15
147146, 1syl6eleq 2555 . . . . . . . . . . . . . 14
148145, 147, 83fsumser 13552 . . . . . . . . . . . . 13
149 fveq2 5871 . . . . . . . . . . . . . . . 16
150149oveq2d 6312 . . . . . . . . . . . . . . 15
151 fveq2 5871 . . . . . . . . . . . . . . . 16
152151oveq2d 6312 . . . . . . . . . . . . . . 15
15391anasss 647 . . . . . . . . . . . . . . 15
154150, 152, 153fsum0diag2 13598 . . . . . . . . . . . . . 14
155 simpll 753 . . . . . . . . . . . . . . . 16
156 elfznn0 11800 . . . . . . . . . . . . . . . . 17
157156adantl 466 . . . . . . . . . . . . . . . 16
158155, 157, 5syl2anc 661 . . . . . . . . . . . . . . 15
159155, 157, 27syl2anc 661 . . . . . . . . . . . . . . 15
160158, 147, 159fsumser 13552 . . . . . . . . . . . . . 14
161154, 160eqtrd 2498 . . . . . . . . . . . . 13
162148, 161oveq12d 6314 . . . . . . . . . . . 12
16393, 139, 1623eqtr3rd 2507 . . . . . . . . . . 11
164163fveq2d 5875 . . . . . . . . . 10
165164breq1d 4462 . . . . . . . . 9
16674, 165sylan2 474 . . . . . . . 8
167166anassrs 648 . . . . . . 7
168167ralbidva 2893 . . . . . 6
169168rexbidva 2965 . . . . 5
170169adantr 465 . . . 4
17173, 170mpbird 232 . . 3
172171ralrimiva 2871 . 2
17331fveq2d 5875 . . . . . . 7
17433, 173eqtr4d 2501 . . . . . 6