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.

Step	Hyp	Ref	Expression
1		nn0uz 11144	. 2
2		0zd 10901	. 2
3		seqex 12109	. . 3
4	3	a1i 11	. 2
5		mertens.6	. . . . 5
6		fzfid 12083	. . . . . 6
7		simpl 457	. . . . . . . 8
8		elfznn0 11800	. . . . . . . 8
9		mertens.3	. . . . . . . 8
10	7, 8, 9	syl2an 477	. . . . . . 7
11		fznn0sub 11745	. . . . . . . . 9
12	11	adantl 466	. . . . . . . 8
13		mertens.4	. . . . . . . . . . . 12
14		mertens.5	. . . . . . . . . . . 12
15	13, 14	eqeltrd 2545	. . . . . . . . . . 11
16	15	ralrimiva 2871	. . . . . . . . . 10
17		fveq2 5871	. . . . . . . . . . . 12
18	17	eleq1d 2526	. . . . . . . . . . 11
19	18	cbvralv 3084	. . . . . . . . . 10
20	16, 19	sylib 196	. . . . . . . . 9
21	20	ad2antrr 725	. . . . . . . 8
22		fveq2 5871	. . . . . . . . . 10
23	22	eleq1d 2526	. . . . . . . . 9
24	23	rspcv 3206	. . . . . . . 8
25	12, 21, 24	sylc 60	. . . . . . 7
26	10, 25	mulcld 9637	. . . . . 6
27	6, 26	fsumcl 13555	. . . . 5
28	5, 27	eqeltrd 2545	. . . 4
29	1, 2, 28	serf 12135	. . 3
30	29	ffvelrnda 6031	. 2
31		mertens.1	. . . . . 6
32	31	adantlr 714	. . . . 5
33		mertens.2	. . . . . 6
34	33	adantlr 714	. . . . 5
35	9	adantlr 714	. . . . 5
36	13	adantlr 714	. . . . 5
37	14	adantlr 714	. . . . 5
38	5	adantlr 714	. . . . 5
39		mertens.7	. . . . . 6
40	39	adantr 465	. . . . 5
41		mertens.8	. . . . . 6
42	41	adantr 465	. . . . 5
43		simpr 461	. . . . 5
44		fveq2 5871	. . . . . . . . . . . 12
45	44	cbvsumv 13518	. . . . . . . . . . 11
46		oveq1 6303	. . . . . . . . . . . . 13
47	46	fveq2d 5875	. . . . . . . . . . . 12
48	47	sumeq1d 13523	. . . . . . . . . . 11
49	45, 48	syl5eq 2510	. . . . . . . . . 10
50	49	fveq2d 5875	. . . . . . . . 9
51	50	eqeq2d 2471	. . . . . . . 8
52	51	cbvrexv 3085	. . . . . . 7
53		eqeq1 2461	. . . . . . . 8
54	53	rexbidv 2968	. . . . . . 7
55	52, 54	syl5bb 257	. . . . . 6
56	55	cbvabv 2600	. . . . 5
57		fveq2 5871	. . . . . . . . . . . 12
58	57	cbvsumv 13518	. . . . . . . . . . 11
59	58	oveq1i 6306	. . . . . . . . . 10
60	59	oveq2i 6307	. . . . . . . . 9
61	60	breq2i 4460	. . . . . . . 8
62		fveq2 5871	. . . . . . . . . . . 12
63	62	cbvsumv 13518	. . . . . . . . . . 11
64		oveq1 6303	. . . . . . . . . . . . 13
65	64	fveq2d 5875	. . . . . . . . . . . 12
66	65	sumeq1d 13523	. . . . . . . . . . 11
67	63, 66	syl5eq 2510	. . . . . . . . . 10
68	67	fveq2d 5875	. . . . . . . . 9
69	68	breq1d 4462	. . . . . . . 8
70	61, 69	syl5bb 257	. . . . . . 7
71	70	cbvralv 3084	. . . . . 6
72	71	anbi2i 694	. . . . 5
73	32, 34, 35, 36, 37, 38, 40, 42, 43, 56, 72	mertenslem2 13694	. . . 4
74		eluznn0 11180	. . . . . . . . 9
75		fzfid 12083	. . . . . . . . . . . . 13
76		simpll 753	. . . . . . . . . . . . . 14
77		elfznn0 11800	. . . . . . . . . . . . . . 15
78	77	adantl 466	. . . . . . . . . . . . . 14
79	1, 2, 13, 14, 41	isumcl 13576	. . . . . . . . . . . . . . . 16
80	79	adantr 465	. . . . . . . . . . . . . . 15
81	31, 9	eqeltrd 2545	. . . . . . . . . . . . . . 15
82	80, 81	mulcld 9637	. . . . . . . . . . . . . 14
83	76, 78, 82	syl2anc 661	. . . . . . . . . . . . 13
84		fzfid 12083	. . . . . . . . . . . . . 14
85		simplll 759	. . . . . . . . . . . . . . . 16
86	77	ad2antlr 726	. . . . . . . . . . . . . . . 16
87	85, 86, 9	syl2anc 661	. . . . . . . . . . . . . . 15
88		elfznn0 11800	. . . . . . . . . . . . . . . . 17
89	88	adantl 466	. . . . . . . . . . . . . . . 16
90	85, 89, 15	syl2anc 661	. . . . . . . . . . . . . . 15
91	87, 90	mulcld 9637	. . . . . . . . . . . . . 14
92	84, 91	fsumcl 13555	. . . . . . . . . . . . 13
93	75, 83, 92	fsumsub 13603	. . . . . . . . . . . 12
94	76, 78, 9	syl2anc 661	. . . . . . . . . . . . . . 15
95	79	ad2antrr 725	. . . . . . . . . . . . . . 15
96	84, 90	fsumcl 13555	. . . . . . . . . . . . . . 15
97	94, 95, 96	subdid 10037	. . . . . . . . . . . . . 14
98		eqid 2457	. . . . . . . . . . . . . . . . . . 19
99		fznn0sub 11745	. . . . . . . . . . . . . . . . . . . . 21
100	99	adantl 466	. . . . . . . . . . . . . . . . . . . 20
101		peano2nn0 10861	. . . . . . . . . . . . . . . . . . . 20
102	100, 101	syl 16	. . . . . . . . . . . . . . . . . . 19
103	76, 13	sylan 471	. . . . . . . . . . . . . . . . . . 19
104	76, 14	sylan 471	. . . . . . . . . . . . . . . . . . 19
105	41	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19
106	1, 98, 102, 103, 104, 105	isumsplit 13652	. . . . . . . . . . . . . . . . . 18
107	100	nn0cnd 10879	. . . . . . . . . . . . . . . . . . . . . . 23
108		ax-1cn 9571	. . . . . . . . . . . . . . . . . . . . . . 23
109		pncan 9849	. . . . . . . . . . . . . . . . . . . . . . 23
110	107, 108, 109	sylancl 662	. . . . . . . . . . . . . . . . . . . . . 22
111	110	oveq2d 6312	. . . . . . . . . . . . . . . . . . . . 21
112	111	sumeq1d 13523	. . . . . . . . . . . . . . . . . . . 20
113	85, 89, 13	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21
114	113	sumeq2dv 13525	. . . . . . . . . . . . . . . . . . . 20
115	112, 114	eqtr4d 2501	. . . . . . . . . . . . . . . . . . 19
116	115	oveq1d 6311	. . . . . . . . . . . . . . . . . 18
117	106, 116	eqtrd 2498	. . . . . . . . . . . . . . . . 17
118	117	oveq1d 6311	. . . . . . . . . . . . . . . 16
119	102	nn0zd 10992	. . . . . . . . . . . . . . . . . 18
120		simplll 759	. . . . . . . . . . . . . . . . . . 19
121		eluznn0 11180	. . . . . . . . . . . . . . . . . . . 20
122	102, 121	sylan 471	. . . . . . . . . . . . . . . . . . 19
123	120, 122, 13	syl2anc 661	. . . . . . . . . . . . . . . . . 18
124	120, 122, 14	syl2anc 661	. . . . . . . . . . . . . . . . . 18
125	103, 104	eqeltrd 2545	. . . . . . . . . . . . . . . . . . . 20
126	1, 102, 125	iserex 13479	. . . . . . . . . . . . . . . . . . 19
127	105, 126	mpbid 210	. . . . . . . . . . . . . . . . . 18
128	98, 119, 123, 124, 127	isumcl 13576	. . . . . . . . . . . . . . . . 17
129	96, 128	pncan2d 9956	. . . . . . . . . . . . . . . 16
130	118, 129	eqtrd 2498	. . . . . . . . . . . . . . 15
131	130	oveq2d 6312	. . . . . . . . . . . . . 14
132	9, 80	mulcomd 9638	. . . . . . . . . . . . . . . . 17
133	31	oveq2d 6312	. . . . . . . . . . . . . . . . 17
134	132, 133	eqtr4d 2501	. . . . . . . . . . . . . . . 16
135	76, 78, 134	syl2anc 661	. . . . . . . . . . . . . . 15
136	84, 94, 90	fsummulc2 13599	. . . . . . . . . . . . . . 15
137	135, 136	oveq12d 6314	. . . . . . . . . . . . . 14
138	97, 131, 137	3eqtr3rd 2507	. . . . . . . . . . . . 13
139	138	sumeq2dv 13525	. . . . . . . . . . . 12
140		fveq2 5871	. . . . . . . . . . . . . . . . 17
141	140	oveq2d 6312	. . . . . . . . . . . . . . . 16
142		eqid 2457	. . . . . . . . . . . . . . . 16
143		ovex 6324	. . . . . . . . . . . . . . . 16
144	141, 142, 143	fvmpt 5956	. . . . . . . . . . . . . . 15
145	78, 144	syl 16	. . . . . . . . . . . . . 14
146		simpr 461	. . . . . . . . . . . . . . 15
147	146, 1	syl6eleq 2555	. . . . . . . . . . . . . 14
148	145, 147, 83	fsumser 13552	. . . . . . . . . . . . 13
149		fveq2 5871	. . . . . . . . . . . . . . . 16
150	149	oveq2d 6312	. . . . . . . . . . . . . . 15
151		fveq2 5871	. . . . . . . . . . . . . . . 16
152	151	oveq2d 6312	. . . . . . . . . . . . . . 15
153	91	anasss 647	. . . . . . . . . . . . . . 15
154	150, 152, 153	fsum0diag2 13598	. . . . . . . . . . . . . 14
155		simpll 753	. . . . . . . . . . . . . . . 16
156		elfznn0 11800	. . . . . . . . . . . . . . . . 17
157	156	adantl 466	. . . . . . . . . . . . . . . 16
158	155, 157, 5	syl2anc 661	. . . . . . . . . . . . . . 15
159	155, 157, 27	syl2anc 661	. . . . . . . . . . . . . . 15
160	158, 147, 159	fsumser 13552	. . . . . . . . . . . . . 14
161	154, 160	eqtrd 2498	. . . . . . . . . . . . 13
162	148, 161	oveq12d 6314	. . . . . . . . . . . 12
163	93, 139, 162	3eqtr3rd 2507	. . . . . . . . . . 11
164	163	fveq2d 5875	. . . . . . . . . 10
165	164	breq1d 4462	. . . . . . . . 9
166	74, 165	sylan2 474	. . . . . . . 8
167	166	anassrs 648	. . . . . . 7
168	167	ralbidva 2893	. . . . . 6
169	168	rexbidva 2965	. . . . 5
170	169	adantr 465	. . . 4
171	73, 170	mpbird 232	. . 3
172	171	ralrimiva 2871	. 2
173	31	fveq2d 5875	. . . . . . 7
174	33, 173	eqtr4d 2501	. . . . . 6