ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mertenslemi1 GIF version

Theorem mertenslemi1 11574
Description: Lemma for mertensabs 11576. (Contributed by Mario Carneiro, 29-Apr-2014.) (Revised by Jim Kingdon, 2-Dec-2022.)
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.p (𝜑𝑃 ∈ ℝ)
mertens.i12 (𝜑 → (𝜓 ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑚 ∈ (ℤ𝑡)(𝐾𝑚) < (((𝐸 / 2) / 𝑠) / (𝑃 + 1)))))
mertens.pge0 (𝜑 → 0 ≤ 𝑃)
mertens.pub (𝜑 → ∀𝑤𝑇 𝑤𝑃)
Assertion
Ref Expression
mertenslemi1 (𝜑 → ∃𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸)
Distinct variable groups:   𝑗,𝑚,𝑛,𝑠,𝑡,𝑦,𝑧,𝐵   𝑗,𝑘,𝐺,𝑚,𝑛,𝑠,𝑦,𝑧   𝜑,𝑗,𝑘,𝑚,𝑦,𝑧   𝑡,𝑘,𝐴,𝑚,𝑛,𝑠,𝑦   𝑗,𝐸,𝑘,𝑚,𝑛,𝑠,𝑡,𝑦,𝑧   𝑗,𝐾,𝑘,𝑚,𝑛,𝑠,𝑡,𝑦,𝑧   𝑗,𝐹,𝑚,𝑛,𝑦   𝜓,𝑗,𝑘,𝑚,𝑛,𝑡,𝑦,𝑧   𝑤,𝑗,𝑇,𝑘,𝑚,𝑛,𝑡,𝑦,𝑧   𝑘,𝐻,𝑚,𝑦   𝑤,𝐵   𝑃,𝑗,𝑚,𝑤
Allowed substitution hints:   𝜑(𝑤,𝑡,𝑛,𝑠)   𝜓(𝑤,𝑠)   𝐴(𝑧,𝑤,𝑗)   𝐵(𝑘)   𝑃(𝑦,𝑧,𝑡,𝑘,𝑛,𝑠)   𝑇(𝑠)   𝐸(𝑤)   𝐹(𝑧,𝑤,𝑡,𝑘,𝑠)   𝐺(𝑤,𝑡)   𝐻(𝑧,𝑤,𝑡,𝑗,𝑛,𝑠)   𝐾(𝑤)

