mertenslem2

	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 ⇝$
	mertens.9	$⊢ φ \to E \in ℝ^{+}$
	mertens.10	$⊢ T = \{z \| \exists n \in (0 \dots s - 1) z = \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\|\}$
	mertens.11	$⊢ ψ \leftrightarrow (s \in ℕ \land \forall n \in ℤ_{\geq s} \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\| < \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1})$
Assertion	mertenslem2	$⊢ φ \to \exists y \in ℕ_{0} \forall m \in ℤ_{\geq y} \|\sum_{j = 0}^{m} A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\| < E$

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		mertens.9	$⊢ φ \to E \in ℝ^{+}$
10		mertens.10	$⊢ T = \{z \| \exists n \in (0 \dots s - 1) z = \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\|\}$
11		mertens.11	$⊢ ψ \leftrightarrow (s \in ℕ \land \forall n \in ℤ_{\geq s} \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\| < \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1})$
12		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
13		1zzd	$⊢ φ \to 1 \in ℤ$
14	9	rphalfcld	$⊢ φ \to \frac{E}{2} \in ℝ^{+}$
15		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
16		0zd	$⊢ φ \to 0 \in ℤ$
17		eqidd	$⊢ (φ \land j \in ℕ_{0}) \to K (j) = K (j)$
18	3	abscld	$⊢ (φ \land j \in ℕ_{0}) \to \|A\| \in ℝ$
19	2 18	eqeltrd	$⊢ (φ \land j \in ℕ_{0}) \to K (j) \in ℝ$
20	15 16 17 19 7	isumrecl	$⊢ φ \to \sum_{j \in ℕ_{0}} K (j) \in ℝ$
21	3	absge0d	$⊢ (φ \land j \in ℕ_{0}) \to 0 \leq \|A\|$
22	21 2	breqtrrd	$⊢ (φ \land j \in ℕ_{0}) \to 0 \leq K (j)$
23	15 16 17 19 7 22	isumge0	$⊢ φ \to 0 \leq \sum_{j \in ℕ_{0}} K (j)$
24	20 23	ge0p1rpd	$⊢ φ \to \sum_{j \in ℕ_{0}} K (j) + 1 \in ℝ^{+}$
25	14 24	rpdivcld	$⊢ φ \to \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1} \in ℝ^{+}$
26		eqidd	$⊢ (φ \land m \in ℕ) \to seq 0 (+ G) (m) = seq 0 (+ G) (m)$
27	15 16 4 5 8	isumclim2	$⊢ φ \to seq 0 (+ G) ⇝ \sum_{k \in ℕ_{0}} B$
28	12 13 25 26 27	climi2	$⊢ φ \to \exists s \in ℕ \forall m \in ℤ_{\geq s} \|seq 0 (+ G) (m) - \sum_{k \in ℕ_{0}} B\| < \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1}$
29		eluznn	$⊢ (s \in ℕ \land m \in ℤ_{\geq s}) \to m \in ℕ$
30	4 5	eqeltrd	$⊢ (φ \land k \in ℕ_{0}) \to G (k) \in ℂ$
31	15 16 30	serf	$⊢ φ \to seq 0 (+ G) : ℕ_{0} ⟶ ℂ$
32		nnnn0	$⊢ m \in ℕ \to m \in ℕ_{0}$
33		ffvelrn	$⊢ (seq 0 (+ G) : ℕ_{0} ⟶ ℂ \land m \in ℕ_{0}) \to seq 0 (+ G) (m) \in ℂ$
34	31 32 33	syl2an	$⊢ (φ \land m \in ℕ) \to seq 0 (+ G) (m) \in ℂ$
35	15 16 4 5 8	isumcl	$⊢ φ \to \sum_{k \in ℕ_{0}} B \in ℂ$
36	35	adantr	$⊢ (φ \land m \in ℕ) \to \sum_{k \in ℕ_{0}} B \in ℂ$
37	34 36	abssubd	$⊢ (φ \land m \in ℕ) \to \|seq 0 (+ G) (m) - \sum_{k \in ℕ_{0}} B\| = \|\sum_{k \in ℕ_{0}} B - seq 0 (+ G) (m)\|$
38		eqid	$⊢ ℤ_{\geq (m + 1)} = ℤ_{\geq (m + 1)}$
39	32	adantl	$⊢ (φ \land m \in ℕ) \to m \in ℕ_{0}$
40		peano2nn0	$⊢ m \in ℕ_{0} \to m + 1 \in ℕ_{0}$
41	39 40	syl	$⊢ (φ \land m \in ℕ) \to m + 1 \in ℕ_{0}$
42	41	nn0zd	$⊢ (φ \land m \in ℕ) \to m + 1 \in ℤ$
43		simpll	$⊢ ((φ \land m \in ℕ) \land k \in ℤ_{\geq (m + 1)}) \to φ$
44		eluznn0	$⊢ (m + 1 \in ℕ_{0} \land k \in ℤ_{\geq (m + 1)}) \to k \in ℕ_{0}$
45	41 44	sylan	$⊢ ((φ \land m \in ℕ) \land k \in ℤ_{\geq (m + 1)}) \to k \in ℕ_{0}$
46	43 45 4	syl2anc	$⊢ ((φ \land m \in ℕ) \land k \in ℤ_{\geq (m + 1)}) \to G (k) = B$
47	43 45 5	syl2anc	$⊢ ((φ \land m \in ℕ) \land k \in ℤ_{\geq (m + 1)}) \to B \in ℂ$
48	8	adantr	$⊢ (φ \land m \in ℕ) \to seq 0 (+ G) \in dom ⇝$
49	30	adantlr	$⊢ ((φ \land m \in ℕ) \land k \in ℕ_{0}) \to G (k) \in ℂ$
50	15 41 49	iserex	$⊢ (φ \land m \in ℕ) \to (seq 0 (+ G) \in dom ⇝ \leftrightarrow seq (m + 1) (+ G) \in dom ⇝)$
51	48 50	mpbid	$⊢ (φ \land m \in ℕ) \to seq (m + 1) (+ G) \in dom ⇝$
52	38 42 46 47 51	isumcl	$⊢ (φ \land m \in ℕ) \to \sum_{k \in ℤ_{\geq (m + 1)}} B \in ℂ$
53	34 52	pncan2d	$⊢ (φ \land m \in ℕ) \to seq 0 (+ G) (m) + \sum_{k \in ℤ_{\geq (m + 1)}} B - seq 0 (+ G) (m) = \sum_{k \in ℤ_{\geq (m + 1)}} B$
54	4	adantlr	$⊢ ((φ \land m \in ℕ) \land k \in ℕ_{0}) \to G (k) = B$
55	5	adantlr	$⊢ ((φ \land m \in ℕ) \land k \in ℕ_{0}) \to B \in ℂ$
56	15 38 41 54 55 48	isumsplit	$⊢ (φ \land m \in ℕ) \to \sum_{k \in ℕ_{0}} B = \sum_{k = 0}^{m + 1 - 1} B + \sum_{k \in ℤ_{\geq (m + 1)}} B$
57		nncn	$⊢ m \in ℕ \to m \in ℂ$
58	57	adantl	$⊢ (φ \land m \in ℕ) \to m \in ℂ$
59		ax-1cn	$⊢ 1 \in ℂ$
60		pncan	$⊢ (m \in ℂ \land 1 \in ℂ) \to m + 1 - 1 = m$
61	58 59 60	sylancl	$⊢ (φ \land m \in ℕ) \to m + 1 - 1 = m$
62	61	oveq2d	$⊢ (φ \land m \in ℕ) \to (0 \dots m + 1 - 1) = (0 \dots m)$
63	62	sumeq1d	$⊢ (φ \land m \in ℕ) \to \sum_{k = 0}^{m + 1 - 1} B = \sum_{k = 0}^{m} B$
64		simpl	$⊢ (φ \land m \in ℕ) \to φ$
65		elfznn0	$⊢ k \in (0 \dots m) \to k \in ℕ_{0}$
66	64 65 4	syl2an	$⊢ ((φ \land m \in ℕ) \land k \in (0 \dots m)) \to G (k) = B$
67	39 15	eleqtrdi	$⊢ (φ \land m \in ℕ) \to m \in ℤ_{\geq 0}$
68	64 65 5	syl2an	$⊢ ((φ \land m \in ℕ) \land k \in (0 \dots m)) \to B \in ℂ$
69	66 67 68	fsumser	$⊢ (φ \land m \in ℕ) \to \sum_{k = 0}^{m} B = seq 0 (+ G) (m)$
70	63 69	eqtrd	$⊢ (φ \land m \in ℕ) \to \sum_{k = 0}^{m + 1 - 1} B = seq 0 (+ G) (m)$
71	70	oveq1d	$⊢ (φ \land m \in ℕ) \to \sum_{k = 0}^{m + 1 - 1} B + \sum_{k \in ℤ_{\geq (m + 1)}} B = seq 0 (+ G) (m) + \sum_{k \in ℤ_{\geq (m + 1)}} B$
72	56 71	eqtrd	$⊢ (φ \land m \in ℕ) \to \sum_{k \in ℕ_{0}} B = seq 0 (+ G) (m) + \sum_{k \in ℤ_{\geq (m + 1)}} B$
73	72	oveq1d	$⊢ (φ \land m \in ℕ) \to \sum_{k \in ℕ_{0}} B - seq 0 (+ G) (m) = seq 0 (+ G) (m) + \sum_{k \in ℤ_{\geq (m + 1)}} B - seq 0 (+ G) (m)$
74	46	sumeq2dv	$⊢ (φ \land m \in ℕ) \to \sum_{k \in ℤ_{\geq (m + 1)}} G (k) = \sum_{k \in ℤ_{\geq (m + 1)}} B$
75	53 73 74	3eqtr4d	$⊢ (φ \land m \in ℕ) \to \sum_{k \in ℕ_{0}} B - seq 0 (+ G) (m) = \sum_{k \in ℤ_{\geq (m + 1)}} G (k)$
76	75	fveq2d	$⊢ (φ \land m \in ℕ) \to \|\sum_{k \in ℕ_{0}} B - seq 0 (+ G) (m)\| = \|\sum_{k \in ℤ_{\geq (m + 1)}} G (k)\|$
77	37 76	eqtrd	$⊢ (φ \land m \in ℕ) \to \|seq 0 (+ G) (m) - \sum_{k \in ℕ_{0}} B\| = \|\sum_{k \in ℤ_{\geq (m + 1)}} G (k)\|$
78	77	breq1d	$⊢ (φ \land m \in ℕ) \to (\|seq 0 (+ G) (m) - \sum_{k \in ℕ_{0}} B\| < \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1} \leftrightarrow \|\sum_{k \in ℤ_{\geq (m + 1)}} G (k)\| < \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1})$
79	29 78	sylan2	$⊢ (φ \land (s \in ℕ \land m \in ℤ_{\geq s})) \to (\|seq 0 (+ G) (m) - \sum_{k \in ℕ_{0}} B\| < \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1} \leftrightarrow \|\sum_{k \in ℤ_{\geq (m + 1)}} G (k)\| < \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1})$
80	79	anassrs	$⊢ ((φ \land s \in ℕ) \land m \in ℤ_{\geq s}) \to (\|seq 0 (+ G) (m) - \sum_{k \in ℕ_{0}} B\| < \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1} \leftrightarrow \|\sum_{k \in ℤ_{\geq (m + 1)}} G (k)\| < \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1})$
81	80	ralbidva	$⊢ (φ \land s \in ℕ) \to (\forall m \in ℤ_{\geq s} \|seq 0 (+ G) (m) - \sum_{k \in ℕ_{0}} B\| < \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1} \leftrightarrow \forall m \in ℤ_{\geq s} \|\sum_{k \in ℤ_{\geq (m + 1)}} G (k)\| < \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1})$
82		fvoveq1	$⊢ m = n \to ℤ_{\geq (m + 1)} = ℤ_{\geq (n + 1)}$
83	82	sumeq1d	$⊢ m = n \to \sum_{k \in ℤ_{\geq (m + 1)}} G (k) = \sum_{k \in ℤ_{\geq (n + 1)}} G (k)$
84	83	fveq2d	$⊢ m = n \to \|\sum_{k \in ℤ_{\geq (m + 1)}} G (k)\| = \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\|$
85	84	breq1d	$⊢ m = n \to (\|\sum_{k \in ℤ_{\geq (m + 1)}} G (k)\| < \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1} \leftrightarrow \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\| < \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1})$
86	85	cbvralvw	$⊢ \forall m \in ℤ_{\geq s} \|\sum_{k \in ℤ_{\geq (m + 1)}} G (k)\| < \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1} \leftrightarrow \forall n \in ℤ_{\geq s} \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\| < \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1}$
87	81 86	bitrdi	$⊢ (φ \land s \in ℕ) \to (\forall m \in ℤ_{\geq s} \|seq 0 (+ G) (m) - \sum_{k \in ℕ_{0}} B\| < \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1} \leftrightarrow \forall n \in ℤ_{\geq s} \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\| < \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1})$
88		0zd	$⊢ (φ \land ψ) \to 0 \in ℤ$
89	14	adantr	$⊢ (φ \land ψ) \to \frac{E}{2} \in ℝ^{+}$
90	11	simplbi	$⊢ ψ \to s \in ℕ$
91	90	adantl	$⊢ (φ \land ψ) \to s \in ℕ$
92	91	nnrpd	$⊢ (φ \land ψ) \to s \in ℝ^{+}$
93	89 92	rpdivcld	$⊢ (φ \land ψ) \to \frac{\frac{E}{2}}{s} \in ℝ^{+}$
94		eqid	$⊢ ℤ_{\geq (n + 1)} = ℤ_{\geq (n + 1)}$
95		elfznn0	$⊢ n \in (0 \dots s - 1) \to n \in ℕ_{0}$
96	95	adantl	$⊢ ((φ \land ψ) \land n \in (0 \dots s - 1)) \to n \in ℕ_{0}$
97		peano2nn0	$⊢ n \in ℕ_{0} \to n + 1 \in ℕ_{0}$
98	96 97	syl	$⊢ ((φ \land ψ) \land n \in (0 \dots s - 1)) \to n + 1 \in ℕ_{0}$
99	98	nn0zd	$⊢ ((φ \land ψ) \land n \in (0 \dots s - 1)) \to n + 1 \in ℤ$
100		eqidd	$⊢ (((φ \land ψ) \land n \in (0 \dots s - 1)) \land k \in ℤ_{\geq (n + 1)}) \to G (k) = G (k)$
101		simplll	$⊢ (((φ \land ψ) \land n \in (0 \dots s - 1)) \land k \in ℤ_{\geq (n + 1)}) \to φ$
102		eluznn0	$⊢ (n + 1 \in ℕ_{0} \land k \in ℤ_{\geq (n + 1)}) \to k \in ℕ_{0}$
103	98 102	sylan	$⊢ (((φ \land ψ) \land n \in (0 \dots s - 1)) \land k \in ℤ_{\geq (n + 1)}) \to k \in ℕ_{0}$
104	101 103 30	syl2anc	$⊢ (((φ \land ψ) \land n \in (0 \dots s - 1)) \land k \in ℤ_{\geq (n + 1)}) \to G (k) \in ℂ$
105	8	ad2antrr	$⊢ ((φ \land ψ) \land n \in (0 \dots s - 1)) \to seq 0 (+ G) \in dom ⇝$
106	30	ad4ant14	$⊢ (((φ \land ψ) \land n \in (0 \dots s - 1)) \land k \in ℕ_{0}) \to G (k) \in ℂ$
107	15 98 106	iserex	$⊢ ((φ \land ψ) \land n \in (0 \dots s - 1)) \to (seq 0 (+ G) \in dom ⇝ \leftrightarrow seq (n + 1) (+ G) \in dom ⇝)$
108	105 107	mpbid	$⊢ ((φ \land ψ) \land n \in (0 \dots s - 1)) \to seq (n + 1) (+ G) \in dom ⇝$
109	94 99 100 104 108	isumcl	$⊢ ((φ \land ψ) \land n \in (0 \dots s - 1)) \to \sum_{k \in ℤ_{\geq (n + 1)}} G (k) \in ℂ$
110	109	abscld	$⊢ ((φ \land ψ) \land n \in (0 \dots s - 1)) \to \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\| \in ℝ$
111		eleq1a	$⊢ \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\| \in ℝ \to (z = \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\| \to z \in ℝ)$
112	110 111	syl	$⊢ ((φ \land ψ) \land n \in (0 \dots s - 1)) \to (z = \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\| \to z \in ℝ)$
113	112	rexlimdva	$⊢ (φ \land ψ) \to (\exists n \in (0 \dots s - 1) z = \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\| \to z \in ℝ)$
114	113	abssdv	$⊢ (φ \land ψ) \to \{z \| \exists n \in (0 \dots s - 1) z = \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\|\} \subseteq ℝ$
115	10 114	eqsstrid	$⊢ (φ \land ψ) \to T \subseteq ℝ$
116		fzfid	$⊢ (φ \land ψ) \to (0 \dots s - 1) \in Fin$
117		abrexfi	$⊢ (0 \dots s - 1) \in Fin \to \{z \| \exists n \in (0 \dots s - 1) z = \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\|\} \in Fin$
118	116 117	syl	$⊢ (φ \land ψ) \to \{z \| \exists n \in (0 \dots s - 1) z = \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\|\} \in Fin$
119	10 118	eqeltrid	$⊢ (φ \land ψ) \to T \in Fin$
120		nnm1nn0	$⊢ s \in ℕ \to s - 1 \in ℕ_{0}$
121	91 120	syl	$⊢ (φ \land ψ) \to s - 1 \in ℕ_{0}$
122	121 15	eleqtrdi	$⊢ (φ \land ψ) \to s - 1 \in ℤ_{\geq 0}$
123		eluzfz1	$⊢ s - 1 \in ℤ_{\geq 0} \to 0 \in (0 \dots s - 1)$
124	122 123	syl	$⊢ (φ \land ψ) \to 0 \in (0 \dots s - 1)$
125		nnnn0	$⊢ k \in ℕ \to k \in ℕ_{0}$
126	125 4	sylan2	$⊢ (φ \land k \in ℕ) \to G (k) = B$
127	126	sumeq2dv	$⊢ φ \to \sum_{k \in ℕ} G (k) = \sum_{k \in ℕ} B$
128	127	adantr	$⊢ (φ \land ψ) \to \sum_{k \in ℕ} G (k) = \sum_{k \in ℕ} B$
129	128	fveq2d	$⊢ (φ \land ψ) \to \|\sum_{k \in ℕ} G (k)\| = \|\sum_{k \in ℕ} B\|$
130	129	eqcomd	$⊢ (φ \land ψ) \to \|\sum_{k \in ℕ} B\| = \|\sum_{k \in ℕ} G (k)\|$
131		fv0p1e1	$⊢ n = 0 \to ℤ_{\geq (n + 1)} = ℤ_{\geq 1}$
132	131 12	eqtr4di	$⊢ n = 0 \to ℤ_{\geq (n + 1)} = ℕ$
133	132	sumeq1d	$⊢ n = 0 \to \sum_{k \in ℤ_{\geq (n + 1)}} G (k) = \sum_{k \in ℕ} G (k)$
134	133	fveq2d	$⊢ n = 0 \to \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\| = \|\sum_{k \in ℕ} G (k)\|$
135	134	rspceeqv	$⊢ (0 \in (0 \dots s - 1) \land \|\sum_{k \in ℕ} B\| = \|\sum_{k \in ℕ} G (k)\|) \to \exists n \in (0 \dots s - 1) \|\sum_{k \in ℕ} B\| = \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\|$
136	124 130 135	syl2anc	$⊢ (φ \land ψ) \to \exists n \in (0 \dots s - 1) \|\sum_{k \in ℕ} B\| = \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\|$
137		fvex	$⊢ \|\sum_{k \in ℕ} B\| \in V$
138		eqeq1	$⊢ z = \|\sum_{k \in ℕ} B\| \to (z = \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\| \leftrightarrow \|\sum_{k \in ℕ} B\| = \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\|)$
139	138	rexbidv	$⊢ z = \|\sum_{k \in ℕ} B\| \to (\exists n \in (0 \dots s - 1) z = \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\| \leftrightarrow \exists n \in (0 \dots s - 1) \|\sum_{k \in ℕ} B\| = \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\|)$
140	137 139 10	elab2	$⊢ \|\sum_{k \in ℕ} B\| \in T \leftrightarrow \exists n \in (0 \dots s - 1) \|\sum_{k \in ℕ} B\| = \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\|$
141	136 140	sylibr	$⊢ (φ \land ψ) \to \|\sum_{k \in ℕ} B\| \in T$
142	141	ne0d	$⊢ (φ \land ψ) \to T \neq \emptyset$
143		ltso	$⊢ < Or ℝ$
144		fisupcl	$⊢ (< Or ℝ \land (T \in Fin \land T \neq \emptyset \land T \subseteq ℝ)) \to sup (T ℝ <) \in T$
145	143 144	mpan	$⊢ (T \in Fin \land T \neq \emptyset \land T \subseteq ℝ) \to sup (T ℝ <) \in T$
146	119 142 115 145	syl3anc	$⊢ (φ \land ψ) \to sup (T ℝ <) \in T$
147	115 146	sseldd	$⊢ (φ \land ψ) \to sup (T ℝ <) \in ℝ$
148		0red	$⊢ (φ \land ψ) \to 0 \in ℝ$
149	125 5	sylan2	$⊢ (φ \land k \in ℕ) \to B \in ℂ$
150		1nn0	$⊢ 1 \in ℕ_{0}$
151	150	a1i	$⊢ φ \to 1 \in ℕ_{0}$
152	15 151 30	iserex	$⊢ φ \to (seq 0 (+ G) \in dom ⇝ \leftrightarrow seq 1 (+ G) \in dom ⇝)$
153	8 152	mpbid	$⊢ φ \to seq 1 (+ G) \in dom ⇝$
154	12 13 126 149 153	isumcl	$⊢ φ \to \sum_{k \in ℕ} B \in ℂ$
155	154	adantr	$⊢ (φ \land ψ) \to \sum_{k \in ℕ} B \in ℂ$
156	155	abscld	$⊢ (φ \land ψ) \to \|\sum_{k \in ℕ} B\| \in ℝ$
157	155	absge0d	$⊢ (φ \land ψ) \to 0 \leq \|\sum_{k \in ℕ} B\|$
158		fimaxre2	$⊢ (T \subseteq ℝ \land T \in Fin) \to \exists z \in ℝ \forall w \in T w \leq z$
159	115 119 158	syl2anc	$⊢ (φ \land ψ) \to \exists z \in ℝ \forall w \in T w \leq z$
160	115 142 159 141	suprubd	$⊢ (φ \land ψ) \to \|\sum_{k \in ℕ} B\| \leq sup (T ℝ <)$
161	148 156 147 157 160	letrd	$⊢ (φ \land ψ) \to 0 \leq sup (T ℝ <)$
162	147 161	ge0p1rpd	$⊢ (φ \land ψ) \to sup (T ℝ <) + 1 \in ℝ^{+}$
163	93 162	rpdivcld	$⊢ (φ \land ψ) \to \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1} \in ℝ^{+}$
164		fveq2	$⊢ n = m \to K (n) = K (m)$
165		eqid	$⊢ (n \in ℕ_{0} ⟼ K (n)) = (n \in ℕ_{0} ⟼ K (n))$
166		fvex	$⊢ K (m) \in V$
167	164 165 166	fvmpt	$⊢ m \in ℕ_{0} \to (n \in ℕ_{0} ⟼ K (n)) (m) = K (m)$
168	167	adantl	$⊢ ((φ \land ψ) \land m \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ K (n)) (m) = K (m)$
169		nn0ex	$⊢ ℕ_{0} \in V$
170	169	mptex	$⊢ (n \in ℕ_{0} ⟼ K (n)) \in V$
171	170	a1i	$⊢ φ \to (n \in ℕ_{0} ⟼ K (n)) \in V$
172		elnn0uz	$⊢ j \in ℕ_{0} \leftrightarrow j \in ℤ_{\geq 0}$
173		fveq2	$⊢ n = j \to K (n) = K (j)$
174		fvex	$⊢ K (j) \in V$
175	173 165 174	fvmpt	$⊢ j \in ℕ_{0} \to (n \in ℕ_{0} ⟼ K (n)) (j) = K (j)$
176	175	adantl	$⊢ (φ \land j \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ K (n)) (j) = K (j)$
177	172 176	sylan2br	$⊢ (φ \land j \in ℤ_{\geq 0}) \to (n \in ℕ_{0} ⟼ K (n)) (j) = K (j)$
178	16 177	seqfeq	$⊢ φ \to seq 0 (+ (n \in ℕ_{0} ⟼ K (n))) = seq 0 (+ K)$
179	178 7	eqeltrd	$⊢ φ \to seq 0 (+ (n \in ℕ_{0} ⟼ K (n))) \in dom ⇝$
180	176 2	eqtrd	$⊢ (φ \land j \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ K (n)) (j) = \|A\|$
181	180 18	eqeltrd	$⊢ (φ \land j \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ K (n)) (j) \in ℝ$
182	181	recnd	$⊢ (φ \land j \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ K (n)) (j) \in ℂ$
183	15 16 171 179 182	serf0	$⊢ φ \to (n \in ℕ_{0} ⟼ K (n)) ⇝ 0$
184	183	adantr	$⊢ (φ \land ψ) \to (n \in ℕ_{0} ⟼ K (n)) ⇝ 0$
185	15 88 163 168 184	climi0	$⊢ (φ \land ψ) \to \exists t \in ℕ_{0} \forall m \in ℤ_{\geq t} \|K (m)\| < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1}$
186		simplll	$⊢ (((φ \land ψ) \land t \in ℕ_{0}) \land m \in ℤ_{\geq t}) \to φ$
187		eluznn0	$⊢ (t \in ℕ_{0} \land m \in ℤ_{\geq t}) \to m \in ℕ_{0}$
188	187	adantll	$⊢ (((φ \land ψ) \land t \in ℕ_{0}) \land m \in ℤ_{\geq t}) \to m \in ℕ_{0}$
189	19 22	absidd	$⊢ (φ \land j \in ℕ_{0}) \to \|K (j)\| = K (j)$
190	189	ralrimiva	$⊢ φ \to \forall j \in ℕ_{0} \|K (j)\| = K (j)$
191		fveq2	$⊢ j = m \to K (j) = K (m)$
192	191	fveq2d	$⊢ j = m \to \|K (j)\| = \|K (m)\|$
193	192 191	eqeq12d	$⊢ j = m \to (\|K (j)\| = K (j) \leftrightarrow \|K (m)\| = K (m))$
194	193	rspccva	$⊢ (\forall j \in ℕ_{0} \|K (j)\| = K (j) \land m \in ℕ_{0}) \to \|K (m)\| = K (m)$
195	190 194	sylan	$⊢ (φ \land m \in ℕ_{0}) \to \|K (m)\| = K (m)$
196	186 188 195	syl2anc	$⊢ (((φ \land ψ) \land t \in ℕ_{0}) \land m \in ℤ_{\geq t}) \to \|K (m)\| = K (m)$
197	196	breq1d	$⊢ (((φ \land ψ) \land t \in ℕ_{0}) \land m \in ℤ_{\geq t}) \to (\|K (m)\| < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1} \leftrightarrow K (m) < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1})$
198	197	ralbidva	$⊢ ((φ \land ψ) \land t \in ℕ_{0}) \to (\forall m \in ℤ_{\geq t} \|K (m)\| < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1} \leftrightarrow \forall m \in ℤ_{\geq t} K (m) < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1})$
199	164	breq1d	$⊢ n = m \to (K (n) < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1} \leftrightarrow K (m) < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1})$
200	199	cbvralvw	$⊢ \forall n \in ℤ_{\geq t} K (n) < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1} \leftrightarrow \forall m \in ℤ_{\geq t} K (m) < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1}$
201	198 200	bitr4di	$⊢ ((φ \land ψ) \land t \in ℕ_{0}) \to (\forall m \in ℤ_{\geq t} \|K (m)\| < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1} \leftrightarrow \forall n \in ℤ_{\geq t} K (n) < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1})$
202	1	ad4ant14	$⊢ (((φ \land ψ) \land (t \in ℕ_{0} \land \forall n \in ℤ_{\geq t} K (n) < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1})) \land j \in ℕ_{0}) \to F (j) = A$
203	2	ad4ant14	$⊢ (((φ \land ψ) \land (t \in ℕ_{0} \land \forall n \in ℤ_{\geq t} K (n) < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1})) \land j \in ℕ_{0}) \to K (j) = \|A\|$
204	3	ad4ant14	$⊢ (((φ \land ψ) \land (t \in ℕ_{0} \land \forall n \in ℤ_{\geq t} K (n) < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1})) \land j \in ℕ_{0}) \to A \in ℂ$
205	4	ad4ant14	$⊢ (((φ \land ψ) \land (t \in ℕ_{0} \land \forall n \in ℤ_{\geq t} K (n) < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1})) \land k \in ℕ_{0}) \to G (k) = B$
206	5	ad4ant14	$⊢ (((φ \land ψ) \land (t \in ℕ_{0} \land \forall n \in ℤ_{\geq t} K (n) < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1})) \land k \in ℕ_{0}) \to B \in ℂ$
207	6	ad4ant14	$⊢ (((φ \land ψ) \land (t \in ℕ_{0} \land \forall n \in ℤ_{\geq t} K (n) < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1})) \land k \in ℕ_{0}) \to H (k) = \sum_{j = 0}^{k} A G (k - j)$
208	7	ad2antrr	$⊢ ((φ \land ψ) \land (t \in ℕ_{0} \land \forall n \in ℤ_{\geq t} K (n) < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1})) \to seq 0 (+ K) \in dom ⇝$
209	8	ad2antrr	$⊢ ((φ \land ψ) \land (t \in ℕ_{0} \land \forall n \in ℤ_{\geq t} K (n) < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1})) \to seq 0 (+ G) \in dom ⇝$
210	9	ad2antrr	$⊢ ((φ \land ψ) \land (t \in ℕ_{0} \land \forall n \in ℤ_{\geq t} K (n) < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1})) \to E \in ℝ^{+}$
211	200	anbi2i	$⊢ (t \in ℕ_{0} \land \forall n \in ℤ_{\geq t} K (n) < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1}) \leftrightarrow (t \in ℕ_{0} \land \forall m \in ℤ_{\geq t} K (m) < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1})$
212	211	anbi2i	$⊢ (ψ \land (t \in ℕ_{0} \land \forall n \in ℤ_{\geq t} K (n) < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1})) \leftrightarrow (ψ \land (t \in ℕ_{0} \land \forall m \in ℤ_{\geq t} K (m) < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1}))$
213	212	biimpi	$⊢ (ψ \land (t \in ℕ_{0} \land \forall n \in ℤ_{\geq t} K (n) < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1})) \to (ψ \land (t \in ℕ_{0} \land \forall m \in ℤ_{\geq t} K (m) < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1}))$
214	213	adantll	$⊢ ((φ \land ψ) \land (t \in ℕ_{0} \land \forall n \in ℤ_{\geq t} K (n) < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1})) \to (ψ \land (t \in ℕ_{0} \land \forall m \in ℤ_{\geq t} K (m) < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1}))$
215	115 142 159	3jca	$⊢ (φ \land ψ) \to (T \subseteq ℝ \land T \neq \emptyset \land \exists z \in ℝ \forall w \in T w \leq z)$
216	161 215	jca	$⊢ (φ \land ψ) \to (0 \leq sup (T ℝ <) \land (T \subseteq ℝ \land T \neq \emptyset \land \exists z \in ℝ \forall w \in T w \leq z))$
217	216	adantr	$⊢ ((φ \land ψ) \land (t \in ℕ_{0} \land \forall n \in ℤ_{\geq t} K (n) < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1})) \to (0 \leq sup (T ℝ <) \land (T \subseteq ℝ \land T \neq \emptyset \land \exists z \in ℝ \forall w \in T w \leq z))$
218	202 203 204 205 206 207 208 209 210 10 11 214 217	mertenslem1	$⊢ ((φ \land ψ) \land (t \in ℕ_{0} \land \forall n \in ℤ_{\geq t} K (n) < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1})) \to \exists y \in ℕ_{0} \forall m \in ℤ_{\geq y} \|\sum_{j = 0}^{m} A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\| < E$
219	218	expr	$⊢ ((φ \land ψ) \land t \in ℕ_{0}) \to (\forall n \in ℤ_{\geq t} K (n) < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1} \to \exists y \in ℕ_{0} \forall m \in ℤ_{\geq y} \|\sum_{j = 0}^{m} A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\| < E)$
220	201 219	sylbid	$⊢ ((φ \land ψ) \land t \in ℕ_{0}) \to (\forall m \in ℤ_{\geq t} \|K (m)\| < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1} \to \exists y \in ℕ_{0} \forall m \in ℤ_{\geq y} \|\sum_{j = 0}^{m} A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\| < E)$
221	220	rexlimdva	$⊢ (φ \land ψ) \to (\exists t \in ℕ_{0} \forall m \in ℤ_{\geq t} \|K (m)\| < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1} \to \exists y \in ℕ_{0} \forall m \in ℤ_{\geq y} \|\sum_{j = 0}^{m} A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\| < E)$
222	185 221	mpd	$⊢ (φ \land ψ) \to \exists y \in ℕ_{0} \forall m \in ℤ_{\geq y} \|\sum_{j = 0}^{m} A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\| < E$
223	222	ex	$⊢ φ \to (ψ \to \exists y \in ℕ_{0} \forall m \in ℤ_{\geq y} \|\sum_{j = 0}^{m} A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\| < E)$
224	11 223	syl5bir	$⊢ φ \to ((s \in ℕ \land \forall n \in ℤ_{\geq s} \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\| < \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1}) \to \exists y \in ℕ_{0} \forall m \in ℤ_{\geq y} \|\sum_{j = 0}^{m} A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\| < E)$
225	224	expdimp	$⊢ (φ \land s \in ℕ) \to (\forall n \in ℤ_{\geq s} \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\| < \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1} \to \exists y \in ℕ_{0} \forall m \in ℤ_{\geq y} \|\sum_{j = 0}^{m} A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\| < E)$
226	87 225	sylbid	$⊢ (φ \land s \in ℕ) \to (\forall m \in ℤ_{\geq s} \|seq 0 (+ G) (m) - \sum_{k \in ℕ_{0}} B\| < \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1} \to \exists y \in ℕ_{0} \forall m \in ℤ_{\geq y} \|\sum_{j = 0}^{m} A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\| < E)$
227	226	rexlimdva	$⊢ φ \to (\exists s \in ℕ \forall m \in ℤ_{\geq s} \|seq 0 (+ G) (m) - \sum_{k \in ℕ_{0}} B\| < \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1} \to \exists y \in ℕ_{0} \forall m \in ℤ_{\geq y} \|\sum_{j = 0}^{m} A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\| < E)$
228	28 227	mpd	$⊢ φ \to \exists y \in ℕ_{0} \forall m \in ℤ_{\geq y} \|\sum_{j = 0}^{m} A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\| < E$

Metamath Proof Explorer

Theorem mertenslem2

Proof