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

Theorem mertenslem1 15302
 Description: Lemma for mertens 15304. (Contributed by Mario Carneiro, 29-Apr-2014.)
Hypotheses
Ref Expression
mertens.1 ((𝜑𝑗 ∈ ℕ0) → (𝐹𝑗) = 𝐴)
mertens.2 ((𝜑𝑗 ∈ ℕ0) → (𝐾𝑗) = (abs‘𝐴))
mertens.3 ((𝜑𝑗 ∈ ℕ0) → 𝐴 ∈ ℂ)
mertens.4 ((𝜑𝑘 ∈ ℕ0) → (𝐺𝑘) = 𝐵)
mertens.5 ((𝜑𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)
mertens.6 ((𝜑𝑘 ∈ ℕ0) → (𝐻𝑘) = Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘𝑗))))
mertens.7 (𝜑 → seq0( + , 𝐾) ∈ dom ⇝ )
mertens.8 (𝜑 → seq0( + , 𝐺) ∈ dom ⇝ )
mertens.9 (𝜑𝐸 ∈ ℝ+)
mertens.10 𝑇 = {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘))}
mertens.11 (𝜓 ↔ (𝑠 ∈ ℕ ∧ ∀𝑛 ∈ (ℤ𝑠)(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
mertens.12 (𝜑 → (𝜓 ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑚 ∈ (ℤ𝑡)(𝐾𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))))
mertens.13 (𝜑 → (0 ≤ sup(𝑇, ℝ, < ) ∧ (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤𝑇 𝑤𝑧)))
Assertion
Ref Expression
mertenslem1 (𝜑 → ∃𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸)
Distinct variable groups:   𝑗,𝑚,𝑛,𝑠,𝑡,𝑦,𝑧,𝐵   𝑗,𝑘,𝐺,𝑚,𝑛,𝑠,𝑦,𝑧   𝜑,𝑗,𝑘,𝑚,𝑦,𝑧   𝑡,𝑘,𝐴,𝑚,𝑛,𝑠,𝑦   𝑗,𝐸,𝑘,𝑚,𝑛,𝑠,𝑡,𝑦,𝑧   𝑗,𝐾,𝑘,𝑚,𝑛,𝑠,𝑡,𝑦,𝑧   𝑗,𝐹,𝑚,𝑛,𝑦   𝜓,𝑗,𝑘,𝑚,𝑛,𝑡,𝑦,𝑧   𝑤,𝑗,𝑇,𝑘,𝑚,𝑛,𝑡,𝑦,𝑧   𝑘,𝐻,𝑚,𝑦
Allowed substitution hints:   𝜑(𝑤,𝑡,𝑛,𝑠)   𝜓(𝑤,𝑠)   𝐴(𝑧,𝑤,𝑗)   𝐵(𝑤,𝑘)   𝑇(𝑠)   𝐸(𝑤)   𝐹(𝑧,𝑤,𝑡,𝑘,𝑠)   𝐺(𝑤,𝑡)   𝐻(𝑧,𝑤,𝑡,𝑗,𝑛,𝑠)   𝐾(𝑤)

Proof of Theorem mertenslem1
StepHypRef Expression
1 mertens.12 . . . . . . 7 (𝜑 → (𝜓 ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑚 ∈ (ℤ𝑡)(𝐾𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))))
21simpld 498 . . . . . 6 (𝜑𝜓)
3 mertens.11 . . . . . 6 (𝜓 ↔ (𝑠 ∈ ℕ ∧ ∀𝑛 ∈ (ℤ𝑠)(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
42, 3sylib 221 . . . . 5 (𝜑 → (𝑠 ∈ ℕ ∧ ∀𝑛 ∈ (ℤ𝑠)(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
54simpld 498 . . . 4 (𝜑𝑠 ∈ ℕ)
65nnnn0d 12008 . . 3 (𝜑𝑠 ∈ ℕ0)
71simprd 499 . . . 4 (𝜑 → (𝑡 ∈ ℕ0 ∧ ∀𝑚 ∈ (ℤ𝑡)(𝐾𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))
87simpld 498 . . 3 (𝜑𝑡 ∈ ℕ0)
96, 8nn0addcld 12012 . 2 (𝜑 → (𝑠 + 𝑡) ∈ ℕ0)
10 fzfid 13404 . . . . . 6 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (0...𝑚) ∈ Fin)
11 simpl 486 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝜑)
12 elfznn0 13063 . . . . . . . 8 (𝑗 ∈ (0...𝑚) → 𝑗 ∈ ℕ0)
13 mertens.3 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → 𝐴 ∈ ℂ)
1411, 12, 13syl2an 598 . . . . . . 7 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → 𝐴 ∈ ℂ)
15 eqid 2759 . . . . . . . 8 (ℤ‘((𝑚𝑗) + 1)) = (ℤ‘((𝑚𝑗) + 1))
16 fznn0sub 13002 . . . . . . . . . . 11 (𝑗 ∈ (0...𝑚) → (𝑚𝑗) ∈ ℕ0)
1716adantl 485 . . . . . . . . . 10 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (𝑚𝑗) ∈ ℕ0)
18 peano2nn0 11988 . . . . . . . . . 10 ((𝑚𝑗) ∈ ℕ0 → ((𝑚𝑗) + 1) ∈ ℕ0)
1917, 18syl 17 . . . . . . . . 9 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((𝑚𝑗) + 1) ∈ ℕ0)
2019nn0zd 12138 . . . . . . . 8 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((𝑚𝑗) + 1) ∈ ℤ)
21 simplll 774 . . . . . . . . 9 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → 𝜑)
22 eluznn0 12371 . . . . . . . . . 10 ((((𝑚𝑗) + 1) ∈ ℕ0𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → 𝑘 ∈ ℕ0)
2319, 22sylan 583 . . . . . . . . 9 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → 𝑘 ∈ ℕ0)
24 mertens.4 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (𝐺𝑘) = 𝐵)
2521, 23, 24syl2anc 587 . . . . . . . 8 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → (𝐺𝑘) = 𝐵)
26 mertens.5 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)
2721, 23, 26syl2anc 587 . . . . . . . 8 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → 𝐵 ∈ ℂ)
28 mertens.8 . . . . . . . . . 10 (𝜑 → seq0( + , 𝐺) ∈ dom ⇝ )
2928ad2antrr 725 . . . . . . . . 9 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → seq0( + , 𝐺) ∈ dom ⇝ )
30 nn0uz 12334 . . . . . . . . . 10 0 = (ℤ‘0)
31 simpll 766 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → 𝜑)
3224, 26eqeltrd 2853 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → (𝐺𝑘) ∈ ℂ)
3331, 32sylan 583 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) ∈ ℂ)
3430, 19, 33iserex 15075 . . . . . . . . 9 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (seq0( + , 𝐺) ∈ dom ⇝ ↔ seq((𝑚𝑗) + 1)( + , 𝐺) ∈ dom ⇝ ))
3529, 34mpbid 235 . . . . . . . 8 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → seq((𝑚𝑗) + 1)( + , 𝐺) ∈ dom ⇝ )
3615, 20, 25, 27, 35isumcl 15178 . . . . . . 7 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵 ∈ ℂ)
3714, 36mulcld 10713 . . . . . 6 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ∈ ℂ)
3810, 37fsumcl 15152 . . . . 5 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ∈ ℂ)
3938abscld 14858 . . . 4 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ∈ ℝ)
4037abscld 14858 . . . . 5 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ∈ ℝ)
4110, 40fsumrecl 15153 . . . 4 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ∈ ℝ)
42 mertens.9 . . . . . 6 (𝜑𝐸 ∈ ℝ+)
4342rpred 12486 . . . . 5 (𝜑𝐸 ∈ ℝ)
4443adantr 484 . . . 4 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝐸 ∈ ℝ)
4510, 37fsumabs 15218 . . . 4 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ≤ Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)))
46 fzfid 13404 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (0...(𝑚𝑠)) ∈ Fin)
476adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑠 ∈ ℕ0)
4847nn0ge0d 12011 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 0 ≤ 𝑠)
49 eluzelz 12306 . . . . . . . . . . . . . . 15 (𝑚 ∈ (ℤ‘(𝑠 + 𝑡)) → 𝑚 ∈ ℤ)
5049adantl 485 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑚 ∈ ℤ)
5150zred 12140 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑚 ∈ ℝ)
5247nn0red 12009 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑠 ∈ ℝ)
5351, 52subge02d 11284 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (0 ≤ 𝑠 ↔ (𝑚𝑠) ≤ 𝑚))
5448, 53mpbid 235 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑚𝑠) ≤ 𝑚)
5547, 30eleqtrdi 2863 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑠 ∈ (ℤ‘0))
565nnzd 12139 . . . . . . . . . . . . . . . . . 18 (𝜑𝑠 ∈ ℤ)
57 uzid 12311 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ℤ → 𝑠 ∈ (ℤ𝑠))
5856, 57syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝑠 ∈ (ℤ𝑠))
59 uzaddcl 12358 . . . . . . . . . . . . . . . . 17 ((𝑠 ∈ (ℤ𝑠) ∧ 𝑡 ∈ ℕ0) → (𝑠 + 𝑡) ∈ (ℤ𝑠))
6058, 8, 59syl2anc 587 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑠 + 𝑡) ∈ (ℤ𝑠))
61 eqid 2759 . . . . . . . . . . . . . . . . 17 (ℤ𝑠) = (ℤ𝑠)
6261uztrn2 12315 . . . . . . . . . . . . . . . 16 (((𝑠 + 𝑡) ∈ (ℤ𝑠) ∧ 𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑚 ∈ (ℤ𝑠))
6360, 62sylan 583 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑚 ∈ (ℤ𝑠))
64 elfzuzb 12964 . . . . . . . . . . . . . . 15 (𝑠 ∈ (0...𝑚) ↔ (𝑠 ∈ (ℤ‘0) ∧ 𝑚 ∈ (ℤ𝑠)))
6555, 63, 64sylanbrc 586 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑠 ∈ (0...𝑚))
66 fznn0sub2 13077 . . . . . . . . . . . . . 14 (𝑠 ∈ (0...𝑚) → (𝑚𝑠) ∈ (0...𝑚))
6765, 66syl 17 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑚𝑠) ∈ (0...𝑚))
68 elfzelz 12970 . . . . . . . . . . . . 13 ((𝑚𝑠) ∈ (0...𝑚) → (𝑚𝑠) ∈ ℤ)
6967, 68syl 17 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑚𝑠) ∈ ℤ)
70 eluz 12310 . . . . . . . . . . . 12 (((𝑚𝑠) ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑚 ∈ (ℤ‘(𝑚𝑠)) ↔ (𝑚𝑠) ≤ 𝑚))
7169, 50, 70syl2anc 587 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑚 ∈ (ℤ‘(𝑚𝑠)) ↔ (𝑚𝑠) ≤ 𝑚))
7254, 71mpbird 260 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑚 ∈ (ℤ‘(𝑚𝑠)))
73 fzss2 13010 . . . . . . . . . 10 (𝑚 ∈ (ℤ‘(𝑚𝑠)) → (0...(𝑚𝑠)) ⊆ (0...𝑚))
7472, 73syl 17 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (0...(𝑚𝑠)) ⊆ (0...𝑚))
7574sselda 3895 . . . . . . . 8 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → 𝑗 ∈ (0...𝑚))
7613abscld 14858 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → (abs‘𝐴) ∈ ℝ)
7711, 12, 76syl2an 598 . . . . . . . . 9 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘𝐴) ∈ ℝ)
7836abscld 14858 . . . . . . . . 9 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ∈ ℝ)
7977, 78remulcld 10723 . . . . . . . 8 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ∈ ℝ)
8075, 79syldan 594 . . . . . . 7 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ∈ ℝ)
8146, 80fsumrecl 15153 . . . . . 6 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ∈ ℝ)
82 fzfid 13404 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (((𝑚𝑠) + 1)...𝑚) ∈ Fin)
83 elfznn0 13063 . . . . . . . . . . . . 13 ((𝑚𝑠) ∈ (0...𝑚) → (𝑚𝑠) ∈ ℕ0)
8467, 83syl 17 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑚𝑠) ∈ ℕ0)
85 peano2nn0 11988 . . . . . . . . . . . 12 ((𝑚𝑠) ∈ ℕ0 → ((𝑚𝑠) + 1) ∈ ℕ0)
8684, 85syl 17 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((𝑚𝑠) + 1) ∈ ℕ0)
8786, 30eleqtrdi 2863 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((𝑚𝑠) + 1) ∈ (ℤ‘0))
88 fzss1 13009 . . . . . . . . . 10 (((𝑚𝑠) + 1) ∈ (ℤ‘0) → (((𝑚𝑠) + 1)...𝑚) ⊆ (0...𝑚))
8987, 88syl 17 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (((𝑚𝑠) + 1)...𝑚) ⊆ (0...𝑚))
9089sselda 3895 . . . . . . . 8 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → 𝑗 ∈ (0...𝑚))
9190, 79syldan 594 . . . . . . 7 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ∈ ℝ)
9282, 91fsumrecl 15153 . . . . . 6 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ∈ ℝ)
9342rphalfcld 12498 . . . . . . . 8 (𝜑 → (𝐸 / 2) ∈ ℝ+)
9493rpred 12486 . . . . . . 7 (𝜑 → (𝐸 / 2) ∈ ℝ)
9594adantr 484 . . . . . 6 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝐸 / 2) ∈ ℝ)
96 elfznn0 13063 . . . . . . . . . . 11 (𝑗 ∈ (0...(𝑚𝑠)) → 𝑗 ∈ ℕ0)
9711, 96, 76syl2an 598 . . . . . . . . . 10 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → (abs‘𝐴) ∈ ℝ)
9846, 97fsumrecl 15153 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) ∈ ℝ)
9998, 95remulcld 10723 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) ∈ ℝ)
100 0zd 12046 . . . . . . . . . . 11 (𝜑 → 0 ∈ ℤ)
101 eqidd 2760 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → (𝐾𝑗) = (𝐾𝑗))
102 mertens.2 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → (𝐾𝑗) = (abs‘𝐴))
103102, 76eqeltrd 2853 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → (𝐾𝑗) ∈ ℝ)
104 mertens.7 . . . . . . . . . . 11 (𝜑 → seq0( + , 𝐾) ∈ dom ⇝ )
10530, 100, 101, 103, 104isumrecl 15182 . . . . . . . . . 10 (𝜑 → Σ𝑗 ∈ ℕ0 (𝐾𝑗) ∈ ℝ)
10613absge0d 14866 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → 0 ≤ (abs‘𝐴))
107106, 102breqtrrd 5065 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → 0 ≤ (𝐾𝑗))
10830, 100, 101, 103, 104, 107isumge0 15183 . . . . . . . . . 10 (𝜑 → 0 ≤ Σ𝑗 ∈ ℕ0 (𝐾𝑗))
109105, 108ge0p1rpd 12516 . . . . . . . . 9 (𝜑 → (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ∈ ℝ+)
110109adantr 484 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ∈ ℝ+)
11199, 110rerpdivcld 12517 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) ∈ ℝ)
11293, 109rpdivcld 12503 . . . . . . . . . . . 12 (𝜑 → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) ∈ ℝ+)
113112rpred 12486 . . . . . . . . . . 11 (𝜑 → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) ∈ ℝ)
114113ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) ∈ ℝ)
11597, 114remulcld 10723 . . . . . . . . 9 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))) ∈ ℝ)
11675, 20syldan 594 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → ((𝑚𝑗) + 1) ∈ ℤ)
117 simplll 774 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → 𝜑)
11875, 19syldan 594 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → ((𝑚𝑗) + 1) ∈ ℕ0)
119118, 22sylan 583 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → 𝑘 ∈ ℕ0)
120117, 119, 24syl2anc 587 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → (𝐺𝑘) = 𝐵)
121117, 119, 26syl2anc 587 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → 𝐵 ∈ ℂ)
12275, 35syldan 594 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → seq((𝑚𝑗) + 1)( + , 𝐺) ∈ dom ⇝ )
12315, 116, 120, 121, 122isumcl 15178 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵 ∈ ℂ)
124123abscld 14858 . . . . . . . . . 10 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ∈ ℝ)
12576, 106jca 515 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → ((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)))
12611, 96, 125syl2an 598 . . . . . . . . . 10 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → ((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)))
127120sumeq2dv 15122 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))(𝐺𝑘) = Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)
128127fveq2d 6668 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))(𝐺𝑘)) = (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵))
129 fvoveq1 7180 . . . . . . . . . . . . . . . 16 (𝑛 = (𝑚𝑗) → (ℤ‘(𝑛 + 1)) = (ℤ‘((𝑚𝑗) + 1)))
130129sumeq1d 15120 . . . . . . . . . . . . . . 15 (𝑛 = (𝑚𝑗) → Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘) = Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))(𝐺𝑘))
131130fveq2d 6668 . . . . . . . . . . . . . 14 (𝑛 = (𝑚𝑗) → (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) = (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))(𝐺𝑘)))
132131breq1d 5047 . . . . . . . . . . . . 13 (𝑛 = (𝑚𝑗) → ((abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) ↔ (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
1334simprd 499 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑛 ∈ (ℤ𝑠)(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
134133ad2antrr 725 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → ∀𝑛 ∈ (ℤ𝑠)(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
135 elfzelz 12970 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...(𝑚𝑠)) → 𝑗 ∈ ℤ)
136135adantl 485 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → 𝑗 ∈ ℤ)
137136zred 12140 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → 𝑗 ∈ ℝ)
13849ad2antlr 726 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → 𝑚 ∈ ℤ)
139138zred 12140 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → 𝑚 ∈ ℝ)
14056ad2antrr 725 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → 𝑠 ∈ ℤ)
141140zred 12140 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → 𝑠 ∈ ℝ)
142 elfzle2 12974 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...(𝑚𝑠)) → 𝑗 ≤ (𝑚𝑠))
143142adantl 485 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → 𝑗 ≤ (𝑚𝑠))
144137, 139, 141, 143lesubd 11296 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → 𝑠 ≤ (𝑚𝑗))
145138, 136zsubcld 12145 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → (𝑚𝑗) ∈ ℤ)
146 eluz 12310 . . . . . . . . . . . . . . 15 ((𝑠 ∈ ℤ ∧ (𝑚𝑗) ∈ ℤ) → ((𝑚𝑗) ∈ (ℤ𝑠) ↔ 𝑠 ≤ (𝑚𝑗)))
147140, 145, 146syl2anc 587 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → ((𝑚𝑗) ∈ (ℤ𝑠) ↔ 𝑠 ≤ (𝑚𝑗)))
148144, 147mpbird 260 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → (𝑚𝑗) ∈ (ℤ𝑠))
149132, 134, 148rspcdva 3546 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
150128, 149eqbrtrrd 5061 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
151124, 114, 150ltled 10840 . . . . . . . . . 10 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ≤ ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
152 lemul2a 11547 . . . . . . . . . 10 ((((abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ∈ ℝ ∧ ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) ∈ ℝ ∧ ((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴))) ∧ (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ≤ ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ≤ ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
153124, 114, 126, 151, 152syl31anc 1371 . . . . . . . . 9 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ≤ ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
15446, 80, 115, 153fsumle 15216 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ≤ Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
15598recnd 10721 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) ∈ ℂ)
15693rpcnd 12488 . . . . . . . . . . 11 (𝜑 → (𝐸 / 2) ∈ ℂ)
157156adantr 484 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝐸 / 2) ∈ ℂ)
158 peano2re 10865 . . . . . . . . . . . . 13 𝑗 ∈ ℕ0 (𝐾𝑗) ∈ ℝ → (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ∈ ℝ)
159105, 158syl 17 . . . . . . . . . . . 12 (𝜑 → (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ∈ ℝ)
160159recnd 10721 . . . . . . . . . . 11 (𝜑 → (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ∈ ℂ)
161160adantr 484 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ∈ ℂ)
162109rpne0d 12491 . . . . . . . . . . 11 (𝜑 → (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ≠ 0)
163162adantr 484 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ≠ 0)
164155, 157, 161, 163divassd 11503 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) = (Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
165 fveq2 6664 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑗 → (𝐾𝑛) = (𝐾𝑗))
166165cbvsumv 15115 . . . . . . . . . . . . . . . 16 Σ𝑛 ∈ ℕ0 (𝐾𝑛) = Σ𝑗 ∈ ℕ0 (𝐾𝑗)
167166oveq1i 7167 . . . . . . . . . . . . . . 15 𝑛 ∈ ℕ0 (𝐾𝑛) + 1) = (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)
168167oveq2i 7168 . . . . . . . . . . . . . 14 ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾𝑛) + 1)) = ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))
169168, 112eqeltrid 2857 . . . . . . . . . . . . 13 (𝜑 → ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾𝑛) + 1)) ∈ ℝ+)
170169rpcnd 12488 . . . . . . . . . . . 12 (𝜑 → ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾𝑛) + 1)) ∈ ℂ)
171170adantr 484 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾𝑛) + 1)) ∈ ℂ)
17276recnd 10721 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → (abs‘𝐴) ∈ ℂ)
17311, 96, 172syl2an 598 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → (abs‘𝐴) ∈ ℂ)
17446, 171, 173fsummulc1 15202 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾𝑛) + 1))) = Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾𝑛) + 1))))
175168oveq2i 7168 . . . . . . . . . 10 𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾𝑛) + 1))) = (Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
176168oveq2i 7168 . . . . . . . . . . . 12 ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾𝑛) + 1))) = ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
177176a1i 11 . . . . . . . . . . 11 (𝑗 ∈ (0...(𝑚𝑠)) → ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾𝑛) + 1))) = ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
178177sumeq2i 15118 . . . . . . . . . 10 Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾𝑛) + 1))) = Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
179174, 175, 1783eqtr3g 2817 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))) = Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
180164, 179eqtrd 2794 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) = Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
181154, 180breqtrrd 5065 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ≤ ((Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
182105adantr 484 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ ℕ0 (𝐾𝑗) ∈ ℝ)
183159adantr 484 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ∈ ℝ)
184 0zd 12046 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 0 ∈ ℤ)
185 fz0ssnn0 13065 . . . . . . . . . . . . 13 (0...(𝑚𝑠)) ⊆ ℕ0
186185a1i 11 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (0...(𝑚𝑠)) ⊆ ℕ0)
187102adantlr 714 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ0) → (𝐾𝑗) = (abs‘𝐴))
18876adantlr 714 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ0) → (abs‘𝐴) ∈ ℝ)
189106adantlr 714 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ0) → 0 ≤ (abs‘𝐴))
190104adantr 484 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → seq0( + , 𝐾) ∈ dom ⇝ )
19130, 184, 46, 186, 187, 188, 189, 190isumless 15262 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) ≤ Σ𝑗 ∈ ℕ0 (abs‘𝐴))
192102sumeq2dv 15122 . . . . . . . . . . . 12 (𝜑 → Σ𝑗 ∈ ℕ0 (𝐾𝑗) = Σ𝑗 ∈ ℕ0 (abs‘𝐴))
193192adantr 484 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ ℕ0 (𝐾𝑗) = Σ𝑗 ∈ ℕ0 (abs‘𝐴))
194191, 193breqtrrd 5065 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) ≤ Σ𝑗 ∈ ℕ0 (𝐾𝑗))
195105ltp1d 11622 . . . . . . . . . . 11 (𝜑 → Σ𝑗 ∈ ℕ0 (𝐾𝑗) < (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))
196195adantr 484 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ ℕ0 (𝐾𝑗) < (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))
19798, 182, 183, 194, 196lelttrd 10850 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) < (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))
19893rpregt0d 12492 . . . . . . . . . . 11 (𝜑 → ((𝐸 / 2) ∈ ℝ ∧ 0 < (𝐸 / 2)))
199198adantr 484 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((𝐸 / 2) ∈ ℝ ∧ 0 < (𝐸 / 2)))
200 ltmul1 11542 . . . . . . . . . 10 ((Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) ∈ ℝ ∧ (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ∈ ℝ ∧ ((𝐸 / 2) ∈ ℝ ∧ 0 < (𝐸 / 2))) → (Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) < (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ↔ (Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) · (𝐸 / 2))))
20198, 183, 199, 200syl3anc 1369 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) < (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ↔ (Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) · (𝐸 / 2))))
202197, 201mpbid 235 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) · (𝐸 / 2)))
203109rpregt0d 12492 . . . . . . . . . 10 (𝜑 → ((Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ∈ ℝ ∧ 0 < (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
204203adantr 484 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ∈ ℝ ∧ 0 < (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
205 ltdivmul 11567 . . . . . . . . 9 (((Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) ∈ ℝ ∧ (𝐸 / 2) ∈ ℝ ∧ ((Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ∈ ℝ ∧ 0 < (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))) → (((Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) < (𝐸 / 2) ↔ (Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) · (𝐸 / 2))))
20699, 95, 204, 205syl3anc 1369 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (((Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) < (𝐸 / 2) ↔ (Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) · (𝐸 / 2))))
207202, 206mpbird 260 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) < (𝐸 / 2))
20881, 111, 95, 181, 207lelttrd 10850 . . . . . 6 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < (𝐸 / 2))
209 mertens.13 . . . . . . . . . . . 12 (𝜑 → (0 ≤ sup(𝑇, ℝ, < ) ∧ (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤𝑇 𝑤𝑧)))
210209simprd 499 . . . . . . . . . . 11 (𝜑 → (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤𝑇 𝑤𝑧))
211 suprcl 11651 . . . . . . . . . . 11 ((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤𝑇 𝑤𝑧) → sup(𝑇, ℝ, < ) ∈ ℝ)
212210, 211syl 17 . . . . . . . . . 10 (𝜑 → sup(𝑇, ℝ, < ) ∈ ℝ)
21394, 212remulcld 10723 . . . . . . . . 9 (𝜑 → ((𝐸 / 2) · sup(𝑇, ℝ, < )) ∈ ℝ)
214209simpld 498 . . . . . . . . . 10 (𝜑 → 0 ≤ sup(𝑇, ℝ, < ))
215212, 214ge0p1rpd 12516 . . . . . . . . 9 (𝜑 → (sup(𝑇, ℝ, < ) + 1) ∈ ℝ+)
216213, 215rerpdivcld 12517 . . . . . . . 8 (𝜑 → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℝ)
217216adantr 484 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℝ)
2185nnrpd 12484 . . . . . . . . . . . . . 14 (𝜑𝑠 ∈ ℝ+)
21993, 218rpdivcld 12503 . . . . . . . . . . . . 13 (𝜑 → ((𝐸 / 2) / 𝑠) ∈ ℝ+)
220219, 215rpdivcld 12503 . . . . . . . . . . . 12 (𝜑 → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℝ+)
221220rpred 12486 . . . . . . . . . . 11 (𝜑 → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℝ)
222221, 212remulcld 10723 . . . . . . . . . 10 (𝜑 → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈ ℝ)
223222ad2antrr 725 . . . . . . . . 9 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈ ℝ)
224 simpll 766 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → 𝜑)
22590, 12syl 17 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → 𝑗 ∈ ℕ0)
226224, 225, 76syl2anc 587 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (abs‘𝐴) ∈ ℝ)
227221ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℝ)
228224, 225, 102syl2anc 587 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (𝐾𝑗) = (abs‘𝐴))
229 fveq2 6664 . . . . . . . . . . . . . 14 (𝑚 = 𝑗 → (𝐾𝑚) = (𝐾𝑗))
230229breq1d 5047 . . . . . . . . . . . . 13 (𝑚 = 𝑗 → ((𝐾𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ↔ (𝐾𝑗) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))
2317simprd 499 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑚 ∈ (ℤ𝑡)(𝐾𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))
232231ad2antrr 725 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → ∀𝑚 ∈ (ℤ𝑡)(𝐾𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))
233 elfzuz 12966 . . . . . . . . . . . . . 14 (𝑗 ∈ (((𝑚𝑠) + 1)...𝑚) → 𝑗 ∈ (ℤ‘((𝑚𝑠) + 1)))
234 eluzle 12309 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ (ℤ‘(𝑠 + 𝑡)) → (𝑠 + 𝑡) ≤ 𝑚)
235234adantl 485 . . . . . . . . . . . . . . . . 17 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑠 + 𝑡) ≤ 𝑚)
2368nn0zd 12138 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑡 ∈ ℤ)
237236adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑡 ∈ ℤ)
238237zred 12140 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑡 ∈ ℝ)
23952, 238, 51leaddsub2d 11294 . . . . . . . . . . . . . . . . 17 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((𝑠 + 𝑡) ≤ 𝑚𝑡 ≤ (𝑚𝑠)))
240235, 239mpbid 235 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑡 ≤ (𝑚𝑠))
241 eluz 12310 . . . . . . . . . . . . . . . . 17 ((𝑡 ∈ ℤ ∧ (𝑚𝑠) ∈ ℤ) → ((𝑚𝑠) ∈ (ℤ𝑡) ↔ 𝑡 ≤ (𝑚𝑠)))
242237, 69, 241syl2anc 587 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((𝑚𝑠) ∈ (ℤ𝑡) ↔ 𝑡 ≤ (𝑚𝑠)))
243240, 242mpbird 260 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑚𝑠) ∈ (ℤ𝑡))
244 peano2uz 12355 . . . . . . . . . . . . . . 15 ((𝑚𝑠) ∈ (ℤ𝑡) → ((𝑚𝑠) + 1) ∈ (ℤ𝑡))
245243, 244syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((𝑚𝑠) + 1) ∈ (ℤ𝑡))
246 uztrn 12314 . . . . . . . . . . . . . 14 ((𝑗 ∈ (ℤ‘((𝑚𝑠) + 1)) ∧ ((𝑚𝑠) + 1) ∈ (ℤ𝑡)) → 𝑗 ∈ (ℤ𝑡))
247233, 245, 246syl2anr 599 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → 𝑗 ∈ (ℤ𝑡))
248230, 232, 247rspcdva 3546 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (𝐾𝑗) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))
249228, 248eqbrtrrd 5061 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (abs‘𝐴) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))
250226, 227, 249ltled 10840 . . . . . . . . . 10 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (abs‘𝐴) ≤ (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))
251210ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤𝑇 𝑤𝑧))
25251adantr 484 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → 𝑚 ∈ ℝ)
253 peano2zm 12078 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ℤ → (𝑠 − 1) ∈ ℤ)
25456, 253syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑠 − 1) ∈ ℤ)
255254zred 12140 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑠 − 1) ∈ ℝ)
256255ad2antrr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (𝑠 − 1) ∈ ℝ)
257225nn0red 12009 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → 𝑗 ∈ ℝ)
25850zcnd 12141 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑚 ∈ ℂ)
25952recnd 10721 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑠 ∈ ℂ)
260 1cnd 10688 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 1 ∈ ℂ)
261258, 259, 260subsubd 11077 . . . . . . . . . . . . . . . . 17 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑚 − (𝑠 − 1)) = ((𝑚𝑠) + 1))
262261adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (𝑚 − (𝑠 − 1)) = ((𝑚𝑠) + 1))
263 elfzle1 12973 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (((𝑚𝑠) + 1)...𝑚) → ((𝑚𝑠) + 1) ≤ 𝑗)
264263adantl 485 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → ((𝑚𝑠) + 1) ≤ 𝑗)
265262, 264eqbrtrd 5059 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (𝑚 − (𝑠 − 1)) ≤ 𝑗)
266252, 256, 257, 265subled 11295 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (𝑚𝑗) ≤ (𝑠 − 1))
26790, 16syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (𝑚𝑗) ∈ ℕ0)
268267, 30eleqtrdi 2863 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (𝑚𝑗) ∈ (ℤ‘0))
269254ad2antrr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (𝑠 − 1) ∈ ℤ)
270 elfz5 12962 . . . . . . . . . . . . . . 15 (((𝑚𝑗) ∈ (ℤ‘0) ∧ (𝑠 − 1) ∈ ℤ) → ((𝑚𝑗) ∈ (0...(𝑠 − 1)) ↔ (𝑚𝑗) ≤ (𝑠 − 1)))
271268, 269, 270syl2anc 587 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → ((𝑚𝑗) ∈ (0...(𝑠 − 1)) ↔ (𝑚𝑗) ≤ (𝑠 − 1)))
272266, 271mpbird 260 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (𝑚𝑗) ∈ (0...(𝑠 − 1)))
273 simplll 774 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → 𝜑)
27490, 19syldan 594 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → ((𝑚𝑗) + 1) ∈ ℕ0)
275274, 22sylan 583 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → 𝑘 ∈ ℕ0)
276273, 275, 24syl2anc 587 . . . . . . . . . . . . . . . 16 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → (𝐺𝑘) = 𝐵)
277276sumeq2dv 15122 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))(𝐺𝑘) = Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)
278277eqcomd 2765 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵 = Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))(𝐺𝑘))
279278fveq2d 6668 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))(𝐺𝑘)))
280131rspceeqv 3559 . . . . . . . . . . . . 13 (((𝑚𝑗) ∈ (0...(𝑠 − 1)) ∧ (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))(𝐺𝑘))) → ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)))
281272, 279, 280syl2anc 587 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)))
282 fvex 6677 . . . . . . . . . . . . 13 (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ∈ V
283 eqeq1 2763 . . . . . . . . . . . . . 14 (𝑧 = (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) → (𝑧 = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) ↔ (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘))))
284283rexbidv 3222 . . . . . . . . . . . . 13 (𝑧 = (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) → (∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) ↔ ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘))))
285 mertens.10 . . . . . . . . . . . . 13 𝑇 = {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘))}
286282, 284, 285elab2 3594 . . . . . . . . . . . 12 ((abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ∈ 𝑇 ↔ ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)))
287281, 286sylibr 237 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ∈ 𝑇)
288 suprub 11652 . . . . . . . . . . 11 (((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤𝑇 𝑤𝑧) ∧ (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ∈ 𝑇) → (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ≤ sup(𝑇, ℝ, < ))
289251, 287, 288syl2anc 587 . . . . . . . . . 10 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ≤ sup(𝑇, ℝ, < ))
290224, 225, 125syl2anc 587 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → ((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)))
29190, 78syldan 594 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ∈ ℝ)
29236absge0d 14866 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → 0 ≤ (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵))
29390, 292syldan 594 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → 0 ≤ (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵))
294291, 293jca 515 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → ((abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ∈ ℝ ∧ 0 ≤ (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)))
295212ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → sup(𝑇, ℝ, < ) ∈ ℝ)
296 lemul12a 11550 . . . . . . . . . . 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(𝑇, ℝ, < ))))
297290, 227, 294, 295, 296syl22anc 837 . . . . . . . . . 10 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (((abs‘𝐴) ≤ (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∧ (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ≤ sup(𝑇, ℝ, < )) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ≤ ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))))
298250, 289, 297mp2and 698 . . . . . . . . 9 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ≤ ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )))
29982, 91, 223, 298fsumle 15216 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ≤ Σ𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )))
300222recnd 10721 . . . . . . . . . . 11 (𝜑 → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈ ℂ)
301300adantr 484 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈ ℂ)
302 fsumconst 15207 . . . . . . . . . 10 (((((𝑚𝑠) + 1)...𝑚) ∈ Fin ∧ ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈ ℂ) → Σ𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) = ((♯‘(((𝑚𝑠) + 1)...𝑚)) · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))))
30382, 301, 302syl2anc 587 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) = ((♯‘(((𝑚𝑠) + 1)...𝑚)) · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))))
304 1zzd 12066 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 1 ∈ ℤ)
30556adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑠 ∈ ℤ)
306 fzen 12987 . . . . . . . . . . . . . 14 ((1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ (𝑚𝑠) ∈ ℤ) → (1...𝑠) ≈ ((1 + (𝑚𝑠))...(𝑠 + (𝑚𝑠))))
307304, 305, 69, 306syl3anc 1369 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (1...𝑠) ≈ ((1 + (𝑚𝑠))...(𝑠 + (𝑚𝑠))))
308 ax-1cn 10647 . . . . . . . . . . . . . . 15 1 ∈ ℂ
30969zcnd 12141 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑚𝑠) ∈ ℂ)
310 addcom 10878 . . . . . . . . . . . . . . 15 ((1 ∈ ℂ ∧ (𝑚𝑠) ∈ ℂ) → (1 + (𝑚𝑠)) = ((𝑚𝑠) + 1))
311308, 309, 310sylancr 590 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (1 + (𝑚𝑠)) = ((𝑚𝑠) + 1))
312259, 258pncan3d 11052 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑠 + (𝑚𝑠)) = 𝑚)
313311, 312oveq12d 7175 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((1 + (𝑚𝑠))...(𝑠 + (𝑚𝑠))) = (((𝑚𝑠) + 1)...𝑚))
314307, 313breqtrd 5063 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (1...𝑠) ≈ (((𝑚𝑠) + 1)...𝑚))
315 fzfid 13404 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (1...𝑠) ∈ Fin)
316 hashen 13771 . . . . . . . . . . . . 13 (((1...𝑠) ∈ Fin ∧ (((𝑚𝑠) + 1)...𝑚) ∈ Fin) → ((♯‘(1...𝑠)) = (♯‘(((𝑚𝑠) + 1)...𝑚)) ↔ (1...𝑠) ≈ (((𝑚𝑠) + 1)...𝑚)))
317315, 82, 316syl2anc 587 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((♯‘(1...𝑠)) = (♯‘(((𝑚𝑠) + 1)...𝑚)) ↔ (1...𝑠) ≈ (((𝑚𝑠) + 1)...𝑚)))
318314, 317mpbird 260 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (♯‘(1...𝑠)) = (♯‘(((𝑚𝑠) + 1)...𝑚)))
319 hashfz1 13770 . . . . . . . . . . . 12 (𝑠 ∈ ℕ0 → (♯‘(1...𝑠)) = 𝑠)
32047, 319syl 17 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (♯‘(1...𝑠)) = 𝑠)
321318, 320eqtr3d 2796 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (♯‘(((𝑚𝑠) + 1)...𝑚)) = 𝑠)
322321oveq1d 7172 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((♯‘(((𝑚𝑠) + 1)...𝑚)) · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))) = (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))))
323212recnd 10721 . . . . . . . . . . . 12 (𝜑 → sup(𝑇, ℝ, < ) ∈ ℂ)
324215rpcnne0d 12495 . . . . . . . . . . . 12 (𝜑 → ((sup(𝑇, ℝ, < ) + 1) ∈ ℂ ∧ (sup(𝑇, ℝ, < ) + 1) ≠ 0))
325 div23 11369 . . . . . . . . . . . 12 (((𝐸 / 2) ∈ ℂ ∧ sup(𝑇, ℝ, < ) ∈ ℂ ∧ ((sup(𝑇, ℝ, < ) + 1) ∈ ℂ ∧ (sup(𝑇, ℝ, < ) + 1) ≠ 0)) → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) = (((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )))
326156, 323, 324, 325syl3anc 1369 . . . . . . . . . . 11 (𝜑 → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) = (((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )))
32756zcnd 12141 . . . . . . . . . . . . . 14 (𝜑𝑠 ∈ ℂ)
328219rpcnd 12488 . . . . . . . . . . . . . 14 (𝜑 → ((𝐸 / 2) / 𝑠) ∈ ℂ)
329 divass 11368 . . . . . . . . . . . . . 14 ((𝑠 ∈ ℂ ∧ ((𝐸 / 2) / 𝑠) ∈ ℂ ∧ ((sup(𝑇, ℝ, < ) + 1) ∈ ℂ ∧ (sup(𝑇, ℝ, < ) + 1) ≠ 0)) → ((𝑠 · ((𝐸 / 2) / 𝑠)) / (sup(𝑇, ℝ, < ) + 1)) = (𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))
330327, 328, 324, 329syl3anc 1369 . . . . . . . . . . . . 13 (𝜑 → ((𝑠 · ((𝐸 / 2) / 𝑠)) / (sup(𝑇, ℝ, < ) + 1)) = (𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))
3315nnne0d 11738 . . . . . . . . . . . . . . 15 (𝜑𝑠 ≠ 0)
332156, 327, 331divcan2d 11470 . . . . . . . . . . . . . 14 (𝜑 → (𝑠 · ((𝐸 / 2) / 𝑠)) = (𝐸 / 2))
333332oveq1d 7172 . . . . . . . . . . . . 13 (𝜑 → ((𝑠 · ((𝐸 / 2) / 𝑠)) / (sup(𝑇, ℝ, < ) + 1)) = ((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)))
334330, 333eqtr3d 2796 . . . . . . . . . . . 12 (𝜑 → (𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) = ((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)))
335334oveq1d 7172 . . . . . . . . . . 11 (𝜑 → ((𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) · sup(𝑇, ℝ, < )) = (((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )))
336220rpcnd 12488 . . . . . . . . . . . 12 (𝜑 → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℂ)
337327, 336, 323mulassd 10716 . . . . . . . . . . 11 (𝜑 → ((𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) · sup(𝑇, ℝ, < )) = (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))))
338326, 335, 3373eqtr2rd 2801 . . . . . . . . . 10 (𝜑 → (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))) = (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)))
339338adantr 484 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))) = (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)))
340303, 322, 3393eqtrd 2798 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) = (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)))
341299, 340breqtrd 5063 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ≤ (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)))
342 peano2re 10865 . . . . . . . . . . 11 (sup(𝑇, ℝ, < ) ∈ ℝ → (sup(𝑇, ℝ, < ) + 1) ∈ ℝ)
343212, 342syl 17 . . . . . . . . . 10 (𝜑 → (sup(𝑇, ℝ, < ) + 1) ∈ ℝ)
344212ltp1d 11622 . . . . . . . . . 10 (𝜑 → sup(𝑇, ℝ, < ) < (sup(𝑇, ℝ, < ) + 1))
345212, 343, 93, 344ltmul2dd 12542 . . . . . . . . 9 (𝜑 → ((𝐸 / 2) · sup(𝑇, ℝ, < )) < ((𝐸 / 2) · (sup(𝑇, ℝ, < ) + 1)))
346213, 94, 215ltdivmul2d 12538 . . . . . . . . 9 (𝜑 → ((((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) < (𝐸 / 2) ↔ ((𝐸 / 2) · sup(𝑇, ℝ, < )) < ((𝐸 / 2) · (sup(𝑇, ℝ, < ) + 1))))
347345, 346mpbird 260 . . . . . . . 8 (𝜑 → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) < (𝐸 / 2))
348347adantr 484 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) < (𝐸 / 2))
34992, 217, 95, 341, 348lelttrd 10850 . . . . . 6 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < (𝐸 / 2))
35081, 92, 95, 95, 208, 349lt2addd 11315 . . . . 5 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) + Σ𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵))) < ((𝐸 / 2) + (𝐸 / 2)))
35114, 36absmuld 14876 . . . . . . 7 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) = ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)))
352351sumeq2dv 15122 . . . . . 6 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) = Σ𝑗 ∈ (0...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)))
35369zred 12140 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑚𝑠) ∈ ℝ)
354353ltp1d 11622 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑚𝑠) < ((𝑚𝑠) + 1))
355 fzdisj 12997 . . . . . . . 8 ((𝑚𝑠) < ((𝑚𝑠) + 1) → ((0...(𝑚𝑠)) ∩ (((𝑚𝑠) + 1)...𝑚)) = ∅)
356354, 355syl 17 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((0...(𝑚𝑠)) ∩ (((𝑚𝑠) + 1)...𝑚)) = ∅)
357 fzsplit 12996 . . . . . . . 8 ((𝑚𝑠) ∈ (0...𝑚) → (0...𝑚) = ((0...(𝑚𝑠)) ∪ (((𝑚𝑠) + 1)...𝑚)))
35867, 357syl 17 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (0...𝑚) = ((0...(𝑚𝑠)) ∪ (((𝑚𝑠) + 1)...𝑚)))
35979recnd 10721 . . . . . . 7 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ∈ ℂ)
360356, 358, 10, 359fsumsplit 15159 . . . . . 6 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) = (Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) + Σ𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵))))
361352, 360eqtr2d 2795 . . . . 5 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) + Σ𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵))) = Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)))
36242rpcnd 12488 . . . . . . 7 (𝜑𝐸 ∈ ℂ)
363362adantr 484 . . . . . 6 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝐸 ∈ ℂ)
3643632halvesd 11934 . . . . 5 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((𝐸 / 2) + (𝐸 / 2)) = 𝐸)
365350, 361, 3643brtr3d 5068 . . . 4 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸)
36639, 41, 44, 45, 365lelttrd 10850 . . 3 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸)
367366ralrimiva 3114 . 2 (𝜑 → ∀𝑚 ∈ (ℤ‘(𝑠 + 𝑡))(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸)
368 fveq2 6664 . . . 4 (𝑦 = (𝑠 + 𝑡) → (ℤ𝑦) = (ℤ‘(𝑠 + 𝑡)))
369368raleqdv 3330 . . 3 (𝑦 = (𝑠 + 𝑡) → (∀𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸 ↔ ∀𝑚 ∈ (ℤ‘(𝑠 + 𝑡))(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸))
370369rspcev 3544 . 2 (((𝑠 + 𝑡) ∈ ℕ0 ∧ ∀𝑚 ∈ (ℤ‘(𝑠 + 𝑡))(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸) → ∃𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸)
3719, 367, 370syl2anc 587 1 (𝜑 → ∃𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1085   = wceq 1539   ∈ wcel 2112  {cab 2736   ≠ wne 2952  ∀wral 3071  ∃wrex 3072   ∪ cun 3859   ∩ cin 3860   ⊆ wss 3861  ∅c0 4228   class class class wbr 5037  dom cdm 5529  ‘cfv 6341  (class class class)co 7157   ≈ cen 8538  Fincfn 8541  supcsup 8951  ℂcc 10587  ℝcr 10588  0cc0 10589  1c1 10590   + caddc 10592   · cmul 10594   < clt 10727   ≤ cle 10728   − cmin 10922   / cdiv 11349  ℕcn 11688  2c2 11743  ℕ0cn0 11948  ℤcz 12034  ℤ≥cuz 12296  ℝ+crp 12444  ...cfz 12953  seqcseq 13432  ♯chash 13754  abscabs 14655   ⇝ cli 14903  Σcsu 15104 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5161  ax-sep 5174  ax-nul 5181  ax-pow 5239  ax-pr 5303  ax-un 7466  ax-inf2 9151  ax-cnex 10645  ax-resscn 10646  ax-1cn 10647  ax-icn 10648  ax-addcl 10649  ax-addrcl 10650  ax-mulcl 10651  ax-mulrcl 10652  ax-mulcom 10653  ax-addass 10654  ax-mulass 10655  ax-distr 10656  ax-i2m1 10657  ax-1ne0 10658  ax-1rid 10659  ax-rnegex 10660  ax-rrecex 10661  ax-cnre 10662  ax-pre-lttri 10663  ax-pre-lttrn 10664  ax-pre-ltadd 10665  ax-pre-mulgt0 10666  ax-pre-sup 10667 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rmo 3079  df-rab 3080  df-v 3412  df-sbc 3700  df-csb 3809  df-dif 3864  df-un 3866  df-in 3868  df-ss 3878  df-pss 3880  df-nul 4229  df-if 4425  df-pw 4500  df-sn 4527  df-pr 4529  df-tp 4531  df-op 4533  df-uni 4803  df-int 4843  df-iun 4889  df-br 5038  df-opab 5100  df-mpt 5118  df-tr 5144  df-id 5435  df-eprel 5440  df-po 5448  df-so 5449  df-fr 5488  df-se 5489  df-we 5490  df-xp 5535  df-rel 5536  df-cnv 5537  df-co 5538  df-dm 5539  df-rn 5540  df-res 5541  df-ima 5542  df-pred 6132  df-ord 6178  df-on 6179  df-lim 6180  df-suc 6181  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-isom 6350  df-riota 7115  df-ov 7160  df-oprab 7161  df-mpo 7162  df-om 7587  df-1st 7700  df-2nd 7701  df-wrecs 7964  df-recs 8025  df-rdg 8063  df-1o 8119  df-er 8306  df-pm 8426  df-en 8542  df-dom 8543  df-sdom 8544  df-fin 8545  df-sup 8953  df-inf 8954  df-oi 9021  df-card 9415  df-pnf 10729  df-mnf 10730  df-xr 10731  df-ltxr 10732  df-le 10733  df-sub 10924  df-neg 10925  df-div 11350  df-nn 11689  df-2 11751  df-3 11752  df-n0 11949  df-z 12035  df-uz 12297  df-rp 12445  df-ico 12799  df-fz 12954  df-fzo 13097  df-fl 13225  df-seq 13433  df-exp 13494  df-hash 13755  df-cj 14520  df-re 14521  df-im 14522  df-sqrt 14656  df-abs 14657  df-clim 14907  df-rlim 14908  df-sum 15105 This theorem is referenced by:  mertenslem2  15303
 Copyright terms: Public domain W3C validator