Proof of Theorem mertenslemi1
StepHypRef Expression
1 mertens.i12 . . . . . . 7 (𝜑 → (𝜓 ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑚 ∈ (ℤ𝑡)(𝐾𝑚) < (((𝐸 / 2) / 𝑠) / (𝑃 + 1)))))
21simpld 112 . . . . . 6 (𝜑𝜓)
3 mertens.11 . . . . . 6 (𝜓 ↔ (𝑠 ∈ ℕ ∧ ∀𝑛 ∈ (ℤ𝑠)(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
42, 3sylib 122 . . . . 5 (𝜑 → (𝑠 ∈ ℕ ∧ ∀𝑛 ∈ (ℤ𝑠)(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
54simpld 112 . . . 4 (𝜑𝑠 ∈ ℕ)
65nnnn0d 9258 . . 3 (𝜑𝑠 ∈ ℕ0)
71simprd 114 . . . 4 (𝜑 → (𝑡 ∈ ℕ0 ∧ ∀𝑚 ∈ (ℤ𝑡)(𝐾𝑚) < (((𝐸 / 2) / 𝑠) / (𝑃 + 1))))
87simpld 112 . . 3 (𝜑𝑡 ∈ ℕ0)
96, 8nn0addcld 9262 . 2 (𝜑 → (𝑠 + 𝑡) ∈ ℕ0)
10 0zd 9294 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 0 ∈ ℤ)
11 eluzelz 9566 . . . . . . . 8 (𝑚 ∈ (ℤ‘(𝑠 + 𝑡)) → 𝑚 ∈ ℤ)
1211adantl 277 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑚 ∈ ℤ)
1310, 12fzfigd 10461 . . . . . 6 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (0...𝑚) ∈ Fin)
14 simpl 109 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝜑)
15 elfznn0 10143 . . . . . . . 8 (𝑗 ∈ (0...𝑚) → 𝑗 ∈ ℕ0)
16 mertens.3 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → 𝐴 ∈ ℂ)
1714, 15, 16syl2an 289 . . . . . . 7 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → 𝐴 ∈ ℂ)
18 eqid 2189 . . . . . . . 8 (ℤ‘((𝑚𝑗) + 1)) = (ℤ‘((𝑚𝑗) + 1))
19 fznn0sub 10086 . . . . . . . . . . 11 (𝑗 ∈ (0...𝑚) → (𝑚𝑗) ∈ ℕ0)
2019adantl 277 . . . . . . . . . 10 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (𝑚𝑗) ∈ ℕ0)
21 peano2nn0 9245 . . . . . . . . . 10 ((𝑚𝑗) ∈ ℕ0 → ((𝑚𝑗) + 1) ∈ ℕ0)
2220, 21syl 14 . . . . . . . . 9 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((𝑚𝑗) + 1) ∈ ℕ0)
2322nn0zd 9402 . . . . . . . 8 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((𝑚𝑗) + 1) ∈ ℤ)
24 simplll 533 . . . . . . . . 9 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → 𝜑)
25 eluznn0 9628 . . . . . . . . . 10 ((((𝑚𝑗) + 1) ∈ ℕ0𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → 𝑘 ∈ ℕ0)
2622, 25sylan 283 . . . . . . . . 9 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → 𝑘 ∈ ℕ0)
27 mertens.4 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (𝐺𝑘) = 𝐵)
2824, 26, 27syl2anc 411 . . . . . . . 8 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → (𝐺𝑘) = 𝐵)
29 mertens.5 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)
3024, 26, 29syl2anc 411 . . . . . . . 8 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → 𝐵 ∈ ℂ)
31 mertens.8 . . . . . . . . . 10 (𝜑 → seq0( + , 𝐺) ∈ dom ⇝ )
3231ad2antrr 488 . . . . . . . . 9 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → seq0( + , 𝐺) ∈ dom ⇝ )
33 nn0uz 9591 . . . . . . . . . 10 0 = (ℤ‘0)
34 simpll 527 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → 𝜑)
3527, 29eqeltrd 2266 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → (𝐺𝑘) ∈ ℂ)
3634, 35sylan 283 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) ∈ ℂ)
3733, 22, 36iserex 11378 . . . . . . . . 9 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (seq0( + , 𝐺) ∈ dom ⇝ ↔ seq((𝑚𝑗) + 1)( + , 𝐺) ∈ dom ⇝ ))
3832, 37mpbid 147 . . . . . . . 8 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → seq((𝑚𝑗) + 1)( + , 𝐺) ∈ dom ⇝ )
3918, 23, 28, 30, 38isumcl 11464 . . . . . . 7 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵 ∈ ℂ)
4017, 39mulcld 8007 . . . . . 6 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ∈ ℂ)
4113, 40fsumcl 11439 . . . . 5 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ∈ ℂ)
4241abscld 11221 . . . 4 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ∈ ℝ)
4340abscld 11221 . . . . 5 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ∈ ℝ)
4413, 43fsumrecl 11440 . . . 4 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ∈ ℝ)
45 mertens.9 . . . . . 6 (𝜑𝐸 ∈ ℝ+)
4645rpred 9725 . . . . 5 (𝜑𝐸 ∈ ℝ)
4746adantr 276 . . . 4 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝐸 ∈ ℝ)
4813, 40fsumabs 11504 . . . 4 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ≤ Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)))
495nnzd 9403 . . . . . . . . . 10 (𝜑𝑠 ∈ ℤ)
5049adantr 276 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑠 ∈ ℤ)
5112, 50zsubcld 9409 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑚𝑠) ∈ ℤ)
5210, 51fzfigd 10461 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (0...(𝑚𝑠)) ∈ Fin)
536adantr 276 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑠 ∈ ℕ0)
5453nn0ge0d 9261 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 0 ≤ 𝑠)
5512zred 9404 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑚 ∈ ℝ)
5653nn0red 9259 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑠 ∈ ℝ)
5755, 56subge02d 8523 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (0 ≤ 𝑠 ↔ (𝑚𝑠) ≤ 𝑚))
5854, 57mpbid 147 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑚𝑠) ≤ 𝑚)
5953, 33eleqtrdi 2282 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑠 ∈ (ℤ‘0))
60 uzid 9571 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ℤ → 𝑠 ∈ (ℤ𝑠))
6149, 60syl 14 . . . . . . . . . . . . . . . . 17 (𝜑𝑠 ∈ (ℤ𝑠))
62 uzaddcl 9615 . . . . . . . . . . . . . . . . 17 ((𝑠 ∈ (ℤ𝑠) ∧ 𝑡 ∈ ℕ0) → (𝑠 + 𝑡) ∈ (ℤ𝑠))
6361, 8, 62syl2anc 411 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑠 + 𝑡) ∈ (ℤ𝑠))
64 eqid 2189 . . . . . . . . . . . . . . . . 17 (ℤ𝑠) = (ℤ𝑠)
6564uztrn2 9574 . . . . . . . . . . . . . . . 16 (((𝑠 + 𝑡) ∈ (ℤ𝑠) ∧ 𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑚 ∈ (ℤ𝑠))
6663, 65sylan 283 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑚 ∈ (ℤ𝑠))
67 elfzuzb 10048 . . . . . . . . . . . . . . 15 (𝑠 ∈ (0...𝑚) ↔ (𝑠 ∈ (ℤ‘0) ∧ 𝑚 ∈ (ℤ𝑠)))
6859, 66, 67sylanbrc 417 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑠 ∈ (0...𝑚))
69 fznn0sub2 10157 . . . . . . . . . . . . . 14 (𝑠 ∈ (0...𝑚) → (𝑚𝑠) ∈ (0...𝑚))
7068, 69syl 14 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑚𝑠) ∈ (0...𝑚))
71 elfzelz 10054 . . . . . . . . . . . . 13 ((𝑚𝑠) ∈ (0...𝑚) → (𝑚𝑠) ∈ ℤ)
7270, 71syl 14 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑚𝑠) ∈ ℤ)
73 eluz 9570 . . . . . . . . . . . 12 (((𝑚𝑠) ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑚 ∈ (ℤ‘(𝑚𝑠)) ↔ (𝑚𝑠) ≤ 𝑚))
7472, 12, 73syl2anc 411 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑚 ∈ (ℤ‘(𝑚𝑠)) ↔ (𝑚𝑠) ≤ 𝑚))
7558, 74mpbird 167 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑚 ∈ (ℤ‘(𝑚𝑠)))
76 fzss2 10093 . . . . . . . . . 10 (𝑚 ∈ (ℤ‘(𝑚𝑠)) → (0...(𝑚𝑠)) ⊆ (0...𝑚))
7775, 76syl 14 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (0...(𝑚𝑠)) ⊆ (0...𝑚))
7877sselda 3170 . . . . . . . 8 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → 𝑗 ∈ (0...𝑚))
7916abscld 11221 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → (abs‘𝐴) ∈ ℝ)
8014, 15, 79syl2an 289 . . . . . . . . 9 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘𝐴) ∈ ℝ)
8139abscld 11221 . . . . . . . . 9 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ∈ ℝ)
8280, 81remulcld 8017 . . . . . . . 8 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ∈ ℝ)
8378, 82syldan 282 . . . . . . 7 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ∈ ℝ)
8452, 83fsumrecl 11440 . . . . . 6 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ∈ ℝ)
8551peano2zd 9407 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((𝑚𝑠) + 1) ∈ ℤ)
8685, 12fzfigd 10461 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (((𝑚𝑠) + 1)...𝑚) ∈ Fin)
87 elfznn0 10143 . . . . . . . . . . . . 13 ((𝑚𝑠) ∈ (0...𝑚) → (𝑚𝑠) ∈ ℕ0)
8870, 87syl 14 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑚𝑠) ∈ ℕ0)
89 peano2nn0 9245 . . . . . . . . . . . 12 ((𝑚𝑠) ∈ ℕ0 → ((𝑚𝑠) + 1) ∈ ℕ0)
9088, 89syl 14 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((𝑚𝑠) + 1) ∈ ℕ0)
9190, 33eleqtrdi 2282 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((𝑚𝑠) + 1) ∈ (ℤ‘0))
92 fzss1 10092 . . . . . . . . . 10 (((𝑚𝑠) + 1) ∈ (ℤ‘0) → (((𝑚𝑠) + 1)...𝑚) ⊆ (0...𝑚))
9391, 92syl 14 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (((𝑚𝑠) + 1)...𝑚) ⊆ (0...𝑚))
9493sselda 3170 . . . . . . . 8 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → 𝑗 ∈ (0...𝑚))
9594, 82syldan 282 . . . . . . 7 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ∈ ℝ)
9686, 95fsumrecl 11440 . . . . . 6 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ∈ ℝ)
9745rphalfcld 9738 . . . . . . . 8 (𝜑 → (𝐸 / 2) ∈ ℝ+)
9897rpred 9725 . . . . . . 7 (𝜑 → (𝐸 / 2) ∈ ℝ)
9998adantr 276 . . . . . 6 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝐸 / 2) ∈ ℝ)
100 elfznn0 10143 . . . . . . . . . . 11 (𝑗 ∈ (0...(𝑚𝑠)) → 𝑗 ∈ ℕ0)
10114, 100, 79syl2an 289 . . . . . . . . . 10 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → (abs‘𝐴) ∈ ℝ)
10252, 101fsumrecl 11440 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) ∈ ℝ)
103102, 99remulcld 8017 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) ∈ ℝ)
104 0zd 9294 . . . . . . . . . . 11 (𝜑 → 0 ∈ ℤ)
105 eqidd 2190 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → (𝐾𝑗) = (𝐾𝑗))
106 mertens.2 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → (𝐾𝑗) = (abs‘𝐴))
107106, 79eqeltrd 2266 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → (𝐾𝑗) ∈ ℝ)
108 mertens.7 . . . . . . . . . . 11 (𝜑 → seq0( + , 𝐾) ∈ dom ⇝ )
10933, 104, 105, 107, 108isumrecl 11468 . . . . . . . . . 10 (𝜑 → Σ𝑗 ∈ ℕ0 (𝐾𝑗) ∈ ℝ)
11016absge0d 11224 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → 0 ≤ (abs‘𝐴))
111110, 106breqtrrd 4046 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → 0 ≤ (𝐾𝑗))
11233, 104, 105, 107, 108, 111isumge0 11469 . . . . . . . . . 10 (𝜑 → 0 ≤ Σ𝑗 ∈ ℕ0 (𝐾𝑗))
113109, 112ge0p1rpd 9756 . . . . . . . . 9 (𝜑 → (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ∈ ℝ+)
114113adantr 276 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ∈ ℝ+)
115103, 114rerpdivcld 9757 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) ∈ ℝ)
11697, 113rpdivcld 9743 . . . . . . . . . . . 12 (𝜑 → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) ∈ ℝ+)
117116rpred 9725 . . . . . . . . . . 11 (𝜑 → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) ∈ ℝ)
118117ad2antrr 488 . . . . . . . . . 10 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) ∈ ℝ)
119101, 118remulcld 8017 . . . . . . . . 9 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))) ∈ ℝ)
12078, 23syldan 282 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → ((𝑚𝑗) + 1) ∈ ℤ)
121 simplll 533 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → 𝜑)
12278, 22syldan 282 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → ((𝑚𝑗) + 1) ∈ ℕ0)
123122, 25sylan 283 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → 𝑘 ∈ ℕ0)
124121, 123, 27syl2anc 411 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → (𝐺𝑘) = 𝐵)
125121, 123, 29syl2anc 411 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → 𝐵 ∈ ℂ)
12678, 38syldan 282 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → seq((𝑚𝑗) + 1)( + , 𝐺) ∈ dom ⇝ )
12718, 120, 124, 125, 126isumcl 11464 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵 ∈ ℂ)
128127abscld 11221 . . . . . . . . . 10 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ∈ ℝ)
12979, 110jca 306 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → ((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)))
13014, 100, 129syl2an 289 . . . . . . . . . 10 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → ((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)))
131124sumeq2dv 11407 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))(𝐺𝑘) = Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)
132131fveq2d 5538 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))(𝐺𝑘)) = (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵))
133 fvoveq1 5918 . . . . . . . . . . . . . . . 16 (𝑛 = (𝑚𝑗) → (ℤ‘(𝑛 + 1)) = (ℤ‘((𝑚𝑗) + 1)))
134133sumeq1d 11405 . . . . . . . . . . . . . . 15 (𝑛 = (𝑚𝑗) → Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘) = Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))(𝐺𝑘))
135134fveq2d 5538 . . . . . . . . . . . . . 14 (𝑛 = (𝑚𝑗) → (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) = (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))(𝐺𝑘)))
136135breq1d 4028 . . . . . . . . . . . . 13 (𝑛 = (𝑚𝑗) → ((abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) ↔ (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
1374simprd 114 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑛 ∈ (ℤ𝑠)(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
138137ad2antrr 488 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → ∀𝑛 ∈ (ℤ𝑠)(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
139 elfzelz 10054 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...(𝑚𝑠)) → 𝑗 ∈ ℤ)
140139adantl 277 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → 𝑗 ∈ ℤ)
141140zred 9404 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → 𝑗 ∈ ℝ)
14211ad2antlr 489 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → 𝑚 ∈ ℤ)
143142zred 9404 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → 𝑚 ∈ ℝ)
14449ad2antrr 488 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → 𝑠 ∈ ℤ)
145144zred 9404 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → 𝑠 ∈ ℝ)
146 elfzle2 10057 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...(𝑚𝑠)) → 𝑗 ≤ (𝑚𝑠))
147146adantl 277 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → 𝑗 ≤ (𝑚𝑠))
148141, 143, 145, 147lesubd 8535 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → 𝑠 ≤ (𝑚𝑗))
149142, 140zsubcld 9409 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → (𝑚𝑗) ∈ ℤ)
150 eluz 9570 . . . . . . . . . . . . . . 15 ((𝑠 ∈ ℤ ∧ (𝑚𝑗) ∈ ℤ) → ((𝑚𝑗) ∈ (ℤ𝑠) ↔ 𝑠 ≤ (𝑚𝑗)))
151144, 149, 150syl2anc 411 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → ((𝑚𝑗) ∈ (ℤ𝑠) ↔ 𝑠 ≤ (𝑚𝑗)))
152148, 151mpbird 167 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → (𝑚𝑗) ∈ (ℤ𝑠))
153136, 138, 152rspcdva 2861 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
154132, 153eqbrtrrd 4042 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
155128, 118, 154ltled 8105 . . . . . . . . . 10 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ≤ ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
156 lemul2a 8845 . . . . . . . . . 10 ((((abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ∈ ℝ ∧ ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) ∈ ℝ ∧ ((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴))) ∧ (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ≤ ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ≤ ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
157128, 118, 130, 155, 156syl31anc 1252 . . . . . . . . 9 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ≤ ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
15852, 83, 119, 157fsumle 11502 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ≤ Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
159102recnd 8015 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) ∈ ℂ)
16097rpcnd 9727 . . . . . . . . . . 11 (𝜑 → (𝐸 / 2) ∈ ℂ)
161160adantr 276 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝐸 / 2) ∈ ℂ)
162 peano2re 8122 . . . . . . . . . . . . 13 𝑗 ∈ ℕ0 (𝐾𝑗) ∈ ℝ → (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ∈ ℝ)
163109, 162syl 14 . . . . . . . . . . . 12 (𝜑 → (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ∈ ℝ)
164163recnd 8015 . . . . . . . . . . 11 (𝜑 → (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ∈ ℂ)
165164adantr 276 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ∈ ℂ)
166114rpap0d 9731 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) # 0)
167159, 161, 165, 166divassapd 8812 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) = (Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
168 fveq2 5534 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑗 → (𝐾𝑛) = (𝐾𝑗))
169168cbvsumv 11400 . . . . . . . . . . . . . . . 16 Σ𝑛 ∈ ℕ0 (𝐾𝑛) = Σ𝑗 ∈ ℕ0 (𝐾𝑗)
170169oveq1i 5905 . . . . . . . . . . . . . . 15 𝑛 ∈ ℕ0 (𝐾𝑛) + 1) = (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)
171170oveq2i 5906 . . . . . . . . . . . . . 14 ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾𝑛) + 1)) = ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))
172171, 116eqeltrid 2276 . . . . . . . . . . . . 13 (𝜑 → ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾𝑛) + 1)) ∈ ℝ+)
173172rpcnd 9727 . . . . . . . . . . . 12 (𝜑 → ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾𝑛) + 1)) ∈ ℂ)
174173adantr 276 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾𝑛) + 1)) ∈ ℂ)
17579recnd 8015 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → (abs‘𝐴) ∈ ℂ)
17614, 100, 175syl2an 289 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → (abs‘𝐴) ∈ ℂ)
17752, 174, 176fsummulc1 11488 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾𝑛) + 1))) = Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾𝑛) + 1))))
178171oveq2i 5906 . . . . . . . . . 10 𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾𝑛) + 1))) = (Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
179171oveq2i 5906 . . . . . . . . . . . 12 ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾𝑛) + 1))) = ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
180179a1i 9 . . . . . . . . . . 11 (𝑗 ∈ (0...(𝑚𝑠)) → ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾𝑛) + 1))) = ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
181180sumeq2i 11403 . . . . . . . . . 10 Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾𝑛) + 1))) = Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
182177, 178, 1813eqtr3g 2245 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))) = Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
183167, 182eqtrd 2222 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) = Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
184158, 183breqtrrd 4046 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ≤ ((Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
185109adantr 276 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ ℕ0 (𝐾𝑗) ∈ ℝ)
186163adantr 276 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ∈ ℝ)
187 fz0ssnn0 10145 . . . . . . . . . . . . 13 (0...(𝑚𝑠)) ⊆ ℕ0
188187a1i 9 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (0...(𝑚𝑠)) ⊆ ℕ0)
189106adantlr 477 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ0) → (𝐾𝑗) = (abs‘𝐴))
190 nn0z 9302 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ0𝑗 ∈ ℤ)
191190adantl 277 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ0) → 𝑗 ∈ ℤ)
192 0zd 9294 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ0) → 0 ∈ ℤ)
19351adantr 276 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ0) → (𝑚𝑠) ∈ ℤ)
194 fzdcel 10069 . . . . . . . . . . . . . 14 ((𝑗 ∈ ℤ ∧ 0 ∈ ℤ ∧ (𝑚𝑠) ∈ ℤ) → DECID 𝑗 ∈ (0...(𝑚𝑠)))
195191, 192, 193, 194syl3anc 1249 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ0) → DECID 𝑗 ∈ (0...(𝑚𝑠)))
196195ralrimiva 2563 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ∀𝑗 ∈ ℕ0 DECID 𝑗 ∈ (0...(𝑚𝑠)))
19779adantlr 477 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ0) → (abs‘𝐴) ∈ ℝ)
198110adantlr 477 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ0) → 0 ≤ (abs‘𝐴))
199108adantr 276 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → seq0( + , 𝐾) ∈ dom ⇝ )
20033, 10, 52, 188, 189, 196, 197, 198, 199isumlessdc 11535 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) ≤ Σ𝑗 ∈ ℕ0 (abs‘𝐴))
201106sumeq2dv 11407 . . . . . . . . . . . 12 (𝜑 → Σ𝑗 ∈ ℕ0 (𝐾𝑗) = Σ𝑗 ∈ ℕ0 (abs‘𝐴))
202201adantr 276 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ ℕ0 (𝐾𝑗) = Σ𝑗 ∈ ℕ0 (abs‘𝐴))
203200, 202breqtrrd 4046 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) ≤ Σ𝑗 ∈ ℕ0 (𝐾𝑗))
204109ltp1d 8916 . . . . . . . . . . 11 (𝜑 → Σ𝑗 ∈ ℕ0 (𝐾𝑗) < (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))
205204adantr 276 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ ℕ0 (𝐾𝑗) < (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))
206102, 185, 186, 203, 205lelttrd 8111 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) < (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))
20797rpregt0d 9732 . . . . . . . . . . 11 (𝜑 → ((𝐸 / 2) ∈ ℝ ∧ 0 < (𝐸 / 2)))
208207adantr 276 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((𝐸 / 2) ∈ ℝ ∧ 0 < (𝐸 / 2)))
209 ltmul1 8578 . . . . . . . . . 10 ((Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) ∈ ℝ ∧ (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ∈ ℝ ∧ ((𝐸 / 2) ∈ ℝ ∧ 0 < (𝐸 / 2))) → (Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) < (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ↔ (Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) · (𝐸 / 2))))
210102, 186, 208, 209syl3anc 1249 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) < (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ↔ (Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) · (𝐸 / 2))))
211206, 210mpbid 147 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) · (𝐸 / 2)))
212113rpregt0d 9732 . . . . . . . . . 10 (𝜑 → ((Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ∈ ℝ ∧ 0 < (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
213212adantr 276 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ∈ ℝ ∧ 0 < (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
214 ltdivmul 8862 . . . . . . . . 9 (((Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) ∈ ℝ ∧ (𝐸 / 2) ∈ ℝ ∧ ((Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ∈ ℝ ∧ 0 < (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))) → (((Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) < (𝐸 / 2) ↔ (Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) · (𝐸 / 2))))
215103, 99, 213, 214syl3anc 1249 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (((Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) < (𝐸 / 2) ↔ (Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) · (𝐸 / 2))))
216211, 215mpbird 167 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) < (𝐸 / 2))
21784, 115, 99, 184, 216lelttrd 8111 . . . . . 6 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < (𝐸 / 2))
218 mertens.p . . . . . . . . . 10 (𝜑𝑃 ∈ ℝ)
21998, 218remulcld 8017 . . . . . . . . 9 (𝜑 → ((𝐸 / 2) · 𝑃) ∈ ℝ)
220 mertens.pge0 . . . . . . . . . 10 (𝜑 → 0 ≤ 𝑃)
221218, 220ge0p1rpd 9756 . . . . . . . . 9 (𝜑 → (𝑃 + 1) ∈ ℝ+)
222219, 221rerpdivcld 9757 . . . . . . . 8 (𝜑 → (((𝐸 / 2) · 𝑃) / (𝑃 + 1)) ∈ ℝ)
223222adantr 276 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (((𝐸 / 2) · 𝑃) / (𝑃 + 1)) ∈ ℝ)
2245nnrpd 9723 . . . . . . . . . . . . . 14 (𝜑𝑠 ∈ ℝ+)
22597, 224rpdivcld 9743 . . . . . . . . . . . . 13 (𝜑 → ((𝐸 / 2) / 𝑠) ∈ ℝ+)
226225, 221rpdivcld 9743 . . . . . . . . . . . 12 (𝜑 → (((𝐸 / 2) / 𝑠) / (𝑃 + 1)) ∈ ℝ+)
227226rpred 9725 . . . . . . . . . . 11 (𝜑 → (((𝐸 / 2) / 𝑠) / (𝑃 + 1)) ∈ ℝ)
228227, 218remulcld 8017 . . . . . . . . . 10 (𝜑 → ((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃) ∈ ℝ)
229228ad2antrr 488 . . . . . . . . 9 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → ((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃) ∈ ℝ)
230 simpll 527 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → 𝜑)
23194, 15syl 14 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → 𝑗 ∈ ℕ0)
232230, 231, 79syl2anc 411 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (abs‘𝐴) ∈ ℝ)
233227ad2antrr 488 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (((𝐸 / 2) / 𝑠) / (𝑃 + 1)) ∈ ℝ)
234230, 231, 106syl2anc 411 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (𝐾𝑗) = (abs‘𝐴))
235 fveq2 5534 . . . . . . . . . . . . . 14 (𝑚 = 𝑗 → (𝐾𝑚) = (𝐾𝑗))
236235breq1d 4028 . . . . . . . . . . . . 13 (𝑚 = 𝑗 → ((𝐾𝑚) < (((𝐸 / 2) / 𝑠) / (𝑃 + 1)) ↔ (𝐾𝑗) < (((𝐸 / 2) / 𝑠) / (𝑃 + 1))))
2377simprd 114 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑚 ∈ (ℤ𝑡)(𝐾𝑚) < (((𝐸 / 2) / 𝑠) / (𝑃 + 1)))
238237ad2antrr 488 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → ∀𝑚 ∈ (ℤ𝑡)(𝐾𝑚) < (((𝐸 / 2) / 𝑠) / (𝑃 + 1)))
239 elfzuz 10050 . . . . . . . . . . . . . 14 (𝑗 ∈ (((𝑚𝑠) + 1)...𝑚) → 𝑗 ∈ (ℤ‘((𝑚𝑠) + 1)))
240 eluzle 9569 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ (ℤ‘(𝑠 + 𝑡)) → (𝑠 + 𝑡) ≤ 𝑚)
241240adantl 277 . . . . . . . . . . . . . . . . 17 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑠 + 𝑡) ≤ 𝑚)
2428nn0zd 9402 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑡 ∈ ℤ)
243242adantr 276 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑡 ∈ ℤ)
244243zred 9404 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑡 ∈ ℝ)
24556, 244, 55leaddsub2d 8533 . . . . . . . . . . . . . . . . 17 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((𝑠 + 𝑡) ≤ 𝑚𝑡 ≤ (𝑚𝑠)))
246241, 245mpbid 147 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑡 ≤ (𝑚𝑠))
247 eluz 9570 . . . . . . . . . . . . . . . . 17 ((𝑡 ∈ ℤ ∧ (𝑚𝑠) ∈ ℤ) → ((𝑚𝑠) ∈ (ℤ𝑡) ↔ 𝑡 ≤ (𝑚𝑠)))
248243, 72, 247syl2anc 411 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((𝑚𝑠) ∈ (ℤ𝑡) ↔ 𝑡 ≤ (𝑚𝑠)))
249246, 248mpbird 167 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑚𝑠) ∈ (ℤ𝑡))
250 peano2uz 9612 . . . . . . . . . . . . . . 15 ((𝑚𝑠) ∈ (ℤ𝑡) → ((𝑚𝑠) + 1) ∈ (ℤ𝑡))
251249, 250syl 14 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((𝑚𝑠) + 1) ∈ (ℤ𝑡))
252 uztrn 9573 . . . . . . . . . . . . . 14 ((𝑗 ∈ (ℤ‘((𝑚𝑠) + 1)) ∧ ((𝑚𝑠) + 1) ∈ (ℤ𝑡)) → 𝑗 ∈ (ℤ𝑡))
253239, 251, 252syl2anr 290 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → 𝑗 ∈ (ℤ𝑡))
254236, 238, 253rspcdva 2861 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (𝐾𝑗) < (((𝐸 / 2) / 𝑠) / (𝑃 + 1)))
255234, 254eqbrtrrd 4042 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (abs‘𝐴) < (((𝐸 / 2) / 𝑠) / (𝑃 + 1)))
256232, 233, 255ltled 8105 . . . . . . . . . 10 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (abs‘𝐴) ≤ (((𝐸 / 2) / 𝑠) / (𝑃 + 1)))
257 breq1 4021 . . . . . . . . . . 11 (𝑤 = (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) → (𝑤𝑃 ↔ (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ≤ 𝑃))
258 mertens.pub . . . . . . . . . . . 12 (𝜑 → ∀𝑤𝑇 𝑤𝑃)
259258ad2antrr 488 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → ∀𝑤𝑇 𝑤𝑃)
26055adantr 276 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → 𝑚 ∈ ℝ)
261 peano2zm 9320 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ℤ → (𝑠 − 1) ∈ ℤ)
26249, 261syl 14 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑠 − 1) ∈ ℤ)
263262zred 9404 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑠 − 1) ∈ ℝ)
264263ad2antrr 488 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (𝑠 − 1) ∈ ℝ)
265231nn0red 9259 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → 𝑗 ∈ ℝ)
26612zcnd 9405 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑚 ∈ ℂ)
26756recnd 8015 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑠 ∈ ℂ)
268 1cnd 8002 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 1 ∈ ℂ)
269266, 267, 268subsubd 8325 . . . . . . . . . . . . . . . . 17 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑚 − (𝑠 − 1)) = ((𝑚𝑠) + 1))
270269adantr 276 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (𝑚 − (𝑠 − 1)) = ((𝑚𝑠) + 1))
271 elfzle1 10056 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (((𝑚𝑠) + 1)...𝑚) → ((𝑚𝑠) + 1) ≤ 𝑗)
272271adantl 277 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → ((𝑚𝑠) + 1) ≤ 𝑗)
273270, 272eqbrtrd 4040 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (𝑚 − (𝑠 − 1)) ≤ 𝑗)
274260, 264, 265, 273subled 8534 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (𝑚𝑗) ≤ (𝑠 − 1))
27594, 19syl 14 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (𝑚𝑗) ∈ ℕ0)
276275, 33eleqtrdi 2282 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (𝑚𝑗) ∈ (ℤ‘0))
277262ad2antrr 488 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (𝑠 − 1) ∈ ℤ)
278 elfz5 10046 . . . . . . . . . . . . . . 15 (((𝑚𝑗) ∈ (ℤ‘0) ∧ (𝑠 − 1) ∈ ℤ) → ((𝑚𝑗) ∈ (0...(𝑠 − 1)) ↔ (𝑚𝑗) ≤ (𝑠 − 1)))
279276, 277, 278syl2anc 411 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → ((𝑚𝑗) ∈ (0...(𝑠 − 1)) ↔ (𝑚𝑗) ≤ (𝑠 − 1)))
280274, 279mpbird 167 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (𝑚𝑗) ∈ (0...(𝑠 − 1)))
281 simplll 533 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → 𝜑)
28294, 22syldan 282 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → ((𝑚𝑗) + 1) ∈ ℕ0)
283282, 25sylan 283 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → 𝑘 ∈ ℕ0)
284281, 283, 27syl2anc 411 . . . . . . . . . . . . . . . 16 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → (𝐺𝑘) = 𝐵)
285284sumeq2dv 11407 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))(𝐺𝑘) = Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)
286285eqcomd 2195 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵 = Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))(𝐺𝑘))
287286fveq2d 5538 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))(𝐺𝑘)))
288135rspceeqv 2874 . . . . . . . . . . . . 13 (((𝑚𝑗) ∈ (0...(𝑠 − 1)) ∧ (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))(𝐺𝑘))) → ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)))
289280, 287, 288syl2anc 411 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)))
29094, 39syldan 282 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵 ∈ ℂ)
291290abscld 11221 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ∈ ℝ)
292 eqeq1 2196 . . . . . . . . . . . . . . 15 (𝑧 = (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) → (𝑧 = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) ↔ (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘))))
293292rexbidv 2491 . . . . . . . . . . . . . 14 (𝑧 = (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) → (∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) ↔ ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘))))
294 mertens.10 . . . . . . . . . . . . . 14 𝑇 = {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘))}
295293, 294elab2g 2899 . . . . . . . . . . . . 13 ((abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ∈ ℝ → ((abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ∈ 𝑇 ↔ ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘))))
296291, 295syl 14 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → ((abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ∈ 𝑇 ↔ ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘))))
297289, 296mpbird 167 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ∈ 𝑇)
298257, 259, 297rspcdva 2861 . . . . . . . . . 10 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ≤ 𝑃)
299230, 231, 129syl2anc 411 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → ((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)))
30094, 81syldan 282 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ∈ ℝ)
30139absge0d 11224 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → 0 ≤ (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵))
30294, 301syldan 282 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → 0 ≤ (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵))
303300, 302jca 306 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → ((abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ∈ ℝ ∧ 0 ≤ (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)))
304218ad2antrr 488 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → 𝑃 ∈ ℝ)
305 lemul12a 8848 . . . . . . . . . . 11 (((((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)) ∧ (((𝐸 / 2) / 𝑠) / (𝑃 + 1)) ∈ ℝ) ∧ (((abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ∈ ℝ ∧ 0 ≤ (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ∧ 𝑃 ∈ ℝ)) → (((abs‘𝐴) ≤ (((𝐸 / 2) / 𝑠) / (𝑃 + 1)) ∧ (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ≤ 𝑃) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ≤ ((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃)))
306299, 233, 303, 304, 305syl22anc 1250 . . . . . . . . . 10 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (((abs‘𝐴) ≤ (((𝐸 / 2) / 𝑠) / (𝑃 + 1)) ∧ (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ≤ 𝑃) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ≤ ((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃)))
307256, 298, 306mp2and 433 . . . . . . . . 9 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ≤ ((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃))
30886, 95, 229, 307fsumle 11502 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ≤ Σ𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃))
309228recnd 8015 . . . . . . . . . . 11 (𝜑 → ((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃) ∈ ℂ)
310309adantr 276 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃) ∈ ℂ)
311 fsumconst 11493 . . . . . . . . . 10 (((((𝑚𝑠) + 1)...𝑚) ∈ Fin ∧ ((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃) ∈ ℂ) → Σ𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃) = ((♯‘(((𝑚𝑠) + 1)...𝑚)) · ((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃)))
31286, 310, 311syl2anc 411 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃) = ((♯‘(((𝑚𝑠) + 1)...𝑚)) · ((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃)))
313 1zzd 9309 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 1 ∈ ℤ)
314 fzen 10072 . . . . . . . . . . . . . 14 ((1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ (𝑚𝑠) ∈ ℤ) → (1...𝑠) ≈ ((1 + (𝑚𝑠))...(𝑠 + (𝑚𝑠))))
315313, 50, 72, 314syl3anc 1249 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (1...𝑠) ≈ ((1 + (𝑚𝑠))...(𝑠 + (𝑚𝑠))))
316 ax-1cn 7933 . . . . . . . . . . . . . . 15 1 ∈ ℂ
31772zcnd 9405 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑚𝑠) ∈ ℂ)
318 addcom 8123 . . . . . . . . . . . . . . 15 ((1 ∈ ℂ ∧ (𝑚𝑠) ∈ ℂ) → (1 + (𝑚𝑠)) = ((𝑚𝑠) + 1))
319316, 317, 318sylancr 414 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (1 + (𝑚𝑠)) = ((𝑚𝑠) + 1))
320267, 266pncan3d 8300 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑠 + (𝑚𝑠)) = 𝑚)
321319, 320oveq12d 5913 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((1 + (𝑚𝑠))...(𝑠 + (𝑚𝑠))) = (((𝑚𝑠) + 1)...𝑚))
322315, 321breqtrd 4044 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (1...𝑠) ≈ (((𝑚𝑠) + 1)...𝑚))
323313, 50fzfigd 10461 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (1...𝑠) ∈ Fin)
324 hashen 10795 . . . . . . . . . . . . 13 (((1...𝑠) ∈ Fin ∧ (((𝑚𝑠) + 1)...𝑚) ∈ Fin) → ((♯‘(1...𝑠)) = (♯‘(((𝑚𝑠) + 1)...𝑚)) ↔ (1...𝑠) ≈ (((𝑚𝑠) + 1)...𝑚)))
325323, 86, 324syl2anc 411 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((♯‘(1...𝑠)) = (♯‘(((𝑚𝑠) + 1)...𝑚)) ↔ (1...𝑠) ≈ (((𝑚𝑠) + 1)...𝑚)))
326322, 325mpbird 167 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (♯‘(1...𝑠)) = (♯‘(((𝑚𝑠) + 1)...𝑚)))
327 hashfz1 10794 . . . . . . . . . . . 12 (𝑠 ∈ ℕ0 → (♯‘(1...𝑠)) = 𝑠)
32853, 327syl 14 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (♯‘(1...𝑠)) = 𝑠)
329326, 328eqtr3d 2224 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (♯‘(((𝑚𝑠) + 1)...𝑚)) = 𝑠)
330329oveq1d 5910 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((♯‘(((𝑚𝑠) + 1)...𝑚)) · ((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃)) = (𝑠 · ((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃)))
331218recnd 8015 . . . . . . . . . . . 12 (𝜑𝑃 ∈ ℂ)
332221rpcnd 9727 . . . . . . . . . . . 12 (𝜑 → (𝑃 + 1) ∈ ℂ)
333221rpap0d 9731 . . . . . . . . . . . 12 (𝜑 → (𝑃 + 1) # 0)
334160, 331, 332, 333div23apd 8814 . . . . . . . . . . 11 (𝜑 → (((𝐸 / 2) · 𝑃) / (𝑃 + 1)) = (((𝐸 / 2) / (𝑃 + 1)) · 𝑃))
33549zcnd 9405 . . . . . . . . . . . . . 14 (𝜑𝑠 ∈ ℂ)
336225rpcnd 9727 . . . . . . . . . . . . . 14 (𝜑 → ((𝐸 / 2) / 𝑠) ∈ ℂ)
337335, 336, 332, 333divassapd 8812 . . . . . . . . . . . . 13 (𝜑 → ((𝑠 · ((𝐸 / 2) / 𝑠)) / (𝑃 + 1)) = (𝑠 · (((𝐸 / 2) / 𝑠) / (𝑃 + 1))))
3385nnap0d 8994 . . . . . . . . . . . . . . 15 (𝜑𝑠 # 0)
339160, 335, 338divcanap2d 8778 . . . . . . . . . . . . . 14 (𝜑 → (𝑠 · ((𝐸 / 2) / 𝑠)) = (𝐸 / 2))
340339oveq1d 5910 . . . . . . . . . . . . 13 (𝜑 → ((𝑠 · ((𝐸 / 2) / 𝑠)) / (𝑃 + 1)) = ((𝐸 / 2) / (𝑃 + 1)))
341337, 340eqtr3d 2224 . . . . . . . . . . . 12 (𝜑 → (𝑠 · (((𝐸 / 2) / 𝑠) / (𝑃 + 1))) = ((𝐸 / 2) / (𝑃 + 1)))
342341oveq1d 5910 . . . . . . . . . . 11 (𝜑 → ((𝑠 · (((𝐸 / 2) / 𝑠) / (𝑃 + 1))) · 𝑃) = (((𝐸 / 2) / (𝑃 + 1)) · 𝑃))
343226rpcnd 9727 . . . . . . . . . . . 12 (𝜑 → (((𝐸 / 2) / 𝑠) / (𝑃 + 1)) ∈ ℂ)
344335, 343, 331mulassd 8010 . . . . . . . . . . 11 (𝜑 → ((𝑠 · (((𝐸 / 2) / 𝑠) / (𝑃 + 1))) · 𝑃) = (𝑠 · ((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃)))
345334, 342, 3443eqtr2rd 2229 . . . . . . . . . 10 (𝜑 → (𝑠 · ((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃)) = (((𝐸 / 2) · 𝑃) / (𝑃 + 1)))
346345adantr 276 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑠 · ((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃)) = (((𝐸 / 2) · 𝑃) / (𝑃 + 1)))
347312, 330, 3463eqtrd 2226 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃) = (((𝐸 / 2) · 𝑃) / (𝑃 + 1)))
348308, 347breqtrd 4044 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ≤ (((𝐸 / 2) · 𝑃) / (𝑃 + 1)))
349 peano2re 8122 . . . . . . . . . . 11 (𝑃 ∈ ℝ → (𝑃 + 1) ∈ ℝ)
350218, 349syl 14 . . . . . . . . . 10 (𝜑 → (𝑃 + 1) ∈ ℝ)
351218ltp1d 8916 . . . . . . . . . 10 (𝜑𝑃 < (𝑃 + 1))
352218, 350, 97, 351ltmul2dd 9782 . . . . . . . . 9 (𝜑 → ((𝐸 / 2) · 𝑃) < ((𝐸 / 2) · (𝑃 + 1)))
353219, 98, 221ltdivmul2d 9778 . . . . . . . . 9 (𝜑 → ((((𝐸 / 2) · 𝑃) / (𝑃 + 1)) < (𝐸 / 2) ↔ ((𝐸 / 2) · 𝑃) < ((𝐸 / 2) · (𝑃 + 1))))
354352, 353mpbird 167 . . . . . . . 8 (𝜑 → (((𝐸 / 2) · 𝑃) / (𝑃 + 1)) < (𝐸 / 2))
355354adantr 276 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (((𝐸 / 2) · 𝑃) / (𝑃 + 1)) < (𝐸 / 2))
35696, 223, 99, 348, 355lelttrd 8111 . . . . . 6 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < (𝐸 / 2))
35784, 96, 99, 99, 217, 356lt2addd 8553 . . . . 5 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) + Σ𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵))) < ((𝐸 / 2) + (𝐸 / 2)))
35817, 39absmuld 11234 . . . . . . 7 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) = ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)))
359358sumeq2dv 11407 . . . . . 6 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) = Σ𝑗 ∈ (0...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)))
36072zred 9404 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑚𝑠) ∈ ℝ)
361360ltp1d 8916 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑚𝑠) < ((𝑚𝑠) + 1))
362 fzdisj 10081 . . . . . . . 8 ((𝑚𝑠) < ((𝑚𝑠) + 1) → ((0...(𝑚𝑠)) ∩ (((𝑚𝑠) + 1)...𝑚)) = ∅)
363361, 362syl 14 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((0...(𝑚𝑠)) ∩ (((𝑚𝑠) + 1)...𝑚)) = ∅)
364 fzsplit 10080 . . . . . . . 8 ((𝑚𝑠) ∈ (0...𝑚) → (0...𝑚) = ((0...(𝑚𝑠)) ∪ (((𝑚𝑠) + 1)...𝑚)))
36570, 364syl 14 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (0...𝑚) = ((0...(𝑚𝑠)) ∪ (((𝑚𝑠) + 1)...𝑚)))
36682recnd 8015 . . . . . . 7 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ∈ ℂ)
367363, 365, 13, 366fsumsplit 11446 . . . . . 6 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) = (Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) + Σ𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵))))
368359, 367eqtr2d 2223 . . . . 5 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) + Σ𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵))) = Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)))
36945rpcnd 9727 . . . . . . 7 (𝜑𝐸 ∈ ℂ)
370369adantr 276 . . . . . 6 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝐸 ∈ ℂ)
3713702halvesd 9193 . . . . 5 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((𝐸 / 2) + (𝐸 / 2)) = 𝐸)
372357, 368, 3713brtr3d 4049 . . . 4 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸)
37342, 44, 47, 48, 372lelttrd 8111 . . 3 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸)
374373ralrimiva 2563 . 2 (𝜑 → ∀𝑚 ∈ (ℤ‘(𝑠 + 𝑡))(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸)
375 fveq2 5534 . . . 4 (𝑦 = (𝑠 + 𝑡) → (ℤ𝑦) = (ℤ‘(𝑠 + 𝑡)))
376375raleqdv 2692 . . 3 (𝑦 = (𝑠 + 𝑡) → (∀𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸 ↔ ∀𝑚 ∈ (ℤ‘(𝑠 + 𝑡))(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸))
377376rspcev 2856 . 2 (((𝑠 + 𝑡) ∈ ℕ0 ∧ ∀𝑚 ∈ (ℤ‘(𝑠 + 𝑡))(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸) → ∃𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸)
3789, 374, 377syl2anc 411 1 (𝜑 → ∃𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105  DECID wdc 835   = wceq 1364  wcel 2160  {cab 2175  wral 2468  wrex 2469  cun 3142  cin 3143  wss 3144  c0 3437   class class class wbr 4018  dom cdm 4644  cfv 5235  (class class class)co 5895  cen 6763  Fincfn 6765  cc 7838  cr 7839  0cc0 7840  1c1 7841   + caddc 7843   · cmul 7845   < clt 8021  cle 8022  cmin 8157   / cdiv 8658  cn 8948  2c2 8999  0cn0 9205  cz 9282  cuz 9557  +crp 9682  ...cfz 10037  seqcseq 10475  chash 10786  abscabs 11037  cli 11317  Σcsu 11392
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-coll 4133  ax-sep 4136  ax-nul 4144  ax-pow 4192  ax-pr 4227  ax-un 4451  ax-setind 4554  ax-iinf 4605  ax-cnex 7931  ax-resscn 7932  ax-1cn 7933  ax-1re 7934  ax-icn 7935  ax-addcl 7936  ax-addrcl 7937  ax-mulcl 7938  ax-mulrcl 7939  ax-addcom 7940  ax-mulcom 7941  ax-addass 7942  ax-mulass 7943  ax-distr 7944  ax-i2m1 7945  ax-0lt1 7946  ax-1rid 7947  ax-0id 7948  ax-rnegex 7949  ax-precex 7950  ax-cnre 7951  ax-pre-ltirr 7952  ax-pre-ltwlin 7953  ax-pre-lttrn 7954  ax-pre-apti 7955  ax-pre-ltadd 7956  ax-pre-mulgt0 7957  ax-pre-mulext 7958  ax-arch 7959  ax-caucvg 7960
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-nel 2456  df-ral 2473  df-rex 2474  df-reu 2475  df-rmo 2476  df-rab 2477  df-v 2754  df-sbc 2978  df-csb 3073  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-nul 3438  df-if 3550  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-int 3860  df-iun 3903  df-br 4019  df-opab 4080  df-mpt 4081  df-tr 4117  df-id 4311  df-po 4314  df-iso 4315  df-iord 4384  df-on 4386  df-ilim 4387  df-suc 4389  df-iom 4608  df-xp 4650  df-rel 4651  df-cnv 4652  df-co 4653  df-dm 4654  df-rn 4655  df-res 4656  df-ima 4657  df-iota 5196  df-fun 5237  df-fn 5238  df-f 5239  df-f1 5240  df-fo 5241  df-f1o 5242  df-fv 5243  df-isom 5244  df-riota 5851  df-ov 5898  df-oprab 5899  df-mpo 5900  df-1st 6164  df-2nd 6165  df-recs 6329  df-irdg 6394  df-frec 6415  df-1o 6440  df-oadd 6444  df-er 6558  df-en 6766  df-dom 6767  df-fin 6768  df-sup 7012  df-pnf 8023  df-mnf 8024  df-xr 8025  df-ltxr 8026  df-le 8027  df-sub 8159  df-neg 8160  df-reap 8561  df-ap 8568  df-div 8659  df-inn 8949  df-2 9007  df-3 9008  df-4 9009  df-n0 9206  df-z 9283  df-uz 9558  df-q 9649  df-rp 9683  df-ico 9923  df-fz 10038  df-fzo 10172  df-seqfrec 10476  df-exp 10550  df-ihash 10787  df-cj 10882  df-re 10883  df-im 10884  df-rsqrt 11038  df-abs 11039  df-clim 11318  df-sumdc 11393
This theorem is referenced by:  mertenslem2  11575
  Copyright terms: Public domain W3C validator