Theorem mertenslem2 14456

Description: Lemma for mertens 14457. (Contributed by Mario Carneiro, 28-Apr-2014.)

Hypotheses

Ref	Expression
mertens.1	⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐹‘𝑗) = 𝐴)
mertens.2	⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) = (abs‘𝐴))
mertens.3	⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝐴 ∈ ℂ)
mertens.4	⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = 𝐵)
mertens.5	⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)
mertens.6	⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐻‘𝑘) = Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗))))
mertens.7	⊢ (𝜑 → seq0( + , 𝐾) ∈ dom ⇝ )
mertens.8	⊢ (𝜑 → seq0( + , 𝐺) ∈ dom ⇝ )
mertens.9	⊢ (𝜑 → 𝐸 ∈ ℝ+)
mertens.10	⊢ 𝑇 = {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))}
mertens.11	⊢ (𝜓 ↔ (𝑠 ∈ ℕ ∧ ∀𝑛 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))))

Assertion

Ref	Expression
mertenslem2	⊢ (𝜑 → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)

Distinct variable groups:   𝑗,𝑚,𝑛,𝑠,𝑦,𝑧,𝐵   𝑗,𝑘,𝐺,𝑚,𝑛,𝑠,𝑦,𝑧   𝜑,𝑗,𝑘,𝑚,𝑦,𝑧   𝐴,𝑘,𝑚,𝑛,𝑠,𝑦   𝑗,𝐸,𝑘,𝑚,𝑛,𝑠,𝑦,𝑧   𝑗,𝐾,𝑘,𝑚,𝑛,𝑠,𝑦,𝑧   𝑗,𝐹,𝑚,𝑛,𝑦   𝜓,𝑗,𝑘,𝑚,𝑛,𝑦,𝑧   𝑇,𝑗,𝑘,𝑚,𝑛,𝑦,𝑧   𝑘,𝐻,𝑚,𝑦   𝜑,𝑛,𝑠

Allowed substitution hints:   𝜓(𝑠)   𝐴(𝑧,𝑗)   𝐵(𝑘)   𝑇(𝑠)   𝐹(𝑧,𝑘,𝑠)   𝐻(𝑧,𝑗,𝑛,𝑠)

Proof of Theorem mertenslem2

