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 15840

Description: Lemma for mertens 15842. (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 495	. . . . . 6 ⊢ (𝜑 → 𝜓)
3		mertens.11	. . . . . 6 ⊢ (𝜓 ↔ (𝑠 ∈ ℕ ∧ ∀𝑛 ∈ (ℤ_≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
4	2, 3	sylib 219	. . . . 5 ⊢ (𝜑 → (𝑠 ∈ ℕ ∧ ∀𝑛 ∈ (ℤ_≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
5	4	simpld 495	. . . 4 ⊢ (𝜑 → 𝑠 ∈ ℕ)
6	5	nnnn0d 12489	. . 3 ⊢ (𝜑 → 𝑠 ∈ ℕ₀)
7	1	simprd 496	. . . 4 ⊢ (𝜑 → (𝑡 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))
8	7	simpld 495	. . 3 ⊢ (𝜑 → 𝑡 ∈ ℕ₀)
9	6, 8	nn0addcld 12493	. 2 ⊢ (𝜑 → (𝑠 + 𝑡) ∈ ℕ₀)
10		fzfid 13926	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (0...𝑚) ∈ Fin)
11		simpl 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝜑)
12		elfznn0 13565	. . . . . . . 8 ⊢ (𝑗 ∈ (0...𝑚) → 𝑗 ∈ ℕ₀)
13		mertens.3	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → 𝐴 ∈ ℂ)
14	11, 12, 13	syl2an 602	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → 𝐴 ∈ ℂ)
15		eqid 2739	. . . . . . . 8 ⊢ (ℤ_≥‘((𝑚 − 𝑗) + 1)) = (ℤ_≥‘((𝑚 − 𝑗) + 1))
16		fznn0sub 13501	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...𝑚) → (𝑚 − 𝑗) ∈ ℕ₀)
17	16	adantl 482	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (𝑚 − 𝑗) ∈ ℕ₀)
18		peano2nn0 12468	. . . . . . . . . 10 ⊢ ((𝑚 − 𝑗) ∈ ℕ₀ → ((𝑚 − 𝑗) + 1) ∈ ℕ₀)
19	17, 18	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((𝑚 − 𝑗) + 1) ∈ ℕ₀)
20	19	nn0zd 12540	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((𝑚 − 𝑗) + 1) ∈ ℤ)
21		simplll 780	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝜑)
22		eluznn0 12858	. . . . . . . . . 10 ⊢ ((((𝑚 − 𝑗) + 1) ∈ ℕ₀ ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ₀)
23	19, 22	sylan 586	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ₀)
24		mertens.4	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝐺‘𝑘) = 𝐵)
25	21, 23, 24	syl2anc 590	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → (𝐺‘𝑘) = 𝐵)
26		mertens.5	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → 𝐵 ∈ ℂ)
27	21, 23, 26	syl2anc 590	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝐵 ∈ ℂ)
28		mertens.8	. . . . . . . . . 10 ⊢ (𝜑 → seq0( + , 𝐺) ∈ dom ⇝ )
29	28	ad2antrr 732	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → seq0( + , 𝐺) ∈ dom ⇝ )
30		nn0uz 12817	. . . . . . . . . 10 ⊢ ℕ₀ = (ℤ_≥‘0)
31		simpll 772	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → 𝜑)
32	24, 26	eqeltrd 2839	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝐺‘𝑘) ∈ ℂ)
33	31, 32	sylan 586	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ ℕ₀) → (𝐺‘𝑘) ∈ ℂ)
34	30, 19, 33	iserex 15610	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (seq0( + , 𝐺) ∈ dom ⇝ ↔ seq((𝑚 − 𝑗) + 1)( + , 𝐺) ∈ dom ⇝ ))
35	29, 34	mpbid 233	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → seq((𝑚 − 𝑗) + 1)( + , 𝐺) ∈ dom ⇝ )
36	15, 20, 25, 27, 35	isumcl 15714	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵 ∈ ℂ)
37	14, 36	mulcld 11156	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℂ)
38	10, 37	fsumcl 15686	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℂ)
39	38	abscld 15392	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
40	37	abscld 15392	. . . . 5 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
41	10, 40	fsumrecl 15687	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
42		mertens.9	. . . . . 6 ⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
43	42	rpred 12977	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ ℝ)
44	43	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝐸 ∈ ℝ)
45	10, 37	fsumabs 15755	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)))
46		fzfid 13926	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (0...(𝑚 − 𝑠)) ∈ Fin)
47	6	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑠 ∈ ℕ₀)
48	47	nn0ge0d 12492	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 0 ≤ 𝑠)
49		eluzelz 12789	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡)) → 𝑚 ∈ ℤ)
50	49	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑚 ∈ ℤ)
51	50	zred 12624	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑚 ∈ ℝ)
52	47	nn0red 12490	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑠 ∈ ℝ)
53	51, 52	subge02d 11733	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (0 ≤ 𝑠 ↔ (𝑚 − 𝑠) ≤ 𝑚))
54	48, 53	mpbid 233	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ≤ 𝑚)
55	47, 30	eleqtrdi 2849	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑠 ∈ (ℤ_≥‘0))
56	5	nnzd 12541	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑠 ∈ ℤ)
57		uzid 12794	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ ℤ → 𝑠 ∈ (ℤ_≥‘𝑠))
58	56, 57	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑠 ∈ (ℤ_≥‘𝑠))
59		uzaddcl 12845	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 ∈ (ℤ_≥‘𝑠) ∧ 𝑡 ∈ ℕ₀) → (𝑠 + 𝑡) ∈ (ℤ_≥‘𝑠))
60	58, 8, 59	syl2anc 590	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑠 + 𝑡) ∈ (ℤ_≥‘𝑠))
61		eqid 2739	. . . . . . . . . . . . . . . . 17 ⊢ (ℤ_≥‘𝑠) = (ℤ_≥‘𝑠)
62	61	uztrn2 12798	. . . . . . . . . . . . . . . 16 ⊢ (((𝑠 + 𝑡) ∈ (ℤ_≥‘𝑠) ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑚 ∈ (ℤ_≥‘𝑠))
63	60, 62	sylan 586	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑚 ∈ (ℤ_≥‘𝑠))
64		elfzuzb 13463	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ (0...𝑚) ↔ (𝑠 ∈ (ℤ_≥‘0) ∧ 𝑚 ∈ (ℤ_≥‘𝑠)))
65	55, 63, 64	sylanbrc 589	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑠 ∈ (0...𝑚))
66		fznn0sub2 13580	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ (0...𝑚) → (𝑚 − 𝑠) ∈ (0...𝑚))
67	65, 66	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ (0...𝑚))
68		elfzelz 13469	. . . . . . . . . . . . 13 ⊢ ((𝑚 − 𝑠) ∈ (0...𝑚) → (𝑚 − 𝑠) ∈ ℤ)
69	67, 68	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ ℤ)
70		eluz 12793	. . . . . . . . . . . 12 ⊢ (((𝑚 − 𝑠) ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑚 ∈ (ℤ_≥‘(𝑚 − 𝑠)) ↔ (𝑚 − 𝑠) ≤ 𝑚))
71	69, 50, 70	syl2anc 590	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 ∈ (ℤ_≥‘(𝑚 − 𝑠)) ↔ (𝑚 − 𝑠) ≤ 𝑚))
72	54, 71	mpbird 258	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑚 ∈ (ℤ_≥‘(𝑚 − 𝑠)))
73		fzss2 13509	. . . . . . . . . 10 ⊢ (𝑚 ∈ (ℤ_≥‘(𝑚 − 𝑠)) → (0...(𝑚 − 𝑠)) ⊆ (0...𝑚))
74	72, 73	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (0...(𝑚 − 𝑠)) ⊆ (0...𝑚))
75	74	sselda 3915	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑗 ∈ (0...𝑚))
76	13	abscld 15392	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (abs‘𝐴) ∈ ℝ)
77	11, 12, 76	syl2an 602	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘𝐴) ∈ ℝ)
78	36	abscld 15392	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ)
79	77, 78	remulcld 11166	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
80	75, 79	syldan 597	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
81	46, 80	fsumrecl 15687	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
82		fzfid 13926	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (((𝑚 − 𝑠) + 1)...𝑚) ∈ Fin)
83		elfznn0 13565	. . . . . . . . . . . . 13 ⊢ ((𝑚 − 𝑠) ∈ (0...𝑚) → (𝑚 − 𝑠) ∈ ℕ₀)
84	67, 83	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ ℕ₀)
85		peano2nn0 12468	. . . . . . . . . . . 12 ⊢ ((𝑚 − 𝑠) ∈ ℕ₀ → ((𝑚 − 𝑠) + 1) ∈ ℕ₀)
86	84, 85	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝑚 − 𝑠) + 1) ∈ ℕ₀)
87	86, 30	eleqtrdi 2849	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝑚 − 𝑠) + 1) ∈ (ℤ_≥‘0))
88		fzss1 13508	. . . . . . . . . 10 ⊢ (((𝑚 − 𝑠) + 1) ∈ (ℤ_≥‘0) → (((𝑚 − 𝑠) + 1)...𝑚) ⊆ (0...𝑚))
89	87, 88	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (((𝑚 − 𝑠) + 1)...𝑚) ⊆ (0...𝑚))
90	89	sselda 3915	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑗 ∈ (0...𝑚))
91	90, 79	syldan 597	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
92	82, 91	fsumrecl 15687	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
93	42	rphalfcld 12989	. . . . . . . 8 ⊢ (𝜑 → (𝐸 / 2) ∈ ℝ⁺)
94	93	rpred 12977	. . . . . . 7 ⊢ (𝜑 → (𝐸 / 2) ∈ ℝ)
95	94	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝐸 / 2) ∈ ℝ)
96		elfznn0 13565	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...(𝑚 − 𝑠)) → 𝑗 ∈ ℕ₀)
97	11, 96, 76	syl2an 602	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘𝐴) ∈ ℝ)
98	46, 97	fsumrecl 15687	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ∈ ℝ)
99	98, 95	remulcld 11166	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) ∈ ℝ)
100		0zd 12527	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ ℤ)
101		eqidd 2740	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (𝐾‘𝑗) = (𝐾‘𝑗))
102		mertens.2	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (𝐾‘𝑗) = (abs‘𝐴))
103	102, 76	eqeltrd 2839	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (𝐾‘𝑗) ∈ ℝ)
104		mertens.7	. . . . . . . . . . 11 ⊢ (𝜑 → seq0( + , 𝐾) ∈ dom ⇝ )
105	30, 100, 101, 103, 104	isumrecl 15718	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) ∈ ℝ)
106	13	absge0d 15400	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → 0 ≤ (abs‘𝐴))
107	106, 102	breqtrrd 5100	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → 0 ≤ (𝐾‘𝑗))
108	30, 100, 101, 103, 104, 107	isumge0 15719	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗))
109	105, 108	ge0p1rpd 13007	. . . . . . . . 9 ⊢ (𝜑 → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ⁺)
110	109	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ⁺)
111	99, 110	rerpdivcld 13008	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) ∈ ℝ)
112	93, 109	rpdivcld 12994	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) ∈ ℝ⁺)
113	112	rpred 12977	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) ∈ ℝ)
114	113	ad2antrr 732	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) ∈ ℝ)
115	97, 114	remulcld 11166	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))) ∈ ℝ)
116	75, 20	syldan 597	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((𝑚 − 𝑗) + 1) ∈ ℤ)
117		simplll 780	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝜑)
118	75, 19	syldan 597	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((𝑚 − 𝑗) + 1) ∈ ℕ₀)
119	118, 22	sylan 586	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ₀)
120	117, 119, 24	syl2anc 590	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → (𝐺‘𝑘) = 𝐵)
121	117, 119, 26	syl2anc 590	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝐵 ∈ ℂ)
122	75, 35	syldan 597	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → seq((𝑚 − 𝑗) + 1)( + , 𝐺) ∈ dom ⇝ )
123	15, 116, 120, 121, 122	isumcl 15714	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵 ∈ ℂ)
124	123	abscld 15392	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ)
125	76, 106	jca 516	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)))
126	11, 96, 125	syl2an 602	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)))
127	120	sumeq2dv 15655	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)
128	127	fveq2d 6831	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)) = (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵))
129		fvoveq1 7379	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = (𝑚 − 𝑗) → (ℤ_≥‘(𝑛 + 1)) = (ℤ_≥‘((𝑚 − 𝑗) + 1)))
130	129	sumeq1d 15653	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = (𝑚 − 𝑗) → Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘))
131	130	fveq2d 6831	. . . . . . . . . . . . . 14 ⊢ (𝑛 = (𝑚 − 𝑗) → (abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) = (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)))
132	131	breq1d 5082	. . . . . . . . . . . . 13 ⊢ (𝑛 = (𝑚 − 𝑗) → ((abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) ↔ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
133	4	simprd 496	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑛 ∈ (ℤ_≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
134	133	ad2antrr 732	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ∀𝑛 ∈ (ℤ_≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
135		elfzelz 13469	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...(𝑚 − 𝑠)) → 𝑗 ∈ ℤ)
136	135	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑗 ∈ ℤ)
137	136	zred 12624	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑗 ∈ ℝ)
138	49	ad2antlr 733	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑚 ∈ ℤ)
139	138	zred 12624	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑚 ∈ ℝ)
140	56	ad2antrr 732	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑠 ∈ ℤ)
141	140	zred 12624	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑠 ∈ ℝ)
142		elfzle2 13473	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...(𝑚 − 𝑠)) → 𝑗 ≤ (𝑚 − 𝑠))
143	142	adantl 482	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑗 ≤ (𝑚 − 𝑠))
144	137, 139, 141, 143	lesubd 11745	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑠 ≤ (𝑚 − 𝑗))
145	138, 136	zsubcld 12629	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (𝑚 − 𝑗) ∈ ℤ)
146		eluz 12793	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 ∈ ℤ ∧ (𝑚 − 𝑗) ∈ ℤ) → ((𝑚 − 𝑗) ∈ (ℤ_≥‘𝑠) ↔ 𝑠 ≤ (𝑚 − 𝑗)))
147	140, 145, 146	syl2anc 590	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((𝑚 − 𝑗) ∈ (ℤ_≥‘𝑠) ↔ 𝑠 ≤ (𝑚 − 𝑗)))
148	144, 147	mpbird 258	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (𝑚 − 𝑗) ∈ (ℤ_≥‘𝑠))
149	132, 134, 148	rspcdva 3561	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
150	128, 149	eqbrtrrd 5096	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
151	124, 114, 150	ltled 11285	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
152		lemul2a 12001	. . . . . . . . . 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 1381	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
154	46, 80, 115, 153	fsumle 15753	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
155	98	recnd 11164	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ∈ ℂ)
156	93	rpcnd 12979	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸 / 2) ∈ ℂ)
157	156	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝐸 / 2) ∈ ℂ)
158		peano2re 11310	. . . . . . . . . . . . 13 ⊢ (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) ∈ ℝ → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ)
159	105, 158	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ)
160	159	recnd 11164	. . . . . . . . . . 11 ⊢ (𝜑 → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℂ)
161	160	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℂ)
162	109	rpne0d 12982	. . . . . . . . . . 11 ⊢ (𝜑 → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ≠ 0)
163	162	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ≠ 0)
164	155, 157, 161, 163	divassd 11957	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) = (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
165		fveq2 6827	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑗 → (𝐾‘𝑛) = (𝐾‘𝑗))
166	165	cbvsumv 15649	. . . . . . . . . . . . . . . 16 ⊢ Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) = Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗)
167	166	oveq1i 7366	. . . . . . . . . . . . . . 15 ⊢ (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1) = (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)
168	167	oveq2i 7367	. . . . . . . . . . . . . 14 ⊢ ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1)) = ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))
169	168, 112	eqeltrid 2843	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1)) ∈ ℝ⁺)
170	169	rpcnd 12979	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1)) ∈ ℂ)
171	170	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1)) ∈ ℂ)
172	76	recnd 11164	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (abs‘𝐴) ∈ ℂ)
173	11, 96, 172	syl2an 602	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘𝐴) ∈ ℂ)
174	46, 171, 173	fsummulc1 15738	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1))) = Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1))))
175	168	oveq2i 7367	. . . . . . . . . 10 ⊢ (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1))) = (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
176	168	oveq2i 7367	. . . . . . . . . . . 12 ⊢ ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1))) = ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
177	176	a1i 11	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...(𝑚 − 𝑠)) → ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1))) = ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
178	177	sumeq2i 15651	. . . . . . . . . 10 ⊢ Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1))) = Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
179	174, 175, 178	3eqtr3g 2797	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))) = Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
180	164, 179	eqtrd 2774	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) = Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
181	154, 180	breqtrrd 5100	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
182	105	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) ∈ ℝ)
183	159	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ)
184		0zd 12527	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 0 ∈ ℤ)
185		fz0ssnn0 13567	. . . . . . . . . . . . 13 ⊢ (0...(𝑚 − 𝑠)) ⊆ ℕ₀
186	185	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (0...(𝑚 − 𝑠)) ⊆ ℕ₀)
187	102	adantlr 721	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ₀) → (𝐾‘𝑗) = (abs‘𝐴))
188	76	adantlr 721	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ₀) → (abs‘𝐴) ∈ ℝ)
189	106	adantlr 721	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ₀) → 0 ≤ (abs‘𝐴))
190	104	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → seq0( + , 𝐾) ∈ dom ⇝ )
191	30, 184, 46, 186, 187, 188, 189, 190	isumless 15801	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ≤ Σ𝑗 ∈ ℕ₀ (abs‘𝐴))
192	102	sumeq2dv 15655	. . . . . . . . . . . 12 ⊢ (𝜑 → Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) = Σ𝑗 ∈ ℕ₀ (abs‘𝐴))
193	192	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) = Σ𝑗 ∈ ℕ₀ (abs‘𝐴))
194	191, 193	breqtrrd 5100	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ≤ Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗))
195	105	ltp1d 12077	. . . . . . . . . . 11 ⊢ (𝜑 → Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))
196	195	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))
197	98, 182, 183, 194, 196	lelttrd 11295	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))
198	93	rpregt0d 12983	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 / 2) ∈ ℝ ∧ 0 < (𝐸 / 2)))
199	198	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝐸 / 2) ∈ ℝ ∧ 0 < (𝐸 / 2)))
200		ltmul1 11996	. . . . . . . . . 10 ⊢ ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ∈ ℝ ∧ (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ ∧ ((𝐸 / 2) ∈ ℝ ∧ 0 < (𝐸 / 2))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ↔ (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) · (𝐸 / 2))))
201	98, 183, 199, 200	syl3anc 1379	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ↔ (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) · (𝐸 / 2))))
202	197, 201	mpbid 233	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) · (𝐸 / 2)))
203	109	rpregt0d 12983	. . . . . . . . . 10 ⊢ (𝜑 → ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ ∧ 0 < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
204	203	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ ∧ 0 < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
205		ltdivmul 12022	. . . . . . . . 9 ⊢ (((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) ∈ ℝ ∧ (𝐸 / 2) ∈ ℝ ∧ ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ ∧ 0 < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))) → (((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) < (𝐸 / 2) ↔ (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) · (𝐸 / 2))))
206	99, 95, 204, 205	syl3anc 1379	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) < (𝐸 / 2) ↔ (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) · (𝐸 / 2))))
207	202, 206	mpbird 258	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) < (𝐸 / 2))
208	81, 111, 95, 181, 207	lelttrd 11295	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < (𝐸 / 2))
209		mertens.13	. . . . . . . . . . . 12 ⊢ (𝜑 → (0 ≤ sup(𝑇, ℝ, < ) ∧ (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧)))
210	209	simprd 496	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧))
211		suprcl 12107	. . . . . . . . . . 11 ⊢ ((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧) → sup(𝑇, ℝ, < ) ∈ ℝ)
212	210, 211	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → sup(𝑇, ℝ, < ) ∈ ℝ)
213	94, 212	remulcld 11166	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 / 2) · sup(𝑇, ℝ, < )) ∈ ℝ)
214	209	simpld 495	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ sup(𝑇, ℝ, < ))
215	212, 214	ge0p1rpd 13007	. . . . . . . . 9 ⊢ (𝜑 → (sup(𝑇, ℝ, < ) + 1) ∈ ℝ⁺)
216	213, 215	rerpdivcld 13008	. . . . . . . 8 ⊢ (𝜑 → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℝ)
217	216	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℝ)
218	5	nnrpd 12975	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑠 ∈ ℝ⁺)
219	93, 218	rpdivcld 12994	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐸 / 2) / 𝑠) ∈ ℝ⁺)
220	219, 215	rpdivcld 12994	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℝ⁺)
221	220	rpred 12977	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℝ)
222	221, 212	remulcld 11166	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈ ℝ)
223	222	ad2antrr 732	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈ ℝ)
224		simpll 772	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝜑)
225	90, 12	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑗 ∈ ℕ₀)
226	224, 225, 76	syl2anc 590	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘𝐴) ∈ ℝ)
227	221	ad2antrr 732	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℝ)
228	224, 225, 102	syl2anc 590	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝐾‘𝑗) = (abs‘𝐴))
229		fveq2 6827	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑗 → (𝐾‘𝑚) = (𝐾‘𝑗))
230	229	breq1d 5082	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑗 → ((𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ↔ (𝐾‘𝑗) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))
231	7	simprd 496	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑚 ∈ (ℤ_≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))
232	231	ad2antrr 732	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ∀𝑚 ∈ (ℤ_≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))
233		elfzuz 13465	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚) → 𝑗 ∈ (ℤ_≥‘((𝑚 − 𝑠) + 1)))
234		eluzle 12792	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡)) → (𝑠 + 𝑡) ≤ 𝑚)
235	234	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑠 + 𝑡) ≤ 𝑚)
236	8	nn0zd 12540	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑡 ∈ ℤ)
237	236	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑡 ∈ ℤ)
238	237	zred 12624	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑡 ∈ ℝ)
239	52, 238, 51	leaddsub2d 11743	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝑠 + 𝑡) ≤ 𝑚 ↔ 𝑡 ≤ (𝑚 − 𝑠)))
240	235, 239	mpbid 233	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑡 ≤ (𝑚 − 𝑠))
241		eluz 12793	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑡 ∈ ℤ ∧ (𝑚 − 𝑠) ∈ ℤ) → ((𝑚 − 𝑠) ∈ (ℤ_≥‘𝑡) ↔ 𝑡 ≤ (𝑚 − 𝑠)))
242	237, 69, 241	syl2anc 590	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝑚 − 𝑠) ∈ (ℤ_≥‘𝑡) ↔ 𝑡 ≤ (𝑚 − 𝑠)))
243	240, 242	mpbird 258	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ (ℤ_≥‘𝑡))
244		peano2uz 12842	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 − 𝑠) ∈ (ℤ_≥‘𝑡) → ((𝑚 − 𝑠) + 1) ∈ (ℤ_≥‘𝑡))
245	243, 244	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝑚 − 𝑠) + 1) ∈ (ℤ_≥‘𝑡))
246		uztrn 12797	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ (ℤ_≥‘((𝑚 − 𝑠) + 1)) ∧ ((𝑚 − 𝑠) + 1) ∈ (ℤ_≥‘𝑡)) → 𝑗 ∈ (ℤ_≥‘𝑡))
247	233, 245, 246	syl2anr 603	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑗 ∈ (ℤ_≥‘𝑡))
248	230, 232, 247	rspcdva 3561	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝐾‘𝑗) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))
249	228, 248	eqbrtrrd 5096	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘𝐴) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))
250	226, 227, 249	ltled 11285	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘𝐴) ≤ (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))
251	210	ad2antrr 732	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧))
252	51	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑚 ∈ ℝ)
253		peano2zm 12561	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ ℤ → (𝑠 − 1) ∈ ℤ)
254	56, 253	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑠 − 1) ∈ ℤ)
255	254	zred 12624	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑠 − 1) ∈ ℝ)
256	255	ad2antrr 732	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑠 − 1) ∈ ℝ)
257	225	nn0red 12490	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑗 ∈ ℝ)
258	50	zcnd 12625	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑚 ∈ ℂ)
259	52	recnd 11164	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑠 ∈ ℂ)
260		1cnd 11130	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 1 ∈ ℂ)
261	258, 259, 260	subsubd 11524	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − (𝑠 − 1)) = ((𝑚 − 𝑠) + 1))
262	261	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − (𝑠 − 1)) = ((𝑚 − 𝑠) + 1))
263		elfzle1 13472	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚) → ((𝑚 − 𝑠) + 1) ≤ 𝑗)
264	263	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((𝑚 − 𝑠) + 1) ≤ 𝑗)
265	262, 264	eqbrtrd 5094	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − (𝑠 − 1)) ≤ 𝑗)
266	252, 256, 257, 265	subled 11744	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − 𝑗) ≤ (𝑠 − 1))
267	90, 16	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − 𝑗) ∈ ℕ₀)
268	267, 30	eleqtrdi 2849	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − 𝑗) ∈ (ℤ_≥‘0))
269	254	ad2antrr 732	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑠 − 1) ∈ ℤ)
270		elfz5 13461	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 − 𝑗) ∈ (ℤ_≥‘0) ∧ (𝑠 − 1) ∈ ℤ) → ((𝑚 − 𝑗) ∈ (0...(𝑠 − 1)) ↔ (𝑚 − 𝑗) ≤ (𝑠 − 1)))
271	268, 269, 270	syl2anc 590	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((𝑚 − 𝑗) ∈ (0...(𝑠 − 1)) ↔ (𝑚 − 𝑗) ≤ (𝑠 − 1)))
272	266, 271	mpbird 258	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − 𝑗) ∈ (0...(𝑠 − 1)))
273		simplll 780	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝜑)
274	90, 19	syldan 597	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((𝑚 − 𝑗) + 1) ∈ ℕ₀)
275	274, 22	sylan 586	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ₀)
276	273, 275, 24	syl2anc 590	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → (𝐺‘𝑘) = 𝐵)
277	276	sumeq2dv 15655	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)
278	277	eqcomd 2745	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵 = Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘))
279	278	fveq2d 6831	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)))
280	131	rspceeqv 3583	. . . . . . . . . . . . 13 ⊢ (((𝑚 − 𝑗) ∈ (0...(𝑠 − 1)) ∧ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘))) → ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)))
281	272, 279, 280	syl2anc 590	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)))
282		fvex 6840	. . . . . . . . . . . . 13 ⊢ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ V
283		eqeq1 2743	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) → (𝑧 = (abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) ↔ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘))))
284	283	rexbidv 3163	. . . . . . . . . . . . 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 3620	. . . . . . . . . . . 12 ⊢ ((abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ 𝑇 ↔ ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)))
287	281, 286	sylibr 235	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ 𝑇)
288		suprub 12108	. . . . . . . . . . 11 ⊢ (((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧) ∧ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ 𝑇) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ sup(𝑇, ℝ, < ))
289	251, 287, 288	syl2anc 590	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ sup(𝑇, ℝ, < ))
290	224, 225, 125	syl2anc 590	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)))
291	90, 78	syldan 597	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ)
292	36	absge0d 15400	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → 0 ≤ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵))
293	90, 292	syldan 597	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 0 ≤ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵))
294	291, 293	jca 516	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ ∧ 0 ≤ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)))
295	212	ad2antrr 732	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → sup(𝑇, ℝ, < ) ∈ ℝ)
296		lemul12a 12004	. . . . . . . . . . 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 844	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (((abs‘𝐴) ≤ (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∧ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ sup(𝑇, ℝ, < )) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))))
298	250, 289, 297	mp2and 705	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )))
299	82, 91, 223, 298	fsumle 15753	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )))
300	222	recnd 11164	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈ ℂ)
301	300	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈ ℂ)
302		fsumconst 15743	. . . . . . . . . 10 ⊢ (((((𝑚 − 𝑠) + 1)...𝑚) ∈ Fin ∧ ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈ ℂ) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) = ((♯‘(((𝑚 − 𝑠) + 1)...𝑚)) · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))))
303	82, 301, 302	syl2anc 590	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) = ((♯‘(((𝑚 − 𝑠) + 1)...𝑚)) · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))))
304		1zzd 12549	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 1 ∈ ℤ)
305	56	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑠 ∈ ℤ)
306		fzen 13486	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ (𝑚 − 𝑠) ∈ ℤ) → (1...𝑠) ≈ ((1 + (𝑚 − 𝑠))...(𝑠 + (𝑚 − 𝑠))))
307	304, 305, 69, 306	syl3anc 1379	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (1...𝑠) ≈ ((1 + (𝑚 − 𝑠))...(𝑠 + (𝑚 − 𝑠))))
308		ax-1cn 11087	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
309	69	zcnd 12625	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ ℂ)
310		addcom 11323	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℂ ∧ (𝑚 − 𝑠) ∈ ℂ) → (1 + (𝑚 − 𝑠)) = ((𝑚 − 𝑠) + 1))
311	308, 309, 310	sylancr 593	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (1 + (𝑚 − 𝑠)) = ((𝑚 − 𝑠) + 1))
312	259, 258	pncan3d 11499	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑠 + (𝑚 − 𝑠)) = 𝑚)
313	311, 312	oveq12d 7374	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((1 + (𝑚 − 𝑠))...(𝑠 + (𝑚 − 𝑠))) = (((𝑚 − 𝑠) + 1)...𝑚))
314	307, 313	breqtrd 5098	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (1...𝑠) ≈ (((𝑚 − 𝑠) + 1)...𝑚))
315		fzfid 13926	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (1...𝑠) ∈ Fin)
316		hashen 14300	. . . . . . . . . . . . 13 ⊢ (((1...𝑠) ∈ Fin ∧ (((𝑚 − 𝑠) + 1)...𝑚) ∈ Fin) → ((♯‘(1...𝑠)) = (♯‘(((𝑚 − 𝑠) + 1)...𝑚)) ↔ (1...𝑠) ≈ (((𝑚 − 𝑠) + 1)...𝑚)))
317	315, 82, 316	syl2anc 590	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((♯‘(1...𝑠)) = (♯‘(((𝑚 − 𝑠) + 1)...𝑚)) ↔ (1...𝑠) ≈ (((𝑚 − 𝑠) + 1)...𝑚)))
318	314, 317	mpbird 258	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (♯‘(1...𝑠)) = (♯‘(((𝑚 − 𝑠) + 1)...𝑚)))
319		hashfz1 14299	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ℕ₀ → (♯‘(1...𝑠)) = 𝑠)
320	47, 319	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (♯‘(1...𝑠)) = 𝑠)
321	318, 320	eqtr3d 2776	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (♯‘(((𝑚 − 𝑠) + 1)...𝑚)) = 𝑠)
322	321	oveq1d 7371	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((♯‘(((𝑚 − 𝑠) + 1)...𝑚)) · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))) = (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))))
323	212	recnd 11164	. . . . . . . . . . . 12 ⊢ (𝜑 → sup(𝑇, ℝ, < ) ∈ ℂ)
324	215	rpcnne0d 12986	. . . . . . . . . . . 12 ⊢ (𝜑 → ((sup(𝑇, ℝ, < ) + 1) ∈ ℂ ∧ (sup(𝑇, ℝ, < ) + 1) ≠ 0))
325		div23 11819	. . . . . . . . . . . 12 ⊢ (((𝐸 / 2) ∈ ℂ ∧ sup(𝑇, ℝ, < ) ∈ ℂ ∧ ((sup(𝑇, ℝ, < ) + 1) ∈ ℂ ∧ (sup(𝑇, ℝ, < ) + 1) ≠ 0)) → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) = (((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )))
326	156, 323, 324, 325	syl3anc 1379	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) = (((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )))
327	56	zcnd 12625	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑠 ∈ ℂ)
328	219	rpcnd 12979	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐸 / 2) / 𝑠) ∈ ℂ)
329		divass 11818	. . . . . . . . . . . . . 14 ⊢ ((𝑠 ∈ ℂ ∧ ((𝐸 / 2) / 𝑠) ∈ ℂ ∧ ((sup(𝑇, ℝ, < ) + 1) ∈ ℂ ∧ (sup(𝑇, ℝ, < ) + 1) ≠ 0)) → ((𝑠 · ((𝐸 / 2) / 𝑠)) / (sup(𝑇, ℝ, < ) + 1)) = (𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))
330	327, 328, 324, 329	syl3anc 1379	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑠 · ((𝐸 / 2) / 𝑠)) / (sup(𝑇, ℝ, < ) + 1)) = (𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))
331	5	nnne0d 12218	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑠 ≠ 0)
332	156, 327, 331	divcan2d 11924	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑠 · ((𝐸 / 2) / 𝑠)) = (𝐸 / 2))
333	332	oveq1d 7371	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑠 · ((𝐸 / 2) / 𝑠)) / (sup(𝑇, ℝ, < ) + 1)) = ((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)))
334	330, 333	eqtr3d 2776	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) = ((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)))
335	334	oveq1d 7371	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) · sup(𝑇, ℝ, < )) = (((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )))
336	220	rpcnd 12979	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℂ)
337	327, 336, 323	mulassd 11159	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) · sup(𝑇, ℝ, < )) = (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))))
338	326, 335, 337	3eqtr2rd 2781	. . . . . . . . . 10 ⊢ (𝜑 → (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))) = (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)))
339	338	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))) = (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)))
340	303, 322, 339	3eqtrd 2778	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) = (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)))
341	299, 340	breqtrd 5098	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)))
342		peano2re 11310	. . . . . . . . . . 11 ⊢ (sup(𝑇, ℝ, < ) ∈ ℝ → (sup(𝑇, ℝ, < ) + 1) ∈ ℝ)
343	212, 342	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (sup(𝑇, ℝ, < ) + 1) ∈ ℝ)
344	212	ltp1d 12077	. . . . . . . . . 10 ⊢ (𝜑 → sup(𝑇, ℝ, < ) < (sup(𝑇, ℝ, < ) + 1))
345	212, 343, 93, 344	ltmul2dd 13033	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 / 2) · sup(𝑇, ℝ, < )) < ((𝐸 / 2) · (sup(𝑇, ℝ, < ) + 1)))
346	213, 94, 215	ltdivmul2d 13029	. . . . . . . . 9 ⊢ (𝜑 → ((((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) < (𝐸 / 2) ↔ ((𝐸 / 2) · sup(𝑇, ℝ, < )) < ((𝐸 / 2) · (sup(𝑇, ℝ, < ) + 1))))
347	345, 346	mpbird 258	. . . . . . . 8 ⊢ (𝜑 → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) < (𝐸 / 2))
348	347	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) < (𝐸 / 2))
349	92, 217, 95, 341, 348	lelttrd 11295	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < (𝐸 / 2))
350	81, 92, 95, 95, 208, 349	lt2addd 11764	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) + Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵))) < ((𝐸 / 2) + (𝐸 / 2)))
351	14, 36	absmuld 15410	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) = ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)))
352	351	sumeq2dv 15655	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) = Σ𝑗 ∈ (0...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)))
353	69	zred 12624	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ ℝ)
354	353	ltp1d 12077	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) < ((𝑚 − 𝑠) + 1))
355		fzdisj 13496	. . . . . . . 8 ⊢ ((𝑚 − 𝑠) < ((𝑚 − 𝑠) + 1) → ((0...(𝑚 − 𝑠)) ∩ (((𝑚 − 𝑠) + 1)...𝑚)) = ∅)
356	354, 355	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((0...(𝑚 − 𝑠)) ∩ (((𝑚 − 𝑠) + 1)...𝑚)) = ∅)
357		fzsplit 13495	. . . . . . . 8 ⊢ ((𝑚 − 𝑠) ∈ (0...𝑚) → (0...𝑚) = ((0...(𝑚 − 𝑠)) ∪ (((𝑚 − 𝑠) + 1)...𝑚)))
358	67, 357	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (0...𝑚) = ((0...(𝑚 − 𝑠)) ∪ (((𝑚 − 𝑠) + 1)...𝑚)))
359	79	recnd 11164	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℂ)
360	356, 358, 10, 359	fsumsplit 15694	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) = (Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) + Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵))))
361	352, 360	eqtr2d 2775	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) + Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵))) = Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)))
362	42	rpcnd 12979	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ ℂ)
363	362	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝐸 ∈ ℂ)
364	363	2halvesd 12414	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝐸 / 2) + (𝐸 / 2)) = 𝐸)
365	350, 361, 364	3brtr3d 5103	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)
366	39, 41, 44, 45, 365	lelttrd 11295	. . 3 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)
367	366	ralrimiva 3131	. 2 ⊢ (𝜑 → ∀𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)
368		fveq2 6827	. . . 4 ⊢ (𝑦 = (𝑠 + 𝑡) → (ℤ_≥‘𝑦) = (ℤ_≥‘(𝑠 + 𝑡)))
369	368	raleqdv 3297	. . 3 ⊢ (𝑦 = (𝑠 + 𝑡) → (∀𝑚 ∈ (ℤ_≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸 ↔ ∀𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸))
370	369	rspcev 3560	. 2 ⊢ (((𝑠 + 𝑡) ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸) → ∃𝑦 ∈ ℕ₀ ∀𝑚 ∈ (ℤ_≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)
371	9, 367, 370	syl2anc 590	1 ⊢ (𝜑 → ∃𝑦 ∈ ℕ₀ ∀𝑚 ∈ (ℤ_≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 ∧ w3a 1092 = wceq 1547 ∈ wcel 2119 {cab 2717 ≠ wne 2934 ∀wral 3053 ∃wrex 3063 ∪ cun 3881 ∩ cin 3882 ⊆ wss 3883 ∅c0 4261 class class class wbr 5072 dom cdm 5618 ‘cfv 6485 (class class class)co 7356 ≈ cen 8880 Fincfn 8883 supcsup 9343 ℂcc 11027 ℝcr 11028 0cc0 11029 1c1 11030 + caddc 11032 · cmul 11034 < clt 11170 ≤ cle 11171 − cmin 11368 / cdiv 11798 ℕcn 12165 2c2 12227 ℕ₀cn0 12428 ℤcz 12515 ℤ_≥cuz 12779 ℝ⁺crp 12933 ...cfz 13452 seqcseq 13954 ♯chash 14283 abscabs 15187 ⇝ cli 15437 Σcsu 15639

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-rep 5199 ax-sep 5218 ax-nul 5228 ax-pow 5294 ax-pr 5362 ax-un 7678 ax-inf2 9553 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106 ax-pre-sup 11107

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-nel 3039 df-ral 3054 df-rex 3064 df-rmo 3344 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3903 df-nul 4262 df-if 4455 df-pw 4531 df-sn 4556 df-pr 4558 df-op 4562 df-uni 4839 df-int 4878 df-iun 4923 df-br 5073 df-opab 5135 df-mpt 5154 df-tr 5180 df-id 5513 df-eprel 5518 df-po 5526 df-so 5527 df-fr 5571 df-se 5572 df-we 5573 df-xp 5624 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-res 5630 df-ima 5631 df-pred 6252 df-ord 6313 df-on 6314 df-lim 6315 df-suc 6316 df-iota 6441 df-fun 6487 df-fn 6488 df-f 6489 df-f1 6490 df-fo 6491 df-f1o 6492 df-fv 6493 df-isom 6494 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-om 7807 df-1st 7931 df-2nd 7932 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-er 8633 df-pm 8766 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-sup 9345 df-inf 9346 df-oi 9415 df-card 9854 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-div 11799 df-nn 12166 df-2 12235 df-3 12236 df-n0 12429 df-z 12516 df-uz 12780 df-rp 12934 df-ico 13295 df-fz 13453 df-fzo 13600 df-fl 13742 df-seq 13955 df-exp 14015 df-hash 14284 df-cj 15052 df-re 15053 df-im 15054 df-sqrt 15188 df-abs 15189 df-clim 15441 df-rlim 15442 df-sum 15640

This theorem is referenced by: mertenslem2 15841

W3C validator