mertens

Description: Mertens' theorem. If A ( j ) is an absolutely convergent series and B ( k ) is convergent, then ( sum_ j e. NN0 A ( j ) x. sum_ k e. NN0 B ( k ) ) = sum_ k e. NN0 sum_ j e. ( 0 ... k ) ( A ( j ) x. B ( k - j ) ) (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)

	Ref	Expression
Hypotheses	mertens.1	$⊢ (φ \land j \in ℕ_{0}) \to F (j) = A$
	mertens.2	$⊢ (φ \land j \in ℕ_{0}) \to K (j) = \|A\|$
	mertens.3	$⊢ (φ \land j \in ℕ_{0}) \to A \in ℂ$
	mertens.4	$⊢ (φ \land k \in ℕ_{0}) \to G (k) = B$
	mertens.5	$⊢ (φ \land k \in ℕ_{0}) \to B \in ℂ$
	mertens.6	$⊢ (φ \land k \in ℕ_{0}) \to H (k) = \sum_{j = 0}^{k} A G (k - j)$
	mertens.7	$⊢ φ \to seq 0 (+ K) \in dom ⇝$
	mertens.8	$⊢ φ \to seq 0 (+ G) \in dom ⇝$
Assertion	mertens	$⊢ φ \to seq 0 (+ H) ⇝ \sum_{j \in ℕ_{0}} A \sum_{k \in ℕ_{0}} B$

Proof

