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 15961

Description: Lemma for mertens 15963. (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 500	. . . . . 6 ⊢ (𝜑 → 𝜓)
3		mertens.11	. . . . . 6 ⊢ (𝜓 ↔ (𝑠 ∈ ℕ ∧ ∀𝑛 ∈ (ℤ_≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
4	2, 3	sylib 221	. . . . 5 ⊢ (𝜑 → (𝑠 ∈ ℕ ∧ ∀𝑛 ∈ (ℤ_≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
5	4	simpld 500	. . . 4 ⊢ (𝜑 → 𝑠 ∈ ℕ)
6	5	nnnn0d 12580	. . 3 ⊢ (𝜑 → 𝑠 ∈ ℕ₀)
7	1	simprd 501	. . . 4 ⊢ (𝜑 → (𝑡 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))
8	7	simpld 500	. . 3 ⊢ (𝜑 → 𝑡 ∈ ℕ₀)
9	6, 8	nn0addcld 12584	. 2 ⊢ (𝜑 → (𝑠 + 𝑡) ∈ ℕ₀)
10		fzfid 14027	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (0...𝑚) ∈ Fin)
11		simpl 488	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝜑)
12		elfznn0 13665	. . . . . . . 8 ⊢ (𝑗 ∈ (0...𝑚) → 𝑗 ∈ ℕ₀)
13		mertens.3	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → 𝐴 ∈ ℂ)
14	11, 12, 13	syl2an 608	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → 𝐴 ∈ ℂ)
15		eqid 2765	. . . . . . . 8 ⊢ (ℤ_≥‘((𝑚 − 𝑗) + 1)) = (ℤ_≥‘((𝑚 − 𝑗) + 1))
16		fznn0sub 13601	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...𝑚) → (𝑚 − 𝑗) ∈ ℕ₀)
17	16	adantl 487	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (𝑚 − 𝑗) ∈ ℕ₀)
18		peano2nn0 12559	. . . . . . . . . 10 ⊢ ((𝑚 − 𝑗) ∈ ℕ₀ → ((𝑚 − 𝑗) + 1) ∈ ℕ₀)
19	17, 18	syl 18	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((𝑚 − 𝑗) + 1) ∈ ℕ₀)
20	19	nn0zd 12631	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((𝑚 − 𝑗) + 1) ∈ ℤ)
21		simplll 787	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝜑)
22		eluznn0 12957	. . . . . . . . . 10 ⊢ ((((𝑚 − 𝑗) + 1) ∈ ℕ₀ ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ₀)
23	19, 22	sylan 592	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ₀)
24		mertens.4	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝐺‘𝑘) = 𝐵)
25	21, 23, 24	syl2anc 596	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → (𝐺‘𝑘) = 𝐵)
26		mertens.5	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → 𝐵 ∈ ℂ)
27	21, 23, 26	syl2anc 596	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝐵 ∈ ℂ)
28		mertens.8	. . . . . . . . . 10 ⊢ (𝜑 → seq0( + , 𝐺) ∈ dom ⇝ )
29	28	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → seq0( + , 𝐺) ∈ dom ⇝ )
30		nn0uz 12916	. . . . . . . . . 10 ⊢ ℕ₀ = (ℤ_≥‘0)
31		simpll 779	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → 𝜑)
32	24, 26	eqeltrd 2865	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝐺‘𝑘) ∈ ℂ)
33	31, 32	sylan 592	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ ℕ₀) → (𝐺‘𝑘) ∈ ℂ)
34	30, 19, 33	iserex 15732	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (seq0( + , 𝐺) ∈ dom ⇝ ↔ seq((𝑚 − 𝑗) + 1)( + , 𝐺) ∈ dom ⇝ ))
35	29, 34	mpbid 235	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → seq((𝑚 − 𝑗) + 1)( + , 𝐺) ∈ dom ⇝ )
36	15, 20, 25, 27, 35	isumcl 15835	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵 ∈ ℂ)
37	14, 36	mulcld 11244	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℂ)
38	10, 37	fsumcl 15807	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℂ)
39	38	abscld 15514	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
40	37	abscld 15514	. . . . 5 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
41	10, 40	fsumrecl 15808	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
42		mertens.9	. . . . . 6 ⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
43	42	rpred 13076	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ ℝ)
44	43	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝐸 ∈ ℝ)
45	10, 37	fsumabs 15876	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)))
46		fzfid 14027	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (0...(𝑚 − 𝑠)) ∈ Fin)
47	6	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑠 ∈ ℕ₀)
48	47	nn0ge0d 12583	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 0 ≤ 𝑠)
49		eluzelz 12888	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡)) → 𝑚 ∈ ℤ)
50	49	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑚 ∈ ℤ)
51	50	zred 12716	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑚 ∈ ℝ)
52	47	nn0red 12581	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑠 ∈ ℝ)
53	51, 52	subge02d 11821	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (0 ≤ 𝑠 ↔ (𝑚 − 𝑠) ≤ 𝑚))
54	48, 53	mpbid 235	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ≤ 𝑚)
55	47, 30	eleqtrdi 2875	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑠 ∈ (ℤ_≥‘0))
56	5	nnzd 12632	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑠 ∈ ℤ)
57		uzid 12893	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ ℤ → 𝑠 ∈ (ℤ_≥‘𝑠))
58	56, 57	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑠 ∈ (ℤ_≥‘𝑠))
59		uzaddcl 12944	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 ∈ (ℤ_≥‘𝑠) ∧ 𝑡 ∈ ℕ₀) → (𝑠 + 𝑡) ∈ (ℤ_≥‘𝑠))
60	58, 8, 59	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑠 + 𝑡) ∈ (ℤ_≥‘𝑠))
61		eqid 2765	. . . . . . . . . . . . . . . . 17 ⊢ (ℤ_≥‘𝑠) = (ℤ_≥‘𝑠)
62	61	uztrn2 12897	. . . . . . . . . . . . . . . 16 ⊢ (((𝑠 + 𝑡) ∈ (ℤ_≥‘𝑠) ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑚 ∈ (ℤ_≥‘𝑠))
63	60, 62	sylan 592	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑚 ∈ (ℤ_≥‘𝑠))
64		elfzuzb 13562	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ (0...𝑚) ↔ (𝑠 ∈ (ℤ_≥‘0) ∧ 𝑚 ∈ (ℤ_≥‘𝑠)))
65	55, 63, 64	sylanbrc 595	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑠 ∈ (0...𝑚))
66		fznn0sub2 13680	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ (0...𝑚) → (𝑚 − 𝑠) ∈ (0...𝑚))
67	65, 66	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ (0...𝑚))
68		elfzelz 13568	. . . . . . . . . . . . 13 ⊢ ((𝑚 − 𝑠) ∈ (0...𝑚) → (𝑚 − 𝑠) ∈ ℤ)
69	67, 68	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ ℤ)
70		eluz 12892	. . . . . . . . . . . 12 ⊢ (((𝑚 − 𝑠) ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑚 ∈ (ℤ_≥‘(𝑚 − 𝑠)) ↔ (𝑚 − 𝑠) ≤ 𝑚))
71	69, 50, 70	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 ∈ (ℤ_≥‘(𝑚 − 𝑠)) ↔ (𝑚 − 𝑠) ≤ 𝑚))
72	54, 71	mpbird 260	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑚 ∈ (ℤ_≥‘(𝑚 − 𝑠)))
73		fzss2 13609	. . . . . . . . . 10 ⊢ (𝑚 ∈ (ℤ_≥‘(𝑚 − 𝑠)) → (0...(𝑚 − 𝑠)) ⊆ (0...𝑚))
74	72, 73	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (0...(𝑚 − 𝑠)) ⊆ (0...𝑚))
75	74	sselda 3938	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑗 ∈ (0...𝑚))
76	13	abscld 15514	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (abs‘𝐴) ∈ ℝ)
77	11, 12, 76	syl2an 608	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘𝐴) ∈ ℝ)
78	36	abscld 15514	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ)
79	77, 78	remulcld 11254	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
80	75, 79	syldan 603	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
81	46, 80	fsumrecl 15808	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
82		fzfid 14027	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (((𝑚 − 𝑠) + 1)...𝑚) ∈ Fin)
83		elfznn0 13665	. . . . . . . . . . . . 13 ⊢ ((𝑚 − 𝑠) ∈ (0...𝑚) → (𝑚 − 𝑠) ∈ ℕ₀)
84	67, 83	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ ℕ₀)
85		peano2nn0 12559	. . . . . . . . . . . 12 ⊢ ((𝑚 − 𝑠) ∈ ℕ₀ → ((𝑚 − 𝑠) + 1) ∈ ℕ₀)
86	84, 85	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝑚 − 𝑠) + 1) ∈ ℕ₀)
87	86, 30	eleqtrdi 2875	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝑚 − 𝑠) + 1) ∈ (ℤ_≥‘0))
88		fzss1 13608	. . . . . . . . . 10 ⊢ (((𝑚 − 𝑠) + 1) ∈ (ℤ_≥‘0) → (((𝑚 − 𝑠) + 1)...𝑚) ⊆ (0...𝑚))
89	87, 88	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (((𝑚 − 𝑠) + 1)...𝑚) ⊆ (0...𝑚))
90	89	sselda 3938	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑗 ∈ (0...𝑚))
91	90, 79	syldan 603	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
92	82, 91	fsumrecl 15808	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
93	42	rphalfcld 13088	. . . . . . . 8 ⊢ (𝜑 → (𝐸 / 2) ∈ ℝ⁺)
94	93	rpred 13076	. . . . . . 7 ⊢ (𝜑 → (𝐸 / 2) ∈ ℝ)
95	94	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝐸 / 2) ∈ ℝ)
96		elfznn0 13665	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...(𝑚 − 𝑠)) → 𝑗 ∈ ℕ₀)
97	11, 96, 76	syl2an 608	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘𝐴) ∈ ℝ)
98	46, 97	fsumrecl 15808	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ∈ ℝ)
99	98, 95	remulcld 11254	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) ∈ ℝ)
100		0zd 12618	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ ℤ)
101		eqidd 2766	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (𝐾‘𝑗) = (𝐾‘𝑗))
102		mertens.2	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (𝐾‘𝑗) = (abs‘𝐴))
103	102, 76	eqeltrd 2865	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (𝐾‘𝑗) ∈ ℝ)
104		mertens.7	. . . . . . . . . . 11 ⊢ (𝜑 → seq0( + , 𝐾) ∈ dom ⇝ )
105	30, 100, 101, 103, 104	isumrecl 15839	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) ∈ ℝ)
106	13	absge0d 15522	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → 0 ≤ (abs‘𝐴))
107	106, 102	breqtrrd 5141	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → 0 ≤ (𝐾‘𝑗))
108	30, 100, 101, 103, 104, 107	isumge0 15840	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗))
109	105, 108	ge0p1rpd 13106	. . . . . . . . 9 ⊢ (𝜑 → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ⁺)
110	109	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ⁺)
111	99, 110	rerpdivcld 13107	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) ∈ ℝ)
112	93, 109	rpdivcld 13093	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) ∈ ℝ⁺)
113	112	rpred 13076	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) ∈ ℝ)
114	113	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) ∈ ℝ)
115	97, 114	remulcld 11254	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))) ∈ ℝ)
116	75, 20	syldan 603	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((𝑚 − 𝑗) + 1) ∈ ℤ)
117		simplll 787	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝜑)
118	75, 19	syldan 603	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((𝑚 − 𝑗) + 1) ∈ ℕ₀)
119	118, 22	sylan 592	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ₀)
120	117, 119, 24	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → (𝐺‘𝑘) = 𝐵)
121	117, 119, 26	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝐵 ∈ ℂ)
122	75, 35	syldan 603	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → seq((𝑚 − 𝑗) + 1)( + , 𝐺) ∈ dom ⇝ )
123	15, 116, 120, 121, 122	isumcl 15835	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵 ∈ ℂ)
124	123	abscld 15514	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ)
125	76, 106	jca 521	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)))
126	11, 96, 125	syl2an 608	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)))
127	120	sumeq2dv 15777	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)
128	127	fveq2d 6889	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)) = (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵))
129		fvoveq1 7442	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = (𝑚 − 𝑗) → (ℤ_≥‘(𝑛 + 1)) = (ℤ_≥‘((𝑚 − 𝑗) + 1)))
130	129	sumeq1d 15775	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = (𝑚 − 𝑗) → Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘))
131	130	fveq2d 6889	. . . . . . . . . . . . . 14 ⊢ (𝑛 = (𝑚 − 𝑗) → (abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) = (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)))
132	131	breq1d 5121	. . . . . . . . . . . . 13 ⊢ (𝑛 = (𝑚 − 𝑗) → ((abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) ↔ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
133	4	simprd 501	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑛 ∈ (ℤ_≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
134	133	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ∀𝑛 ∈ (ℤ_≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
135		elfzelz 13568	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...(𝑚 − 𝑠)) → 𝑗 ∈ ℤ)
136	135	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑗 ∈ ℤ)
137	136	zred 12716	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑗 ∈ ℝ)
138	49	ad2antlr 740	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑚 ∈ ℤ)
139	138	zred 12716	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑚 ∈ ℝ)
140	56	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑠 ∈ ℤ)
141	140	zred 12716	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑠 ∈ ℝ)
142		elfzle2 13572	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...(𝑚 − 𝑠)) → 𝑗 ≤ (𝑚 − 𝑠))
143	142	adantl 487	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑗 ≤ (𝑚 − 𝑠))
144	137, 139, 141, 143	lesubd 11833	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑠 ≤ (𝑚 − 𝑗))
145	138, 136	zsubcld 12721	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (𝑚 − 𝑗) ∈ ℤ)
146		eluz 12892	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 ∈ ℤ ∧ (𝑚 − 𝑗) ∈ ℤ) → ((𝑚 − 𝑗) ∈ (ℤ_≥‘𝑠) ↔ 𝑠 ≤ (𝑚 − 𝑗)))
147	140, 145, 146	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((𝑚 − 𝑗) ∈ (ℤ_≥‘𝑠) ↔ 𝑠 ≤ (𝑚 − 𝑗)))
148	144, 147	mpbird 260	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (𝑚 − 𝑗) ∈ (ℤ_≥‘𝑠))
149	132, 134, 148	rspcdva 3584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
150	128, 149	eqbrtrrd 5137	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
151	124, 114, 150	ltled 11373	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
152		lemul2a 12085	. . . . . . . . . 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 1400	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
154	46, 80, 115, 153	fsumle 15874	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
155	98	recnd 11252	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ∈ ℂ)
156	93	rpcnd 13078	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸 / 2) ∈ ℂ)
157	156	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝐸 / 2) ∈ ℂ)
158		peano2re 11398	. . . . . . . . . . . . 13 ⊢ (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) ∈ ℝ → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ)
159	105, 158	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ)
160	159	recnd 11252	. . . . . . . . . . 11 ⊢ (𝜑 → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℂ)
161	160	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℂ)
162	109	rpne0d 13081	. . . . . . . . . . 11 ⊢ (𝜑 → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ≠ 0)
163	162	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ≠ 0)
164	155, 157, 161, 163	divassd 12041	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) = (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
165		fveq2 6885	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑗 → (𝐾‘𝑛) = (𝐾‘𝑗))
166	165	cbvsumv 15771	. . . . . . . . . . . . . . . 16 ⊢ Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) = Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗)
167	166	oveq1i 7429	. . . . . . . . . . . . . . 15 ⊢ (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1) = (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)
168	167	oveq2i 7430	. . . . . . . . . . . . . 14 ⊢ ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1)) = ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))
169	168, 112	eqeltrid 2869	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1)) ∈ ℝ⁺)
170	169	rpcnd 13078	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1)) ∈ ℂ)
171	170	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1)) ∈ ℂ)
172	76	recnd 11252	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (abs‘𝐴) ∈ ℂ)
173	11, 96, 172	syl2an 608	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘𝐴) ∈ ℂ)
174	46, 171, 173	fsummulc1 15859	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1))) = Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1))))
175	168	oveq2i 7430	. . . . . . . . . 10 ⊢ (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1))) = (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
176	168	oveq2i 7430	. . . . . . . . . . . 12 ⊢ ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1))) = ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
177	176	a1i 11	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...(𝑚 − 𝑠)) → ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1))) = ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
178	177	sumeq2i 15773	. . . . . . . . . 10 ⊢ Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1))) = Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
179	174, 175, 178	3eqtr3g 2823	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))) = Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
180	164, 179	eqtrd 2800	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) = Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
181	154, 180	breqtrrd 5141	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
182	105	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) ∈ ℝ)
183	159	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ)
184		0zd 12618	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 0 ∈ ℤ)
185		fz0ssnn0 13667	. . . . . . . . . . . . 13 ⊢ (0...(𝑚 − 𝑠)) ⊆ ℕ₀
186	185	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (0...(𝑚 − 𝑠)) ⊆ ℕ₀)
187	102	adantlr 728	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ₀) → (𝐾‘𝑗) = (abs‘𝐴))
188	76	adantlr 728	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ₀) → (abs‘𝐴) ∈ ℝ)
189	106	adantlr 728	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ₀) → 0 ≤ (abs‘𝐴))
190	104	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → seq0( + , 𝐾) ∈ dom ⇝ )
191	30, 184, 46, 186, 187, 188, 189, 190	isumless 15922	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ≤ Σ𝑗 ∈ ℕ₀ (abs‘𝐴))
192	102	sumeq2dv 15777	. . . . . . . . . . . 12 ⊢ (𝜑 → Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) = Σ𝑗 ∈ ℕ₀ (abs‘𝐴))
193	192	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) = Σ𝑗 ∈ ℕ₀ (abs‘𝐴))
194	191, 193	breqtrrd 5141	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ≤ Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗))
195	105	ltp1d 12160	. . . . . . . . . . 11 ⊢ (𝜑 → Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))
196	195	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))
197	98, 182, 183, 194, 196	lelttrd 11383	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))
198	93	rpregt0d 13082	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 / 2) ∈ ℝ ∧ 0 < (𝐸 / 2)))
199	198	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝐸 / 2) ∈ ℝ ∧ 0 < (𝐸 / 2)))
200		ltmul1 12080	. . . . . . . . . 10 ⊢ ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ∈ ℝ ∧ (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ ∧ ((𝐸 / 2) ∈ ℝ ∧ 0 < (𝐸 / 2))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ↔ (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) · (𝐸 / 2))))
201	98, 183, 199, 200	syl3anc 1398	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ↔ (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) · (𝐸 / 2))))
202	197, 201	mpbid 235	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) · (𝐸 / 2)))
203	109	rpregt0d 13082	. . . . . . . . . 10 ⊢ (𝜑 → ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ ∧ 0 < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
204	203	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ ∧ 0 < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
205		ltdivmul 12105	. . . . . . . . 9 ⊢ (((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) ∈ ℝ ∧ (𝐸 / 2) ∈ ℝ ∧ ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ ∧ 0 < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))) → (((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) < (𝐸 / 2) ↔ (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) · (𝐸 / 2))))
206	99, 95, 204, 205	syl3anc 1398	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) < (𝐸 / 2) ↔ (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) · (𝐸 / 2))))
207	202, 206	mpbird 260	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) < (𝐸 / 2))
208	81, 111, 95, 181, 207	lelttrd 11383	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < (𝐸 / 2))
209		mertens.13	. . . . . . . . . . . 12 ⊢ (𝜑 → (0 ≤ sup(𝑇, ℝ, < ) ∧ (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧)))
210	209	simprd 501	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧))
211		suprcl 12190	. . . . . . . . . . 11 ⊢ ((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧) → sup(𝑇, ℝ, < ) ∈ ℝ)
212	210, 211	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → sup(𝑇, ℝ, < ) ∈ ℝ)
213	94, 212	remulcld 11254	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 / 2) · sup(𝑇, ℝ, < )) ∈ ℝ)
214	209	simpld 500	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ sup(𝑇, ℝ, < ))
215	212, 214	ge0p1rpd 13106	. . . . . . . . 9 ⊢ (𝜑 → (sup(𝑇, ℝ, < ) + 1) ∈ ℝ⁺)
216	213, 215	rerpdivcld 13107	. . . . . . . 8 ⊢ (𝜑 → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℝ)
217	216	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℝ)
218	5	nnrpd 13074	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑠 ∈ ℝ⁺)
219	93, 218	rpdivcld 13093	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐸 / 2) / 𝑠) ∈ ℝ⁺)
220	219, 215	rpdivcld 13093	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℝ⁺)
221	220	rpred 13076	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℝ)
222	221, 212	remulcld 11254	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈ ℝ)
223	222	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈ ℝ)
224		simpll 779	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝜑)
225	90, 12	syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑗 ∈ ℕ₀)
226	224, 225, 76	syl2anc 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘𝐴) ∈ ℝ)
227	221	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℝ)
228	224, 225, 102	syl2anc 596	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝐾‘𝑗) = (abs‘𝐴))
229		fveq2 6885	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑗 → (𝐾‘𝑚) = (𝐾‘𝑗))
230	229	breq1d 5121	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑗 → ((𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ↔ (𝐾‘𝑗) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))
231	7	simprd 501	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑚 ∈ (ℤ_≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))
232	231	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ∀𝑚 ∈ (ℤ_≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))
233		elfzuz 13564	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚) → 𝑗 ∈ (ℤ_≥‘((𝑚 − 𝑠) + 1)))
234		eluzle 12891	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡)) → (𝑠 + 𝑡) ≤ 𝑚)
235	234	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑠 + 𝑡) ≤ 𝑚)
236	8	nn0zd 12631	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑡 ∈ ℤ)
237	236	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑡 ∈ ℤ)
238	237	zred 12716	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑡 ∈ ℝ)
239	52, 238, 51	leaddsub2d 11831	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝑠 + 𝑡) ≤ 𝑚 ↔ 𝑡 ≤ (𝑚 − 𝑠)))
240	235, 239	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑡 ≤ (𝑚 − 𝑠))
241		eluz 12892	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑡 ∈ ℤ ∧ (𝑚 − 𝑠) ∈ ℤ) → ((𝑚 − 𝑠) ∈ (ℤ_≥‘𝑡) ↔ 𝑡 ≤ (𝑚 − 𝑠)))
242	237, 69, 241	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝑚 − 𝑠) ∈ (ℤ_≥‘𝑡) ↔ 𝑡 ≤ (𝑚 − 𝑠)))
243	240, 242	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ (ℤ_≥‘𝑡))
244		peano2uz 12941	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 − 𝑠) ∈ (ℤ_≥‘𝑡) → ((𝑚 − 𝑠) + 1) ∈ (ℤ_≥‘𝑡))
245	243, 244	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝑚 − 𝑠) + 1) ∈ (ℤ_≥‘𝑡))
246		uztrn 12896	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ (ℤ_≥‘((𝑚 − 𝑠) + 1)) ∧ ((𝑚 − 𝑠) + 1) ∈ (ℤ_≥‘𝑡)) → 𝑗 ∈ (ℤ_≥‘𝑡))
247	233, 245, 246	syl2anr 609	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑗 ∈ (ℤ_≥‘𝑡))
248	230, 232, 247	rspcdva 3584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝐾‘𝑗) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))
249	228, 248	eqbrtrrd 5137	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘𝐴) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))
250	226, 227, 249	ltled 11373	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘𝐴) ≤ (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))
251	210	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧))
252	51	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑚 ∈ ℝ)
253		peano2zm 12652	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ ℤ → (𝑠 − 1) ∈ ℤ)
254	56, 253	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑠 − 1) ∈ ℤ)
255	254	zred 12716	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑠 − 1) ∈ ℝ)
256	255	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑠 − 1) ∈ ℝ)
257	225	nn0red 12581	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑗 ∈ ℝ)
258	50	zcnd 12717	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑚 ∈ ℂ)
259	52	recnd 11252	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑠 ∈ ℂ)
260		1cnd 11217	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 1 ∈ ℂ)
261	258, 259, 260	subsubd 11612	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − (𝑠 − 1)) = ((𝑚 − 𝑠) + 1))
262	261	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − (𝑠 − 1)) = ((𝑚 − 𝑠) + 1))
263		elfzle1 13571	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚) → ((𝑚 − 𝑠) + 1) ≤ 𝑗)
264	263	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((𝑚 − 𝑠) + 1) ≤ 𝑗)
265	262, 264	eqbrtrd 5135	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − (𝑠 − 1)) ≤ 𝑗)
266	252, 256, 257, 265	subled 11832	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − 𝑗) ≤ (𝑠 − 1))
267	90, 16	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − 𝑗) ∈ ℕ₀)
268	267, 30	eleqtrdi 2875	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − 𝑗) ∈ (ℤ_≥‘0))
269	254	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑠 − 1) ∈ ℤ)
270		elfz5 13560	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 − 𝑗) ∈ (ℤ_≥‘0) ∧ (𝑠 − 1) ∈ ℤ) → ((𝑚 − 𝑗) ∈ (0...(𝑠 − 1)) ↔ (𝑚 − 𝑗) ≤ (𝑠 − 1)))
271	268, 269, 270	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((𝑚 − 𝑗) ∈ (0...(𝑠 − 1)) ↔ (𝑚 − 𝑗) ≤ (𝑠 − 1)))
272	266, 271	mpbird 260	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − 𝑗) ∈ (0...(𝑠 − 1)))
273		simplll 787	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝜑)
274	90, 19	syldan 603	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((𝑚 − 𝑗) + 1) ∈ ℕ₀)
275	274, 22	sylan 592	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ₀)
276	273, 275, 24	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → (𝐺‘𝑘) = 𝐵)
277	276	sumeq2dv 15777	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)
278	277	eqcomd 2771	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵 = Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘))
279	278	fveq2d 6889	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)))
280	131	rspceeqv 3606	. . . . . . . . . . . . 13 ⊢ (((𝑚 − 𝑗) ∈ (0...(𝑠 − 1)) ∧ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘))) → ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)))
281	272, 279, 280	syl2anc 596	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)))
282		fvex 6898	. . . . . . . . . . . . 13 ⊢ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ V
283		eqeq1 2769	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) → (𝑧 = (abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) ↔ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘))))
284	283	rexbidv 3191	. . . . . . . . . . . . 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 3643	. . . . . . . . . . . 12 ⊢ ((abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ 𝑇 ↔ ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)))
287	281, 286	sylibr 237	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ 𝑇)
288		suprub 12191	. . . . . . . . . . 11 ⊢ (((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧) ∧ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ 𝑇) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ sup(𝑇, ℝ, < ))
289	251, 287, 288	syl2anc 596	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ sup(𝑇, ℝ, < ))
290	224, 225, 125	syl2anc 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)))
291	90, 78	syldan 603	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ)
292	36	absge0d 15522	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → 0 ≤ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵))
293	90, 292	syldan 603	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 0 ≤ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵))
294	291, 293	jca 521	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ ∧ 0 ≤ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)))
295	212	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → sup(𝑇, ℝ, < ) ∈ ℝ)
296		lemul12a 12088	. . . . . . . . . . 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 852	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (((abs‘𝐴) ≤ (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∧ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ sup(𝑇, ℝ, < )) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))))
298	250, 289, 297	mp2and 712	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )))
299	82, 91, 223, 298	fsumle 15874	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )))
300	222	recnd 11252	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈ ℂ)
301	300	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈ ℂ)
302		fsumconst 15864	. . . . . . . . . 10 ⊢ (((((𝑚 − 𝑠) + 1)...𝑚) ∈ Fin ∧ ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈ ℂ) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) = ((♯‘(((𝑚 − 𝑠) + 1)...𝑚)) · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))))
303	82, 301, 302	syl2anc 596	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) = ((♯‘(((𝑚 − 𝑠) + 1)...𝑚)) · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))))
304		1zzd 12640	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 1 ∈ ℤ)
305	56	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑠 ∈ ℤ)
306		fzen 13585	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ (𝑚 − 𝑠) ∈ ℤ) → (1...𝑠) ≈ ((1 + (𝑚 − 𝑠))...(𝑠 + (𝑚 − 𝑠))))
307	304, 305, 69, 306	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (1...𝑠) ≈ ((1 + (𝑚 − 𝑠))...(𝑠 + (𝑚 − 𝑠))))
308		ax-1cn 11173	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
309	69	zcnd 12717	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ ℂ)
310		addcom 11411	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℂ ∧ (𝑚 − 𝑠) ∈ ℂ) → (1 + (𝑚 − 𝑠)) = ((𝑚 − 𝑠) + 1))
311	308, 309, 310	sylancr 599	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (1 + (𝑚 − 𝑠)) = ((𝑚 − 𝑠) + 1))
312	259, 258	pncan3d 11587	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑠 + (𝑚 − 𝑠)) = 𝑚)
313	311, 312	oveq12d 7437	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((1 + (𝑚 − 𝑠))...(𝑠 + (𝑚 − 𝑠))) = (((𝑚 − 𝑠) + 1)...𝑚))
314	307, 313	breqtrd 5139	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (1...𝑠) ≈ (((𝑚 − 𝑠) + 1)...𝑚))
315		fzfid 14027	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (1...𝑠) ∈ Fin)
316		hashen 14401	. . . . . . . . . . . . 13 ⊢ (((1...𝑠) ∈ Fin ∧ (((𝑚 − 𝑠) + 1)...𝑚) ∈ Fin) → ((♯‘(1...𝑠)) = (♯‘(((𝑚 − 𝑠) + 1)...𝑚)) ↔ (1...𝑠) ≈ (((𝑚 − 𝑠) + 1)...𝑚)))
317	315, 82, 316	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((♯‘(1...𝑠)) = (♯‘(((𝑚 − 𝑠) + 1)...𝑚)) ↔ (1...𝑠) ≈ (((𝑚 − 𝑠) + 1)...𝑚)))
318	314, 317	mpbird 260	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (♯‘(1...𝑠)) = (♯‘(((𝑚 − 𝑠) + 1)...𝑚)))
319		hashfz1 14400	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ℕ₀ → (♯‘(1...𝑠)) = 𝑠)
320	47, 319	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (♯‘(1...𝑠)) = 𝑠)
321	318, 320	eqtr3d 2802	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (♯‘(((𝑚 − 𝑠) + 1)...𝑚)) = 𝑠)
322	321	oveq1d 7434	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((♯‘(((𝑚 − 𝑠) + 1)...𝑚)) · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))) = (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))))
323	212	recnd 11252	. . . . . . . . . . . 12 ⊢ (𝜑 → sup(𝑇, ℝ, < ) ∈ ℂ)
324	215	rpcnne0d 13085	. . . . . . . . . . . 12 ⊢ (𝜑 → ((sup(𝑇, ℝ, < ) + 1) ∈ ℂ ∧ (sup(𝑇, ℝ, < ) + 1) ≠ 0))
325		div23 11906	. . . . . . . . . . . 12 ⊢ (((𝐸 / 2) ∈ ℂ ∧ sup(𝑇, ℝ, < ) ∈ ℂ ∧ ((sup(𝑇, ℝ, < ) + 1) ∈ ℂ ∧ (sup(𝑇, ℝ, < ) + 1) ≠ 0)) → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) = (((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )))
326	156, 323, 324, 325	syl3anc 1398	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) = (((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )))
327	56	zcnd 12717	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑠 ∈ ℂ)
328	219	rpcnd 13078	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐸 / 2) / 𝑠) ∈ ℂ)
329		divass 11905	. . . . . . . . . . . . . 14 ⊢ ((𝑠 ∈ ℂ ∧ ((𝐸 / 2) / 𝑠) ∈ ℂ ∧ ((sup(𝑇, ℝ, < ) + 1) ∈ ℂ ∧ (sup(𝑇, ℝ, < ) + 1) ≠ 0)) → ((𝑠 · ((𝐸 / 2) / 𝑠)) / (sup(𝑇, ℝ, < ) + 1)) = (𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))
330	327, 328, 324, 329	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑠 · ((𝐸 / 2) / 𝑠)) / (sup(𝑇, ℝ, < ) + 1)) = (𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))
331	5	nnne0d 12301	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑠 ≠ 0)
332	156, 327, 331	divcan2d 12008	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑠 · ((𝐸 / 2) / 𝑠)) = (𝐸 / 2))
333	332	oveq1d 7434	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑠 · ((𝐸 / 2) / 𝑠)) / (sup(𝑇, ℝ, < ) + 1)) = ((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)))
334	330, 333	eqtr3d 2802	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) = ((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)))
335	334	oveq1d 7434	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) · sup(𝑇, ℝ, < )) = (((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )))
336	220	rpcnd 13078	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℂ)
337	327, 336, 323	mulassd 11247	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) · sup(𝑇, ℝ, < )) = (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))))
338	326, 335, 337	3eqtr2rd 2807	. . . . . . . . . 10 ⊢ (𝜑 → (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))) = (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)))
339	338	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))) = (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)))
340	303, 322, 339	3eqtrd 2804	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) = (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)))
341	299, 340	breqtrd 5139	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)))
342		peano2re 11398	. . . . . . . . . . 11 ⊢ (sup(𝑇, ℝ, < ) ∈ ℝ → (sup(𝑇, ℝ, < ) + 1) ∈ ℝ)
343	212, 342	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (sup(𝑇, ℝ, < ) + 1) ∈ ℝ)
344	212	ltp1d 12160	. . . . . . . . . 10 ⊢ (𝜑 → sup(𝑇, ℝ, < ) < (sup(𝑇, ℝ, < ) + 1))
345	212, 343, 93, 344	ltmul2dd 13132	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 / 2) · sup(𝑇, ℝ, < )) < ((𝐸 / 2) · (sup(𝑇, ℝ, < ) + 1)))
346	213, 94, 215	ltdivmul2d 13128	. . . . . . . . 9 ⊢ (𝜑 → ((((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) < (𝐸 / 2) ↔ ((𝐸 / 2) · sup(𝑇, ℝ, < )) < ((𝐸 / 2) · (sup(𝑇, ℝ, < ) + 1))))
347	345, 346	mpbird 260	. . . . . . . 8 ⊢ (𝜑 → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) < (𝐸 / 2))
348	347	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) < (𝐸 / 2))
349	92, 217, 95, 341, 348	lelttrd 11383	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < (𝐸 / 2))
350	81, 92, 95, 95, 208, 349	lt2addd 11852	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) + Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵))) < ((𝐸 / 2) + (𝐸 / 2)))
351	14, 36	absmuld 15532	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) = ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)))
352	351	sumeq2dv 15777	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) = Σ𝑗 ∈ (0...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)))
353	69	zred 12716	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ ℝ)
354	353	ltp1d 12160	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) < ((𝑚 − 𝑠) + 1))
355		fzdisj 13596	. . . . . . . 8 ⊢ ((𝑚 − 𝑠) < ((𝑚 − 𝑠) + 1) → ((0...(𝑚 − 𝑠)) ∩ (((𝑚 − 𝑠) + 1)...𝑚)) = ∅)
356	354, 355	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((0...(𝑚 − 𝑠)) ∩ (((𝑚 − 𝑠) + 1)...𝑚)) = ∅)
357		fzsplit 13595	. . . . . . . 8 ⊢ ((𝑚 − 𝑠) ∈ (0...𝑚) → (0...𝑚) = ((0...(𝑚 − 𝑠)) ∪ (((𝑚 − 𝑠) + 1)...𝑚)))
358	67, 357	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (0...𝑚) = ((0...(𝑚 − 𝑠)) ∪ (((𝑚 − 𝑠) + 1)...𝑚)))
359	79	recnd 11252	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℂ)
360	356, 358, 10, 359	fsumsplit 15815	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) = (Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) + Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵))))
361	352, 360	eqtr2d 2801	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) + Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵))) = Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)))
362	42	rpcnd 13078	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ ℂ)
363	362	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝐸 ∈ ℂ)
364	363	2halvesd 12505	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝐸 / 2) + (𝐸 / 2)) = 𝐸)
365	350, 361, 364	3brtr3d 5144	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)
366	39, 41, 44, 45, 365	lelttrd 11383	. . 3 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)
367	366	ralrimiva 3159	. 2 ⊢ (𝜑 → ∀𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)
368		fveq2 6885	. . . 4 ⊢ (𝑦 = (𝑠 + 𝑡) → (ℤ_≥‘𝑦) = (ℤ_≥‘(𝑠 + 𝑡)))
369	368	raleqdv 3325	. . 3 ⊢ (𝑦 = (𝑠 + 𝑡) → (∀𝑚 ∈ (ℤ_≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸 ↔ ∀𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸))
370	369	rspcev 3583	. 2 ⊢ (((𝑠 + 𝑡) ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸) → ∃𝑦 ∈ ℕ₀ ∀𝑚 ∈ (ℤ_≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)
371	9, 367, 370	syl2anc 596	1 ⊢ (𝜑 → ∃𝑦 ∈ ℕ₀ ∀𝑚 ∈ (ℤ_≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2146 {cab 2743 ≠ wne 2960 ∀wral 3081 ∃wrex 3091 ∪ cun 3904 ∩ cin 3905 ⊆ wss 3906 ∅c0 4286 class class class wbr 5111 dom cdm 5663 ‘cfv 6540 (class class class)co 7419 ≈ cen 8946 Fincfn 8949 supcsup 9407 ℂcc 11113 ℝcr 11114 0cc0 11115 1c1 11116 + caddc 11118 · cmul 11120 < clt 11258 ≤ cle 11259 − cmin 11456 / cdiv 11886 ℕcn 12248 2c2 12310 ℕ₀cn0 12519 ℤcz 12606 ℤ_≥cuz 12878 ℝ⁺crp 13032 ...cfz 13551 seqcseq 14055 ♯chash 14384 abscabs 15309 ⇝ cli 15559 Σcsu 15761

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742 ax-inf2 9617 ax-cnex 11171 ax-resscn 11172 ax-1cn 11173 ax-icn 11174 ax-addcl 11175 ax-addrcl 11176 ax-mulcl 11177 ax-mulrcl 11178 ax-mulcom 11179 ax-addass 11180 ax-mulass 11181 ax-distr 11182 ax-i2m1 11183 ax-1ne0 11184 ax-1rid 11185 ax-rnegex 11186 ax-rrecex 11187 ax-cnre 11188 ax-pre-lttri 11189 ax-pre-lttrn 11190 ax-pre-ltadd 11191 ax-pre-mulgt0 11192 ax-pre-sup 11193

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-se 5617 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7376 df-ov 7422 df-oprab 7423 df-mpo 7424 df-om 7869 df-1st 7992 df-2nd 7993 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-er 8700 df-pm 8833 df-en 8950 df-dom 8951 df-sdom 8952 df-fin 8953 df-sup 9409 df-inf 9410 df-oi 9479 df-card 9941 df-pnf 11260 df-mnf 11261 df-xr 11262 df-ltxr 11263 df-le 11264 df-sub 11458 df-neg 11459 df-div 11887 df-nn 12249 df-2 12318 df-3 12319 df-n0 12520 df-z 12607 df-uz 12879 df-rp 13033 df-ico 13394 df-fz 13552 df-fzo 13700 df-fl 13843 df-seq 14056 df-exp 14116 df-hash 14385 df-cj 15174 df-re 15175 df-im 15176 df-sqrt 15310 df-abs 15311 df-clim 15563 df-rlim 15564 df-sum 15762

This theorem is used by: mertenslem2 15962

W3C validator