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 14989

Description: Lemma for mertens 14991. (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 490	. . . . . 6 ⊢ (𝜑 → 𝜓)
3		mertens.11	. . . . . 6 ⊢ (𝜓 ↔ (𝑠 ∈ ℕ ∧ ∀𝑛 ∈ (ℤ_≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
4	2, 3	sylib 210	. . . . 5 ⊢ (𝜑 → (𝑠 ∈ ℕ ∧ ∀𝑛 ∈ (ℤ_≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
5	4	simpld 490	. . . 4 ⊢ (𝜑 → 𝑠 ∈ ℕ)
6	5	nnnn0d 11678	. . 3 ⊢ (𝜑 → 𝑠 ∈ ℕ₀)
7	1	simprd 491	. . . 4 ⊢ (𝜑 → (𝑡 ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))
8	7	simpld 490	. . 3 ⊢ (𝜑 → 𝑡 ∈ ℕ₀)
9	6, 8	nn0addcld 11682	. 2 ⊢ (𝜑 → (𝑠 + 𝑡) ∈ ℕ₀)
10		fzfid 13067	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (0...𝑚) ∈ Fin)
11		simpl 476	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝜑)
12		elfznn0 12727	. . . . . . . 8 ⊢ (𝑗 ∈ (0...𝑚) → 𝑗 ∈ ℕ₀)
13		mertens.3	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → 𝐴 ∈ ℂ)
14	11, 12, 13	syl2an 589	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → 𝐴 ∈ ℂ)
15		eqid 2825	. . . . . . . 8 ⊢ (ℤ_≥‘((𝑚 − 𝑗) + 1)) = (ℤ_≥‘((𝑚 − 𝑗) + 1))
16		fznn0sub 12666	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...𝑚) → (𝑚 − 𝑗) ∈ ℕ₀)
17	16	adantl 475	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (𝑚 − 𝑗) ∈ ℕ₀)
18		peano2nn0 11660	. . . . . . . . . 10 ⊢ ((𝑚 − 𝑗) ∈ ℕ₀ → ((𝑚 − 𝑗) + 1) ∈ ℕ₀)
19	17, 18	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((𝑚 − 𝑗) + 1) ∈ ℕ₀)
20	19	nn0zd 11808	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((𝑚 − 𝑗) + 1) ∈ ℤ)
21		simplll 791	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝜑)
22		eluznn0 12040	. . . . . . . . . 10 ⊢ ((((𝑚 − 𝑗) + 1) ∈ ℕ₀ ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ₀)
23	19, 22	sylan 575	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ₀)
24		mertens.4	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝐺‘𝑘) = 𝐵)
25	21, 23, 24	syl2anc 579	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → (𝐺‘𝑘) = 𝐵)
26		mertens.5	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → 𝐵 ∈ ℂ)
27	21, 23, 26	syl2anc 579	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝐵 ∈ ℂ)
28		mertens.8	. . . . . . . . . 10 ⊢ (𝜑 → seq0( + , 𝐺) ∈ dom ⇝ )
29	28	ad2antrr 717	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → seq0( + , 𝐺) ∈ dom ⇝ )
30		nn0uz 12004	. . . . . . . . . 10 ⊢ ℕ₀ = (ℤ_≥‘0)
31		simpll 783	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → 𝜑)
32	24, 26	eqeltrd 2906	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝐺‘𝑘) ∈ ℂ)
33	31, 32	sylan 575	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ ℕ₀) → (𝐺‘𝑘) ∈ ℂ)
34	30, 19, 33	iserex 14764	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (seq0( + , 𝐺) ∈ dom ⇝ ↔ seq((𝑚 − 𝑗) + 1)( + , 𝐺) ∈ dom ⇝ ))
35	29, 34	mpbid 224	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → seq((𝑚 − 𝑗) + 1)( + , 𝐺) ∈ dom ⇝ )
36	15, 20, 25, 27, 35	isumcl 14867	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵 ∈ ℂ)
37	14, 36	mulcld 10377	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℂ)
38	10, 37	fsumcl 14841	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℂ)
39	38	abscld 14552	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
40	37	abscld 14552	. . . . 5 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
41	10, 40	fsumrecl 14842	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
42		mertens.9	. . . . . 6 ⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
43	42	rpred 12156	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ ℝ)
44	43	adantr 474	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝐸 ∈ ℝ)
45	10, 37	fsumabs 14907	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)))
46		fzfid 13067	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (0...(𝑚 − 𝑠)) ∈ Fin)
47	6	adantr 474	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑠 ∈ ℕ₀)
48	47	nn0ge0d 11681	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 0 ≤ 𝑠)
49		eluzelz 11978	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡)) → 𝑚 ∈ ℤ)
50	49	adantl 475	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑚 ∈ ℤ)
51	50	zred 11810	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑚 ∈ ℝ)
52	47	nn0red 11679	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑠 ∈ ℝ)
53	51, 52	subge02d 10944	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (0 ≤ 𝑠 ↔ (𝑚 − 𝑠) ≤ 𝑚))
54	48, 53	mpbid 224	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ≤ 𝑚)
55	47, 30	syl6eleq 2916	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑠 ∈ (ℤ_≥‘0))
56	5	nnzd 11809	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑠 ∈ ℤ)
57		uzid 11983	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ ℤ → 𝑠 ∈ (ℤ_≥‘𝑠))
58	56, 57	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑠 ∈ (ℤ_≥‘𝑠))
59		uzaddcl 12026	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 ∈ (ℤ_≥‘𝑠) ∧ 𝑡 ∈ ℕ₀) → (𝑠 + 𝑡) ∈ (ℤ_≥‘𝑠))
60	58, 8, 59	syl2anc 579	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑠 + 𝑡) ∈ (ℤ_≥‘𝑠))
61		eqid 2825	. . . . . . . . . . . . . . . . 17 ⊢ (ℤ_≥‘𝑠) = (ℤ_≥‘𝑠)
62	61	uztrn2 11986	. . . . . . . . . . . . . . . 16 ⊢ (((𝑠 + 𝑡) ∈ (ℤ_≥‘𝑠) ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑚 ∈ (ℤ_≥‘𝑠))
63	60, 62	sylan 575	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑚 ∈ (ℤ_≥‘𝑠))
64		elfzuzb 12629	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ (0...𝑚) ↔ (𝑠 ∈ (ℤ_≥‘0) ∧ 𝑚 ∈ (ℤ_≥‘𝑠)))
65	55, 63, 64	sylanbrc 578	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑠 ∈ (0...𝑚))
66		fznn0sub2 12741	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ (0...𝑚) → (𝑚 − 𝑠) ∈ (0...𝑚))
67	65, 66	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ (0...𝑚))
68		elfzelz 12635	. . . . . . . . . . . . 13 ⊢ ((𝑚 − 𝑠) ∈ (0...𝑚) → (𝑚 − 𝑠) ∈ ℤ)
69	67, 68	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ ℤ)
70		eluz 11982	. . . . . . . . . . . 12 ⊢ (((𝑚 − 𝑠) ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑚 ∈ (ℤ_≥‘(𝑚 − 𝑠)) ↔ (𝑚 − 𝑠) ≤ 𝑚))
71	69, 50, 70	syl2anc 579	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 ∈ (ℤ_≥‘(𝑚 − 𝑠)) ↔ (𝑚 − 𝑠) ≤ 𝑚))
72	54, 71	mpbird 249	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑚 ∈ (ℤ_≥‘(𝑚 − 𝑠)))
73		fzss2 12674	. . . . . . . . . 10 ⊢ (𝑚 ∈ (ℤ_≥‘(𝑚 − 𝑠)) → (0...(𝑚 − 𝑠)) ⊆ (0...𝑚))
74	72, 73	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (0...(𝑚 − 𝑠)) ⊆ (0...𝑚))
75	74	sselda 3827	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑗 ∈ (0...𝑚))
76	13	abscld 14552	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (abs‘𝐴) ∈ ℝ)
77	11, 12, 76	syl2an 589	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘𝐴) ∈ ℝ)
78	36	abscld 14552	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ)
79	77, 78	remulcld 10387	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
80	75, 79	syldan 585	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
81	46, 80	fsumrecl 14842	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
82		fzfid 13067	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (((𝑚 − 𝑠) + 1)...𝑚) ∈ Fin)
83		elfznn0 12727	. . . . . . . . . . . . 13 ⊢ ((𝑚 − 𝑠) ∈ (0...𝑚) → (𝑚 − 𝑠) ∈ ℕ₀)
84	67, 83	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ ℕ₀)
85		peano2nn0 11660	. . . . . . . . . . . 12 ⊢ ((𝑚 − 𝑠) ∈ ℕ₀ → ((𝑚 − 𝑠) + 1) ∈ ℕ₀)
86	84, 85	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝑚 − 𝑠) + 1) ∈ ℕ₀)
87	86, 30	syl6eleq 2916	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝑚 − 𝑠) + 1) ∈ (ℤ_≥‘0))
88		fzss1 12673	. . . . . . . . . 10 ⊢ (((𝑚 − 𝑠) + 1) ∈ (ℤ_≥‘0) → (((𝑚 − 𝑠) + 1)...𝑚) ⊆ (0...𝑚))
89	87, 88	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (((𝑚 − 𝑠) + 1)...𝑚) ⊆ (0...𝑚))
90	89	sselda 3827	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑗 ∈ (0...𝑚))
91	90, 79	syldan 585	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
92	82, 91	fsumrecl 14842	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ)
93	42	rphalfcld 12168	. . . . . . . 8 ⊢ (𝜑 → (𝐸 / 2) ∈ ℝ⁺)
94	93	rpred 12156	. . . . . . 7 ⊢ (𝜑 → (𝐸 / 2) ∈ ℝ)
95	94	adantr 474	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝐸 / 2) ∈ ℝ)
96		elfznn0 12727	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...(𝑚 − 𝑠)) → 𝑗 ∈ ℕ₀)
97	11, 96, 76	syl2an 589	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘𝐴) ∈ ℝ)
98	46, 97	fsumrecl 14842	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ∈ ℝ)
99	98, 95	remulcld 10387	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) ∈ ℝ)
100		0zd 11716	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ ℤ)
101		eqidd 2826	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (𝐾‘𝑗) = (𝐾‘𝑗))
102		mertens.2	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (𝐾‘𝑗) = (abs‘𝐴))
103	102, 76	eqeltrd 2906	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (𝐾‘𝑗) ∈ ℝ)
104		mertens.7	. . . . . . . . . . 11 ⊢ (𝜑 → seq0( + , 𝐾) ∈ dom ⇝ )
105	30, 100, 101, 103, 104	isumrecl 14871	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) ∈ ℝ)
106	13	absge0d 14560	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → 0 ≤ (abs‘𝐴))
107	106, 102	breqtrrd 4901	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → 0 ≤ (𝐾‘𝑗))
108	30, 100, 101, 103, 104, 107	isumge0 14872	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗))
109	105, 108	ge0p1rpd 12186	. . . . . . . . 9 ⊢ (𝜑 → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ⁺)
110	109	adantr 474	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ⁺)
111	99, 110	rerpdivcld 12187	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) ∈ ℝ)
112	93, 109	rpdivcld 12173	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) ∈ ℝ⁺)
113	112	rpred 12156	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) ∈ ℝ)
114	113	ad2antrr 717	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) ∈ ℝ)
115	97, 114	remulcld 10387	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))) ∈ ℝ)
116	75, 20	syldan 585	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((𝑚 − 𝑗) + 1) ∈ ℤ)
117		simplll 791	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝜑)
118	75, 19	syldan 585	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((𝑚 − 𝑗) + 1) ∈ ℕ₀)
119	118, 22	sylan 575	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ₀)
120	117, 119, 24	syl2anc 579	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → (𝐺‘𝑘) = 𝐵)
121	117, 119, 26	syl2anc 579	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝐵 ∈ ℂ)
122	75, 35	syldan 585	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → seq((𝑚 − 𝑗) + 1)( + , 𝐺) ∈ dom ⇝ )
123	15, 116, 120, 121, 122	isumcl 14867	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵 ∈ ℂ)
124	123	abscld 14552	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ)
125	76, 106	jca 507	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)))
126	11, 96, 125	syl2an 589	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)))
127	120	sumeq2dv 14810	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)
128	127	fveq2d 6437	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)) = (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵))
129		fvoveq1 6928	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = (𝑚 − 𝑗) → (ℤ_≥‘(𝑛 + 1)) = (ℤ_≥‘((𝑚 − 𝑗) + 1)))
130	129	sumeq1d 14808	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = (𝑚 − 𝑗) → Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘))
131	130	fveq2d 6437	. . . . . . . . . . . . . 14 ⊢ (𝑛 = (𝑚 − 𝑗) → (abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) = (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)))
132	131	breq1d 4883	. . . . . . . . . . . . 13 ⊢ (𝑛 = (𝑚 − 𝑗) → ((abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) ↔ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
133	4	simprd 491	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑛 ∈ (ℤ_≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
134	133	ad2antrr 717	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ∀𝑛 ∈ (ℤ_≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
135		elfzelz 12635	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...(𝑚 − 𝑠)) → 𝑗 ∈ ℤ)
136	135	adantl 475	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑗 ∈ ℤ)
137	136	zred 11810	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑗 ∈ ℝ)
138	49	ad2antlr 718	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑚 ∈ ℤ)
139	138	zred 11810	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑚 ∈ ℝ)
140	56	ad2antrr 717	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑠 ∈ ℤ)
141	140	zred 11810	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑠 ∈ ℝ)
142		elfzle2 12638	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...(𝑚 − 𝑠)) → 𝑗 ≤ (𝑚 − 𝑠))
143	142	adantl 475	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑗 ≤ (𝑚 − 𝑠))
144	137, 139, 141, 143	lesubd 10956	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑠 ≤ (𝑚 − 𝑗))
145	138, 136	zsubcld 11815	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (𝑚 − 𝑗) ∈ ℤ)
146		eluz 11982	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 ∈ ℤ ∧ (𝑚 − 𝑗) ∈ ℤ) → ((𝑚 − 𝑗) ∈ (ℤ_≥‘𝑠) ↔ 𝑠 ≤ (𝑚 − 𝑗)))
147	140, 145, 146	syl2anc 579	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((𝑚 − 𝑗) ∈ (ℤ_≥‘𝑠) ↔ 𝑠 ≤ (𝑚 − 𝑗)))
148	144, 147	mpbird 249	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (𝑚 − 𝑗) ∈ (ℤ_≥‘𝑠))
149	132, 134, 148	rspcdva 3532	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
150	128, 149	eqbrtrrd 4897	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
151	124, 114, 150	ltled 10504	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
152		lemul2a 11208	. . . . . . . . . 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 1496	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
154	46, 80, 115, 153	fsumle 14905	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
155	98	recnd 10385	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ∈ ℂ)
156	93	rpcnd 12158	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸 / 2) ∈ ℂ)
157	156	adantr 474	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝐸 / 2) ∈ ℂ)
158		peano2re 10528	. . . . . . . . . . . . 13 ⊢ (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) ∈ ℝ → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ)
159	105, 158	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ)
160	159	recnd 10385	. . . . . . . . . . 11 ⊢ (𝜑 → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℂ)
161	160	adantr 474	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℂ)
162	109	rpne0d 12161	. . . . . . . . . . 11 ⊢ (𝜑 → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ≠ 0)
163	162	adantr 474	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ≠ 0)
164	155, 157, 161, 163	divassd 11162	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) = (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
165		fveq2 6433	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑗 → (𝐾‘𝑛) = (𝐾‘𝑗))
166	165	cbvsumv 14803	. . . . . . . . . . . . . . . 16 ⊢ Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) = Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗)
167	166	oveq1i 6915	. . . . . . . . . . . . . . 15 ⊢ (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1) = (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)
168	167	oveq2i 6916	. . . . . . . . . . . . . 14 ⊢ ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1)) = ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))
169	168, 112	syl5eqel 2910	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1)) ∈ ℝ⁺)
170	169	rpcnd 12158	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1)) ∈ ℂ)
171	170	adantr 474	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1)) ∈ ℂ)
172	76	recnd 10385	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (abs‘𝐴) ∈ ℂ)
173	11, 96, 172	syl2an 589	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘𝐴) ∈ ℂ)
174	46, 171, 173	fsummulc1 14891	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1))) = Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1))))
175	168	oveq2i 6916	. . . . . . . . . 10 ⊢ (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1))) = (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
176	168	oveq2i 6916	. . . . . . . . . . . 12 ⊢ ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1))) = ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
177	176	a1i 11	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...(𝑚 − 𝑠)) → ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1))) = ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
178	177	sumeq2i 14806	. . . . . . . . . 10 ⊢ Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ₀ (𝐾‘𝑛) + 1))) = Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
179	174, 175, 178	3eqtr3g 2884	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))) = Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
180	164, 179	eqtrd 2861	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) = Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))))
181	154, 180	breqtrrd 4901	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
182	105	adantr 474	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) ∈ ℝ)
183	159	adantr 474	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ)
184		0zd 11716	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 0 ∈ ℤ)
185		fz0ssnn0 12729	. . . . . . . . . . . . 13 ⊢ (0...(𝑚 − 𝑠)) ⊆ ℕ₀
186	185	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (0...(𝑚 − 𝑠)) ⊆ ℕ₀)
187	102	adantlr 706	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ₀) → (𝐾‘𝑗) = (abs‘𝐴))
188	76	adantlr 706	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ₀) → (abs‘𝐴) ∈ ℝ)
189	106	adantlr 706	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ₀) → 0 ≤ (abs‘𝐴))
190	104	adantr 474	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → seq0( + , 𝐾) ∈ dom ⇝ )
191	30, 184, 46, 186, 187, 188, 189, 190	isumless 14951	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ≤ Σ𝑗 ∈ ℕ₀ (abs‘𝐴))
192	102	sumeq2dv 14810	. . . . . . . . . . . 12 ⊢ (𝜑 → Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) = Σ𝑗 ∈ ℕ₀ (abs‘𝐴))
193	192	adantr 474	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) = Σ𝑗 ∈ ℕ₀ (abs‘𝐴))
194	191, 193	breqtrrd 4901	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ≤ Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗))
195	105	ltp1d 11284	. . . . . . . . . . 11 ⊢ (𝜑 → Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))
196	195	adantr 474	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))
197	98, 182, 183, 194, 196	lelttrd 10514	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))
198	93	rpregt0d 12162	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 / 2) ∈ ℝ ∧ 0 < (𝐸 / 2)))
199	198	adantr 474	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝐸 / 2) ∈ ℝ ∧ 0 < (𝐸 / 2)))
200		ltmul1 11203	. . . . . . . . . 10 ⊢ ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ∈ ℝ ∧ (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ ∧ ((𝐸 / 2) ∈ ℝ ∧ 0 < (𝐸 / 2))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ↔ (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) · (𝐸 / 2))))
201	98, 183, 199, 200	syl3anc 1494	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ↔ (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) · (𝐸 / 2))))
202	197, 201	mpbid 224	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) · (𝐸 / 2)))
203	109	rpregt0d 12162	. . . . . . . . . 10 ⊢ (𝜑 → ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ ∧ 0 < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
204	203	adantr 474	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ ∧ 0 < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)))
205		ltdivmul 11228	. . . . . . . . 9 ⊢ (((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) ∈ ℝ ∧ (𝐸 / 2) ∈ ℝ ∧ ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) ∈ ℝ ∧ 0 < (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1))) → (((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) < (𝐸 / 2) ↔ (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) · (𝐸 / 2))))
206	99, 95, 204, 205	syl3anc 1494	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) < (𝐸 / 2) ↔ (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1) · (𝐸 / 2))))
207	202, 206	mpbird 249	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ₀ (𝐾‘𝑗) + 1)) < (𝐸 / 2))
208	81, 111, 95, 181, 207	lelttrd 10514	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < (𝐸 / 2))
209		mertens.13	. . . . . . . . . . . 12 ⊢ (𝜑 → (0 ≤ sup(𝑇, ℝ, < ) ∧ (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧)))
210	209	simprd 491	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧))
211		suprcl 11313	. . . . . . . . . . 11 ⊢ ((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧) → sup(𝑇, ℝ, < ) ∈ ℝ)
212	210, 211	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → sup(𝑇, ℝ, < ) ∈ ℝ)
213	94, 212	remulcld 10387	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 / 2) · sup(𝑇, ℝ, < )) ∈ ℝ)
214	209	simpld 490	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ sup(𝑇, ℝ, < ))
215	212, 214	ge0p1rpd 12186	. . . . . . . . 9 ⊢ (𝜑 → (sup(𝑇, ℝ, < ) + 1) ∈ ℝ⁺)
216	213, 215	rerpdivcld 12187	. . . . . . . 8 ⊢ (𝜑 → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℝ)
217	216	adantr 474	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℝ)
218	5	nnrpd 12154	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑠 ∈ ℝ⁺)
219	93, 218	rpdivcld 12173	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐸 / 2) / 𝑠) ∈ ℝ⁺)
220	219, 215	rpdivcld 12173	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℝ⁺)
221	220	rpred 12156	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℝ)
222	221, 212	remulcld 10387	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈ ℝ)
223	222	ad2antrr 717	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈ ℝ)
224		simpll 783	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝜑)
225	90, 12	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑗 ∈ ℕ₀)
226	224, 225, 76	syl2anc 579	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘𝐴) ∈ ℝ)
227	221	ad2antrr 717	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℝ)
228	224, 225, 102	syl2anc 579	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝐾‘𝑗) = (abs‘𝐴))
229		fveq2 6433	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑗 → (𝐾‘𝑚) = (𝐾‘𝑗))
230	229	breq1d 4883	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑗 → ((𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ↔ (𝐾‘𝑗) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))
231	7	simprd 491	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑚 ∈ (ℤ_≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))
232	231	ad2antrr 717	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ∀𝑚 ∈ (ℤ_≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))
233		elfzuz 12631	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚) → 𝑗 ∈ (ℤ_≥‘((𝑚 − 𝑠) + 1)))
234		eluzle 11981	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡)) → (𝑠 + 𝑡) ≤ 𝑚)
235	234	adantl 475	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑠 + 𝑡) ≤ 𝑚)
236	8	nn0zd 11808	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑡 ∈ ℤ)
237	236	adantr 474	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑡 ∈ ℤ)
238	237	zred 11810	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑡 ∈ ℝ)
239	52, 238, 51	leaddsub2d 10954	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝑠 + 𝑡) ≤ 𝑚 ↔ 𝑡 ≤ (𝑚 − 𝑠)))
240	235, 239	mpbid 224	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑡 ≤ (𝑚 − 𝑠))
241		eluz 11982	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑡 ∈ ℤ ∧ (𝑚 − 𝑠) ∈ ℤ) → ((𝑚 − 𝑠) ∈ (ℤ_≥‘𝑡) ↔ 𝑡 ≤ (𝑚 − 𝑠)))
242	237, 69, 241	syl2anc 579	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝑚 − 𝑠) ∈ (ℤ_≥‘𝑡) ↔ 𝑡 ≤ (𝑚 − 𝑠)))
243	240, 242	mpbird 249	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ (ℤ_≥‘𝑡))
244		peano2uz 12023	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 − 𝑠) ∈ (ℤ_≥‘𝑡) → ((𝑚 − 𝑠) + 1) ∈ (ℤ_≥‘𝑡))
245	243, 244	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝑚 − 𝑠) + 1) ∈ (ℤ_≥‘𝑡))
246		uztrn 11985	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ (ℤ_≥‘((𝑚 − 𝑠) + 1)) ∧ ((𝑚 − 𝑠) + 1) ∈ (ℤ_≥‘𝑡)) → 𝑗 ∈ (ℤ_≥‘𝑡))
247	233, 245, 246	syl2anr 590	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑗 ∈ (ℤ_≥‘𝑡))
248	230, 232, 247	rspcdva 3532	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝐾‘𝑗) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))
249	228, 248	eqbrtrrd 4897	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘𝐴) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))
250	226, 227, 249	ltled 10504	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘𝐴) ≤ (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))
251	210	ad2antrr 717	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧))
252	51	adantr 474	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑚 ∈ ℝ)
253		peano2zm 11748	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ ℤ → (𝑠 − 1) ∈ ℤ)
254	56, 253	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑠 − 1) ∈ ℤ)
255	254	zred 11810	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑠 − 1) ∈ ℝ)
256	255	ad2antrr 717	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑠 − 1) ∈ ℝ)
257	225	nn0red 11679	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑗 ∈ ℝ)
258	50	zcnd 11811	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑚 ∈ ℂ)
259	52	recnd 10385	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑠 ∈ ℂ)
260		1cnd 10351	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 1 ∈ ℂ)
261	258, 259, 260	subsubd 10741	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − (𝑠 − 1)) = ((𝑚 − 𝑠) + 1))
262	261	adantr 474	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − (𝑠 − 1)) = ((𝑚 − 𝑠) + 1))
263		elfzle1 12637	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚) → ((𝑚 − 𝑠) + 1) ≤ 𝑗)
264	263	adantl 475	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((𝑚 − 𝑠) + 1) ≤ 𝑗)
265	262, 264	eqbrtrd 4895	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − (𝑠 − 1)) ≤ 𝑗)
266	252, 256, 257, 265	subled 10955	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − 𝑗) ≤ (𝑠 − 1))
267	90, 16	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − 𝑗) ∈ ℕ₀)
268	267, 30	syl6eleq 2916	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − 𝑗) ∈ (ℤ_≥‘0))
269	254	ad2antrr 717	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑠 − 1) ∈ ℤ)
270		elfz5 12627	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 − 𝑗) ∈ (ℤ_≥‘0) ∧ (𝑠 − 1) ∈ ℤ) → ((𝑚 − 𝑗) ∈ (0...(𝑠 − 1)) ↔ (𝑚 − 𝑗) ≤ (𝑠 − 1)))
271	268, 269, 270	syl2anc 579	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((𝑚 − 𝑗) ∈ (0...(𝑠 − 1)) ↔ (𝑚 − 𝑗) ≤ (𝑠 − 1)))
272	266, 271	mpbird 249	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − 𝑗) ∈ (0...(𝑠 − 1)))
273		simplll 791	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝜑)
274	90, 19	syldan 585	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((𝑚 − 𝑗) + 1) ∈ ℕ₀)
275	274, 22	sylan 575	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ₀)
276	273, 275, 24	syl2anc 579	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))) → (𝐺‘𝑘) = 𝐵)
277	276	sumeq2dv 14810	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)
278	277	eqcomd 2831	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵 = Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘))
279	278	fveq2d 6437	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)))
280	131	rspceeqv 3544	. . . . . . . . . . . . 13 ⊢ (((𝑚 − 𝑗) ∈ (0...(𝑠 − 1)) ∧ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘))) → ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)))
281	272, 279, 280	syl2anc 579	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)))
282		fvex 6446	. . . . . . . . . . . . 13 ⊢ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ V
283		eqeq1 2829	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) → (𝑧 = (abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)) ↔ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘))))
284	283	rexbidv 3262	. . . . . . . . . . . . 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 3575	. . . . . . . . . . . 12 ⊢ ((abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ 𝑇 ↔ ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ_≥‘(𝑛 + 1))(𝐺‘𝑘)))
287	281, 286	sylibr 226	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ 𝑇)
288		suprub 11314	. . . . . . . . . . 11 ⊢ (((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧) ∧ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ 𝑇) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ sup(𝑇, ℝ, < ))
289	251, 287, 288	syl2anc 579	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ sup(𝑇, ℝ, < ))
290	224, 225, 125	syl2anc 579	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)))
291	90, 78	syldan 585	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ)
292	36	absge0d 14560	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → 0 ≤ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵))
293	90, 292	syldan 585	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 0 ≤ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵))
294	291, 293	jca 507	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ ∧ 0 ≤ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)))
295	212	ad2antrr 717	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → sup(𝑇, ℝ, < ) ∈ ℝ)
296		lemul12a 11211	. . . . . . . . . . 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 872	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (((abs‘𝐴) ≤ (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∧ (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ sup(𝑇, ℝ, < )) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))))
298	250, 289, 297	mp2and 690	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )))
299	82, 91, 223, 298	fsumle 14905	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )))
300	222	recnd 10385	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈ ℂ)
301	300	adantr 474	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈ ℂ)
302		fsumconst 14896	. . . . . . . . . 10 ⊢ (((((𝑚 − 𝑠) + 1)...𝑚) ∈ Fin ∧ ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈ ℂ) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) = ((♯‘(((𝑚 − 𝑠) + 1)...𝑚)) · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))))
303	82, 301, 302	syl2anc 579	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) = ((♯‘(((𝑚 − 𝑠) + 1)...𝑚)) · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))))
304		1zzd 11736	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 1 ∈ ℤ)
305	56	adantr 474	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝑠 ∈ ℤ)
306		fzen 12651	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ (𝑚 − 𝑠) ∈ ℤ) → (1...𝑠) ≈ ((1 + (𝑚 − 𝑠))...(𝑠 + (𝑚 − 𝑠))))
307	304, 305, 69, 306	syl3anc 1494	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (1...𝑠) ≈ ((1 + (𝑚 − 𝑠))...(𝑠 + (𝑚 − 𝑠))))
308		ax-1cn 10310	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
309	69	zcnd 11811	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ ℂ)
310		addcom 10541	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℂ ∧ (𝑚 − 𝑠) ∈ ℂ) → (1 + (𝑚 − 𝑠)) = ((𝑚 − 𝑠) + 1))
311	308, 309, 310	sylancr 581	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (1 + (𝑚 − 𝑠)) = ((𝑚 − 𝑠) + 1))
312	259, 258	pncan3d 10716	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑠 + (𝑚 − 𝑠)) = 𝑚)
313	311, 312	oveq12d 6923	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((1 + (𝑚 − 𝑠))...(𝑠 + (𝑚 − 𝑠))) = (((𝑚 − 𝑠) + 1)...𝑚))
314	307, 313	breqtrd 4899	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (1...𝑠) ≈ (((𝑚 − 𝑠) + 1)...𝑚))
315		fzfid 13067	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (1...𝑠) ∈ Fin)
316		hashen 13427	. . . . . . . . . . . . 13 ⊢ (((1...𝑠) ∈ Fin ∧ (((𝑚 − 𝑠) + 1)...𝑚) ∈ Fin) → ((♯‘(1...𝑠)) = (♯‘(((𝑚 − 𝑠) + 1)...𝑚)) ↔ (1...𝑠) ≈ (((𝑚 − 𝑠) + 1)...𝑚)))
317	315, 82, 316	syl2anc 579	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((♯‘(1...𝑠)) = (♯‘(((𝑚 − 𝑠) + 1)...𝑚)) ↔ (1...𝑠) ≈ (((𝑚 − 𝑠) + 1)...𝑚)))
318	314, 317	mpbird 249	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (♯‘(1...𝑠)) = (♯‘(((𝑚 − 𝑠) + 1)...𝑚)))
319		hashfz1 13426	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ℕ₀ → (♯‘(1...𝑠)) = 𝑠)
320	47, 319	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (♯‘(1...𝑠)) = 𝑠)
321	318, 320	eqtr3d 2863	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (♯‘(((𝑚 − 𝑠) + 1)...𝑚)) = 𝑠)
322	321	oveq1d 6920	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((♯‘(((𝑚 − 𝑠) + 1)...𝑚)) · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))) = (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))))
323	212	recnd 10385	. . . . . . . . . . . 12 ⊢ (𝜑 → sup(𝑇, ℝ, < ) ∈ ℂ)
324	215	rpcnne0d 12165	. . . . . . . . . . . 12 ⊢ (𝜑 → ((sup(𝑇, ℝ, < ) + 1) ∈ ℂ ∧ (sup(𝑇, ℝ, < ) + 1) ≠ 0))
325		div23 11029	. . . . . . . . . . . 12 ⊢ (((𝐸 / 2) ∈ ℂ ∧ sup(𝑇, ℝ, < ) ∈ ℂ ∧ ((sup(𝑇, ℝ, < ) + 1) ∈ ℂ ∧ (sup(𝑇, ℝ, < ) + 1) ≠ 0)) → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) = (((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )))
326	156, 323, 324, 325	syl3anc 1494	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) = (((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )))
327	56	zcnd 11811	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑠 ∈ ℂ)
328	219	rpcnd 12158	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐸 / 2) / 𝑠) ∈ ℂ)
329		divass 11028	. . . . . . . . . . . . . 14 ⊢ ((𝑠 ∈ ℂ ∧ ((𝐸 / 2) / 𝑠) ∈ ℂ ∧ ((sup(𝑇, ℝ, < ) + 1) ∈ ℂ ∧ (sup(𝑇, ℝ, < ) + 1) ≠ 0)) → ((𝑠 · ((𝐸 / 2) / 𝑠)) / (sup(𝑇, ℝ, < ) + 1)) = (𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))
330	327, 328, 324, 329	syl3anc 1494	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑠 · ((𝐸 / 2) / 𝑠)) / (sup(𝑇, ℝ, < ) + 1)) = (𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))
331	5	nnne0d 11401	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑠 ≠ 0)
332	156, 327, 331	divcan2d 11129	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑠 · ((𝐸 / 2) / 𝑠)) = (𝐸 / 2))
333	332	oveq1d 6920	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑠 · ((𝐸 / 2) / 𝑠)) / (sup(𝑇, ℝ, < ) + 1)) = ((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)))
334	330, 333	eqtr3d 2863	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) = ((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)))
335	334	oveq1d 6920	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) · sup(𝑇, ℝ, < )) = (((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )))
336	220	rpcnd 12158	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℂ)
337	327, 336, 323	mulassd 10380	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) · sup(𝑇, ℝ, < )) = (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))))
338	326, 335, 337	3eqtr2rd 2868	. . . . . . . . . 10 ⊢ (𝜑 → (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))) = (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)))
339	338	adantr 474	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))) = (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)))
340	303, 322, 339	3eqtrd 2865	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) = (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)))
341	299, 340	breqtrd 4899	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)))
342		peano2re 10528	. . . . . . . . . . 11 ⊢ (sup(𝑇, ℝ, < ) ∈ ℝ → (sup(𝑇, ℝ, < ) + 1) ∈ ℝ)
343	212, 342	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (sup(𝑇, ℝ, < ) + 1) ∈ ℝ)
344	212	ltp1d 11284	. . . . . . . . . 10 ⊢ (𝜑 → sup(𝑇, ℝ, < ) < (sup(𝑇, ℝ, < ) + 1))
345	212, 343, 93, 344	ltmul2dd 12212	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 / 2) · sup(𝑇, ℝ, < )) < ((𝐸 / 2) · (sup(𝑇, ℝ, < ) + 1)))
346	213, 94, 215	ltdivmul2d 12208	. . . . . . . . 9 ⊢ (𝜑 → ((((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) < (𝐸 / 2) ↔ ((𝐸 / 2) · sup(𝑇, ℝ, < )) < ((𝐸 / 2) · (sup(𝑇, ℝ, < ) + 1))))
347	345, 346	mpbird 249	. . . . . . . 8 ⊢ (𝜑 → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) < (𝐸 / 2))
348	347	adantr 474	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) < (𝐸 / 2))
349	92, 217, 95, 341, 348	lelttrd 10514	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < (𝐸 / 2))
350	81, 92, 95, 95, 208, 349	lt2addd 10975	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) + Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵))) < ((𝐸 / 2) + (𝐸 / 2)))
351	14, 36	absmuld 14570	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) = ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)))
352	351	sumeq2dv 14810	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) = Σ𝑗 ∈ (0...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)))
353	69	zred 11810	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ ℝ)
354	353	ltp1d 11284	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) < ((𝑚 − 𝑠) + 1))
355		fzdisj 12661	. . . . . . . 8 ⊢ ((𝑚 − 𝑠) < ((𝑚 − 𝑠) + 1) → ((0...(𝑚 − 𝑠)) ∩ (((𝑚 − 𝑠) + 1)...𝑚)) = ∅)
356	354, 355	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((0...(𝑚 − 𝑠)) ∩ (((𝑚 − 𝑠) + 1)...𝑚)) = ∅)
357		fzsplit 12660	. . . . . . . 8 ⊢ ((𝑚 − 𝑠) ∈ (0...𝑚) → (0...𝑚) = ((0...(𝑚 − 𝑠)) ∪ (((𝑚 − 𝑠) + 1)...𝑚)))
358	67, 357	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (0...𝑚) = ((0...(𝑚 − 𝑠)) ∪ (((𝑚 − 𝑠) + 1)...𝑚)))
359	79	recnd 10385	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℂ)
360	356, 358, 10, 359	fsumsplit 14848	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) = (Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) + Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵))))
361	352, 360	eqtr2d 2862	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) + Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵))) = Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)))
362	42	rpcnd 12158	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ ℂ)
363	362	adantr 474	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → 𝐸 ∈ ℂ)
364	363	2halvesd 11604	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → ((𝐸 / 2) + (𝐸 / 2)) = 𝐸)
365	350, 361, 364	3brtr3d 4904	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)
366	39, 41, 44, 45, 365	lelttrd 10514	. . 3 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))) → (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)
367	366	ralrimiva 3175	. 2 ⊢ (𝜑 → ∀𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)
368		fveq2 6433	. . . 4 ⊢ (𝑦 = (𝑠 + 𝑡) → (ℤ_≥‘𝑦) = (ℤ_≥‘(𝑠 + 𝑡)))
369	368	raleqdv 3356	. . 3 ⊢ (𝑦 = (𝑠 + 𝑡) → (∀𝑚 ∈ (ℤ_≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸 ↔ ∀𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸))
370	369	rspcev 3526	. 2 ⊢ (((𝑠 + 𝑡) ∈ ℕ₀ ∧ ∀𝑚 ∈ (ℤ_≥‘(𝑠 + 𝑡))(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸) → ∃𝑦 ∈ ℕ₀ ∀𝑚 ∈ (ℤ_≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)
371	9, 367, 370	syl2anc 579	1 ⊢ (𝜑 → ∃𝑦 ∈ ℕ₀ ∀𝑚 ∈ (ℤ_≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ_≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 ∧ w3a 1111 = wceq 1656 ∈ wcel 2164 {cab 2811 ≠ wne 2999 ∀wral 3117 ∃wrex 3118 ∪ cun 3796 ∩ cin 3797 ⊆ wss 3798 ∅c0 4144 class class class wbr 4873 dom cdm 5342 ‘cfv 6123 (class class class)co 6905 ≈ cen 8219 Fincfn 8222 supcsup 8615 ℂcc 10250 ℝcr 10251 0cc0 10252 1c1 10253 + caddc 10255 · cmul 10257 < clt 10391 ≤ cle 10392 − cmin 10585 / cdiv 11009 ℕcn 11350 2c2 11406 ℕ₀cn0 11618 ℤcz 11704 ℤ_≥cuz 11968 ℝ⁺crp 12112 ...cfz 12619 seqcseq 13095 ♯chash 13410 abscabs 14351 ⇝ cli 14592 Σcsu 14793

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-8 2166 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-13 2389 ax-ext 2803 ax-rep 4994 ax-sep 5005 ax-nul 5013 ax-pow 5065 ax-pr 5127 ax-un 7209 ax-inf2 8815 ax-cnex 10308 ax-resscn 10309 ax-1cn 10310 ax-icn 10311 ax-addcl 10312 ax-addrcl 10313 ax-mulcl 10314 ax-mulrcl 10315 ax-mulcom 10316 ax-addass 10317 ax-mulass 10318 ax-distr 10319 ax-i2m1 10320 ax-1ne0 10321 ax-1rid 10322 ax-rnegex 10323 ax-rrecex 10324 ax-cnre 10325 ax-pre-lttri 10326 ax-pre-lttrn 10327 ax-pre-ltadd 10328 ax-pre-mulgt0 10329 ax-pre-sup 10330

This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-3or 1112 df-3an 1113 df-tru 1660 df-fal 1670 df-ex 1879 df-nf 1883 df-sb 2068 df-mo 2605 df-eu 2640 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-ne 3000 df-nel 3103 df-ral 3122 df-rex 3123 df-reu 3124 df-rmo 3125 df-rab 3126 df-v 3416 df-sbc 3663 df-csb 3758 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-pss 3814 df-nul 4145 df-if 4307 df-pw 4380 df-sn 4398 df-pr 4400 df-tp 4402 df-op 4404 df-uni 4659 df-int 4698 df-iun 4742 df-br 4874 df-opab 4936 df-mpt 4953 df-tr 4976 df-id 5250 df-eprel 5255 df-po 5263 df-so 5264 df-fr 5301 df-se 5302 df-we 5303 df-xp 5348 df-rel 5349 df-cnv 5350 df-co 5351 df-dm 5352 df-rn 5353 df-res 5354 df-ima 5355 df-pred 5920 df-ord 5966 df-on 5967 df-lim 5968 df-suc 5969 df-iota 6086 df-fun 6125 df-fn 6126 df-f 6127 df-f1 6128 df-fo 6129 df-f1o 6130 df-fv 6131 df-isom 6132 df-riota 6866 df-ov 6908 df-oprab 6909 df-mpt2 6910 df-om 7327 df-1st 7428 df-2nd 7429 df-wrecs 7672 df-recs 7734 df-rdg 7772 df-1o 7826 df-oadd 7830 df-er 8009 df-pm 8125 df-en 8223 df-dom 8224 df-sdom 8225 df-fin 8226 df-sup 8617 df-inf 8618 df-oi 8684 df-card 9078 df-pnf 10393 df-mnf 10394 df-xr 10395 df-ltxr 10396 df-le 10397 df-sub 10587 df-neg 10588 df-div 11010 df-nn 11351 df-2 11414 df-3 11415 df-n0 11619 df-z 11705 df-uz 11969 df-rp 12113 df-ico 12469 df-fz 12620 df-fzo 12761 df-fl 12888 df-seq 13096 df-exp 13155 df-hash 13411 df-cj 14216 df-re 14217 df-im 14218 df-sqrt 14352 df-abs 14353 df-clim 14596 df-rlim 14597 df-sum 14794

This theorem is referenced by: mertenslem2 14990

W3C validator