mertenslem1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > mertenslem1		Structured version Visualization version GIF version

Theorem mertenslem1 15914

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

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

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

Distinct variable groups: 𝑗,𝑚,𝑛,𝑠,𝑡,𝑦,𝑧,𝐵 𝑗,𝑘,𝐺,𝑚,𝑛,𝑠,𝑦,𝑧 𝜑,𝑗,𝑘,𝑚,𝑦,𝑧 𝑡,𝑘,𝐴,𝑚,𝑛,𝑠,𝑦 𝑗,𝐸,𝑘,𝑚,𝑛,𝑠,𝑡,𝑦,𝑧 𝑗,𝐾,𝑘,𝑚,𝑛,𝑠,𝑡,𝑦,𝑧 𝑗,𝐹,𝑚,𝑛,𝑦 𝜓,𝑗,𝑘,𝑚,𝑛,𝑡,𝑦,𝑧 𝑤,𝑗,𝑇,𝑘,𝑚,𝑛,𝑡,𝑦,𝑧 𝑘,𝐻,𝑚,𝑦 Allowed substitution hints: 𝜑(𝑤,𝑡,𝑛,𝑠) 𝜓(𝑤,𝑠) 𝐴(𝑧,𝑤,𝑗) 𝐵(𝑤,𝑘) 𝑇(𝑠) 𝐸(𝑤) 𝐹(𝑧,𝑤,𝑡,𝑘,𝑠) 𝐺(𝑤,𝑡) 𝐻(𝑧,𝑤,𝑡,𝑗,𝑛,𝑠) 𝐾(𝑤)