Step	Hyp	Ref	Expression
1		mertens.1	$⊢ (φ \land j \in ℕ_{0}) \to F (j) = A$
2		mertens.2	$⊢ (φ \land j \in ℕ_{0}) \to K (j) = \|A\|$
3		mertens.3	$⊢ (φ \land j \in ℕ_{0}) \to A \in ℂ$
4		mertens.4	$⊢ (φ \land k \in ℕ_{0}) \to G (k) = B$
5		mertens.5	$⊢ (φ \land k \in ℕ_{0}) \to B \in ℂ$
6		mertens.6	$⊢ (φ \land k \in ℕ_{0}) \to H (k) = \sum_{j = 0}^{k} A G (k - j)$
7		mertens.7	$⊢ φ \to seq 0 (+ K) \in dom ⇝$
8		mertens.8	$⊢ φ \to seq 0 (+ G) \in dom ⇝$
9		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
10		0zd	$⊢ φ \to 0 \in ℤ$
11		seqex	$⊢ seq 0 (+ H) \in V$
12	11	a1i	$⊢ φ \to seq 0 (+ H) \in V$
13		fzfid	$⊢ (φ \land k \in ℕ_{0}) \to (0 \dots k) \in Fin$
14		simpl	$⊢ (φ \land k \in ℕ_{0}) \to φ$
15		elfznn0	$⊢ j \in (0 \dots k) \to j \in ℕ_{0}$
16	14 15 3	syl2an	$⊢ ((φ \land k \in ℕ_{0}) \land j \in (0 \dots k)) \to A \in ℂ$
17		fveq2	$⊢ i = k - j \to G (i) = G (k - j)$
18	17	eleq1d	$⊢ i = k - j \to (G (i) \in ℂ \leftrightarrow G (k - j) \in ℂ)$
19	4 5	eqeltrd	$⊢ (φ \land k \in ℕ_{0}) \to G (k) \in ℂ$
20	19	ralrimiva	$⊢ φ \to \forall k \in ℕ_{0} G (k) \in ℂ$
21		fveq2	$⊢ k = i \to G (k) = G (i)$
22	21	eleq1d	$⊢ k = i \to (G (k) \in ℂ \leftrightarrow G (i) \in ℂ)$
23	22	cbvralvw	$⊢ \forall k \in ℕ_{0} G (k) \in ℂ \leftrightarrow \forall i \in ℕ_{0} G (i) \in ℂ$
24	20 23	sylib	$⊢ φ \to \forall i \in ℕ_{0} G (i) \in ℂ$
25	24	ad2antrr	$⊢ ((φ \land k \in ℕ_{0}) \land j \in (0 \dots k)) \to \forall i \in ℕ_{0} G (i) \in ℂ$
26		fznn0sub	$⊢ j \in (0 \dots k) \to k - j \in ℕ_{0}$
27	26	adantl	$⊢ ((φ \land k \in ℕ_{0}) \land j \in (0 \dots k)) \to k - j \in ℕ_{0}$
28	18 25 27	rspcdva	$⊢ ((φ \land k \in ℕ_{0}) \land j \in (0 \dots k)) \to G (k - j) \in ℂ$
29	16 28	mulcld	$⊢ ((φ \land k \in ℕ_{0}) \land j \in (0 \dots k)) \to A G (k - j) \in ℂ$
30	13 29	fsumcl	$⊢ (φ \land k \in ℕ_{0}) \to \sum_{j = 0}^{k} A G (k - j) \in ℂ$
31	6 30	eqeltrd	$⊢ (φ \land k \in ℕ_{0}) \to H (k) \in ℂ$
32	9 10 31	serf	$⊢ φ \to seq 0 (+ H) : ℕ_{0} ⟶ ℂ$
33	32	ffvelrnda	$⊢ (φ \land m \in ℕ_{0}) \to seq 0 (+ H) (m) \in ℂ$
34	1	adantlr	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ_{0}) \to F (j) = A$
35	2	adantlr	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ_{0}) \to K (j) = \|A\|$
36	3	adantlr	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ_{0}) \to A \in ℂ$
37	4	adantlr	$⊢ ((φ \land x \in ℝ^{+}) \land k \in ℕ_{0}) \to G (k) = B$
38	5	adantlr	$⊢ ((φ \land x \in ℝ^{+}) \land k \in ℕ_{0}) \to B \in ℂ$
39	6	adantlr	$⊢ ((φ \land x \in ℝ^{+}) \land k \in ℕ_{0}) \to H (k) = \sum_{j = 0}^{k} A G (k - j)$
40	7	adantr	$⊢ (φ \land x \in ℝ^{+}) \to seq 0 (+ K) \in dom ⇝$
41	8	adantr	$⊢ (φ \land x \in ℝ^{+}) \to seq 0 (+ G) \in dom ⇝$
42		simpr	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℝ^{+}$
43		fveq2	$⊢ l = k \to G (l) = G (k)$
44	43	cbvsumv	$⊢ \sum_{l \in ℤ_{\geq (i + 1)}} G (l) = \sum_{k \in ℤ_{\geq (i + 1)}} G (k)$
45		fvoveq1	$⊢ i = n \to ℤ_{\geq (i + 1)} = ℤ_{\geq (n + 1)}$
46	45	sumeq1d	$⊢ i = n \to \sum_{k \in ℤ_{\geq (i + 1)}} G (k) = \sum_{k \in ℤ_{\geq (n + 1)}} G (k)$
47	44 46	eqtrid	$⊢ i = n \to \sum_{l \in ℤ_{\geq (i + 1)}} G (l) = \sum_{k \in ℤ_{\geq (n + 1)}} G (k)$
48	47	fveq2d	$⊢ i = n \to \|\sum_{l \in ℤ_{\geq (i + 1)}} G (l)\| = \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\|$
49	48	eqeq2d	$⊢ i = n \to (u = \|\sum_{l \in ℤ_{\geq (i + 1)}} G (l)\| \leftrightarrow u = \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\|)$
50	49	cbvrexvw	$⊢ \exists i \in (0 \dots s - 1) u = \|\sum_{l \in ℤ_{\geq (i + 1)}} G (l)\| \leftrightarrow \exists n \in (0 \dots s - 1) u = \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\|$
51		eqeq1	$⊢ u = z \to (u = \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\| \leftrightarrow z = \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\|)$
52	51	rexbidv	$⊢ u = z \to (\exists n \in (0 \dots s - 1) u = \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\| \leftrightarrow \exists n \in (0 \dots s - 1) z = \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\|)$
53	50 52	syl5bb	$⊢ u = z \to (\exists i \in (0 \dots s - 1) u = \|\sum_{l \in ℤ_{\geq (i + 1)}} G (l)\| \leftrightarrow \exists n \in (0 \dots s - 1) z = \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\|)$
54	53	cbvabv	$⊢ \{u \| \exists i \in (0 \dots s - 1) u = \|\sum_{l \in ℤ_{\geq (i + 1)}} G (l)\|\} = \{z \| \exists n \in (0 \dots s - 1) z = \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\|\}$
55		fveq2	$⊢ i = j \to K (i) = K (j)$
56	55	cbvsumv	$⊢ \sum_{i \in ℕ_{0}} K (i) = \sum_{j \in ℕ_{0}} K (j)$
57	56	oveq1i	$⊢ \sum_{i \in ℕ_{0}} K (i) + 1 = \sum_{j \in ℕ_{0}} K (j) + 1$
58	57	oveq2i	$⊢ \frac{\frac{x}{2}}{\sum_{i \in ℕ_{0}} K (i) + 1} = \frac{\frac{x}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1}$
59	58	breq2i	$⊢ \|\sum_{i \in ℤ_{\geq (u + 1)}} G (i)\| < \frac{\frac{x}{2}}{\sum_{i \in ℕ_{0}} K (i) + 1} \leftrightarrow \|\sum_{i \in ℤ_{\geq (u + 1)}} G (i)\| < \frac{\frac{x}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1}$
60		fveq2	$⊢ i = k \to G (i) = G (k)$
61	60	cbvsumv	$⊢ \sum_{i \in ℤ_{\geq (u + 1)}} G (i) = \sum_{k \in ℤ_{\geq (u + 1)}} G (k)$
62		fvoveq1	$⊢ u = n \to ℤ_{\geq (u + 1)} = ℤ_{\geq (n + 1)}$
63	62	sumeq1d	$⊢ u = n \to \sum_{k \in ℤ_{\geq (u + 1)}} G (k) = \sum_{k \in ℤ_{\geq (n + 1)}} G (k)$
64	61 63	eqtrid	$⊢ u = n \to \sum_{i \in ℤ_{\geq (u + 1)}} G (i) = \sum_{k \in ℤ_{\geq (n + 1)}} G (k)$
65	64	fveq2d	$⊢ u = n \to \|\sum_{i \in ℤ_{\geq (u + 1)}} G (i)\| = \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\|$
66	65	breq1d	$⊢ u = n \to (\|\sum_{i \in ℤ_{\geq (u + 1)}} G (i)\| < \frac{\frac{x}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1} \leftrightarrow \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\| < \frac{\frac{x}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1})$
67	59 66	syl5bb	$⊢ u = n \to (\|\sum_{i \in ℤ_{\geq (u + 1)}} G (i)\| < \frac{\frac{x}{2}}{\sum_{i \in ℕ_{0}} K (i) + 1} \leftrightarrow \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\| < \frac{\frac{x}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1})$
68	67	cbvralvw	$⊢ \forall u \in ℤ_{\geq s} \|\sum_{i \in ℤ_{\geq (u + 1)}} G (i)\| < \frac{\frac{x}{2}}{\sum_{i \in ℕ_{0}} K (i) + 1} \leftrightarrow \forall n \in ℤ_{\geq s} \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\| < \frac{\frac{x}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1}$
69	68	anbi2i	$⊢ (s \in ℕ \land \forall u \in ℤ_{\geq s} \|\sum_{i \in ℤ_{\geq (u + 1)}} G (i)\| < \frac{\frac{x}{2}}{\sum_{i \in ℕ_{0}} K (i) + 1}) \leftrightarrow (s \in ℕ \land \forall n \in ℤ_{\geq s} \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\| < \frac{\frac{x}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1})$
70	34 35 36 37 38 39 40 41 42 54 69	mertenslem2	$⊢ (φ \land x \in ℝ^{+}) \to \exists y \in ℕ_{0} \forall m \in ℤ_{\geq y} \|\sum_{j = 0}^{m} A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\| < x$
71		eluznn0	$⊢ (y \in ℕ_{0} \land m \in ℤ_{\geq y}) \to m \in ℕ_{0}$
72		fzfid	$⊢ (φ \land m \in ℕ_{0}) \to (0 \dots m) \in Fin$
73		simpll	$⊢ ((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \to φ$
74		elfznn0	$⊢ j \in (0 \dots m) \to j \in ℕ_{0}$
75	74	adantl	$⊢ ((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \to j \in ℕ_{0}$
76	9 10 4 5 8	isumcl	$⊢ φ \to \sum_{k \in ℕ_{0}} B \in ℂ$
77	76	adantr	$⊢ (φ \land j \in ℕ_{0}) \to \sum_{k \in ℕ_{0}} B \in ℂ$
78	1 3	eqeltrd	$⊢ (φ \land j \in ℕ_{0}) \to F (j) \in ℂ$
79	77 78	mulcld	$⊢ (φ \land j \in ℕ_{0}) \to \sum_{k \in ℕ_{0}} B F (j) \in ℂ$
80	73 75 79	syl2anc	$⊢ ((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \to \sum_{k \in ℕ_{0}} B F (j) \in ℂ$
81		fzfid	$⊢ ((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \to (0 \dots m - j) \in Fin$
82		simplll	$⊢ (((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \land k \in (0 \dots m - j)) \to φ$
83	74	ad2antlr	$⊢ (((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \land k \in (0 \dots m - j)) \to j \in ℕ_{0}$
84	82 83 3	syl2anc	$⊢ (((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \land k \in (0 \dots m - j)) \to A \in ℂ$
85		elfznn0	$⊢ k \in (0 \dots m - j) \to k \in ℕ_{0}$
86	85	adantl	$⊢ (((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \land k \in (0 \dots m - j)) \to k \in ℕ_{0}$
87	82 86 19	syl2anc	$⊢ (((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \land k \in (0 \dots m - j)) \to G (k) \in ℂ$
88	84 87	mulcld	$⊢ (((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \land k \in (0 \dots m - j)) \to A G (k) \in ℂ$
89	81 88	fsumcl	$⊢ ((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \to \sum_{k = 0}^{m - j} A G (k) \in ℂ$
90	72 80 89	fsumsub	$⊢ (φ \land m \in ℕ_{0}) \to \sum_{j = 0}^{m} (\sum_{k \in ℕ_{0}} B F (j) - \sum_{k = 0}^{m - j} A G (k)) = \sum_{j = 0}^{m} \sum_{k \in ℕ_{0}} B F (j) - \sum_{j = 0}^{m} \sum_{k = 0}^{m - j} A G (k)$
91	73 75 3	syl2anc	$⊢ ((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \to A \in ℂ$
92	76	ad2antrr	$⊢ ((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \to \sum_{k \in ℕ_{0}} B \in ℂ$
93	81 87	fsumcl	$⊢ ((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \to \sum_{k = 0}^{m - j} G (k) \in ℂ$
94	91 92 93	subdid	$⊢ ((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \to A (\sum_{k \in ℕ_{0}} B - \sum_{k = 0}^{m - j} G (k)) = A \sum_{k \in ℕ_{0}} B - A \sum_{k = 0}^{m - j} G (k)$
95		eqid	$⊢ ℤ_{\geq (m - j + 1)} = ℤ_{\geq (m - j + 1)}$
96		fznn0sub	$⊢ j \in (0 \dots m) \to m - j \in ℕ_{0}$
97	96	adantl	$⊢ ((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \to m - j \in ℕ_{0}$
98		peano2nn0	$⊢ m - j \in ℕ_{0} \to m - j + 1 \in ℕ_{0}$
99	97 98	syl	$⊢ ((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \to m - j + 1 \in ℕ_{0}$
100	99	nn0zd	$⊢ ((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \to m - j + 1 \in ℤ$
101		simplll	$⊢ (((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \land k \in ℤ_{\geq (m - j + 1)}) \to φ$
102		eluznn0	$⊢ (m - j + 1 \in ℕ_{0} \land k \in ℤ_{\geq (m - j + 1)}) \to k \in ℕ_{0}$
103	99 102	sylan	$⊢ (((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \land k \in ℤ_{\geq (m - j + 1)}) \to k \in ℕ_{0}$
104	101 103 4	syl2anc	$⊢ (((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \land k \in ℤ_{\geq (m - j + 1)}) \to G (k) = B$
105	101 103 5	syl2anc	$⊢ (((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \land k \in ℤ_{\geq (m - j + 1)}) \to B \in ℂ$
106	8	ad2antrr	$⊢ ((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \to seq 0 (+ G) \in dom ⇝$
107	73 4	sylan	$⊢ (((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \land k \in ℕ_{0}) \to G (k) = B$
108	73 5	sylan	$⊢ (((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \land k \in ℕ_{0}) \to B \in ℂ$
109	107 108	eqeltrd	$⊢ (((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \land k \in ℕ_{0}) \to G (k) \in ℂ$
110	9 99 109	iserex	$⊢ ((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \to (seq 0 (+ G) \in dom ⇝ \leftrightarrow seq (m - j + 1) (+ G) \in dom ⇝)$
111	106 110	mpbid	$⊢ ((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \to seq (m - j + 1) (+ G) \in dom ⇝$
112	95 100 104 105 111	isumcl	$⊢ ((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \to \sum_{k \in ℤ_{\geq (m - j + 1)}} B \in ℂ$
113	9 95 99 107 108 106	isumsplit	$⊢ ((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \to \sum_{k \in ℕ_{0}} B = \sum_{k = 0}^{(m - j) + 1 - 1} B + \sum_{k \in ℤ_{\geq (m - j + 1)}} B$
114	97	nn0cnd	$⊢ ((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \to m - j \in ℂ$
115		ax-1cn	$⊢ 1 \in ℂ$
116		pncan	$⊢ (m - j \in ℂ \land 1 \in ℂ) \to (m - j) + 1 - 1 = m - j$
117	114 115 116	sylancl	$⊢ ((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \to (m - j) + 1 - 1 = m - j$
118	117	oveq2d	$⊢ ((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \to (0 \dots (m - j) + 1 - 1) = (0 \dots m - j)$
119	118	sumeq1d	$⊢ ((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \to \sum_{k = 0}^{(m - j) + 1 - 1} B = \sum_{k = 0}^{m - j} B$
120	82 86 4	syl2anc	$⊢ (((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \land k \in (0 \dots m - j)) \to G (k) = B$
121	120	sumeq2dv	$⊢ ((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \to \sum_{k = 0}^{m - j} G (k) = \sum_{k = 0}^{m - j} B$
122	119 121	eqtr4d	$⊢ ((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \to \sum_{k = 0}^{(m - j) + 1 - 1} B = \sum_{k = 0}^{m - j} G (k)$
123	122	oveq1d	$⊢ ((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \to \sum_{k = 0}^{(m - j) + 1 - 1} B + \sum_{k \in ℤ_{\geq (m - j + 1)}} B = \sum_{k = 0}^{m - j} G (k) + \sum_{k \in ℤ_{\geq (m - j + 1)}} B$
124	113 123	eqtrd	$⊢ ((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \to \sum_{k \in ℕ_{0}} B = \sum_{k = 0}^{m - j} G (k) + \sum_{k \in ℤ_{\geq (m - j + 1)}} B$
125	93 112 124	mvrladdd	$⊢ ((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \to \sum_{k \in ℕ_{0}} B - \sum_{k = 0}^{m - j} G (k) = \sum_{k \in ℤ_{\geq (m - j + 1)}} B$
126	125	oveq2d	$⊢ ((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \to A (\sum_{k \in ℕ_{0}} B - \sum_{k = 0}^{m - j} G (k)) = A \sum_{k \in ℤ_{\geq (m - j + 1)}} B$
127	3 77	mulcomd	$⊢ (φ \land j \in ℕ_{0}) \to A \sum_{k \in ℕ_{0}} B = \sum_{k \in ℕ_{0}} B A$
128	1	oveq2d	$⊢ (φ \land j \in ℕ_{0}) \to \sum_{k \in ℕ_{0}} B F (j) = \sum_{k \in ℕ_{0}} B A$
129	127 128	eqtr4d	$⊢ (φ \land j \in ℕ_{0}) \to A \sum_{k \in ℕ_{0}} B = \sum_{k \in ℕ_{0}} B F (j)$
130	73 75 129	syl2anc	$⊢ ((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \to A \sum_{k \in ℕ_{0}} B = \sum_{k \in ℕ_{0}} B F (j)$
131	81 91 87	fsummulc2	$⊢ ((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \to A \sum_{k = 0}^{m - j} G (k) = \sum_{k = 0}^{m - j} A G (k)$
132	130 131	oveq12d	$⊢ ((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \to A \sum_{k \in ℕ_{0}} B - A \sum_{k = 0}^{m - j} G (k) = \sum_{k \in ℕ_{0}} B F (j) - \sum_{k = 0}^{m - j} A G (k)$
133	94 126 132	3eqtr3rd	$⊢ ((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \to \sum_{k \in ℕ_{0}} B F (j) - \sum_{k = 0}^{m - j} A G (k) = A \sum_{k \in ℤ_{\geq (m - j + 1)}} B$
134	133	sumeq2dv	$⊢ (φ \land m \in ℕ_{0}) \to \sum_{j = 0}^{m} (\sum_{k \in ℕ_{0}} B F (j) - \sum_{k = 0}^{m - j} A G (k)) = \sum_{j = 0}^{m} A \sum_{k \in ℤ_{\geq (m - j + 1)}} B$
135		fveq2	$⊢ n = j \to F (n) = F (j)$
136	135	oveq2d	$⊢ n = j \to \sum_{k \in ℕ_{0}} B F (n) = \sum_{k \in ℕ_{0}} B F (j)$
137		eqid	$⊢ (n \in ℕ_{0} ⟼ \sum_{k \in ℕ_{0}} B F (n)) = (n \in ℕ_{0} ⟼ \sum_{k \in ℕ_{0}} B F (n))$
138		ovex	$⊢ \sum_{k \in ℕ_{0}} B F (j) \in V$
139	136 137 138	fvmpt	$⊢ j \in ℕ_{0} \to (n \in ℕ_{0} ⟼ \sum_{k \in ℕ_{0}} B F (n)) (j) = \sum_{k \in ℕ_{0}} B F (j)$
140	75 139	syl	$⊢ ((φ \land m \in ℕ_{0}) \land j \in (0 \dots m)) \to (n \in ℕ_{0} ⟼ \sum_{k \in ℕ_{0}} B F (n)) (j) = \sum_{k \in ℕ_{0}} B F (j)$
141		simpr	$⊢ (φ \land m \in ℕ_{0}) \to m \in ℕ_{0}$
142	141 9	eleqtrdi	$⊢ (φ \land m \in ℕ_{0}) \to m \in ℤ_{\geq 0}$
143	140 142 80	fsumser	$⊢ (φ \land m \in ℕ_{0}) \to \sum_{j = 0}^{m} \sum_{k \in ℕ_{0}} B F (j) = seq 0 (+ (n \in ℕ_{0} ⟼ \sum_{k \in ℕ_{0}} B F (n))) (m)$
144		fveq2	$⊢ n = k \to G (n) = G (k)$
145	144	oveq2d	$⊢ n = k \to A G (n) = A G (k)$
146		fveq2	$⊢ n = k - j \to G (n) = G (k - j)$
147	146	oveq2d	$⊢ n = k - j \to A G (n) = A G (k - j)$
148	88	anasss	$⊢ ((φ \land m \in ℕ_{0}) \land (j \in (0 \dots m) \land k \in (0 \dots m - j))) \to A G (k) \in ℂ$
149	145 147 148	fsum0diag2	$⊢ (φ \land m \in ℕ_{0}) \to \sum_{j = 0}^{m} \sum_{k = 0}^{m - j} A G (k) = \sum_{k = 0}^{m} \sum_{j = 0}^{k} A G (k - j)$
150		simpll	$⊢ ((φ \land m \in ℕ_{0}) \land k \in (0 \dots m)) \to φ$
151		elfznn0	$⊢ k \in (0 \dots m) \to k \in ℕ_{0}$
152	151	adantl	$⊢ ((φ \land m \in ℕ_{0}) \land k \in (0 \dots m)) \to k \in ℕ_{0}$
153	150 152 6	syl2anc	$⊢ ((φ \land m \in ℕ_{0}) \land k \in (0 \dots m)) \to H (k) = \sum_{j = 0}^{k} A G (k - j)$
154	150 152 30	syl2anc	$⊢ ((φ \land m \in ℕ_{0}) \land k \in (0 \dots m)) \to \sum_{j = 0}^{k} A G (k - j) \in ℂ$
155	153 142 154	fsumser	$⊢ (φ \land m \in ℕ_{0}) \to \sum_{k = 0}^{m} \sum_{j = 0}^{k} A G (k - j) = seq 0 (+ H) (m)$
156	149 155	eqtrd	$⊢ (φ \land m \in ℕ_{0}) \to \sum_{j = 0}^{m} \sum_{k = 0}^{m - j} A G (k) = seq 0 (+ H) (m)$
157	143 156	oveq12d	$⊢ (φ \land m \in ℕ_{0}) \to \sum_{j = 0}^{m} \sum_{k \in ℕ_{0}} B F (j) - \sum_{j = 0}^{m} \sum_{k = 0}^{m - j} A G (k) = seq 0 (+ (n \in ℕ_{0} ⟼ \sum_{k \in ℕ_{0}} B F (n))) (m) - seq 0 (+ H) (m)$
158	90 134 157	3eqtr3rd	$⊢ (φ \land m \in ℕ_{0}) \to seq 0 (+ (n \in ℕ_{0} ⟼ \sum_{k \in ℕ_{0}} B F (n))) (m) - seq 0 (+ H) (m) = \sum_{j = 0}^{m} A \sum_{k \in ℤ_{\geq (m - j + 1)}} B$
159	158	fveq2d	$⊢ (φ \land m \in ℕ_{0}) \to \|seq 0 (+ (n \in ℕ_{0} ⟼ \sum_{k \in ℕ_{0}} B F (n))) (m) - seq 0 (+ H) (m)\| = \|\sum_{j = 0}^{m} A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\|$
160	159	breq1d	$⊢ (φ \land m \in ℕ_{0}) \to (\|seq 0 (+ (n \in ℕ_{0} ⟼ \sum_{k \in ℕ_{0}} B F (n))) (m) - seq 0 (+ H) (m)\| < x \leftrightarrow \|\sum_{j = 0}^{m} A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\| < x)$
161	71 160	sylan2	$⊢ (φ \land (y \in ℕ_{0} \land m \in ℤ_{\geq y})) \to (\|seq 0 (+ (n \in ℕ_{0} ⟼ \sum_{k \in ℕ_{0}} B F (n))) (m) - seq 0 (+ H) (m)\| < x \leftrightarrow \|\sum_{j = 0}^{m} A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\| < x)$
162	161	anassrs	$⊢ ((φ \land y \in ℕ_{0}) \land m \in ℤ_{\geq y}) \to (\|seq 0 (+ (n \in ℕ_{0} ⟼ \sum_{k \in ℕ_{0}} B F (n))) (m) - seq 0 (+ H) (m)\| < x \leftrightarrow \|\sum_{j = 0}^{m} A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\| < x)$
163	162	ralbidva	$⊢ (φ \land y \in ℕ_{0}) \to (\forall m \in ℤ_{\geq y} \|seq 0 (+ (n \in ℕ_{0} ⟼ \sum_{k \in ℕ_{0}} B F (n))) (m) - seq 0 (+ H) (m)\| < x \leftrightarrow \forall m \in ℤ_{\geq y} \|\sum_{j = 0}^{m} A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\| < x)$
164	163	rexbidva	$⊢ φ \to (\exists y \in ℕ_{0} \forall m \in ℤ_{\geq y} \|seq 0 (+ (n \in ℕ_{0} ⟼ \sum_{k \in ℕ_{0}} B F (n))) (m) - seq 0 (+ H) (m)\| < x \leftrightarrow \exists y \in ℕ_{0} \forall m \in ℤ_{\geq y} \|\sum_{j = 0}^{m} A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\| < x)$
165	164	adantr	$⊢ (φ \land x \in ℝ^{+}) \to (\exists y \in ℕ_{0} \forall m \in ℤ_{\geq y} \|seq 0 (+ (n \in ℕ_{0} ⟼ \sum_{k \in ℕ_{0}} B F (n))) (m) - seq 0 (+ H) (m)\| < x \leftrightarrow \exists y \in ℕ_{0} \forall m \in ℤ_{\geq y} \|\sum_{j = 0}^{m} A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\| < x)$
166	70 165	mpbird	$⊢ (φ \land x \in ℝ^{+}) \to \exists y \in ℕ_{0} \forall m \in ℤ_{\geq y} \|seq 0 (+ (n \in ℕ_{0} ⟼ \sum_{k \in ℕ_{0}} B F (n))) (m) - seq 0 (+ H) (m)\| < x$
167	166	ralrimiva	$⊢ φ \to \forall x \in ℝ^{+} \exists y \in ℕ_{0} \forall m \in ℤ_{\geq y} \|seq 0 (+ (n \in ℕ_{0} ⟼ \sum_{k \in ℕ_{0}} B F (n))) (m) - seq 0 (+ H) (m)\| < x$
168	1	fveq2d	$⊢ (φ \land j \in ℕ_{0}) \to \|F (j)\| = \|A\|$
169	2 168	eqtr4d	$⊢ (φ \land j \in ℕ_{0}) \to K (j) = \|F (j)\|$
170	9 10 169 78 7	abscvgcvg	$⊢ φ \to seq 0 (+ F) \in dom ⇝$
171	9 10 1 3 170	isumclim2	$⊢ φ \to seq 0 (+ F) ⇝ \sum_{j \in ℕ_{0}} A$
172	78	ralrimiva	$⊢ φ \to \forall j \in ℕ_{0} F (j) \in ℂ$
173		fveq2	$⊢ j = m \to F (j) = F (m)$
174	173	eleq1d	$⊢ j = m \to (F (j) \in ℂ \leftrightarrow F (m) \in ℂ)$
175	174	rspccva	$⊢ (\forall j \in ℕ_{0} F (j) \in ℂ \land m \in ℕ_{0}) \to F (m) \in ℂ$
176	172 175	sylan	$⊢ (φ \land m \in ℕ_{0}) \to F (m) \in ℂ$
177		fveq2	$⊢ n = m \to F (n) = F (m)$
178	177	oveq2d	$⊢ n = m \to \sum_{k \in ℕ_{0}} B F (n) = \sum_{k \in ℕ_{0}} B F (m)$
179		ovex	$⊢ \sum_{k \in ℕ_{0}} B F (m) \in V$
180	178 137 179	fvmpt	$⊢ m \in ℕ_{0} \to (n \in ℕ_{0} ⟼ \sum_{k \in ℕ_{0}} B F (n)) (m) = \sum_{k \in ℕ_{0}} B F (m)$
181	180	adantl	$⊢ (φ \land m \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ \sum_{k \in ℕ_{0}} B F (n)) (m) = \sum_{k \in ℕ_{0}} B F (m)$
182	9 10 76 171 176 181	isermulc2	$⊢ φ \to seq 0 (+ (n \in ℕ_{0} ⟼ \sum_{k \in ℕ_{0}} B F (n))) ⇝ \sum_{k \in ℕ_{0}} B \sum_{j \in ℕ_{0}} A$
183	9 10 1 3 170	isumcl	$⊢ φ \to \sum_{j \in ℕ_{0}} A \in ℂ$
184	76 183	mulcomd	$⊢ φ \to \sum_{k \in ℕ_{0}} B \sum_{j \in ℕ_{0}} A = \sum_{j \in ℕ_{0}} A \sum_{k \in ℕ_{0}} B$
185	182 184	breqtrd	$⊢ φ \to seq 0 (+ (n \in ℕ_{0} ⟼ \sum_{k \in ℕ_{0}} B F (n))) ⇝ \sum_{j \in ℕ_{0}} A \sum_{k \in ℕ_{0}} B$
186	9 10 12 33 167 185	2clim	$⊢ φ \to seq 0 (+ H) ⇝ \sum_{j \in ℕ_{0}} A \sum_{k \in ℕ_{0}} B$

Metamath Proof Explorer

Theorem mertens

Proof