Dummy variables 𝑡 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nnuz 11599	. . 3 ⊢ ℕ = (ℤ≥‘1)
2		1zzd 11285	. . 3 ⊢ (𝜑 → 1 ∈ ℤ)
3		mertens.9	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ ℝ+)
4	3	rphalfcld 11760	. . . 4 ⊢ (𝜑 → (𝐸 / 2) ∈ ℝ+)
5		nn0uz 11598	. . . . . 6 ⊢ ℕ0 = (ℤ≥‘0)
6		0zd 11266	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℤ)
7		eqidd 2611	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) = (𝐾‘𝑗))
8		mertens.2	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) = (abs‘𝐴))
9		mertens.3	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝐴 ∈ ℂ)
10	9	abscld 14023	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (abs‘𝐴) ∈ ℝ)
11	8, 10	eqeltrd 2688	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) ∈ ℝ)
12		mertens.7	. . . . . 6 ⊢ (𝜑 → seq0( + , 𝐾) ∈ dom ⇝ )
13	5, 6, 7, 11, 12	isumrecl 14338	. . . . 5 ⊢ (𝜑 → Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) ∈ ℝ)
14	9	absge0d 14031	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 0 ≤ (abs‘𝐴))
15	14, 8	breqtrrd 4611	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 0 ≤ (𝐾‘𝑗))
16	5, 6, 7, 11, 12, 15	isumge0 14339	. . . . 5 ⊢ (𝜑 → 0 ≤ Σ𝑗 ∈ ℕ0 (𝐾‘𝑗))
17	13, 16	ge0p1rpd 11778	. . . 4 ⊢ (𝜑 → (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ∈ ℝ+)
18	4, 17	rpdivcld 11765	. . 3 ⊢ (𝜑 → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ∈ ℝ+)
19		eqidd 2611	. . 3 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (seq0( + , 𝐺)‘𝑚) = (seq0( + , 𝐺)‘𝑚))
20		mertens.4	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = 𝐵)
21		mertens.5	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)
22		mertens.8	. . . 4 ⊢ (𝜑 → seq0( + , 𝐺) ∈ dom ⇝ )
23	5, 6, 20, 21, 22	isumclim2 14331	. . 3 ⊢ (𝜑 → seq0( + , 𝐺) ⇝ Σ𝑘 ∈ ℕ0 𝐵)
24	1, 2, 18, 19, 23	climi2 14090	. 2 ⊢ (𝜑 → ∃𝑠 ∈ ℕ ∀𝑚 ∈ (ℤ≥‘𝑠)(abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))
25		eluznn 11634	. . . . . . . 8 ⊢ ((𝑠 ∈ ℕ ∧ 𝑚 ∈ (ℤ≥‘𝑠)) → 𝑚 ∈ ℕ)
26	20, 21	eqeltrd 2688	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) ∈ ℂ)
27	5, 6, 26	serf 12691	. . . . . . . . . . . 12 ⊢ (𝜑 → seq0( + , 𝐺):ℕ0⟶ℂ)
28		nnnn0 11176	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℕ0)
29		ffvelrn 6265	. . . . . . . . . . . 12 ⊢ ((seq0( + , 𝐺):ℕ0⟶ℂ ∧ 𝑚 ∈ ℕ0) → (seq0( + , 𝐺)‘𝑚) ∈ ℂ)
30	27, 28, 29	syl2an 493	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (seq0( + , 𝐺)‘𝑚) ∈ ℂ)
31	5, 6, 20, 21, 22	isumcl 14334	. . . . . . . . . . . 12 ⊢ (𝜑 → Σ𝑘 ∈ ℕ0 𝐵 ∈ ℂ)
32	31	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈ ℕ0 𝐵 ∈ ℂ)
33	30, 32	abssubd 14040	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) = (abs‘(Σ𝑘 ∈ ℕ0 𝐵 − (seq0( + , 𝐺)‘𝑚))))
34		eqid 2610	. . . . . . . . . . . . . 14 ⊢ (ℤ≥‘(𝑚 + 1)) = (ℤ≥‘(𝑚 + 1))
35	28	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℕ0)
36		peano2nn0 11210	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ0 → (𝑚 + 1) ∈ ℕ0)
37	35, 36	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑚 + 1) ∈ ℕ0)
38	37	nn0zd 11356	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑚 + 1) ∈ ℤ)
39		simpll 786	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘(𝑚 + 1))) → 𝜑)
40		eluznn0 11633	. . . . . . . . . . . . . . . 16 ⊢ (((𝑚 + 1) ∈ ℕ0 ∧ 𝑘 ∈ (ℤ≥‘(𝑚 + 1))) → 𝑘 ∈ ℕ0)
41	37, 40	sylan 487	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘(𝑚 + 1))) → 𝑘 ∈ ℕ0)
42	39, 41, 20	syl2anc 691	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘(𝑚 + 1))) → (𝐺‘𝑘) = 𝐵)
43	39, 41, 21	syl2anc 691	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘(𝑚 + 1))) → 𝐵 ∈ ℂ)
44	22	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → seq0( + , 𝐺) ∈ dom ⇝ )
45	26	adantlr 747	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) ∈ ℂ)
46	5, 37, 45	iserex 14235	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (seq0( + , 𝐺) ∈ dom ⇝ ↔ seq(𝑚 + 1)( + , 𝐺) ∈ dom ⇝ ))
47	44, 46	mpbid 221	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → seq(𝑚 + 1)( + , 𝐺) ∈ dom ⇝ )
48	34, 38, 42, 43, 47	isumcl 14334	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))𝐵 ∈ ℂ)
49	30, 48	pncan2d 10273	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((seq0( + , 𝐺)‘𝑚) + Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))𝐵) − (seq0( + , 𝐺)‘𝑚)) = Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))𝐵)
50	20	adantlr 747	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = 𝐵)
51	21	adantlr 747	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)
52	5, 34, 37, 50, 51, 44	isumsplit 14411	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈ ℕ0 𝐵 = (Σ𝑘 ∈ (0...((𝑚 + 1) − 1))𝐵 + Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))𝐵))
53		nncn 10905	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
54	53	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℂ)
55		ax-1cn 9873	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℂ
56		pncan 10166	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑚 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑚 + 1) − 1) = 𝑚)
57	54, 55, 56	sylancl 693	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑚 + 1) − 1) = 𝑚)
58	57	oveq2d 6565	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (0...((𝑚 + 1) − 1)) = (0...𝑚))
59	58	sumeq1d 14279	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈ (0...((𝑚 + 1) − 1))𝐵 = Σ𝑘 ∈ (0...𝑚)𝐵)
60		simpl 472	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝜑)
61		elfznn0 12302	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (0...𝑚) → 𝑘 ∈ ℕ0)
62	60, 61, 20	syl2an 493	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑚)) → (𝐺‘𝑘) = 𝐵)
63	35, 5	syl6eleq 2698	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ (ℤ≥‘0))
64	60, 61, 21	syl2an 493	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑚)) → 𝐵 ∈ ℂ)
65	62, 63, 64	fsumser 14308	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈ (0...𝑚)𝐵 = (seq0( + , 𝐺)‘𝑚))
66	59, 65	eqtrd 2644	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈ (0...((𝑚 + 1) − 1))𝐵 = (seq0( + , 𝐺)‘𝑚))
67	66	oveq1d 6564	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (Σ𝑘 ∈ (0...((𝑚 + 1) − 1))𝐵 + Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))𝐵) = ((seq0( + , 𝐺)‘𝑚) + Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))𝐵))
68	52, 67	eqtrd 2644	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈ ℕ0 𝐵 = ((seq0( + , 𝐺)‘𝑚) + Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))𝐵))
69	68	oveq1d 6564	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (Σ𝑘 ∈ ℕ0 𝐵 − (seq0( + , 𝐺)‘𝑚)) = (((seq0( + , 𝐺)‘𝑚) + Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))𝐵) − (seq0( + , 𝐺)‘𝑚)))
70	42	sumeq2dv 14281	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))𝐵)
71	49, 69, 70	3eqtr4d 2654	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (Σ𝑘 ∈ ℕ0 𝐵 − (seq0( + , 𝐺)‘𝑚)) = Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))(𝐺‘𝑘))
72	71	fveq2d 6107	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (abs‘(Σ𝑘 ∈ ℕ0 𝐵 − (seq0( + , 𝐺)‘𝑚))) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))(𝐺‘𝑘)))
73	33, 72	eqtrd 2644	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))(𝐺‘𝑘)))
74	73	breq1d 4593	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ↔ (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))))
75	25, 74	sylan2 490	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑠 ∈ ℕ ∧ 𝑚 ∈ (ℤ≥‘𝑠))) → ((abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ↔ (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))))
76	75	anassrs 678	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘𝑠)) → ((abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ↔ (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))))
77	76	ralbidva 2968	. . . . 5 ⊢ ((𝜑 ∧ 𝑠 ∈ ℕ) → (∀𝑚 ∈ (ℤ≥‘𝑠)(abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ↔ ∀𝑚 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))))
78		oveq1 6556	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → (𝑚 + 1) = (𝑛 + 1))
79	78	fveq2d 6107	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (ℤ≥‘(𝑚 + 1)) = (ℤ≥‘(𝑛 + 1)))
80	79	sumeq1d 14279	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))
81	80	fveq2d 6107	. . . . . . 7 ⊢ (𝑚 = 𝑛 → (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))(𝐺‘𝑘)) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)))
82	81	breq1d 4593	. . . . . 6 ⊢ (𝑚 = 𝑛 → ((abs‘Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ↔ (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))))
83	82	cbvralv 3147	. . . . 5 ⊢ (∀𝑚 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ↔ ∀𝑛 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))
84	77, 83	syl6bb 275	. . . 4 ⊢ ((𝜑 ∧ 𝑠 ∈ ℕ) → (∀𝑚 ∈ (ℤ≥‘𝑠)(abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ↔ ∀𝑛 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))))
85		mertens.11	. . . . . 6 ⊢ (𝜓 ↔ (𝑠 ∈ ℕ ∧ ∀𝑛 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))))
86		0zd 11266	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → 0 ∈ ℤ)
87	4	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝐸 / 2) ∈ ℝ+)
88	85	simplbi 475	. . . . . . . . . . . . 13 ⊢ (𝜓 → 𝑠 ∈ ℕ)
89	88	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → 𝑠 ∈ ℕ)
90	89	nnrpd 11746	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → 𝑠 ∈ ℝ+)
91	87, 90	rpdivcld 11765	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → ((𝐸 / 2) / 𝑠) ∈ ℝ+)
92		mertens.10	. . . . . . . . . . . . 13 ⊢ 𝑇 = {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))}
93		eqid 2610	. . . . . . . . . . . . . . . . . 18 ⊢ (ℤ≥‘(𝑛 + 1)) = (ℤ≥‘(𝑛 + 1))
94		elfznn0 12302	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ (0...(𝑠 − 1)) → 𝑛 ∈ ℕ0)
95	94	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → 𝑛 ∈ ℕ0)
96		peano2nn0 11210	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ0 → (𝑛 + 1) ∈ ℕ0)
97	95, 96	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → (𝑛 + 1) ∈ ℕ0)
98	97	nn0zd 11356	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → (𝑛 + 1) ∈ ℤ)
99		eqidd 2611	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) ∧ 𝑘 ∈ (ℤ≥‘(𝑛 + 1))) → (𝐺‘𝑘) = (𝐺‘𝑘))
100		simplll 794	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) ∧ 𝑘 ∈ (ℤ≥‘(𝑛 + 1))) → 𝜑)
101		eluznn0 11633	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 + 1) ∈ ℕ0 ∧ 𝑘 ∈ (ℤ≥‘(𝑛 + 1))) → 𝑘 ∈ ℕ0)
102	97, 101	sylan 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) ∧ 𝑘 ∈ (ℤ≥‘(𝑛 + 1))) → 𝑘 ∈ ℕ0)
103	100, 102, 26	syl2anc 691	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) ∧ 𝑘 ∈ (ℤ≥‘(𝑛 + 1))) → (𝐺‘𝑘) ∈ ℂ)
104	22	ad2antrr 758	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → seq0( + , 𝐺) ∈ dom ⇝ )
105		simpll 786	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → 𝜑)
106	105, 26	sylan 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) ∈ ℂ)
107	5, 97, 106	iserex 14235	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → (seq0( + , 𝐺) ∈ dom ⇝ ↔ seq(𝑛 + 1)( + , 𝐺) ∈ dom ⇝ ))
108	104, 107	mpbid 221	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → seq(𝑛 + 1)( + , 𝐺) ∈ dom ⇝ )
109	93, 98, 99, 103, 108	isumcl 14334	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘) ∈ ℂ)
110	109	abscld 14023	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) ∈ ℝ)
111		eleq1a 2683	. . . . . . . . . . . . . . . 16 ⊢ ((abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) ∈ ℝ → (𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) → 𝑧 ∈ ℝ))
112	110, 111	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → (𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) → 𝑧 ∈ ℝ))
113	112	rexlimdva 3013	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → (∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) → 𝑧 ∈ ℝ))
114	113	abssdv 3639	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))} ⊆ ℝ)
115	92, 114	syl5eqss 3612	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → 𝑇 ⊆ ℝ)
116		fzfid 12634	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → (0...(𝑠 − 1)) ∈ Fin)
117		abrexfi 8149	. . . . . . . . . . . . . . 15 ⊢ ((0...(𝑠 − 1)) ∈ Fin → {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))} ∈ Fin)
118	116, 117	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))} ∈ Fin)
119	92, 118	syl5eqel 2692	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → 𝑇 ∈ Fin)
120		nnm1nn0 11211	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ ℕ → (𝑠 − 1) ∈ ℕ0)
121	89, 120	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜓) → (𝑠 − 1) ∈ ℕ0)
122	121, 5	syl6eleq 2698	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜓) → (𝑠 − 1) ∈ (ℤ≥‘0))
123		eluzfz1 12219	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 − 1) ∈ (ℤ≥‘0) → 0 ∈ (0...(𝑠 − 1)))
124	122, 123	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜓) → 0 ∈ (0...(𝑠 − 1)))
125		nnnn0 11176	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
126	125, 20	sylan2 490	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) = 𝐵)
127	126	sumeq2dv 14281	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → Σ𝑘 ∈ ℕ (𝐺‘𝑘) = Σ𝑘 ∈ ℕ 𝐵)
128	127	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜓) → Σ𝑘 ∈ ℕ (𝐺‘𝑘) = Σ𝑘 ∈ ℕ 𝐵)
129	128	fveq2d 6107	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜓) → (abs‘Σ𝑘 ∈ ℕ (𝐺‘𝑘)) = (abs‘Σ𝑘 ∈ ℕ 𝐵))
130	129	eqcomd 2616	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜓) → (abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈ ℕ (𝐺‘𝑘)))
131		oveq1 6556	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 0 → (𝑛 + 1) = (0 + 1))
132		0p1e1 11009	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0 + 1) = 1
133	131, 132	syl6eq 2660	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 0 → (𝑛 + 1) = 1)
134	133	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 0 → (ℤ≥‘(𝑛 + 1)) = (ℤ≥‘1))
135	134, 1	syl6eqr 2662	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 0 → (ℤ≥‘(𝑛 + 1)) = ℕ)
136	135	sumeq1d 14279	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 0 → Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘) = Σ𝑘 ∈ ℕ (𝐺‘𝑘))
137	136	fveq2d 6107	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 0 → (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) = (abs‘Σ𝑘 ∈ ℕ (𝐺‘𝑘)))
138	137	eqeq2d 2620	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 0 → ((abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) ↔ (abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈ ℕ (𝐺‘𝑘))))
139	138	rspcev 3282	. . . . . . . . . . . . . . . 16 ⊢ ((0 ∈ (0...(𝑠 − 1)) ∧ (abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈ ℕ (𝐺‘𝑘))) → ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)))
140	124, 130, 139	syl2anc 691	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)))
141		fvex 6113	. . . . . . . . . . . . . . . 16 ⊢ (abs‘Σ𝑘 ∈ ℕ 𝐵) ∈ V
142		eqeq1 2614	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (abs‘Σ𝑘 ∈ ℕ 𝐵) → (𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) ↔ (abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))))
143	142	rexbidv 3034	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (abs‘Σ𝑘 ∈ ℕ 𝐵) → (∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) ↔ ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))))
144	141, 143, 92	elab2 3323	. . . . . . . . . . . . . . 15 ⊢ ((abs‘Σ𝑘 ∈ ℕ 𝐵) ∈ 𝑇 ↔ ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)))
145	140, 144	sylibr 223	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → (abs‘Σ𝑘 ∈ ℕ 𝐵) ∈ 𝑇)
146		ne0i 3880	. . . . . . . . . . . . . 14 ⊢ ((abs‘Σ𝑘 ∈ ℕ 𝐵) ∈ 𝑇 → 𝑇 ≠ ∅)
147	145, 146	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → 𝑇 ≠ ∅)
148		ltso 9997	. . . . . . . . . . . . . 14 ⊢ < Or ℝ
149		fisupcl 8258	. . . . . . . . . . . . . 14 ⊢ (( < Or ℝ ∧ (𝑇 ∈ Fin ∧ 𝑇 ≠ ∅ ∧ 𝑇 ⊆ ℝ)) → sup(𝑇, ℝ, < ) ∈ 𝑇)
150	148, 149	mpan 702	. . . . . . . . . . . . 13 ⊢ ((𝑇 ∈ Fin ∧ 𝑇 ≠ ∅ ∧ 𝑇 ⊆ ℝ) → sup(𝑇, ℝ, < ) ∈ 𝑇)
151	119, 147, 115, 150	syl3anc 1318	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → sup(𝑇, ℝ, < ) ∈ 𝑇)
152	115, 151	sseldd 3569	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → sup(𝑇, ℝ, < ) ∈ ℝ)
153		0red 9920	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → 0 ∈ ℝ)
154	125, 21	sylan2 490	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐵 ∈ ℂ)
155		1nn0 11185	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℕ0
156	155	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ∈ ℕ0)
157	5, 156, 26	iserex 14235	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (seq0( + , 𝐺) ∈ dom ⇝ ↔ seq1( + , 𝐺) ∈ dom ⇝ ))
158	22, 157	mpbid 221	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → seq1( + , 𝐺) ∈ dom ⇝ )
159	1, 2, 126, 154, 158	isumcl 14334	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Σ𝑘 ∈ ℕ 𝐵 ∈ ℂ)
160	159	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → Σ𝑘 ∈ ℕ 𝐵 ∈ ℂ)
161	160	abscld 14023	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → (abs‘Σ𝑘 ∈ ℕ 𝐵) ∈ ℝ)
162	160	absge0d 14031	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → 0 ≤ (abs‘Σ𝑘 ∈ ℕ 𝐵))
163		fimaxre2 10848	. . . . . . . . . . . . . . 15 ⊢ ((𝑇 ⊆ ℝ ∧ 𝑇 ∈ Fin) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧)
164	115, 119, 163	syl2anc 691	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧)
165	115, 147, 164	3jca 1235	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧))
166		suprub 10863	. . . . . . . . . . . . 13 ⊢ (((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧) ∧ (abs‘Σ𝑘 ∈ ℕ 𝐵) ∈ 𝑇) → (abs‘Σ𝑘 ∈ ℕ 𝐵) ≤ sup(𝑇, ℝ, < ))
167	165, 145, 166	syl2anc 691	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → (abs‘Σ𝑘 ∈ ℕ 𝐵) ≤ sup(𝑇, ℝ, < ))
168	153, 161, 152, 162, 167	letrd 10073	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → 0 ≤ sup(𝑇, ℝ, < ))
169	152, 168	ge0p1rpd 11778	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (sup(𝑇, ℝ, < ) + 1) ∈ ℝ+)
170	91, 169	rpdivcld 11765	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℝ+)
171		fveq2 6103	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑚 → (𝐾‘𝑛) = (𝐾‘𝑚))
172		eqid 2610	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ0 ↦ (𝐾‘𝑛)) = (𝑛 ∈ ℕ0 ↦ (𝐾‘𝑛))
173		fvex 6113	. . . . . . . . . . 11 ⊢ (𝐾‘𝑚) ∈ V
174	171, 172, 173	fvmpt 6191	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ (𝐾‘𝑛))‘𝑚) = (𝐾‘𝑚))
175	174	adantl 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑚 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (𝐾‘𝑛))‘𝑚) = (𝐾‘𝑚))
176		nn0ex 11175	. . . . . . . . . . . . 13 ⊢ ℕ0 ∈ V
177	176	mptex 6390	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ0 ↦ (𝐾‘𝑛)) ∈ V
178	177	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ (𝐾‘𝑛)) ∈ V)
179		elnn0uz 11601	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ℕ0 ↔ 𝑗 ∈ (ℤ≥‘0))
180		fveq2 6103	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑗 → (𝐾‘𝑛) = (𝐾‘𝑗))
181		fvex 6113	. . . . . . . . . . . . . . . 16 ⊢ (𝐾‘𝑗) ∈ V
182	180, 172, 181	fvmpt 6191	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ (𝐾‘𝑛))‘𝑗) = (𝐾‘𝑗))
183	182	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (𝐾‘𝑛))‘𝑗) = (𝐾‘𝑗))
184	179, 183	sylan2br 492	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘0)) → ((𝑛 ∈ ℕ0 ↦ (𝐾‘𝑛))‘𝑗) = (𝐾‘𝑗))
185	6, 184	seqfeq 12688	. . . . . . . . . . . 12 ⊢ (𝜑 → seq0( + , (𝑛 ∈ ℕ0 ↦ (𝐾‘𝑛))) = seq0( + , 𝐾))
186	185, 12	eqeltrd 2688	. . . . . . . . . . 11 ⊢ (𝜑 → seq0( + , (𝑛 ∈ ℕ0 ↦ (𝐾‘𝑛))) ∈ dom ⇝ )
187	183, 8	eqtrd 2644	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (𝐾‘𝑛))‘𝑗) = (abs‘𝐴))
188	187, 10	eqeltrd 2688	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (𝐾‘𝑛))‘𝑗) ∈ ℝ)
189	188	recnd 9947	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (𝐾‘𝑛))‘𝑗) ∈ ℂ)
190	5, 6, 178, 186, 189	serf0 14259	. . . . . . . . . 10 ⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ (𝐾‘𝑛)) ⇝ 0)
191	190	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝑛 ∈ ℕ0 ↦ (𝐾‘𝑛)) ⇝ 0)
192	5, 86, 170, 175, 191	climi0 14091	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ∃𝑡 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑡)(abs‘(𝐾‘𝑚)) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))
193		simplll 794	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑡 ∈ ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑡)) → 𝜑)
194		eluznn0 11633	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℕ0 ∧ 𝑚 ∈ (ℤ≥‘𝑡)) → 𝑚 ∈ ℕ0)
195	194	adantll 746	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑡 ∈ ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑡)) → 𝑚 ∈ ℕ0)
196	11, 15	absidd 14009	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (abs‘(𝐾‘𝑗)) = (𝐾‘𝑗))
197	196	ralrimiva 2949	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑗 ∈ ℕ0 (abs‘(𝐾‘𝑗)) = (𝐾‘𝑗))
198		fveq2 6103	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑚 → (𝐾‘𝑗) = (𝐾‘𝑚))
199	198	fveq2d 6107	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑚 → (abs‘(𝐾‘𝑗)) = (abs‘(𝐾‘𝑚)))
200	199, 198	eqeq12d 2625	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑚 → ((abs‘(𝐾‘𝑗)) = (𝐾‘𝑗) ↔ (abs‘(𝐾‘𝑚)) = (𝐾‘𝑚)))
201	200	rspccva 3281	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑗 ∈ ℕ0 (abs‘(𝐾‘𝑗)) = (𝐾‘𝑗) ∧ 𝑚 ∈ ℕ0) → (abs‘(𝐾‘𝑚)) = (𝐾‘𝑚))
202	197, 201	sylan 487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (abs‘(𝐾‘𝑚)) = (𝐾‘𝑚))
203	193, 195, 202	syl2anc 691	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑡 ∈ ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑡)) → (abs‘(𝐾‘𝑚)) = (𝐾‘𝑚))
204	203	breq1d 4593	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑡 ∈ ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑡)) → ((abs‘(𝐾‘𝑚)) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ↔ (𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))
205	204	ralbidva 2968	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑡 ∈ ℕ0) → (∀𝑚 ∈ (ℤ≥‘𝑡)(abs‘(𝐾‘𝑚)) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ↔ ∀𝑚 ∈ (ℤ≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))
206	171	breq1d 4593	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑚 → ((𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ↔ (𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))
207	206	cbvralv 3147	. . . . . . . . . . 11 ⊢ (∀𝑛 ∈ (ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ↔ ∀𝑚 ∈ (ℤ≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))
208	205, 207	syl6bbr 277	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑡 ∈ ℕ0) → (∀𝑚 ∈ (ℤ≥‘𝑡)(abs‘(𝐾‘𝑚)) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ↔ ∀𝑛 ∈ (ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))
209		simpll 786	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) → 𝜑)
210		mertens.1	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐹‘𝑗) = 𝐴)
211	209, 210	sylan 487	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) ∧ 𝑗 ∈ ℕ0) → (𝐹‘𝑗) = 𝐴)
212	209, 8	sylan 487	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) = (abs‘𝐴))
213	209, 9	sylan 487	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) ∧ 𝑗 ∈ ℕ0) → 𝐴 ∈ ℂ)
214	209, 20	sylan 487	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = 𝐵)
215	209, 21	sylan 487	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)
216		mertens.6	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐻‘𝑘) = Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗))))
217	209, 216	sylan 487	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) ∧ 𝑘 ∈ ℕ0) → (𝐻‘𝑘) = Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗))))
218	12	ad2antrr 758	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) → seq0( + , 𝐾) ∈ dom ⇝ )
219	22	ad2antrr 758	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) → seq0( + , 𝐺) ∈ dom ⇝ )
220	3	ad2antrr 758	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) → 𝐸 ∈ ℝ+)
221	207	anbi2i 726	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) ↔ (𝑡 ∈ ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))
222	221	anbi2i 726	. . . . . . . . . . . . . 14 ⊢ ((𝜓 ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) ↔ (𝜓 ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))))
223	222	biimpi 205	. . . . . . . . . . . . 13 ⊢ ((𝜓 ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) → (𝜓 ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))))
224	223	adantll 746	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) → (𝜓 ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))))
225	168, 165	jca 553	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → (0 ≤ sup(𝑇, ℝ, < ) ∧ (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧)))
226	225	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) → (0 ≤ sup(𝑇, ℝ, < ) ∧ (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧)))
227	211, 212, 213, 214, 215, 217, 218, 219, 220, 92, 85, 224, 226	mertenslem1 14455	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)
228	227	expr 641	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑡 ∈ ℕ0) → (∀𝑛 ∈ (ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸))
229	208, 228	sylbid 229	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑡 ∈ ℕ0) → (∀𝑚 ∈ (ℤ≥‘𝑡)(abs‘(𝐾‘𝑚)) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸))
230	229	rexlimdva 3013	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (∃𝑡 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑡)(abs‘(𝐾‘𝑚)) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸))
231	192, 230	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)
232	231	ex 449	. . . . . 6 ⊢ (𝜑 → (𝜓 → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸))
233	85, 232	syl5bir 232	. . . . 5 ⊢ (𝜑 → ((𝑠 ∈ ℕ ∧ ∀𝑛 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸))
234	233	expdimp 452	. . . 4 ⊢ ((𝜑 ∧ 𝑠 ∈ ℕ) → (∀𝑛 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸))
235	84, 234	sylbid 229	. . 3 ⊢ ((𝜑 ∧ 𝑠 ∈ ℕ) → (∀𝑚 ∈ (ℤ≥‘𝑠)(abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸))
236	235	rexlimdva 3013	. 2 ⊢ (𝜑 → (∃𝑠 ∈ ℕ ∀𝑚 ∈ (ℤ≥‘𝑠)(abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸))
237	24, 236	mpd 15	1 ⊢ (𝜑 → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  {cab 2596   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ⊆ wss 3540  ∅c0 3874   class class class wbr 4583   ↦ cmpt 4643   Or wor 4958  dom cdm 5038  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  Fincfn 7841  supcsup 8229  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820   < clt 9953   ≤ cle 9954   − cmin 10145   / cdiv 10563  ℕcn 10897  2c2 10947  ℕ₀cn0 11169  ℤ_≥cuz 11563  ℝ⁺crp 11708  ...cfz 12197  seqcseq 12663  abscabs 13822   ⇝ cli 14063  Σcsu 14264

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893  ax-addf 9894  ax-mulf 9895

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-rp 11709  df-ico 12052  df-fz 12198  df-fzo 12335  df-fl 12455  df-seq 12664  df-exp 12723  df-hash 12980  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-limsup 14050  df-clim 14067  df-rlim 14068  df-sum 14265

This theorem is referenced by:  mertens  14457