**Proof of Theorem mertenslem1**
Step	Hyp	Ref	Expression
1		mertens.12	. . . . . . 7 ⊢ (𝜑 → (𝜓 ∧ (𝑡 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))))
2	1	simpld 498	. . . . . 6 ⊢ (𝜑 → 𝜓)
3		mertens.11	. . . . . 6 ⊢ (𝜓 ↔ (𝑠 ∈ ℕ ∧ ∀𝑛 ∈ (ℤ_≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
4	2, 3	sylib 220	. . . . 5 ⊢ (𝜑 → (𝑠 ∈ ℕ ∧ ∀𝑛 ∈ (ℤ_≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
5	4	simpld 498	. . . 4 ⊢ (𝜑 → 𝑠 ∈ ℕ)
6	5	nnnn0d 12542	. . 3 ⊢ (𝜑 → 𝑠 ∈ ℕ₀)
7	1	simprd 499	. . . 4 ⊢ (𝜑 → (𝑡 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))
8	7	simpld 498	. . 3 ⊢ (𝜑 → 𝑡 ∈ ℕ₀)
9	6, 8	nn0addcld 12546	. 2 ⊢ (𝜑 → (𝑠 + 𝑡) ∈ ℕ₀)
10		fzfid 13986	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (0...𝑚) ∈ Fin)
11		simpl 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝜑)
12		elfznn0 13625	. . . . . . . 8 ⊢ (𝑗 ∈ (0...𝑚) → 𝑗 ∈ ℕ₀)
13		mertens.3	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → 𝐴 ∈ ℂ)
14	11, 12, 13	syl2an 605	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → 𝐴 ∈ ℂ)
15		eqid 2762	. . . . . . . 8 ⊢ (ℤ_≥‘((𝑚 − 𝑗) + 1)) = (ℤ_≥‘((𝑚 − 𝑗) + 1))
16		fznn0sub 13561	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...𝑚) → (𝑚 − 𝑗) ∈ ℕ₀)
17	16	adantl 485	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (𝑚 − 𝑗) ∈ ℕ₀)
18		peano2nn0 12521	. . . . . . . . . 10 ⊢ ((𝑚 − 𝑗) ∈ ℕ₀ → ((𝑚 − 𝑗) + 1) ∈ ℕ₀)
19	17, 18	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((𝑚 − 𝑗) + 1) ∈ ℕ₀)
20	19	nn0zd 12593	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((𝑚 − 𝑗) + 1) ∈ ℤ)
21		simplll 784	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝜑)
22		eluznn0 12918	. . . . . . . . . 10 ⊢ ((((𝑚 − 𝑗) + 1) ∈ ℕ₀ ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ₀)
23	19, 22	sylan 589	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ₀)
24		mertens.4	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝐺‘𝑘) = 𝐵)
25	21, 23, 24	syl2anc 593	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → (𝐺‘𝑘) = 𝐵)
26		mertens.5	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → 𝐵 ∈ ℂ)
27	21, 23, 26	syl2anc 593	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝐵 ∈ ℂ)
28		mertens.8	. . . . . . . . . 10 ⊢ (𝜑 → seq0( + , 𝐺) ∈ dom ⇝ )
29	28	ad2antrr 736	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → seq0( + , 𝐺) ∈ dom ⇝ )
30		nn0uz 12877	. . . . . . . . . 10 ⊢ ℕ₀ = (ℤ_≥‘0)
31		simpll 776	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → 𝜑)
32	24, 26	eqeltrd 2862	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝐺‘𝑘) ∈ ℂ)
33	31, 32	sylan 589	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ ℕ₀) → (𝐺‘𝑘) ∈ ℂ)
34	30, 19, 33	iserex 15684	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (seq0( + , 𝐺) ∈ dom ⇝ ↔ seq((𝑚 − 𝑗) + 1)( + , 𝐺) ∈ dom ⇝ ))
35	29, 34	mpbid 234	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → seq((𝑚 − 𝑗) + 1)( + , 𝐺) ∈ dom ⇝ )
36	15, 20, 25, 27, 35	isumcl 15788	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵 ∈ ℂ)
37	14, 36	mulcld 11202	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℂ)
38	10, 37	fsumcl 15760	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℂ)
39	38	abscld 15466	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
40	37	abscld 15466	. . . . 5 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
41	10, 40	fsumrecl 15761	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
42		mertens.9	. . . . . 6 ⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
43	42	rpred 13037	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ ℝ)
44	43	adantr 484	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝐸 ∈ ℝ)
45	10, 37	fsumabs 15829	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)))
46		fzfid 13986	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (0...(𝑚 − 𝑠)) ∈ Fin)
47	6	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑠 ∈ ℕ₀)
48	47	nn0ge0d 12545	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 0 ≤ 𝑠)
49		eluzelz 12849	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡)) → 𝑚 ∈ ℤ)
50	49	adantl 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑚 ∈ ℤ)
51	50	zred 12677	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑚 ∈ ℝ)
52	47	nn0red 12543	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑠 ∈ ℝ)
53	51, 52	subge02d 11779	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (0 ≤ 𝑠 ↔ (𝑚 − 𝑠) ≤ 𝑚))
54	48, 53	mpbid 234	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ≤ 𝑚)
55	47, 30	eleqtrdi 2872	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑠 ∈ (ℤ_≥‘0))
56	5	nnzd 12594	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑠 ∈ ℤ)
57		uzid 12854	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ ℤ → 𝑠 ∈ (ℤ_≥‘𝑠))
58	56, 57	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑠 ∈ (ℤ_≥‘𝑠))
59		uzaddcl 12905	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 ∈ (ℤ_≥‘𝑠) ∧ 𝑡 ∈ ℕ₀) → (𝑠 + 𝑡) ∈ (ℤ_≥‘𝑠))
60	58, 8, 59	syl2anc 593	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑠 + 𝑡) ∈ (ℤ_≥‘𝑠))
61		eqid 2762	. . . . . . . . . . . . . . . . 17 ⊢ (ℤ_≥‘𝑠) = (ℤ_≥‘𝑠)
62	61	uztrn2 12858	. . . . . . . . . . . . . . . 16 ⊢ (((𝑠 + 𝑡) ∈ (ℤ_≥‘𝑠) ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑚 ∈ (ℤ_≥‘𝑠))
63	60, 62	sylan 589	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑚 ∈ (ℤ_≥‘𝑠))
64		elfzuzb 13523	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ (0...𝑚) ↔ (𝑠 ∈ (ℤ_≥‘0) ∧ 𝑚 ∈ (ℤ_≥‘𝑠)))
65	55, 63, 64	sylanbrc 592	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑠 ∈ (0...𝑚))
66		fznn0sub2 13640	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ (0...𝑚) → (𝑚 − 𝑠) ∈ (0...𝑚))
67	65, 66	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ (0...𝑚))
68		elfzelz 13529	. . . . . . . . . . . . 13 ⊢ ((𝑚 − 𝑠) ∈ (0...𝑚) → (𝑚 − 𝑠) ∈ ℤ)
69	67, 68	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ ℤ)
70		eluz 12853	. . . . . . . . . . . 12 ⊢ (((𝑚 − 𝑠) ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑚 ∈ (ℤ_≥‘(𝑚 − 𝑠)) ↔ (𝑚 − 𝑠) ≤ 𝑚))
71	69, 50, 70	syl2anc 593	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 ∈ (ℤ_≥‘(𝑚 − 𝑠)) ↔ (𝑚 − 𝑠) ≤ 𝑚))
72	54, 71	mpbird 259	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑚 ∈ (ℤ_≥‘(𝑚 − 𝑠)))
73		fzss2 13569	. . . . . . . . . 10 ⊢ (𝑚 ∈ (ℤ_≥‘(𝑚 − 𝑠)) → (0...(𝑚 − 𝑠)) ⊆ (0...𝑚))
74	72, 73	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (0...(𝑚 − 𝑠)) ⊆ (0...𝑚))
75	74	sselda 3936	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑗 ∈ (0...𝑚))
76	13	abscld 15466	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (abs‘𝐴) ∈ ℝ)
77	11, 12, 76	syl2an 605	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘𝐴) ∈ ℝ)
78	36	abscld 15466	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ)
79	77, 78	remulcld 11212	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
80	75, 79	syldan 600	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
81	46, 80	fsumrecl 15761	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
82		fzfid 13986	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (((𝑚 − 𝑠) + 1)...𝑚) ∈ Fin)
83		elfznn0 13625	. . . . . . . . . . . . 13 ⊢ ((𝑚 − 𝑠) ∈ (0...𝑚) → (𝑚 − 𝑠) ∈ ℕ₀)
84	67, 83	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ ℕ₀)
85		peano2nn0 12521	. . . . . . . . . . . 12 ⊢ ((𝑚 − 𝑠) ∈ ℕ₀ → ((𝑚 − 𝑠) + 1) ∈ ℕ₀)
86	84, 85	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝑚 − 𝑠) + 1) ∈ ℕ₀)
87	86, 30	eleqtrdi 2872	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝑚 − 𝑠) + 1) ∈ (ℤ_≥‘0))
88		fzss1 13568	. . . . . . . . . 10 ⊢ (((𝑚 − 𝑠) + 1) ∈ (ℤ_≥‘0) → (((𝑚 − 𝑠) + 1)...𝑚) ⊆ (0...𝑚))
89	87, 88	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (((𝑚 − 𝑠) + 1)...𝑚) ⊆ (0...𝑚))
90	89	sselda 3936	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑗 ∈ (0...𝑚))
91	90, 79	syldan 600	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
92	82, 91	fsumrecl 15761	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
93	42	rphalfcld 13049	. . . . . . . 8 ⊢ (𝜑 → (𝐸 / 2) ∈ ℝ⁺)
94	93	rpred 13037	. . . . . . 7 ⊢ (𝜑 → (𝐸 / 2) ∈ ℝ)
95	94	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝐸 / 2) ∈ ℝ)
96		elfznn0 13625	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...(𝑚 − 𝑠)) → 𝑗 ∈ ℕ₀)
97	11, 96, 76	syl2an 605	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘𝐴) ∈ ℝ)
98	46, 97	fsumrecl 15761	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ∈ ℝ)
99	98, 95	remulcld 11212	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) ∈ ℝ)
100		0zd 12580	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ ℤ)
101		eqidd 2763	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (𝐾‘𝑗) = (𝐾‘𝑗))
102		mertens.2	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (𝐾‘𝑗) = (abs‘𝐴))
103	102, 76	eqeltrd 2862	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (𝐾‘𝑗) ∈ ℝ)
104		mertens.7	. . . . . . . . . . 11 ⊢ (𝜑 → seq0( + , 𝐾) ∈ dom ⇝ )
105	30, 100, 101, 103, 104	isumrecl 15792	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) ∈ ℝ)
106	13	absge0d 15474	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → 0 ≤ (abs‘𝐴))
107	106, 102	breqtrrd 5128	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → 0 ≤ (𝐾‘𝑗))
108	30, 100, 101, 103, 104, 107	isumge0 15793	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗))
109	105, 108	ge0p1rpd 13067	. . . . . . . . 9 ⊢ (𝜑 → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ⁺)
110	109	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ⁺)
111	99, 110	rerpdivcld 13068	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) ∈ ℝ)
112	93, 109	rpdivcld 13054	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) ∈ ℝ⁺)
113	112	rpred 13037	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) ∈ ℝ)
114	113	ad2antrr 736	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) ∈ ℝ)
115	97, 114	remulcld 11212	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))) ∈ ℝ)
116	75, 20	syldan 600	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((𝑚 − 𝑗) + 1) ∈ ℤ)
117		simplll 784	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝜑)
118	75, 19	syldan 600	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((𝑚 − 𝑗) + 1) ∈ ℕ₀)
119	118, 22	sylan 589	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ₀)
120	117, 119, 24	syl2anc 593	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → (𝐺‘𝑘) = 𝐵)
121	117, 119, 26	syl2anc 593	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝐵 ∈ ℂ)
122	75, 35	syldan 600	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → seq((𝑚 − 𝑗) + 1)( + , 𝐺) ∈ dom ⇝ )
123	15, 116, 120, 121, 122	isumcl 15788	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵 ∈ ℂ)
124	123	abscld 15466	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ)
125	76, 106	jca 519	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)))
126	11, 96, 125	syl2an 605	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)))
127	120	sumeq2dv 15729	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)
128	127	fveq2d 6871	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)) = (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵))
129		fvoveq1 7419	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = (𝑚 − 𝑗) → (ℤ_≥‘(𝑛 + 1)) = (ℤ_≥‘((𝑚 − 𝑗) + 1)))
130	129	sumeq1d 15727	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = (𝑚 − 𝑗) → Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘))
131	130	fveq2d 6871	. . . . . . . . . . . . . 14 ⊢ (𝑛 = (𝑚 − 𝑗) → (abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) = (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)))
132	131	breq1d 5110	. . . . . . . . . . . . 13 ⊢ (𝑛 = (𝑚 − 𝑗) → ((abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) ↔ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
133	4	simprd 499	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑛 ∈ (ℤ_≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
134	133	ad2antrr 736	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ∀𝑛 ∈ (ℤ_≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
135		elfzelz 13529	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...(𝑚 − 𝑠)) → 𝑗 ∈ ℤ)
136	135	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑗 ∈ ℤ)
137	136	zred 12677	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑗 ∈ ℝ)
138	49	ad2antlr 737	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑚 ∈ ℤ)
139	138	zred 12677	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑚 ∈ ℝ)
140	56	ad2antrr 736	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑠 ∈ ℤ)
141	140	zred 12677	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑠 ∈ ℝ)
142		elfzle2 13533	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...(𝑚 − 𝑠)) → 𝑗 ≤ (𝑚 − 𝑠))
143	142	adantl 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑗 ≤ (𝑚 − 𝑠))
144	137, 139, 141, 143	lesubd 11791	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑠 ≤ (𝑚 − 𝑗))
145	138, 136	zsubcld 12682	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (𝑚 − 𝑗) ∈ ℤ)
146		eluz 12853	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 ∈ ℤ ∧ (𝑚 − 𝑗) ∈ ℤ) → ((𝑚 − 𝑗) ∈ (ℤ_≥‘𝑠) ↔ 𝑠 ≤ (𝑚 − 𝑗)))
147	140, 145, 146	syl2anc 593	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((𝑚 − 𝑗) ∈ (ℤ_≥‘𝑠) ↔ 𝑠 ≤ (𝑚 − 𝑗)))
148	144, 147	mpbird 259	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (𝑚 − 𝑗) ∈ (ℤ_≥‘𝑠))
149	132, 134, 148	rspcdva 3582	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
150	128, 149	eqbrtrrd 5124	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
151	124, 114, 150	ltled 11331	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
152		lemul2a 12046	. . . . . . . . . 10 ⊢ ((((abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ ∧ ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) ∈ ℝ ∧ ((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴))) ∧ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
153	124, 114, 126, 151, 152	syl31anc 1392	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
154	46, 80, 115, 153	fsumle 15827	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
155	98	recnd 11210	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ∈ ℂ)
156	93	rpcnd 13039	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸 / 2) ∈ ℂ)
157	156	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝐸 / 2) ∈ ℂ)
158		peano2re 11356	. . . . . . . . . . . . 13 ⊢ (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) ∈ ℝ → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ)
159	105, 158	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ)
160	159	recnd 11210	. . . . . . . . . . 11 ⊢ (𝜑 → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℂ)
161	160	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℂ)
162	109	rpne0d 13042	. . . . . . . . . . 11 ⊢ (𝜑 → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ≠ 0)
163	162	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ≠ 0)
164	155, 157, 161, 163	divassd 12002	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) = (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
165		fveq2 6867	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑗 → (𝐾‘𝑛) = (𝐾‘𝑗))
166	165	cbvsumv 15723	. . . . . . . . . . . . . . . 16 ⊢ Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) = Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗)
167	166	oveq1i 7406	. . . . . . . . . . . . . . 15 ⊢ (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1) = (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)
168	167	oveq2i 7407	. . . . . . . . . . . . . 14 ⊢ ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1)) = ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))
169	168, 112	eqeltrid 2866	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1)) ∈ ℝ⁺)
170	169	rpcnd 13039	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1)) ∈ ℂ)
171	170	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1)) ∈ ℂ)
172	76	recnd 11210	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (abs‘𝐴) ∈ ℂ)
173	11, 96, 172	syl2an 605	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘𝐴) ∈ ℂ)
174	46, 171, 173	fsummulc1 15812	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1))) = Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1))))
175	168	oveq2i 7407	. . . . . . . . . 10 ⊢ (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1))) = (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
176	168	oveq2i 7407	. . . . . . . . . . . 12 ⊢ ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1))) = ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
177	176	a1i 11	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...(𝑚 − 𝑠)) → ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1))) = ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
178	177	sumeq2i 15725	. . . . . . . . . 10 ⊢ Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1))) = Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
179	174, 175, 178	3eqtr3g 2820	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))) = Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
180	164, 179	eqtrd 2797	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) = Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
181	154, 180	breqtrrd 5128	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
182	105	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) ∈ ℝ)
183	159	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ)
184		0zd 12580	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 0 ∈ ℤ)
185		fz0ssnn0 13627	. . . . . . . . . . . . 13 ⊢ (0...(𝑚 − 𝑠)) ⊆ ℕ₀
186	185	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (0...(𝑚 − 𝑠)) ⊆ ℕ₀)
187	102	adantlr 725	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ₀) → (𝐾‘𝑗) = (abs‘𝐴))
188	76	adantlr 725	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ₀) → (abs‘𝐴) ∈ ℝ)
189	106	adantlr 725	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ₀) → 0 ≤ (abs‘𝐴))
190	104	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → seq0( + , 𝐾) ∈ dom ⇝ )
191	30, 184, 46, 186, 187, 188, 189, 190	isumless 15875	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ≤ Σ𝑗 ∈ ℕ₀ (abs‘𝐴))
192	102	sumeq2dv 15729	. . . . . . . . . . . 12 ⊢ (𝜑 → Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) = Σ𝑗 ∈ ℕ₀ (abs‘𝐴))
193	192	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) = Σ𝑗 ∈ ℕ₀ (abs‘𝐴))
194	191, 193	breqtrrd 5128	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ≤ Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗))
195	105	ltp1d 12122	. . . . . . . . . . 11 ⊢ (𝜑 → Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))
196	195	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))
197	98, 182, 183, 194, 196	lelttrd 11341	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))
198	93	rpregt0d 13043	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 / 2) ∈ ℝ ∧ 0 < (𝐸 / 2)))
199	198	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝐸 / 2) ∈ ℝ ∧ 0 < (𝐸 / 2)))
200		ltmul1 12041	. . . . . . . . . 10 ⊢ ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ∈ ℝ ∧ (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ ∧ ((𝐸 / 2) ∈ ℝ ∧ 0 < (𝐸 / 2))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ↔ (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) · (𝐸 / 2))))
201	98, 183, 199, 200	syl3anc 1390	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ↔ (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) · (𝐸 / 2))))
202	197, 201	mpbid 234	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) · (𝐸 / 2)))
203	109	rpregt0d 13043	. . . . . . . . . 10 ⊢ (𝜑 → ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ ∧ 0 < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
204	203	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ ∧ 0 < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
205		ltdivmul 12067	. . . . . . . . 9 ⊢ (((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) ∈ ℝ ∧ (𝐸 / 2) ∈ ℝ ∧ ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ ∧ 0 < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))) → (((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) < (𝐸 / 2) ↔ (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) · (𝐸 / 2))))
206	99, 95, 204, 205	syl3anc 1390	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) < (𝐸 / 2) ↔ (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) · (𝐸 / 2))))
207	202, 206	mpbird 259	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) < (𝐸 / 2))
208	81, 111, 95, 181, 207	lelttrd 11341	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < (𝐸 / 2))
209		mertens.13	. . . . . . . . . . . 12 ⊢ (𝜑 → (0 ≤ sup(𝑇, ℝ, < ) ∧ (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧)))
210	209	simprd 499	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧))
211		suprcl 12152	. . . . . . . . . . 11 ⊢ ((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧) → sup(𝑇, ℝ, < ) ∈ ℝ)
212	210, 211	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → sup(𝑇, ℝ, < ) ∈ ℝ)
213	94, 212	remulcld 11212	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 / 2) · sup(𝑇, ℝ, < )) ∈ ℝ)
214	209	simpld 498	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ sup(𝑇, ℝ, < ))
215	212, 214	ge0p1rpd 13067	. . . . . . . . 9 ⊢ (𝜑 → (sup(𝑇, ℝ, < ) + 1) ∈ ℝ⁺)
216	213, 215	rerpdivcld 13068	. . . . . . . 8 ⊢ (𝜑 → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℝ)
217	216	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℝ)
218	5	nnrpd 13035	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑠 ∈ ℝ⁺)
219	93, 218	rpdivcld 13054	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐸 / 2) / 𝑠) ∈ ℝ⁺)
220	219, 215	rpdivcld 13054	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℝ⁺)
221	220	rpred 13037	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℝ)
222	221, 212	remulcld 11212	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈ ℝ)
223	222	ad2antrr 736	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈ ℝ)
224		simpll 776	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝜑)
225	90, 12	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑗 ∈ ℕ₀)
226	224, 225, 76	syl2anc 593	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘𝐴) ∈ ℝ)
227	221	ad2antrr 736	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℝ)
228	224, 225, 102	syl2anc 593	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝐾‘𝑗) = (abs‘𝐴))
229		fveq2 6867	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑗 → (𝐾‘𝑚) = (𝐾‘𝑗))
230	229	breq1d 5110	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑗 → ((𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ↔ (𝐾‘𝑗) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))
231	7	simprd 499	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑚 ∈ (ℤ_≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))
232	231	ad2antrr 736	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ∀𝑚 ∈ (ℤ_≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))
233		elfzuz 13525	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚) → 𝑗 ∈ (ℤ_≥‘((𝑚 − 𝑠) + 1)))
234		eluzle 12852	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡)) → (𝑠 + 𝑡) ≤ 𝑚)
235	234	adantl 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑠 + 𝑡) ≤ 𝑚)
236	8	nn0zd 12593	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑡 ∈ ℤ)
237	236	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑡 ∈ ℤ)
238	237	zred 12677	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑡 ∈ ℝ)
239	52, 238, 51	leaddsub2d 11789	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝑠 + 𝑡) ≤ 𝑚 ↔ 𝑡 ≤ (𝑚 − 𝑠)))
240	235, 239	mpbid 234	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑡 ≤ (𝑚 − 𝑠))
241		eluz 12853	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑡 ∈ ℤ ∧ (𝑚 − 𝑠) ∈ ℤ) → ((𝑚 − 𝑠) ∈ (ℤ_≥‘𝑡) ↔ 𝑡 ≤ (𝑚 − 𝑠)))
242	237, 69, 241	syl2anc 593	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝑚 − 𝑠) ∈ (ℤ_≥‘𝑡) ↔ 𝑡 ≤ (𝑚 − 𝑠)))
243	240, 242	mpbird 259	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ (ℤ_≥‘𝑡))
244		peano2uz 12902	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 − 𝑠) ∈ (ℤ_≥‘𝑡) → ((𝑚 − 𝑠) + 1) ∈ (ℤ_≥‘𝑡))
245	243, 244	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝑚 − 𝑠) + 1) ∈ (ℤ_≥‘𝑡))
246		uztrn 12857	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ (ℤ_≥‘((𝑚 − 𝑠) + 1)) ∧ ((𝑚 − 𝑠) + 1) ∈ (ℤ_≥‘𝑡)) → 𝑗 ∈ (ℤ_≥‘𝑡))
247	233, 245, 246	syl2anr 606	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑗 ∈ (ℤ_≥‘𝑡))
248	230, 232, 247	rspcdva 3582	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝐾‘𝑗) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))
249	228, 248	eqbrtrrd 5124	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘𝐴) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))
250	226, 227, 249	ltled 11331	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘𝐴) ≤ (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))
251	210	ad2antrr 736	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧))
252	51	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑚 ∈ ℝ)
253		peano2zm 12614	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ ℤ → (𝑠 − 1) ∈ ℤ)
254	56, 253	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑠 − 1) ∈ ℤ)
255	254	zred 12677	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑠 − 1) ∈ ℝ)
256	255	ad2antrr 736	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑠 − 1) ∈ ℝ)
257	225	nn0red 12543	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑗 ∈ ℝ)
258	50	zcnd 12678	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑚 ∈ ℂ)
259	52	recnd 11210	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑠 ∈ ℂ)
260		1cnd 11175	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 1 ∈ ℂ)
261	258, 259, 260	subsubd 11570	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − (𝑠 − 1)) = ((𝑚 − 𝑠) + 1))
262	261	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − (𝑠 − 1)) = ((𝑚 − 𝑠) + 1))
263		elfzle1 13532	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚) → ((𝑚 − 𝑠) + 1) ≤ 𝑗)
264	263	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((𝑚 − 𝑠) + 1) ≤ 𝑗)
265	262, 264	eqbrtrd 5122	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − (𝑠 − 1)) ≤ 𝑗)
266	252, 256, 257, 265	subled 11790	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − 𝑗) ≤ (𝑠 − 1))
267	90, 16	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − 𝑗) ∈ ℕ₀)
268	267, 30	eleqtrdi 2872	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − 𝑗) ∈ (ℤ_≥‘0))
269	254	ad2antrr 736	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑠 − 1) ∈ ℤ)
270		elfz5 13521	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 − 𝑗) ∈ (ℤ_≥‘0) ∧ (𝑠 − 1) ∈ ℤ) → ((𝑚 − 𝑗) ∈ (0...(𝑠 − 1)) ↔ (𝑚 − 𝑗) ≤ (𝑠 − 1)))
271	268, 269, 270	syl2anc 593	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((𝑚 − 𝑗) ∈ (0...(𝑠 − 1)) ↔ (𝑚 − 𝑗) ≤ (𝑠 − 1)))
272	266, 271	mpbird 259	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − 𝑗) ∈ (0...(𝑠 − 1)))
273		simplll 784	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝜑)
274	90, 19	syldan 600	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((𝑚 − 𝑗) + 1) ∈ ℕ₀)
275	274, 22	sylan 589	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ₀)
276	273, 275, 24	syl2anc 593	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → (𝐺‘𝑘) = 𝐵)
277	276	sumeq2dv 15729	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)
278	277	eqcomd 2768	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵 = Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘))
279	278	fveq2d 6871	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)))
280	131	rspceeqv 3604	. . . . . . . . . . . . 13 ⊢ (((𝑚 − 𝑗) ∈ (0...(𝑠 − 1)) ∧ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘))) → ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)))
281	272, 279, 280	syl2anc 593	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)))
282		fvex 6880	. . . . . . . . . . . . 13 ⊢ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ V
283		eqeq1 2766	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) → (𝑧 = (abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) ↔ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘))))
284	283	rexbidv 3186	. . . . . . . . . . . . 13 ⊢ (𝑧 = (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) → (∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) ↔ ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘))))
285		mertens.10	. . . . . . . . . . . . 13 ⊢ 𝑇 = {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘))}
286	282, 284, 285	elab2 3641	. . . . . . . . . . . 12 ⊢ ((abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ 𝑇 ↔ ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)))
287	281, 286	sylibr 236	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ 𝑇)
288		suprub 12153	. . . . . . . . . . 11 ⊢ (((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧) ∧ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ 𝑇) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ sup(𝑇, ℝ, < ))
289	251, 287, 288	syl2anc 593	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ sup(𝑇, ℝ, < ))
290	224, 225, 125	syl2anc 593	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)))
291	90, 78	syldan 600	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ)
292	36	absge0d 15474	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → 0 ≤ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵))
293	90, 292	syldan 600	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 0 ≤ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵))
294	291, 293	jca 519	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ ∧ 0 ≤ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)))
295	212	ad2antrr 736	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → sup(𝑇, ℝ, < ) ∈ ℝ)
296		lemul12a 12049	. . . . . . . . . . 11 ⊢ (((((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)) ∧ (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℝ) ∧ (((abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ ∧ 0 ≤ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∧ sup(𝑇, ℝ, < ) ∈ ℝ)) → (((abs‘𝐴) ≤ (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∧ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ sup(𝑇, ℝ, < )) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))))
297	290, 227, 294, 295, 296	syl22anc 849	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (((abs‘𝐴) ≤ (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∧ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ sup(𝑇, ℝ, < )) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))))
298	250, 289, 297	mp2and 709	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )))
299	82, 91, 223, 298	fsumle 15827	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )))
300	222	recnd 11210	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈ ℂ)
301	300	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈ ℂ)
302		fsumconst 15817	. . . . . . . . . 10 ⊢ (((((𝑚 − 𝑠) + 1)...𝑚) ∈ Fin ∧ ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈ ℂ) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) = ((♯‘(((𝑚 − 𝑠) + 1)...𝑚)) · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))))
303	82, 301, 302	syl2anc 593	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) = ((♯‘(((𝑚 − 𝑠) + 1)...𝑚)) · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))))
304		1zzd 12602	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 1 ∈ ℤ)
305	56	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑠 ∈ ℤ)
306		fzen 13546	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ (𝑚 − 𝑠) ∈ ℤ) → (1...𝑠) ≈ ((1 + (𝑚 − 𝑠))...(𝑠 + (𝑚 − 𝑠))))
307	304, 305, 69, 306	syl3anc 1390	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (1...𝑠) ≈ ((1 + (𝑚 − 𝑠))...(𝑠 + (𝑚 − 𝑠))))
308		ax-1cn 11131	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
309	69	zcnd 12678	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ ℂ)
310		addcom 11369	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℂ ∧ (𝑚 − 𝑠) ∈ ℂ) → (1 + (𝑚 − 𝑠)) = ((𝑚 − 𝑠) + 1))
311	308, 309, 310	sylancr 596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (1 + (𝑚 − 𝑠)) = ((𝑚 − 𝑠) + 1))
312	259, 258	pncan3d 11545	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑠 + (𝑚 − 𝑠)) = 𝑚)
313	311, 312	oveq12d 7414	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((1 + (𝑚 − 𝑠))...(𝑠 + (𝑚 − 𝑠))) = (((𝑚 − 𝑠) + 1)...𝑚))
314	307, 313	breqtrd 5126	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (1...𝑠) ≈ (((𝑚 − 𝑠) + 1)...𝑚))
315		fzfid 13986	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (1...𝑠) ∈ Fin)
316		hashen 14360	. . . . . . . . . . . . 13 ⊢ (((1...𝑠) ∈ Fin ∧ (((𝑚 − 𝑠) + 1)...𝑚) ∈ Fin) → ((♯‘(1...𝑠)) = (♯‘(((𝑚 − 𝑠) + 1)...𝑚)) ↔ (1...𝑠) ≈ (((𝑚 − 𝑠) + 1)...𝑚)))
317	315, 82, 316	syl2anc 593	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((♯‘(1...𝑠)) = (♯‘(((𝑚 − 𝑠) + 1)...𝑚)) ↔ (1...𝑠) ≈ (((𝑚 − 𝑠) + 1)...𝑚)))
318	314, 317	mpbird 259	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (♯‘(1...𝑠)) = (♯‘(((𝑚 − 𝑠) + 1)...𝑚)))
319		hashfz1 14359	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ℕ₀ → (♯‘(1...𝑠)) = 𝑠)
320	47, 319	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (♯‘(1...𝑠)) = 𝑠)
321	318, 320	eqtr3d 2799	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (♯‘(((𝑚 − 𝑠) + 1)...𝑚)) = 𝑠)
322	321	oveq1d 7411	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((♯‘(((𝑚 − 𝑠) + 1)...𝑚)) · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))) = (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))))
323	212	recnd 11210	. . . . . . . . . . . 12 ⊢ (𝜑 → sup(𝑇, ℝ, < ) ∈ ℂ)
324	215	rpcnne0d 13046	. . . . . . . . . . . 12 ⊢ (𝜑 → ((sup(𝑇, ℝ, < ) + 1) ∈ ℂ ∧ (sup(𝑇, ℝ, < ) + 1) ≠ 0))
325		div23 11864	. . . . . . . . . . . 12 ⊢ (((𝐸 / 2) ∈ ℂ ∧ sup(𝑇, ℝ, < ) ∈ ℂ ∧ ((sup(𝑇, ℝ, < ) + 1) ∈ ℂ ∧ (sup(𝑇, ℝ, < ) + 1) ≠ 0)) → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) = (((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )))
326	156, 323, 324, 325	syl3anc 1390	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) = (((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )))
327	56	zcnd 12678	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑠 ∈ ℂ)
328	219	rpcnd 13039	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐸 / 2) / 𝑠) ∈ ℂ)
329		divass 11863	. . . . . . . . . . . . . 14 ⊢ ((𝑠 ∈ ℂ ∧ ((𝐸 / 2) / 𝑠) ∈ ℂ ∧ ((sup(𝑇, ℝ, < ) + 1) ∈ ℂ ∧ (sup(𝑇, ℝ, < ) + 1) ≠ 0)) → ((𝑠 · ((𝐸 / 2) / 𝑠)) / (sup(𝑇, ℝ, < ) + 1)) = (𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))
330	327, 328, 324, 329	syl3anc 1390	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑠 · ((𝐸 / 2) / 𝑠)) / (sup(𝑇, ℝ, < ) + 1)) = (𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))
331	5	nnne0d 12263	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑠 ≠ 0)
332	156, 327, 331	divcan2d 11969	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑠 · ((𝐸 / 2) / 𝑠)) = (𝐸 / 2))
333	332	oveq1d 7411	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑠 · ((𝐸 / 2) / 𝑠)) / (sup(𝑇, ℝ, < ) + 1)) = ((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)))
334	330, 333	eqtr3d 2799	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) = ((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)))
335	334	oveq1d 7411	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) · sup(𝑇, ℝ, < )) = (((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )))
336	220	rpcnd 13039	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℂ)
337	327, 336, 323	mulassd 11205	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) · sup(𝑇, ℝ, < )) = (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))))
338	326, 335, 337	3eqtr2rd 2804	. . . . . . . . . 10 ⊢ (𝜑 → (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))) = (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)))
339	338	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))) = (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)))
340	303, 322, 339	3eqtrd 2801	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) = (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)))
341	299, 340	breqtrd 5126	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)))
342		peano2re 11356	. . . . . . . . . . 11 ⊢ (sup(𝑇, ℝ, < ) ∈ ℝ → (sup(𝑇, ℝ, < ) + 1) ∈ ℝ)
343	212, 342	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (sup(𝑇, ℝ, < ) + 1) ∈ ℝ)
344	212	ltp1d 12122	. . . . . . . . . 10 ⊢ (𝜑 → sup(𝑇, ℝ, < ) < (sup(𝑇, ℝ, < ) + 1))
345	212, 343, 93, 344	ltmul2dd 13093	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 / 2) · sup(𝑇, ℝ, < )) < ((𝐸 / 2) · (sup(𝑇, ℝ, < ) + 1)))
346	213, 94, 215	ltdivmul2d 13089	. . . . . . . . 9 ⊢ (𝜑 → ((((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) < (𝐸 / 2) ↔ ((𝐸 / 2) · sup(𝑇, ℝ, < )) < ((𝐸 / 2) · (sup(𝑇, ℝ, < ) + 1))))
347	345, 346	mpbird 259	. . . . . . . 8 ⊢ (𝜑 → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) < (𝐸 / 2))
348	347	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) < (𝐸 / 2))
349	92, 217, 95, 341, 348	lelttrd 11341	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < (𝐸 / 2))
350	81, 92, 95, 95, 208, 349	lt2addd 11810	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) + Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵))) < ((𝐸 / 2) + (𝐸 / 2)))
351	14, 36	absmuld 15484	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) = ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)))
352	351	sumeq2dv 15729	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) = Σ𝑗 ∈ (0...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)))
353	69	zred 12677	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ ℝ)
354	353	ltp1d 12122	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) < ((𝑚 − 𝑠) + 1))
355		fzdisj 13556	. . . . . . . 8 ⊢ ((𝑚 − 𝑠) < ((𝑚 − 𝑠) + 1) → ((0...(𝑚 − 𝑠)) ∩ (((𝑚 − 𝑠) + 1)...𝑚)) = ∅)
356	354, 355	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((0...(𝑚 − 𝑠)) ∩ (((𝑚 − 𝑠) + 1)...𝑚)) = ∅)
357		fzsplit 13555	. . . . . . . 8 ⊢ ((𝑚 − 𝑠) ∈ (0...𝑚) → (0...𝑚) = ((0...(𝑚 − 𝑠)) ∪ (((𝑚 − 𝑠) + 1)...𝑚)))
358	67, 357	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (0...𝑚) = ((0...(𝑚 − 𝑠)) ∪ (((𝑚 − 𝑠) + 1)...𝑚)))
359	79	recnd 11210	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℂ)
360	356, 358, 10, 359	fsumsplit 15768	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) = (Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) + Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵))))
361	352, 360	eqtr2d 2798	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) + Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵))) = Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)))
362	42	rpcnd 13039	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ ℂ)
363	362	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝐸 ∈ ℂ)
364	363	2halvesd 12467	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝐸 / 2) + (𝐸 / 2)) = 𝐸)
365	350, 361, 364	3brtr3d 5131	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)
366	39, 41, 44, 45, 365	lelttrd 11341	. . 3 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)
367	366	ralrimiva 3154	. 2 ⊢ (𝜑 → ∀𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)
368		fveq2 6867	. . . 4 ⊢ (𝑦 = (𝑠 + 𝑡) → (ℤ_≥‘𝑦) = (ℤ_≥‘(𝑠 + 𝑡)))
369	368	raleqdv 3320	. . 3 ⊢ (𝑦 = (𝑠 + 𝑡) → (∀𝑚 ∈ (ℤ_≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸 ↔ ∀𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸))
370	369	rspcev 3581	. 2 ⊢ (((𝑠 + 𝑡) ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸) → ∃𝑦 ∈ ℕ₀ ∀𝑚 ∈ (ℤ_≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)
371	9, 367, 370	syl2anc 593	1 ⊢ (𝜑 → ∃𝑦 ∈ ℕ₀ ∀𝑚 ∈ (ℤ_≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 399 ∧ w3a 1098 = wceq 1560 ∈ wcel 2142 {cab 2740 ≠ wne 2957 ∀wral 3076 ∃wrex 3086 ∪ cun 3902 ∩ cin 3903 ⊆ wss 3904 ∅c0 4285 class class class wbr 5100 dom cdm 5647 ‘cfv 6521 (class class class)co 7396 ≈ cen 8924 Fincfn 8927 supcsup 9386 ℂcc 11071 ℝcr 11072 0cc0 11073 1c1 11074 + caddc 11076 · cmul 11078 < clt 11216 ≤ cle 11217 − cmin 11414 / cdiv 11844 ℕcn 12210 2c2 12272 ℕ₀cn0 12481 ℤcz 12568 ℤ_≥cuz 12839 ℝ⁺crp 12993 ...cfz 13512 seqcseq 14014 ♯chash 14343 abscabs 15261 ⇝ cli 15511 Σcsu 15713

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5227 ax-sep 5246 ax-nul 5256 ax-pow 5322 ax-pr 5390 ax-un 7718 ax-inf2 9596 ax-cnex 11129 ax-resscn 11130 ax-1cn 11131 ax-icn 11132 ax-addcl 11133 ax-addrcl 11134 ax-mulcl 11135 ax-mulrcl 11136 ax-mulcom 11137 ax-addass 11138 ax-mulass 11139 ax-distr 11140 ax-i2m1 11141 ax-1ne0 11142 ax-1rid 11143 ax-rnegex 11144 ax-rrecex 11145 ax-cnre 11146 ax-pre-lttri 11147 ax-pre-lttrn 11148 ax-pre-ltadd 11149 ax-pre-mulgt0 11150 ax-pre-sup 11151

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1099 df-3an 1100 df-tru 1563 df-fal 1573 df-ex 1800 df-nf 1804 df-sb 2091 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3456 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4481 df-pw 4557 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-int 4906 df-iun 4951 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5542 df-eprel 5547 df-po 5555 df-so 5556 df-fr 5600 df-se 5601 df-we 5602 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-pred 6288 df-ord 6349 df-on 6350 df-lim 6351 df-suc 6352 df-iota 6477 df-fun 6523 df-fn 6524 df-f 6525 df-f1 6526 df-fo 6527 df-f1o 6528 df-fv 6529 df-isom 6530 df-riota 7353 df-ov 7399 df-oprab 7400 df-mpo 7401 df-om 7847 df-1st 7970 df-2nd 7971 df-frecs 8262 df-wrecs 8293 df-recs 8342 df-rdg 8381 df-1o 8437 df-er 8678 df-pm 8811 df-en 8928 df-dom 8929 df-sdom 8930 df-fin 8931 df-sup 9388 df-inf 9389 df-oi 9458 df-card 9897 df-pnf 11218 df-mnf 11219 df-xr 11220 df-ltxr 11221 df-le 11222 df-sub 11416 df-neg 11417 df-div 11845 df-nn 12211 df-2 12280 df-3 12281 df-n0 12482 df-z 12569 df-uz 12840 df-rp 12994 df-ico 13355 df-fz 13513 df-fzo 13660 df-fl 13802 df-seq 14015 df-exp 14075 df-hash 14344 df-cj 15126 df-re 15127 df-im 15128 df-sqrt 15262 df-abs 15263 df-clim 15515 df-rlim 15516 df-sum 15714

This theorem is referenced by: mertenslem2 15915

W3C validator