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 15239

Description: Lemma for mertens 15241. (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 497	. . . . . 6 ⊢ (𝜑 → 𝜓)
3		mertens.11	. . . . . 6 ⊢ (𝜓 ↔ (𝑠 ∈ ℕ ∧ ∀𝑛 ∈ (ℤ_≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
4	2, 3	sylib 220	. . . . 5 ⊢ (𝜑 → (𝑠 ∈ ℕ ∧ ∀𝑛 ∈ (ℤ_≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
5	4	simpld 497	. . . 4 ⊢ (𝜑 → 𝑠 ∈ ℕ)
6	5	nnnn0d 11954	. . 3 ⊢ (𝜑 → 𝑠 ∈ ℕ₀)
7	1	simprd 498	. . . 4 ⊢ (𝜑 → (𝑡 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))
8	7	simpld 497	. . 3 ⊢ (𝜑 → 𝑡 ∈ ℕ₀)
9	6, 8	nn0addcld 11958	. 2 ⊢ (𝜑 → (𝑠 + 𝑡) ∈ ℕ₀)
10		fzfid 13340	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (0...𝑚) ∈ Fin)
11		simpl 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝜑)
12		elfznn0 12999	. . . . . . . 8 ⊢ (𝑗 ∈ (0...𝑚) → 𝑗 ∈ ℕ₀)
13		mertens.3	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → 𝐴 ∈ ℂ)
14	11, 12, 13	syl2an 597	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → 𝐴 ∈ ℂ)
15		eqid 2821	. . . . . . . 8 ⊢ (ℤ_≥‘((𝑚 − 𝑗) + 1)) = (ℤ_≥‘((𝑚 − 𝑗) + 1))
16		fznn0sub 12938	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...𝑚) → (𝑚 − 𝑗) ∈ ℕ₀)
17	16	adantl 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (𝑚 − 𝑗) ∈ ℕ₀)
18		peano2nn0 11936	. . . . . . . . . 10 ⊢ ((𝑚 − 𝑗) ∈ ℕ₀ → ((𝑚 − 𝑗) + 1) ∈ ℕ₀)
19	17, 18	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((𝑚 − 𝑗) + 1) ∈ ℕ₀)
20	19	nn0zd 12084	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((𝑚 − 𝑗) + 1) ∈ ℤ)
21		simplll 773	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝜑)
22		eluznn0 12316	. . . . . . . . . 10 ⊢ ((((𝑚 − 𝑗) + 1) ∈ ℕ₀ ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ₀)
23	19, 22	sylan 582	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ₀)
24		mertens.4	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝐺‘𝑘) = 𝐵)
25	21, 23, 24	syl2anc 586	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → (𝐺‘𝑘) = 𝐵)
26		mertens.5	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → 𝐵 ∈ ℂ)
27	21, 23, 26	syl2anc 586	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝐵 ∈ ℂ)
28		mertens.8	. . . . . . . . . 10 ⊢ (𝜑 → seq0( + , 𝐺) ∈ dom ⇝ )
29	28	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → seq0( + , 𝐺) ∈ dom ⇝ )
30		nn0uz 12279	. . . . . . . . . 10 ⊢ ℕ₀ = (ℤ_≥‘0)
31		simpll 765	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → 𝜑)
32	24, 26	eqeltrd 2913	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝐺‘𝑘) ∈ ℂ)
33	31, 32	sylan 582	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ ℕ₀) → (𝐺‘𝑘) ∈ ℂ)
34	30, 19, 33	iserex 15012	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (seq0( + , 𝐺) ∈ dom ⇝ ↔ seq((𝑚 − 𝑗) + 1)( + , 𝐺) ∈ dom ⇝ ))
35	29, 34	mpbid 234	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → seq((𝑚 − 𝑗) + 1)( + , 𝐺) ∈ dom ⇝ )
36	15, 20, 25, 27, 35	isumcl 15115	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵 ∈ ℂ)
37	14, 36	mulcld 10660	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℂ)
38	10, 37	fsumcl 15089	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℂ)
39	38	abscld 14795	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
40	37	abscld 14795	. . . . 5 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
41	10, 40	fsumrecl 15090	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
42		mertens.9	. . . . . 6 ⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
43	42	rpred 12430	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ ℝ)
44	43	adantr 483	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝐸 ∈ ℝ)
45	10, 37	fsumabs 15155	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)))
46		fzfid 13340	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (0...(𝑚 − 𝑠)) ∈ Fin)
47	6	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑠 ∈ ℕ₀)
48	47	nn0ge0d 11957	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 0 ≤ 𝑠)
49		eluzelz 12252	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡)) → 𝑚 ∈ ℤ)
50	49	adantl 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑚 ∈ ℤ)
51	50	zred 12086	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑚 ∈ ℝ)
52	47	nn0red 11955	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑠 ∈ ℝ)
53	51, 52	subge02d 11231	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (0 ≤ 𝑠 ↔ (𝑚 − 𝑠) ≤ 𝑚))
54	48, 53	mpbid 234	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ≤ 𝑚)
55	47, 30	eleqtrdi 2923	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑠 ∈ (ℤ_≥‘0))
56	5	nnzd 12085	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑠 ∈ ℤ)
57		uzid 12257	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ ℤ → 𝑠 ∈ (ℤ_≥‘𝑠))
58	56, 57	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑠 ∈ (ℤ_≥‘𝑠))
59		uzaddcl 12303	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 ∈ (ℤ_≥‘𝑠) ∧ 𝑡 ∈ ℕ₀) → (𝑠 + 𝑡) ∈ (ℤ_≥‘𝑠))
60	58, 8, 59	syl2anc 586	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑠 + 𝑡) ∈ (ℤ_≥‘𝑠))
61		eqid 2821	. . . . . . . . . . . . . . . . 17 ⊢ (ℤ_≥‘𝑠) = (ℤ_≥‘𝑠)
62	61	uztrn2 12261	. . . . . . . . . . . . . . . 16 ⊢ (((𝑠 + 𝑡) ∈ (ℤ_≥‘𝑠) ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑚 ∈ (ℤ_≥‘𝑠))
63	60, 62	sylan 582	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑚 ∈ (ℤ_≥‘𝑠))
64		elfzuzb 12901	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ (0...𝑚) ↔ (𝑠 ∈ (ℤ_≥‘0) ∧ 𝑚 ∈ (ℤ_≥‘𝑠)))
65	55, 63, 64	sylanbrc 585	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑠 ∈ (0...𝑚))
66		fznn0sub2 13013	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ (0...𝑚) → (𝑚 − 𝑠) ∈ (0...𝑚))
67	65, 66	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ (0...𝑚))
68		elfzelz 12907	. . . . . . . . . . . . 13 ⊢ ((𝑚 − 𝑠) ∈ (0...𝑚) → (𝑚 − 𝑠) ∈ ℤ)
69	67, 68	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ ℤ)
70		eluz 12256	. . . . . . . . . . . 12 ⊢ (((𝑚 − 𝑠) ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑚 ∈ (ℤ_≥‘(𝑚 − 𝑠)) ↔ (𝑚 − 𝑠) ≤ 𝑚))
71	69, 50, 70	syl2anc 586	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 ∈ (ℤ_≥‘(𝑚 − 𝑠)) ↔ (𝑚 − 𝑠) ≤ 𝑚))
72	54, 71	mpbird 259	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑚 ∈ (ℤ_≥‘(𝑚 − 𝑠)))
73		fzss2 12946	. . . . . . . . . 10 ⊢ (𝑚 ∈ (ℤ_≥‘(𝑚 − 𝑠)) → (0...(𝑚 − 𝑠)) ⊆ (0...𝑚))
74	72, 73	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (0...(𝑚 − 𝑠)) ⊆ (0...𝑚))
75	74	sselda 3966	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑗 ∈ (0...𝑚))
76	13	abscld 14795	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (abs‘𝐴) ∈ ℝ)
77	11, 12, 76	syl2an 597	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘𝐴) ∈ ℝ)
78	36	abscld 14795	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ)
79	77, 78	remulcld 10670	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
80	75, 79	syldan 593	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
81	46, 80	fsumrecl 15090	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
82		fzfid 13340	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (((𝑚 − 𝑠) + 1)...𝑚) ∈ Fin)
83		elfznn0 12999	. . . . . . . . . . . . 13 ⊢ ((𝑚 − 𝑠) ∈ (0...𝑚) → (𝑚 − 𝑠) ∈ ℕ₀)
84	67, 83	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ ℕ₀)
85		peano2nn0 11936	. . . . . . . . . . . 12 ⊢ ((𝑚 − 𝑠) ∈ ℕ₀ → ((𝑚 − 𝑠) + 1) ∈ ℕ₀)
86	84, 85	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝑚 − 𝑠) + 1) ∈ ℕ₀)
87	86, 30	eleqtrdi 2923	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝑚 − 𝑠) + 1) ∈ (ℤ_≥‘0))
88		fzss1 12945	. . . . . . . . . 10 ⊢ (((𝑚 − 𝑠) + 1) ∈ (ℤ_≥‘0) → (((𝑚 − 𝑠) + 1)...𝑚) ⊆ (0...𝑚))
89	87, 88	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (((𝑚 − 𝑠) + 1)...𝑚) ⊆ (0...𝑚))
90	89	sselda 3966	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑗 ∈ (0...𝑚))
91	90, 79	syldan 593	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
92	82, 91	fsumrecl 15090	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
93	42	rphalfcld 12442	. . . . . . . 8 ⊢ (𝜑 → (𝐸 / 2) ∈ ℝ⁺)
94	93	rpred 12430	. . . . . . 7 ⊢ (𝜑 → (𝐸 / 2) ∈ ℝ)
95	94	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝐸 / 2) ∈ ℝ)
96		elfznn0 12999	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...(𝑚 − 𝑠)) → 𝑗 ∈ ℕ₀)
97	11, 96, 76	syl2an 597	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘𝐴) ∈ ℝ)
98	46, 97	fsumrecl 15090	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ∈ ℝ)
99	98, 95	remulcld 10670	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) ∈ ℝ)
100		0zd 11992	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ ℤ)
101		eqidd 2822	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (𝐾‘𝑗) = (𝐾‘𝑗))
102		mertens.2	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (𝐾‘𝑗) = (abs‘𝐴))
103	102, 76	eqeltrd 2913	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (𝐾‘𝑗) ∈ ℝ)
104		mertens.7	. . . . . . . . . . 11 ⊢ (𝜑 → seq0( + , 𝐾) ∈ dom ⇝ )
105	30, 100, 101, 103, 104	isumrecl 15119	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) ∈ ℝ)
106	13	absge0d 14803	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → 0 ≤ (abs‘𝐴))
107	106, 102	breqtrrd 5093	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → 0 ≤ (𝐾‘𝑗))
108	30, 100, 101, 103, 104, 107	isumge0 15120	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗))
109	105, 108	ge0p1rpd 12460	. . . . . . . . 9 ⊢ (𝜑 → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ⁺)
110	109	adantr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ⁺)
111	99, 110	rerpdivcld 12461	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) ∈ ℝ)
112	93, 109	rpdivcld 12447	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) ∈ ℝ⁺)
113	112	rpred 12430	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) ∈ ℝ)
114	113	ad2antrr 724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) ∈ ℝ)
115	97, 114	remulcld 10670	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))) ∈ ℝ)
116	75, 20	syldan 593	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((𝑚 − 𝑗) + 1) ∈ ℤ)
117		simplll 773	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝜑)
118	75, 19	syldan 593	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((𝑚 − 𝑗) + 1) ∈ ℕ₀)
119	118, 22	sylan 582	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ₀)
120	117, 119, 24	syl2anc 586	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → (𝐺‘𝑘) = 𝐵)
121	117, 119, 26	syl2anc 586	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝐵 ∈ ℂ)
122	75, 35	syldan 593	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → seq((𝑚 − 𝑗) + 1)( + , 𝐺) ∈ dom ⇝ )
123	15, 116, 120, 121, 122	isumcl 15115	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵 ∈ ℂ)
124	123	abscld 14795	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ)
125	76, 106	jca 514	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)))
126	11, 96, 125	syl2an 597	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)))
127	120	sumeq2dv 15059	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)
128	127	fveq2d 6673	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)) = (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵))
129		fvoveq1 7178	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = (𝑚 − 𝑗) → (ℤ_≥‘(𝑛 + 1)) = (ℤ_≥‘((𝑚 − 𝑗) + 1)))
130	129	sumeq1d 15057	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = (𝑚 − 𝑗) → Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘))
131	130	fveq2d 6673	. . . . . . . . . . . . . 14 ⊢ (𝑛 = (𝑚 − 𝑗) → (abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) = (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)))
132	131	breq1d 5075	. . . . . . . . . . . . 13 ⊢ (𝑛 = (𝑚 − 𝑗) → ((abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) ↔ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
133	4	simprd 498	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑛 ∈ (ℤ_≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
134	133	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ∀𝑛 ∈ (ℤ_≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
135		elfzelz 12907	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...(𝑚 − 𝑠)) → 𝑗 ∈ ℤ)
136	135	adantl 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑗 ∈ ℤ)
137	136	zred 12086	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑗 ∈ ℝ)
138	49	ad2antlr 725	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑚 ∈ ℤ)
139	138	zred 12086	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑚 ∈ ℝ)
140	56	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑠 ∈ ℤ)
141	140	zred 12086	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑠 ∈ ℝ)
142		elfzle2 12910	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...(𝑚 − 𝑠)) → 𝑗 ≤ (𝑚 − 𝑠))
143	142	adantl 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑗 ≤ (𝑚 − 𝑠))
144	137, 139, 141, 143	lesubd 11243	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑠 ≤ (𝑚 − 𝑗))
145	138, 136	zsubcld 12091	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (𝑚 − 𝑗) ∈ ℤ)
146		eluz 12256	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 ∈ ℤ ∧ (𝑚 − 𝑗) ∈ ℤ) → ((𝑚 − 𝑗) ∈ (ℤ_≥‘𝑠) ↔ 𝑠 ≤ (𝑚 − 𝑗)))
147	140, 145, 146	syl2anc 586	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((𝑚 − 𝑗) ∈ (ℤ_≥‘𝑠) ↔ 𝑠 ≤ (𝑚 − 𝑗)))
148	144, 147	mpbird 259	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (𝑚 − 𝑗) ∈ (ℤ_≥‘𝑠))
149	132, 134, 148	rspcdva 3624	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
150	128, 149	eqbrtrrd 5089	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
151	124, 114, 150	ltled 10787	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
152		lemul2a 11494	. . . . . . . . . 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 1369	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
154	46, 80, 115, 153	fsumle 15153	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
155	98	recnd 10668	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ∈ ℂ)
156	93	rpcnd 12432	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸 / 2) ∈ ℂ)
157	156	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝐸 / 2) ∈ ℂ)
158		peano2re 10812	. . . . . . . . . . . . 13 ⊢ (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) ∈ ℝ → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ)
159	105, 158	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ)
160	159	recnd 10668	. . . . . . . . . . 11 ⊢ (𝜑 → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℂ)
161	160	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℂ)
162	109	rpne0d 12435	. . . . . . . . . . 11 ⊢ (𝜑 → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ≠ 0)
163	162	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ≠ 0)
164	155, 157, 161, 163	divassd 11450	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) = (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
165		fveq2 6669	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑗 → (𝐾‘𝑛) = (𝐾‘𝑗))
166	165	cbvsumv 15052	. . . . . . . . . . . . . . . 16 ⊢ Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) = Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗)
167	166	oveq1i 7165	. . . . . . . . . . . . . . 15 ⊢ (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1) = (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)
168	167	oveq2i 7166	. . . . . . . . . . . . . 14 ⊢ ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1)) = ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))
169	168, 112	eqeltrid 2917	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1)) ∈ ℝ⁺)
170	169	rpcnd 12432	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1)) ∈ ℂ)
171	170	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1)) ∈ ℂ)
172	76	recnd 10668	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (abs‘𝐴) ∈ ℂ)
173	11, 96, 172	syl2an 597	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘𝐴) ∈ ℂ)
174	46, 171, 173	fsummulc1 15139	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1))) = Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1))))
175	168	oveq2i 7166	. . . . . . . . . 10 ⊢ (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1))) = (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
176	168	oveq2i 7166	. . . . . . . . . . . 12 ⊢ ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1))) = ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
177	176	a1i 11	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...(𝑚 − 𝑠)) → ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1))) = ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
178	177	sumeq2i 15055	. . . . . . . . . 10 ⊢ Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1))) = Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
179	174, 175, 178	3eqtr3g 2879	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))) = Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
180	164, 179	eqtrd 2856	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) = Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
181	154, 180	breqtrrd 5093	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
182	105	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) ∈ ℝ)
183	159	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ)
184		0zd 11992	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 0 ∈ ℤ)
185		fz0ssnn0 13001	. . . . . . . . . . . . 13 ⊢ (0...(𝑚 − 𝑠)) ⊆ ℕ₀
186	185	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (0...(𝑚 − 𝑠)) ⊆ ℕ₀)
187	102	adantlr 713	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ₀) → (𝐾‘𝑗) = (abs‘𝐴))
188	76	adantlr 713	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ₀) → (abs‘𝐴) ∈ ℝ)
189	106	adantlr 713	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ₀) → 0 ≤ (abs‘𝐴))
190	104	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → seq0( + , 𝐾) ∈ dom ⇝ )
191	30, 184, 46, 186, 187, 188, 189, 190	isumless 15199	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ≤ Σ𝑗 ∈ ℕ₀ (abs‘𝐴))
192	102	sumeq2dv 15059	. . . . . . . . . . . 12 ⊢ (𝜑 → Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) = Σ𝑗 ∈ ℕ₀ (abs‘𝐴))
193	192	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) = Σ𝑗 ∈ ℕ₀ (abs‘𝐴))
194	191, 193	breqtrrd 5093	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ≤ Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗))
195	105	ltp1d 11569	. . . . . . . . . . 11 ⊢ (𝜑 → Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))
196	195	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))
197	98, 182, 183, 194, 196	lelttrd 10797	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))
198	93	rpregt0d 12436	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 / 2) ∈ ℝ ∧ 0 < (𝐸 / 2)))
199	198	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝐸 / 2) ∈ ℝ ∧ 0 < (𝐸 / 2)))
200		ltmul1 11489	. . . . . . . . . 10 ⊢ ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ∈ ℝ ∧ (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ ∧ ((𝐸 / 2) ∈ ℝ ∧ 0 < (𝐸 / 2))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ↔ (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) · (𝐸 / 2))))
201	98, 183, 199, 200	syl3anc 1367	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ↔ (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) · (𝐸 / 2))))
202	197, 201	mpbid 234	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) · (𝐸 / 2)))
203	109	rpregt0d 12436	. . . . . . . . . 10 ⊢ (𝜑 → ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ ∧ 0 < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
204	203	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ ∧ 0 < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
205		ltdivmul 11514	. . . . . . . . 9 ⊢ (((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) ∈ ℝ ∧ (𝐸 / 2) ∈ ℝ ∧ ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ ∧ 0 < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))) → (((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) < (𝐸 / 2) ↔ (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) · (𝐸 / 2))))
206	99, 95, 204, 205	syl3anc 1367	. . . . . . . 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 10797	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < (𝐸 / 2))
209		mertens.13	. . . . . . . . . . . 12 ⊢ (𝜑 → (0 ≤ sup(𝑇, ℝ, < ) ∧ (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧)))
210	209	simprd 498	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧))
211		suprcl 11600	. . . . . . . . . . 11 ⊢ ((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧) → sup(𝑇, ℝ, < ) ∈ ℝ)
212	210, 211	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → sup(𝑇, ℝ, < ) ∈ ℝ)
213	94, 212	remulcld 10670	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 / 2) · sup(𝑇, ℝ, < )) ∈ ℝ)
214	209	simpld 497	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ sup(𝑇, ℝ, < ))
215	212, 214	ge0p1rpd 12460	. . . . . . . . 9 ⊢ (𝜑 → (sup(𝑇, ℝ, < ) + 1) ∈ ℝ⁺)
216	213, 215	rerpdivcld 12461	. . . . . . . 8 ⊢ (𝜑 → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℝ)
217	216	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℝ)
218	5	nnrpd 12428	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑠 ∈ ℝ⁺)
219	93, 218	rpdivcld 12447	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐸 / 2) / 𝑠) ∈ ℝ⁺)
220	219, 215	rpdivcld 12447	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℝ⁺)
221	220	rpred 12430	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℝ)
222	221, 212	remulcld 10670	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈ ℝ)
223	222	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈ ℝ)
224		simpll 765	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝜑)
225	90, 12	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑗 ∈ ℕ₀)
226	224, 225, 76	syl2anc 586	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘𝐴) ∈ ℝ)
227	221	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℝ)
228	224, 225, 102	syl2anc 586	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝐾‘𝑗) = (abs‘𝐴))
229		fveq2 6669	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑗 → (𝐾‘𝑚) = (𝐾‘𝑗))
230	229	breq1d 5075	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑗 → ((𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ↔ (𝐾‘𝑗) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))
231	7	simprd 498	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑚 ∈ (ℤ_≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))
232	231	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ∀𝑚 ∈ (ℤ_≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))
233		elfzuz 12903	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚) → 𝑗 ∈ (ℤ_≥‘((𝑚 − 𝑠) + 1)))
234		eluzle 12255	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡)) → (𝑠 + 𝑡) ≤ 𝑚)
235	234	adantl 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑠 + 𝑡) ≤ 𝑚)
236	8	nn0zd 12084	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑡 ∈ ℤ)
237	236	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑡 ∈ ℤ)
238	237	zred 12086	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑡 ∈ ℝ)
239	52, 238, 51	leaddsub2d 11241	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝑠 + 𝑡) ≤ 𝑚 ↔ 𝑡 ≤ (𝑚 − 𝑠)))
240	235, 239	mpbid 234	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑡 ≤ (𝑚 − 𝑠))
241		eluz 12256	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑡 ∈ ℤ ∧ (𝑚 − 𝑠) ∈ ℤ) → ((𝑚 − 𝑠) ∈ (ℤ_≥‘𝑡) ↔ 𝑡 ≤ (𝑚 − 𝑠)))
242	237, 69, 241	syl2anc 586	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝑚 − 𝑠) ∈ (ℤ_≥‘𝑡) ↔ 𝑡 ≤ (𝑚 − 𝑠)))
243	240, 242	mpbird 259	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ (ℤ_≥‘𝑡))
244		peano2uz 12300	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 − 𝑠) ∈ (ℤ_≥‘𝑡) → ((𝑚 − 𝑠) + 1) ∈ (ℤ_≥‘𝑡))
245	243, 244	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝑚 − 𝑠) + 1) ∈ (ℤ_≥‘𝑡))
246		uztrn 12260	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ (ℤ_≥‘((𝑚 − 𝑠) + 1)) ∧ ((𝑚 − 𝑠) + 1) ∈ (ℤ_≥‘𝑡)) → 𝑗 ∈ (ℤ_≥‘𝑡))
247	233, 245, 246	syl2anr 598	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑗 ∈ (ℤ_≥‘𝑡))
248	230, 232, 247	rspcdva 3624	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝐾‘𝑗) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))
249	228, 248	eqbrtrrd 5089	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘𝐴) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))
250	226, 227, 249	ltled 10787	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘𝐴) ≤ (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))
251	210	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧))
252	51	adantr 483	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑚 ∈ ℝ)
253		peano2zm 12024	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ ℤ → (𝑠 − 1) ∈ ℤ)
254	56, 253	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑠 − 1) ∈ ℤ)
255	254	zred 12086	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑠 − 1) ∈ ℝ)
256	255	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑠 − 1) ∈ ℝ)
257	225	nn0red 11955	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑗 ∈ ℝ)
258	50	zcnd 12087	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑚 ∈ ℂ)
259	52	recnd 10668	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑠 ∈ ℂ)
260		1cnd 10635	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 1 ∈ ℂ)
261	258, 259, 260	subsubd 11024	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − (𝑠 − 1)) = ((𝑚 − 𝑠) + 1))
262	261	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − (𝑠 − 1)) = ((𝑚 − 𝑠) + 1))
263		elfzle1 12909	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚) → ((𝑚 − 𝑠) + 1) ≤ 𝑗)
264	263	adantl 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((𝑚 − 𝑠) + 1) ≤ 𝑗)
265	262, 264	eqbrtrd 5087	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − (𝑠 − 1)) ≤ 𝑗)
266	252, 256, 257, 265	subled 11242	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − 𝑗) ≤ (𝑠 − 1))
267	90, 16	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − 𝑗) ∈ ℕ₀)
268	267, 30	eleqtrdi 2923	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − 𝑗) ∈ (ℤ_≥‘0))
269	254	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑠 − 1) ∈ ℤ)
270		elfz5 12899	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 − 𝑗) ∈ (ℤ_≥‘0) ∧ (𝑠 − 1) ∈ ℤ) → ((𝑚 − 𝑗) ∈ (0...(𝑠 − 1)) ↔ (𝑚 − 𝑗) ≤ (𝑠 − 1)))
271	268, 269, 270	syl2anc 586	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((𝑚 − 𝑗) ∈ (0...(𝑠 − 1)) ↔ (𝑚 − 𝑗) ≤ (𝑠 − 1)))
272	266, 271	mpbird 259	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − 𝑗) ∈ (0...(𝑠 − 1)))
273		simplll 773	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝜑)
274	90, 19	syldan 593	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((𝑚 − 𝑗) + 1) ∈ ℕ₀)
275	274, 22	sylan 582	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ₀)
276	273, 275, 24	syl2anc 586	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → (𝐺‘𝑘) = 𝐵)
277	276	sumeq2dv 15059	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)
278	277	eqcomd 2827	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵 = Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘))
279	278	fveq2d 6673	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)))
280	131	rspceeqv 3637	. . . . . . . . . . . . 13 ⊢ (((𝑚 − 𝑗) ∈ (0...(𝑠 − 1)) ∧ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘))) → ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)))
281	272, 279, 280	syl2anc 586	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)))
282		fvex 6682	. . . . . . . . . . . . 13 ⊢ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ V
283		eqeq1 2825	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) → (𝑧 = (abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) ↔ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘))))
284	283	rexbidv 3297	. . . . . . . . . . . . 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 3669	. . . . . . . . . . . 12 ⊢ ((abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ 𝑇 ↔ ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)))
287	281, 286	sylibr 236	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ 𝑇)
288		suprub 11601	. . . . . . . . . . 11 ⊢ (((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧) ∧ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ 𝑇) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ sup(𝑇, ℝ, < ))
289	251, 287, 288	syl2anc 586	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ sup(𝑇, ℝ, < ))
290	224, 225, 125	syl2anc 586	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)))
291	90, 78	syldan 593	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ)
292	36	absge0d 14803	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → 0 ≤ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵))
293	90, 292	syldan 593	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 0 ≤ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵))
294	291, 293	jca 514	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ ∧ 0 ≤ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)))
295	212	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → sup(𝑇, ℝ, < ) ∈ ℝ)
296		lemul12a 11497	. . . . . . . . . . 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 836	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (((abs‘𝐴) ≤ (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∧ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ sup(𝑇, ℝ, < )) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))))
298	250, 289, 297	mp2and 697	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )))
299	82, 91, 223, 298	fsumle 15153	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )))
300	222	recnd 10668	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈ ℂ)
301	300	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈ ℂ)
302		fsumconst 15144	. . . . . . . . . 10 ⊢ (((((𝑚 − 𝑠) + 1)...𝑚) ∈ Fin ∧ ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈ ℂ) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) = ((♯‘(((𝑚 − 𝑠) + 1)...𝑚)) · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))))
303	82, 301, 302	syl2anc 586	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) = ((♯‘(((𝑚 − 𝑠) + 1)...𝑚)) · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))))
304		1zzd 12012	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 1 ∈ ℤ)
305	56	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑠 ∈ ℤ)
306		fzen 12923	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ (𝑚 − 𝑠) ∈ ℤ) → (1...𝑠) ≈ ((1 + (𝑚 − 𝑠))...(𝑠 + (𝑚 − 𝑠))))
307	304, 305, 69, 306	syl3anc 1367	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (1...𝑠) ≈ ((1 + (𝑚 − 𝑠))...(𝑠 + (𝑚 − 𝑠))))
308		ax-1cn 10594	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
309	69	zcnd 12087	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ ℂ)
310		addcom 10825	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℂ ∧ (𝑚 − 𝑠) ∈ ℂ) → (1 + (𝑚 − 𝑠)) = ((𝑚 − 𝑠) + 1))
311	308, 309, 310	sylancr 589	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (1 + (𝑚 − 𝑠)) = ((𝑚 − 𝑠) + 1))
312	259, 258	pncan3d 10999	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑠 + (𝑚 − 𝑠)) = 𝑚)
313	311, 312	oveq12d 7173	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((1 + (𝑚 − 𝑠))...(𝑠 + (𝑚 − 𝑠))) = (((𝑚 − 𝑠) + 1)...𝑚))
314	307, 313	breqtrd 5091	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (1...𝑠) ≈ (((𝑚 − 𝑠) + 1)...𝑚))
315		fzfid 13340	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (1...𝑠) ∈ Fin)
316		hashen 13706	. . . . . . . . . . . . 13 ⊢ (((1...𝑠) ∈ Fin ∧ (((𝑚 − 𝑠) + 1)...𝑚) ∈ Fin) → ((♯‘(1...𝑠)) = (♯‘(((𝑚 − 𝑠) + 1)...𝑚)) ↔ (1...𝑠) ≈ (((𝑚 − 𝑠) + 1)...𝑚)))
317	315, 82, 316	syl2anc 586	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((♯‘(1...𝑠)) = (♯‘(((𝑚 − 𝑠) + 1)...𝑚)) ↔ (1...𝑠) ≈ (((𝑚 − 𝑠) + 1)...𝑚)))
318	314, 317	mpbird 259	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (♯‘(1...𝑠)) = (♯‘(((𝑚 − 𝑠) + 1)...𝑚)))
319		hashfz1 13705	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ℕ₀ → (♯‘(1...𝑠)) = 𝑠)
320	47, 319	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (♯‘(1...𝑠)) = 𝑠)
321	318, 320	eqtr3d 2858	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (♯‘(((𝑚 − 𝑠) + 1)...𝑚)) = 𝑠)
322	321	oveq1d 7170	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((♯‘(((𝑚 − 𝑠) + 1)...𝑚)) · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))) = (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))))
323	212	recnd 10668	. . . . . . . . . . . 12 ⊢ (𝜑 → sup(𝑇, ℝ, < ) ∈ ℂ)
324	215	rpcnne0d 12439	. . . . . . . . . . . 12 ⊢ (𝜑 → ((sup(𝑇, ℝ, < ) + 1) ∈ ℂ ∧ (sup(𝑇, ℝ, < ) + 1) ≠ 0))
325		div23 11316	. . . . . . . . . . . 12 ⊢ (((𝐸 / 2) ∈ ℂ ∧ sup(𝑇, ℝ, < ) ∈ ℂ ∧ ((sup(𝑇, ℝ, < ) + 1) ∈ ℂ ∧ (sup(𝑇, ℝ, < ) + 1) ≠ 0)) → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) = (((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )))
326	156, 323, 324, 325	syl3anc 1367	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) = (((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )))
327	56	zcnd 12087	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑠 ∈ ℂ)
328	219	rpcnd 12432	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐸 / 2) / 𝑠) ∈ ℂ)
329		divass 11315	. . . . . . . . . . . . . 14 ⊢ ((𝑠 ∈ ℂ ∧ ((𝐸 / 2) / 𝑠) ∈ ℂ ∧ ((sup(𝑇, ℝ, < ) + 1) ∈ ℂ ∧ (sup(𝑇, ℝ, < ) + 1) ≠ 0)) → ((𝑠 · ((𝐸 / 2) / 𝑠)) / (sup(𝑇, ℝ, < ) + 1)) = (𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))
330	327, 328, 324, 329	syl3anc 1367	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑠 · ((𝐸 / 2) / 𝑠)) / (sup(𝑇, ℝ, < ) + 1)) = (𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))
331	5	nnne0d 11686	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑠 ≠ 0)
332	156, 327, 331	divcan2d 11417	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑠 · ((𝐸 / 2) / 𝑠)) = (𝐸 / 2))
333	332	oveq1d 7170	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑠 · ((𝐸 / 2) / 𝑠)) / (sup(𝑇, ℝ, < ) + 1)) = ((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)))
334	330, 333	eqtr3d 2858	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) = ((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)))
335	334	oveq1d 7170	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) · sup(𝑇, ℝ, < )) = (((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )))
336	220	rpcnd 12432	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℂ)
337	327, 336, 323	mulassd 10663	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) · sup(𝑇, ℝ, < )) = (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))))
338	326, 335, 337	3eqtr2rd 2863	. . . . . . . . . 10 ⊢ (𝜑 → (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))) = (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)))
339	338	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))) = (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)))
340	303, 322, 339	3eqtrd 2860	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) = (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)))
341	299, 340	breqtrd 5091	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)))
342		peano2re 10812	. . . . . . . . . . 11 ⊢ (sup(𝑇, ℝ, < ) ∈ ℝ → (sup(𝑇, ℝ, < ) + 1) ∈ ℝ)
343	212, 342	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (sup(𝑇, ℝ, < ) + 1) ∈ ℝ)
344	212	ltp1d 11569	. . . . . . . . . 10 ⊢ (𝜑 → sup(𝑇, ℝ, < ) < (sup(𝑇, ℝ, < ) + 1))
345	212, 343, 93, 344	ltmul2dd 12486	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 / 2) · sup(𝑇, ℝ, < )) < ((𝐸 / 2) · (sup(𝑇, ℝ, < ) + 1)))
346	213, 94, 215	ltdivmul2d 12482	. . . . . . . . 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 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) < (𝐸 / 2))
349	92, 217, 95, 341, 348	lelttrd 10797	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < (𝐸 / 2))
350	81, 92, 95, 95, 208, 349	lt2addd 11262	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) + Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵))) < ((𝐸 / 2) + (𝐸 / 2)))
351	14, 36	absmuld 14813	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) = ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)))
352	351	sumeq2dv 15059	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) = Σ𝑗 ∈ (0...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)))
353	69	zred 12086	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ ℝ)
354	353	ltp1d 11569	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) < ((𝑚 − 𝑠) + 1))
355		fzdisj 12933	. . . . . . . 8 ⊢ ((𝑚 − 𝑠) < ((𝑚 − 𝑠) + 1) → ((0...(𝑚 − 𝑠)) ∩ (((𝑚 − 𝑠) + 1)...𝑚)) = ∅)
356	354, 355	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((0...(𝑚 − 𝑠)) ∩ (((𝑚 − 𝑠) + 1)...𝑚)) = ∅)
357		fzsplit 12932	. . . . . . . 8 ⊢ ((𝑚 − 𝑠) ∈ (0...𝑚) → (0...𝑚) = ((0...(𝑚 − 𝑠)) ∪ (((𝑚 − 𝑠) + 1)...𝑚)))
358	67, 357	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (0...𝑚) = ((0...(𝑚 − 𝑠)) ∪ (((𝑚 − 𝑠) + 1)...𝑚)))
359	79	recnd 10668	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℂ)
360	356, 358, 10, 359	fsumsplit 15096	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) = (Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) + Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵))))
361	352, 360	eqtr2d 2857	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) + Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵))) = Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)))
362	42	rpcnd 12432	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ ℂ)
363	362	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝐸 ∈ ℂ)
364	363	2halvesd 11882	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝐸 / 2) + (𝐸 / 2)) = 𝐸)
365	350, 361, 364	3brtr3d 5096	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)
366	39, 41, 44, 45, 365	lelttrd 10797	. . 3 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)
367	366	ralrimiva 3182	. 2 ⊢ (𝜑 → ∀𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)
368		fveq2 6669	. . . 4 ⊢ (𝑦 = (𝑠 + 𝑡) → (ℤ_≥‘𝑦) = (ℤ_≥‘(𝑠 + 𝑡)))
369	368	raleqdv 3415	. . 3 ⊢ (𝑦 = (𝑠 + 𝑡) → (∀𝑚 ∈ (ℤ_≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸 ↔ ∀𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸))
370	369	rspcev 3622	. 2 ⊢ (((𝑠 + 𝑡) ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸) → ∃𝑦 ∈ ℕ₀ ∀𝑚 ∈ (ℤ_≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)
371	9, 367, 370	syl2anc 586	1 ⊢ (𝜑 → ∃𝑦 ∈ ℕ₀ ∀𝑚 ∈ (ℤ_≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1533 ∈ wcel 2110 {cab 2799 ≠ wne 3016 ∀wral 3138 ∃wrex 3139 ∪ cun 3933 ∩ cin 3934 ⊆ wss 3935 ∅c0 4290 class class class wbr 5065 dom cdm 5554 ‘cfv 6354 (class class class)co 7155 ≈ cen 8505 Fincfn 8508 supcsup 8903 ℂcc 10534 ℝcr 10535 0cc0 10536 1c1 10537 + caddc 10539 · cmul 10541 < clt 10674 ≤ cle 10675 − cmin 10869 / cdiv 11296 ℕcn 11637 2c2 11691 ℕ₀cn0 11896 ℤcz 11980 ℤ_≥cuz 12242 ℝ⁺crp 12388 ...cfz 12891 seqcseq 13368 ♯chash 13689 abscabs 14592 ⇝ cli 14840 Σcsu 15041

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-rep 5189 ax-sep 5202 ax-nul 5209 ax-pow 5265 ax-pr 5329 ax-un 7460 ax-inf2 9103 ax-cnex 10592 ax-resscn 10593 ax-1cn 10594 ax-icn 10595 ax-addcl 10596 ax-addrcl 10597 ax-mulcl 10598 ax-mulrcl 10599 ax-mulcom 10600 ax-addass 10601 ax-mulass 10602 ax-distr 10603 ax-i2m1 10604 ax-1ne0 10605 ax-1rid 10606 ax-rnegex 10607 ax-rrecex 10608 ax-cnre 10609 ax-pre-lttri 10610 ax-pre-lttrn 10611 ax-pre-ltadd 10612 ax-pre-mulgt0 10613 ax-pre-sup 10614

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-fal 1546 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3772 df-csb 3883 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-pss 3953 df-nul 4291 df-if 4467 df-pw 4540 df-sn 4567 df-pr 4569 df-tp 4571 df-op 4573 df-uni 4838 df-int 4876 df-iun 4920 df-br 5066 df-opab 5128 df-mpt 5146 df-tr 5172 df-id 5459 df-eprel 5464 df-po 5473 df-so 5474 df-fr 5513 df-se 5514 df-we 5515 df-xp 5560 df-rel 5561 df-cnv 5562 df-co 5563 df-dm 5564 df-rn 5565 df-res 5566 df-ima 5567 df-pred 6147 df-ord 6193 df-on 6194 df-lim 6195 df-suc 6196 df-iota 6313 df-fun 6356 df-fn 6357 df-f 6358 df-f1 6359 df-fo 6360 df-f1o 6361 df-fv 6362 df-isom 6363 df-riota 7113 df-ov 7158 df-oprab 7159 df-mpo 7160 df-om 7580 df-1st 7688 df-2nd 7689 df-wrecs 7946 df-recs 8007 df-rdg 8045 df-1o 8101 df-oadd 8105 df-er 8288 df-pm 8408 df-en 8509 df-dom 8510 df-sdom 8511 df-fin 8512 df-sup 8905 df-inf 8906 df-oi 8973 df-card 9367 df-pnf 10676 df-mnf 10677 df-xr 10678 df-ltxr 10679 df-le 10680 df-sub 10871 df-neg 10872 df-div 11297 df-nn 11638 df-2 11699 df-3 11700 df-n0 11897 df-z 11981 df-uz 12243 df-rp 12389 df-ico 12743 df-fz 12892 df-fzo 13033 df-fl 13161 df-seq 13369 df-exp 13429 df-hash 13690 df-cj 14457 df-re 14458 df-im 14459 df-sqrt 14593 df-abs 14594 df-clim 14844 df-rlim 14845 df-sum 15042

This theorem is referenced by: mertenslem2 15240

W3C validator