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

Theorem mertenslemi1 11311
 Description: Lemma for mertensabs 11313. (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 111 . . . . . 6 (𝜑𝜓)
3 mertens.11 . . . . . 6 (𝜓 ↔ (𝑠 ∈ ℕ ∧ ∀𝑛 ∈ (ℤ𝑠)(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
42, 3sylib 121 . . . . 5 (𝜑 → (𝑠 ∈ ℕ ∧ ∀𝑛 ∈ (ℤ𝑠)(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
54simpld 111 . . . 4 (𝜑𝑠 ∈ ℕ)
65nnnn0d 9037 . . 3 (𝜑𝑠 ∈ ℕ0)
71simprd 113 . . . 4 (𝜑 → (𝑡 ∈ ℕ0 ∧ ∀𝑚 ∈ (ℤ𝑡)(𝐾𝑚) < (((𝐸 / 2) / 𝑠) / (𝑃 + 1))))
87simpld 111 . . 3 (𝜑𝑡 ∈ ℕ0)
96, 8nn0addcld 9041 . 2 (𝜑 → (𝑠 + 𝑡) ∈ ℕ0)
10 0zd 9073 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 0 ∈ ℤ)
11 eluzelz 9342 . . . . . . . 8 (𝑚 ∈ (ℤ‘(𝑠 + 𝑡)) → 𝑚 ∈ ℤ)
1211adantl 275 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑚 ∈ ℤ)
1310, 12fzfigd 10211 . . . . . 6 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (0...𝑚) ∈ Fin)
14 simpl 108 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝜑)
15 elfznn0 9901 . . . . . . . 8 (𝑗 ∈ (0...𝑚) → 𝑗 ∈ ℕ0)
16 mertens.3 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → 𝐴 ∈ ℂ)
1714, 15, 16syl2an 287 . . . . . . 7 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → 𝐴 ∈ ℂ)
18 eqid 2139 . . . . . . . 8 (ℤ‘((𝑚𝑗) + 1)) = (ℤ‘((𝑚𝑗) + 1))
19 fznn0sub 9844 . . . . . . . . . . 11 (𝑗 ∈ (0...𝑚) → (𝑚𝑗) ∈ ℕ0)
2019adantl 275 . . . . . . . . . 10 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (𝑚𝑗) ∈ ℕ0)
21 peano2nn0 9024 . . . . . . . . . 10 ((𝑚𝑗) ∈ ℕ0 → ((𝑚𝑗) + 1) ∈ ℕ0)
2220, 21syl 14 . . . . . . . . 9 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((𝑚𝑗) + 1) ∈ ℕ0)
2322nn0zd 9178 . . . . . . . 8 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((𝑚𝑗) + 1) ∈ ℤ)
24 simplll 522 . . . . . . . . 9 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → 𝜑)
25 eluznn0 9400 . . . . . . . . . 10 ((((𝑚𝑗) + 1) ∈ ℕ0𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → 𝑘 ∈ ℕ0)
2622, 25sylan 281 . . . . . . . . 9 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → 𝑘 ∈ ℕ0)
27 mertens.4 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (𝐺𝑘) = 𝐵)
2824, 26, 27syl2anc 408 . . . . . . . 8 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → (𝐺𝑘) = 𝐵)
29 mertens.5 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)
3024, 26, 29syl2anc 408 . . . . . . . 8 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → 𝐵 ∈ ℂ)
31 mertens.8 . . . . . . . . . 10 (𝜑 → seq0( + , 𝐺) ∈ dom ⇝ )
3231ad2antrr 479 . . . . . . . . 9 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → seq0( + , 𝐺) ∈ dom ⇝ )
33 nn0uz 9367 . . . . . . . . . 10 0 = (ℤ‘0)
34 simpll 518 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → 𝜑)
3527, 29eqeltrd 2216 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → (𝐺𝑘) ∈ ℂ)
3634, 35sylan 281 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) ∈ ℂ)
3733, 22, 36iserex 11115 . . . . . . . . 9 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (seq0( + , 𝐺) ∈ dom ⇝ ↔ seq((𝑚𝑗) + 1)( + , 𝐺) ∈ dom ⇝ ))
3832, 37mpbid 146 . . . . . . . 8 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → seq((𝑚𝑗) + 1)( + , 𝐺) ∈ dom ⇝ )
3918, 23, 28, 30, 38isumcl 11201 . . . . . . 7 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵 ∈ ℂ)
4017, 39mulcld 7793 . . . . . 6 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ∈ ℂ)
4113, 40fsumcl 11176 . . . . 5 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ∈ ℂ)
4241abscld 10960 . . . 4 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ∈ ℝ)
4340abscld 10960 . . . . 5 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ∈ ℝ)
4413, 43fsumrecl 11177 . . . 4 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ∈ ℝ)
45 mertens.9 . . . . . 6 (𝜑𝐸 ∈ ℝ+)
4645rpred 9490 . . . . 5 (𝜑𝐸 ∈ ℝ)
4746adantr 274 . . . 4 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝐸 ∈ ℝ)
4813, 40fsumabs 11241 . . . 4 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ≤ Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)))
495nnzd 9179 . . . . . . . . . 10 (𝜑𝑠 ∈ ℤ)
5049adantr 274 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑠 ∈ ℤ)
5112, 50zsubcld 9185 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑚𝑠) ∈ ℤ)
5210, 51fzfigd 10211 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (0...(𝑚𝑠)) ∈ Fin)
536adantr 274 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑠 ∈ ℕ0)
5453nn0ge0d 9040 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 0 ≤ 𝑠)
5512zred 9180 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑚 ∈ ℝ)
5653nn0red 9038 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑠 ∈ ℝ)
5755, 56subge02d 8306 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (0 ≤ 𝑠 ↔ (𝑚𝑠) ≤ 𝑚))
5854, 57mpbid 146 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑚𝑠) ≤ 𝑚)
5953, 33eleqtrdi 2232 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑠 ∈ (ℤ‘0))
60 uzid 9347 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ℤ → 𝑠 ∈ (ℤ𝑠))
6149, 60syl 14 . . . . . . . . . . . . . . . . 17 (𝜑𝑠 ∈ (ℤ𝑠))
62 uzaddcl 9388 . . . . . . . . . . . . . . . . 17 ((𝑠 ∈ (ℤ𝑠) ∧ 𝑡 ∈ ℕ0) → (𝑠 + 𝑡) ∈ (ℤ𝑠))
6361, 8, 62syl2anc 408 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑠 + 𝑡) ∈ (ℤ𝑠))
64 eqid 2139 . . . . . . . . . . . . . . . . 17 (ℤ𝑠) = (ℤ𝑠)
6564uztrn2 9350 . . . . . . . . . . . . . . . 16 (((𝑠 + 𝑡) ∈ (ℤ𝑠) ∧ 𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑚 ∈ (ℤ𝑠))
6663, 65sylan 281 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑚 ∈ (ℤ𝑠))
67 elfzuzb 9807 . . . . . . . . . . . . . . 15 (𝑠 ∈ (0...𝑚) ↔ (𝑠 ∈ (ℤ‘0) ∧ 𝑚 ∈ (ℤ𝑠)))
6859, 66, 67sylanbrc 413 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑠 ∈ (0...𝑚))
69 fznn0sub2 9912 . . . . . . . . . . . . . 14 (𝑠 ∈ (0...𝑚) → (𝑚𝑠) ∈ (0...𝑚))
7068, 69syl 14 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑚𝑠) ∈ (0...𝑚))
71 elfzelz 9813 . . . . . . . . . . . . 13 ((𝑚𝑠) ∈ (0...𝑚) → (𝑚𝑠) ∈ ℤ)
7270, 71syl 14 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑚𝑠) ∈ ℤ)
73 eluz 9346 . . . . . . . . . . . 12 (((𝑚𝑠) ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑚 ∈ (ℤ‘(𝑚𝑠)) ↔ (𝑚𝑠) ≤ 𝑚))
7472, 12, 73syl2anc 408 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑚 ∈ (ℤ‘(𝑚𝑠)) ↔ (𝑚𝑠) ≤ 𝑚))
7558, 74mpbird 166 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑚 ∈ (ℤ‘(𝑚𝑠)))
76 fzss2 9851 . . . . . . . . . 10 (𝑚 ∈ (ℤ‘(𝑚𝑠)) → (0...(𝑚𝑠)) ⊆ (0...𝑚))
7775, 76syl 14 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (0...(𝑚𝑠)) ⊆ (0...𝑚))
7877sselda 3097 . . . . . . . 8 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → 𝑗 ∈ (0...𝑚))
7916abscld 10960 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → (abs‘𝐴) ∈ ℝ)
8014, 15, 79syl2an 287 . . . . . . . . 9 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘𝐴) ∈ ℝ)
8139abscld 10960 . . . . . . . . 9 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ∈ ℝ)
8280, 81remulcld 7803 . . . . . . . 8 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ∈ ℝ)
8378, 82syldan 280 . . . . . . 7 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ∈ ℝ)
8452, 83fsumrecl 11177 . . . . . 6 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ∈ ℝ)
8551peano2zd 9183 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((𝑚𝑠) + 1) ∈ ℤ)
8685, 12fzfigd 10211 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (((𝑚𝑠) + 1)...𝑚) ∈ Fin)
87 elfznn0 9901 . . . . . . . . . . . . 13 ((𝑚𝑠) ∈ (0...𝑚) → (𝑚𝑠) ∈ ℕ0)
8870, 87syl 14 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑚𝑠) ∈ ℕ0)
89 peano2nn0 9024 . . . . . . . . . . . 12 ((𝑚𝑠) ∈ ℕ0 → ((𝑚𝑠) + 1) ∈ ℕ0)
9088, 89syl 14 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((𝑚𝑠) + 1) ∈ ℕ0)
9190, 33eleqtrdi 2232 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((𝑚𝑠) + 1) ∈ (ℤ‘0))
92 fzss1 9850 . . . . . . . . . 10 (((𝑚𝑠) + 1) ∈ (ℤ‘0) → (((𝑚𝑠) + 1)...𝑚) ⊆ (0...𝑚))
9391, 92syl 14 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (((𝑚𝑠) + 1)...𝑚) ⊆ (0...𝑚))
9493sselda 3097 . . . . . . . 8 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → 𝑗 ∈ (0...𝑚))
9594, 82syldan 280 . . . . . . 7 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ∈ ℝ)
9686, 95fsumrecl 11177 . . . . . 6 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ∈ ℝ)
9745rphalfcld 9503 . . . . . . . 8 (𝜑 → (𝐸 / 2) ∈ ℝ+)
9897rpred 9490 . . . . . . 7 (𝜑 → (𝐸 / 2) ∈ ℝ)
9998adantr 274 . . . . . 6 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝐸 / 2) ∈ ℝ)
100 elfznn0 9901 . . . . . . . . . . 11 (𝑗 ∈ (0...(𝑚𝑠)) → 𝑗 ∈ ℕ0)
10114, 100, 79syl2an 287 . . . . . . . . . 10 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → (abs‘𝐴) ∈ ℝ)
10252, 101fsumrecl 11177 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) ∈ ℝ)
103102, 99remulcld 7803 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) ∈ ℝ)
104 0zd 9073 . . . . . . . . . . 11 (𝜑 → 0 ∈ ℤ)
105 eqidd 2140 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → (𝐾𝑗) = (𝐾𝑗))
106 mertens.2 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → (𝐾𝑗) = (abs‘𝐴))
107106, 79eqeltrd 2216 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → (𝐾𝑗) ∈ ℝ)
108 mertens.7 . . . . . . . . . . 11 (𝜑 → seq0( + , 𝐾) ∈ dom ⇝ )
10933, 104, 105, 107, 108isumrecl 11205 . . . . . . . . . 10 (𝜑 → Σ𝑗 ∈ ℕ0 (𝐾𝑗) ∈ ℝ)
11016absge0d 10963 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → 0 ≤ (abs‘𝐴))
111110, 106breqtrrd 3956 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → 0 ≤ (𝐾𝑗))
11233, 104, 105, 107, 108, 111isumge0 11206 . . . . . . . . . 10 (𝜑 → 0 ≤ Σ𝑗 ∈ ℕ0 (𝐾𝑗))
113109, 112ge0p1rpd 9521 . . . . . . . . 9 (𝜑 → (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ∈ ℝ+)
114113adantr 274 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ∈ ℝ+)
115103, 114rerpdivcld 9522 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) ∈ ℝ)
11697, 113rpdivcld 9508 . . . . . . . . . . . 12 (𝜑 → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) ∈ ℝ+)
117116rpred 9490 . . . . . . . . . . 11 (𝜑 → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) ∈ ℝ)
118117ad2antrr 479 . . . . . . . . . 10 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) ∈ ℝ)
119101, 118remulcld 7803 . . . . . . . . 9 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))) ∈ ℝ)
12078, 23syldan 280 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → ((𝑚𝑗) + 1) ∈ ℤ)
121 simplll 522 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → 𝜑)
12278, 22syldan 280 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → ((𝑚𝑗) + 1) ∈ ℕ0)
123122, 25sylan 281 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → 𝑘 ∈ ℕ0)
124121, 123, 27syl2anc 408 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → (𝐺𝑘) = 𝐵)
125121, 123, 29syl2anc 408 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → 𝐵 ∈ ℂ)
12678, 38syldan 280 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → seq((𝑚𝑗) + 1)( + , 𝐺) ∈ dom ⇝ )
12718, 120, 124, 125, 126isumcl 11201 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵 ∈ ℂ)
128127abscld 10960 . . . . . . . . . 10 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ∈ ℝ)
12979, 110jca 304 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → ((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)))
13014, 100, 129syl2an 287 . . . . . . . . . 10 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → ((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)))
131124sumeq2dv 11144 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))(𝐺𝑘) = Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)
132131fveq2d 5425 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))(𝐺𝑘)) = (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵))
133 fvoveq1 5797 . . . . . . . . . . . . . . . 16 (𝑛 = (𝑚𝑗) → (ℤ‘(𝑛 + 1)) = (ℤ‘((𝑚𝑗) + 1)))
134133sumeq1d 11142 . . . . . . . . . . . . . . 15 (𝑛 = (𝑚𝑗) → Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘) = Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))(𝐺𝑘))
135134fveq2d 5425 . . . . . . . . . . . . . 14 (𝑛 = (𝑚𝑗) → (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) = (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))(𝐺𝑘)))
136135breq1d 3939 . . . . . . . . . . . . 13 (𝑛 = (𝑚𝑗) → ((abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) ↔ (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
1374simprd 113 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑛 ∈ (ℤ𝑠)(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
138137ad2antrr 479 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → ∀𝑛 ∈ (ℤ𝑠)(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
139 elfzelz 9813 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...(𝑚𝑠)) → 𝑗 ∈ ℤ)
140139adantl 275 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → 𝑗 ∈ ℤ)
141140zred 9180 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → 𝑗 ∈ ℝ)
14211ad2antlr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → 𝑚 ∈ ℤ)
143142zred 9180 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → 𝑚 ∈ ℝ)
14449ad2antrr 479 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → 𝑠 ∈ ℤ)
145144zred 9180 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → 𝑠 ∈ ℝ)
146 elfzle2 9815 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...(𝑚𝑠)) → 𝑗 ≤ (𝑚𝑠))
147146adantl 275 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → 𝑗 ≤ (𝑚𝑠))
148141, 143, 145, 147lesubd 8318 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → 𝑠 ≤ (𝑚𝑗))
149142, 140zsubcld 9185 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → (𝑚𝑗) ∈ ℤ)
150 eluz 9346 . . . . . . . . . . . . . . 15 ((𝑠 ∈ ℤ ∧ (𝑚𝑗) ∈ ℤ) → ((𝑚𝑗) ∈ (ℤ𝑠) ↔ 𝑠 ≤ (𝑚𝑗)))
151144, 149, 150syl2anc 408 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → ((𝑚𝑗) ∈ (ℤ𝑠) ↔ 𝑠 ≤ (𝑚𝑗)))
152148, 151mpbird 166 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → (𝑚𝑗) ∈ (ℤ𝑠))
153136, 138, 152rspcdva 2794 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
154132, 153eqbrtrrd 3952 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
155128, 118, 154ltled 7888 . . . . . . . . . 10 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ≤ ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
156 lemul2a 8624 . . . . . . . . . 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 1219 . . . . . . . . 9 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ≤ ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
15852, 83, 119, 157fsumle 11239 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ≤ Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
159102recnd 7801 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) ∈ ℂ)
16097rpcnd 9492 . . . . . . . . . . 11 (𝜑 → (𝐸 / 2) ∈ ℂ)
161160adantr 274 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝐸 / 2) ∈ ℂ)
162 peano2re 7905 . . . . . . . . . . . . 13 𝑗 ∈ ℕ0 (𝐾𝑗) ∈ ℝ → (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ∈ ℝ)
163109, 162syl 14 . . . . . . . . . . . 12 (𝜑 → (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ∈ ℝ)
164163recnd 7801 . . . . . . . . . . 11 (𝜑 → (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ∈ ℂ)
165164adantr 274 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ∈ ℂ)
166114rpap0d 9496 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) # 0)
167159, 161, 165, 166divassapd 8593 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) = (Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
168 fveq2 5421 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑗 → (𝐾𝑛) = (𝐾𝑗))
169168cbvsumv 11137 . . . . . . . . . . . . . . . 16 Σ𝑛 ∈ ℕ0 (𝐾𝑛) = Σ𝑗 ∈ ℕ0 (𝐾𝑗)
170169oveq1i 5784 . . . . . . . . . . . . . . 15 𝑛 ∈ ℕ0 (𝐾𝑛) + 1) = (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)
171170oveq2i 5785 . . . . . . . . . . . . . 14 ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾𝑛) + 1)) = ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))
172171, 116eqeltrid 2226 . . . . . . . . . . . . 13 (𝜑 → ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾𝑛) + 1)) ∈ ℝ+)
173172rpcnd 9492 . . . . . . . . . . . 12 (𝜑 → ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾𝑛) + 1)) ∈ ℂ)
174173adantr 274 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾𝑛) + 1)) ∈ ℂ)
17579recnd 7801 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → (abs‘𝐴) ∈ ℂ)
17614, 100, 175syl2an 287 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚𝑠))) → (abs‘𝐴) ∈ ℂ)
17752, 174, 176fsummulc1 11225 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾𝑛) + 1))) = Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾𝑛) + 1))))
178171oveq2i 5785 . . . . . . . . . 10 𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾𝑛) + 1))) = (Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
179171oveq2i 5785 . . . . . . . . . . . 12 ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾𝑛) + 1))) = ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
180179a1i 9 . . . . . . . . . . 11 (𝑗 ∈ (0...(𝑚𝑠)) → ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾𝑛) + 1))) = ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
181180sumeq2i 11140 . . . . . . . . . 10 Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾𝑛) + 1))) = Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
182177, 178, 1813eqtr3g 2195 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))) = Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
183167, 182eqtrd 2172 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) = Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
184158, 183breqtrrd 3956 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ≤ ((Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
185109adantr 274 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ ℕ0 (𝐾𝑗) ∈ ℝ)
186163adantr 274 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ∈ ℝ)
187 fz0ssnn0 9903 . . . . . . . . . . . . 13 (0...(𝑚𝑠)) ⊆ ℕ0
188187a1i 9 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (0...(𝑚𝑠)) ⊆ ℕ0)
189106adantlr 468 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ0) → (𝐾𝑗) = (abs‘𝐴))
190 nn0z 9081 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ0𝑗 ∈ ℤ)
191190adantl 275 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ0) → 𝑗 ∈ ℤ)
192 0zd 9073 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ0) → 0 ∈ ℤ)
19351adantr 274 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ0) → (𝑚𝑠) ∈ ℤ)
194 fzdcel 9827 . . . . . . . . . . . . . 14 ((𝑗 ∈ ℤ ∧ 0 ∈ ℤ ∧ (𝑚𝑠) ∈ ℤ) → DECID 𝑗 ∈ (0...(𝑚𝑠)))
195191, 192, 193, 194syl3anc 1216 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ0) → DECID 𝑗 ∈ (0...(𝑚𝑠)))
196195ralrimiva 2505 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ∀𝑗 ∈ ℕ0 DECID 𝑗 ∈ (0...(𝑚𝑠)))
19779adantlr 468 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ0) → (abs‘𝐴) ∈ ℝ)
198110adantlr 468 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ0) → 0 ≤ (abs‘𝐴))
199108adantr 274 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → seq0( + , 𝐾) ∈ dom ⇝ )
20033, 10, 52, 188, 189, 196, 197, 198, 199isumlessdc 11272 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) ≤ Σ𝑗 ∈ ℕ0 (abs‘𝐴))
201106sumeq2dv 11144 . . . . . . . . . . . 12 (𝜑 → Σ𝑗 ∈ ℕ0 (𝐾𝑗) = Σ𝑗 ∈ ℕ0 (abs‘𝐴))
202201adantr 274 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ ℕ0 (𝐾𝑗) = Σ𝑗 ∈ ℕ0 (abs‘𝐴))
203200, 202breqtrrd 3956 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) ≤ Σ𝑗 ∈ ℕ0 (𝐾𝑗))
204109ltp1d 8695 . . . . . . . . . . 11 (𝜑 → Σ𝑗 ∈ ℕ0 (𝐾𝑗) < (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))
205204adantr 274 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ ℕ0 (𝐾𝑗) < (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))
206102, 185, 186, 203, 205lelttrd 7894 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) < (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))
20797rpregt0d 9497 . . . . . . . . . . 11 (𝜑 → ((𝐸 / 2) ∈ ℝ ∧ 0 < (𝐸 / 2)))
208207adantr 274 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((𝐸 / 2) ∈ ℝ ∧ 0 < (𝐸 / 2)))
209 ltmul1 8361 . . . . . . . . . 10 ((Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) ∈ ℝ ∧ (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ∈ ℝ ∧ ((𝐸 / 2) ∈ ℝ ∧ 0 < (𝐸 / 2))) → (Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) < (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ↔ (Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) · (𝐸 / 2))))
210102, 186, 208, 209syl3anc 1216 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) < (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ↔ (Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) · (𝐸 / 2))))
211206, 210mpbid 146 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) · (𝐸 / 2)))
212113rpregt0d 9497 . . . . . . . . . 10 (𝜑 → ((Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ∈ ℝ ∧ 0 < (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
213212adantr 274 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ∈ ℝ ∧ 0 < (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
214 ltdivmul 8641 . . . . . . . . 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 1216 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (((Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) < (𝐸 / 2) ↔ (Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) · (𝐸 / 2))))
216211, 215mpbird 166 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) < (𝐸 / 2))
21784, 115, 99, 184, 216lelttrd 7894 . . . . . 6 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < (𝐸 / 2))
218 mertens.p . . . . . . . . . 10 (𝜑𝑃 ∈ ℝ)
21998, 218remulcld 7803 . . . . . . . . 9 (𝜑 → ((𝐸 / 2) · 𝑃) ∈ ℝ)
220 mertens.pge0 . . . . . . . . . 10 (𝜑 → 0 ≤ 𝑃)
221218, 220ge0p1rpd 9521 . . . . . . . . 9 (𝜑 → (𝑃 + 1) ∈ ℝ+)
222219, 221rerpdivcld 9522 . . . . . . . 8 (𝜑 → (((𝐸 / 2) · 𝑃) / (𝑃 + 1)) ∈ ℝ)
223222adantr 274 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (((𝐸 / 2) · 𝑃) / (𝑃 + 1)) ∈ ℝ)
2245nnrpd 9489 . . . . . . . . . . . . . 14 (𝜑𝑠 ∈ ℝ+)
22597, 224rpdivcld 9508 . . . . . . . . . . . . 13 (𝜑 → ((𝐸 / 2) / 𝑠) ∈ ℝ+)
226225, 221rpdivcld 9508 . . . . . . . . . . . 12 (𝜑 → (((𝐸 / 2) / 𝑠) / (𝑃 + 1)) ∈ ℝ+)
227226rpred 9490 . . . . . . . . . . 11 (𝜑 → (((𝐸 / 2) / 𝑠) / (𝑃 + 1)) ∈ ℝ)
228227, 218remulcld 7803 . . . . . . . . . 10 (𝜑 → ((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃) ∈ ℝ)
229228ad2antrr 479 . . . . . . . . 9 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → ((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃) ∈ ℝ)
230 simpll 518 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → 𝜑)
23194, 15syl 14 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → 𝑗 ∈ ℕ0)
232230, 231, 79syl2anc 408 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (abs‘𝐴) ∈ ℝ)
233227ad2antrr 479 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (((𝐸 / 2) / 𝑠) / (𝑃 + 1)) ∈ ℝ)
234230, 231, 106syl2anc 408 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (𝐾𝑗) = (abs‘𝐴))
235 fveq2 5421 . . . . . . . . . . . . . 14 (𝑚 = 𝑗 → (𝐾𝑚) = (𝐾𝑗))
236235breq1d 3939 . . . . . . . . . . . . 13 (𝑚 = 𝑗 → ((𝐾𝑚) < (((𝐸 / 2) / 𝑠) / (𝑃 + 1)) ↔ (𝐾𝑗) < (((𝐸 / 2) / 𝑠) / (𝑃 + 1))))
2377simprd 113 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑚 ∈ (ℤ𝑡)(𝐾𝑚) < (((𝐸 / 2) / 𝑠) / (𝑃 + 1)))
238237ad2antrr 479 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → ∀𝑚 ∈ (ℤ𝑡)(𝐾𝑚) < (((𝐸 / 2) / 𝑠) / (𝑃 + 1)))
239 elfzuz 9809 . . . . . . . . . . . . . 14 (𝑗 ∈ (((𝑚𝑠) + 1)...𝑚) → 𝑗 ∈ (ℤ‘((𝑚𝑠) + 1)))
240 eluzle 9345 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ (ℤ‘(𝑠 + 𝑡)) → (𝑠 + 𝑡) ≤ 𝑚)
241240adantl 275 . . . . . . . . . . . . . . . . 17 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑠 + 𝑡) ≤ 𝑚)
2428nn0zd 9178 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑡 ∈ ℤ)
243242adantr 274 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑡 ∈ ℤ)
244243zred 9180 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑡 ∈ ℝ)
24556, 244, 55leaddsub2d 8316 . . . . . . . . . . . . . . . . 17 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((𝑠 + 𝑡) ≤ 𝑚𝑡 ≤ (𝑚𝑠)))
246241, 245mpbid 146 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑡 ≤ (𝑚𝑠))
247 eluz 9346 . . . . . . . . . . . . . . . . 17 ((𝑡 ∈ ℤ ∧ (𝑚𝑠) ∈ ℤ) → ((𝑚𝑠) ∈ (ℤ𝑡) ↔ 𝑡 ≤ (𝑚𝑠)))
248243, 72, 247syl2anc 408 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((𝑚𝑠) ∈ (ℤ𝑡) ↔ 𝑡 ≤ (𝑚𝑠)))
249246, 248mpbird 166 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑚𝑠) ∈ (ℤ𝑡))
250 peano2uz 9385 . . . . . . . . . . . . . . 15 ((𝑚𝑠) ∈ (ℤ𝑡) → ((𝑚𝑠) + 1) ∈ (ℤ𝑡))
251249, 250syl 14 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((𝑚𝑠) + 1) ∈ (ℤ𝑡))
252 uztrn 9349 . . . . . . . . . . . . . 14 ((𝑗 ∈ (ℤ‘((𝑚𝑠) + 1)) ∧ ((𝑚𝑠) + 1) ∈ (ℤ𝑡)) → 𝑗 ∈ (ℤ𝑡))
253239, 251, 252syl2anr 288 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → 𝑗 ∈ (ℤ𝑡))
254236, 238, 253rspcdva 2794 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (𝐾𝑗) < (((𝐸 / 2) / 𝑠) / (𝑃 + 1)))
255234, 254eqbrtrrd 3952 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (abs‘𝐴) < (((𝐸 / 2) / 𝑠) / (𝑃 + 1)))
256232, 233, 255ltled 7888 . . . . . . . . . 10 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (abs‘𝐴) ≤ (((𝐸 / 2) / 𝑠) / (𝑃 + 1)))
257 breq1 3932 . . . . . . . . . . 11 (𝑤 = (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) → (𝑤𝑃 ↔ (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ≤ 𝑃))
258 mertens.pub . . . . . . . . . . . 12 (𝜑 → ∀𝑤𝑇 𝑤𝑃)
259258ad2antrr 479 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → ∀𝑤𝑇 𝑤𝑃)
26055adantr 274 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → 𝑚 ∈ ℝ)
261 peano2zm 9099 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ℤ → (𝑠 − 1) ∈ ℤ)
26249, 261syl 14 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑠 − 1) ∈ ℤ)
263262zred 9180 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑠 − 1) ∈ ℝ)
264263ad2antrr 479 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (𝑠 − 1) ∈ ℝ)
265231nn0red 9038 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → 𝑗 ∈ ℝ)
26612zcnd 9181 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑚 ∈ ℂ)
26756recnd 7801 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝑠 ∈ ℂ)
268 1cnd 7789 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 1 ∈ ℂ)
269266, 267, 268subsubd 8108 . . . . . . . . . . . . . . . . 17 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑚 − (𝑠 − 1)) = ((𝑚𝑠) + 1))
270269adantr 274 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (𝑚 − (𝑠 − 1)) = ((𝑚𝑠) + 1))
271 elfzle1 9814 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (((𝑚𝑠) + 1)...𝑚) → ((𝑚𝑠) + 1) ≤ 𝑗)
272271adantl 275 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → ((𝑚𝑠) + 1) ≤ 𝑗)
273270, 272eqbrtrd 3950 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (𝑚 − (𝑠 − 1)) ≤ 𝑗)
274260, 264, 265, 273subled 8317 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (𝑚𝑗) ≤ (𝑠 − 1))
27594, 19syl 14 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (𝑚𝑗) ∈ ℕ0)
276275, 33eleqtrdi 2232 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (𝑚𝑗) ∈ (ℤ‘0))
277262ad2antrr 479 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (𝑠 − 1) ∈ ℤ)
278 elfz5 9805 . . . . . . . . . . . . . . 15 (((𝑚𝑗) ∈ (ℤ‘0) ∧ (𝑠 − 1) ∈ ℤ) → ((𝑚𝑗) ∈ (0...(𝑠 − 1)) ↔ (𝑚𝑗) ≤ (𝑠 − 1)))
279276, 277, 278syl2anc 408 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → ((𝑚𝑗) ∈ (0...(𝑠 − 1)) ↔ (𝑚𝑗) ≤ (𝑠 − 1)))
280274, 279mpbird 166 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (𝑚𝑗) ∈ (0...(𝑠 − 1)))
281 simplll 522 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → 𝜑)
28294, 22syldan 280 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → ((𝑚𝑗) + 1) ∈ ℕ0)
283282, 25sylan 281 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → 𝑘 ∈ ℕ0)
284281, 283, 27syl2anc 408 . . . . . . . . . . . . . . . 16 ((((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → (𝐺𝑘) = 𝐵)
285284sumeq2dv 11144 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))(𝐺𝑘) = Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)
286285eqcomd 2145 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵 = Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))(𝐺𝑘))
287286fveq2d 5425 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))(𝐺𝑘)))
288135rspceeqv 2807 . . . . . . . . . . . . 13 (((𝑚𝑗) ∈ (0...(𝑠 − 1)) ∧ (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))(𝐺𝑘))) → ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)))
289280, 287, 288syl2anc 408 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)))
29094, 39syldan 280 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵 ∈ ℂ)
291290abscld 10960 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ∈ ℝ)
292 eqeq1 2146 . . . . . . . . . . . . . . 15 (𝑧 = (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) → (𝑧 = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) ↔ (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘))))
293292rexbidv 2438 . . . . . . . . . . . . . 14 (𝑧 = (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) → (∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) ↔ ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘))))
294 mertens.10 . . . . . . . . . . . . . 14 𝑇 = {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘))}
295293, 294elab2g 2831 . . . . . . . . . . . . 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 166 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ∈ 𝑇)
298257, 259, 297rspcdva 2794 . . . . . . . . . 10 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ≤ 𝑃)
299230, 231, 129syl2anc 408 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → ((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)))
30094, 81syldan 280 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ∈ ℝ)
30139absge0d 10963 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → 0 ≤ (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵))
30294, 301syldan 280 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → 0 ≤ (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵))
303300, 302jca 304 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → ((abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ∈ ℝ ∧ 0 ≤ (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)))
304218ad2antrr 479 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → 𝑃 ∈ ℝ)
305 lemul12a 8627 . . . . . . . . . . 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 1217 . . . . . . . . . 10 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → (((abs‘𝐴) ≤ (((𝐸 / 2) / 𝑠) / (𝑃 + 1)) ∧ (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) ≤ 𝑃) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ≤ ((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃)))
307256, 298, 306mp2and 429 . . . . . . . . 9 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ≤ ((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃))
30886, 95, 229, 307fsumle 11239 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ≤ Σ𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃))
309228recnd 7801 . . . . . . . . . . 11 (𝜑 → ((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃) ∈ ℂ)
310309adantr 274 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃) ∈ ℂ)
311 fsumconst 11230 . . . . . . . . . 10 (((((𝑚𝑠) + 1)...𝑚) ∈ Fin ∧ ((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃) ∈ ℂ) → Σ𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃) = ((♯‘(((𝑚𝑠) + 1)...𝑚)) · ((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃)))
31286, 310, 311syl2anc 408 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃) = ((♯‘(((𝑚𝑠) + 1)...𝑚)) · ((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃)))
313 1zzd 9088 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 1 ∈ ℤ)
314 fzen 9830 . . . . . . . . . . . . . 14 ((1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ (𝑚𝑠) ∈ ℤ) → (1...𝑠) ≈ ((1 + (𝑚𝑠))...(𝑠 + (𝑚𝑠))))
315313, 50, 72, 314syl3anc 1216 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (1...𝑠) ≈ ((1 + (𝑚𝑠))...(𝑠 + (𝑚𝑠))))
316 ax-1cn 7720 . . . . . . . . . . . . . . 15 1 ∈ ℂ
31772zcnd 9181 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑚𝑠) ∈ ℂ)
318 addcom 7906 . . . . . . . . . . . . . . 15 ((1 ∈ ℂ ∧ (𝑚𝑠) ∈ ℂ) → (1 + (𝑚𝑠)) = ((𝑚𝑠) + 1))
319316, 317, 318sylancr 410 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (1 + (𝑚𝑠)) = ((𝑚𝑠) + 1))
320267, 266pncan3d 8083 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑠 + (𝑚𝑠)) = 𝑚)
321319, 320oveq12d 5792 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((1 + (𝑚𝑠))...(𝑠 + (𝑚𝑠))) = (((𝑚𝑠) + 1)...𝑚))
322315, 321breqtrd 3954 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (1...𝑠) ≈ (((𝑚𝑠) + 1)...𝑚))
323313, 50fzfigd 10211 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (1...𝑠) ∈ Fin)
324 hashen 10537 . . . . . . . . . . . . 13 (((1...𝑠) ∈ Fin ∧ (((𝑚𝑠) + 1)...𝑚) ∈ Fin) → ((♯‘(1...𝑠)) = (♯‘(((𝑚𝑠) + 1)...𝑚)) ↔ (1...𝑠) ≈ (((𝑚𝑠) + 1)...𝑚)))
325323, 86, 324syl2anc 408 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((♯‘(1...𝑠)) = (♯‘(((𝑚𝑠) + 1)...𝑚)) ↔ (1...𝑠) ≈ (((𝑚𝑠) + 1)...𝑚)))
326322, 325mpbird 166 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (♯‘(1...𝑠)) = (♯‘(((𝑚𝑠) + 1)...𝑚)))
327 hashfz1 10536 . . . . . . . . . . . 12 (𝑠 ∈ ℕ0 → (♯‘(1...𝑠)) = 𝑠)
32853, 327syl 14 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (♯‘(1...𝑠)) = 𝑠)
329326, 328eqtr3d 2174 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (♯‘(((𝑚𝑠) + 1)...𝑚)) = 𝑠)
330329oveq1d 5789 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((♯‘(((𝑚𝑠) + 1)...𝑚)) · ((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃)) = (𝑠 · ((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃)))
331218recnd 7801 . . . . . . . . . . . 12 (𝜑𝑃 ∈ ℂ)
332221rpcnd 9492 . . . . . . . . . . . 12 (𝜑 → (𝑃 + 1) ∈ ℂ)
333221rpap0d 9496 . . . . . . . . . . . 12 (𝜑 → (𝑃 + 1) # 0)
334160, 331, 332, 333div23apd 8595 . . . . . . . . . . 11 (𝜑 → (((𝐸 / 2) · 𝑃) / (𝑃 + 1)) = (((𝐸 / 2) / (𝑃 + 1)) · 𝑃))
33549zcnd 9181 . . . . . . . . . . . . . 14 (𝜑𝑠 ∈ ℂ)
336225rpcnd 9492 . . . . . . . . . . . . . 14 (𝜑 → ((𝐸 / 2) / 𝑠) ∈ ℂ)
337335, 336, 332, 333divassapd 8593 . . . . . . . . . . . . 13 (𝜑 → ((𝑠 · ((𝐸 / 2) / 𝑠)) / (𝑃 + 1)) = (𝑠 · (((𝐸 / 2) / 𝑠) / (𝑃 + 1))))
3385nnap0d 8773 . . . . . . . . . . . . . . 15 (𝜑𝑠 # 0)
339160, 335, 338divcanap2d 8559 . . . . . . . . . . . . . 14 (𝜑 → (𝑠 · ((𝐸 / 2) / 𝑠)) = (𝐸 / 2))
340339oveq1d 5789 . . . . . . . . . . . . 13 (𝜑 → ((𝑠 · ((𝐸 / 2) / 𝑠)) / (𝑃 + 1)) = ((𝐸 / 2) / (𝑃 + 1)))
341337, 340eqtr3d 2174 . . . . . . . . . . . 12 (𝜑 → (𝑠 · (((𝐸 / 2) / 𝑠) / (𝑃 + 1))) = ((𝐸 / 2) / (𝑃 + 1)))
342341oveq1d 5789 . . . . . . . . . . 11 (𝜑 → ((𝑠 · (((𝐸 / 2) / 𝑠) / (𝑃 + 1))) · 𝑃) = (((𝐸 / 2) / (𝑃 + 1)) · 𝑃))
343226rpcnd 9492 . . . . . . . . . . . 12 (𝜑 → (((𝐸 / 2) / 𝑠) / (𝑃 + 1)) ∈ ℂ)
344335, 343, 331mulassd 7796 . . . . . . . . . . 11 (𝜑 → ((𝑠 · (((𝐸 / 2) / 𝑠) / (𝑃 + 1))) · 𝑃) = (𝑠 · ((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃)))
345334, 342, 3443eqtr2rd 2179 . . . . . . . . . 10 (𝜑 → (𝑠 · ((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃)) = (((𝐸 / 2) · 𝑃) / (𝑃 + 1)))
346345adantr 274 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑠 · ((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃)) = (((𝐸 / 2) · 𝑃) / (𝑃 + 1)))
347312, 330, 3463eqtrd 2176 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (𝑃 + 1)) · 𝑃) = (((𝐸 / 2) · 𝑃) / (𝑃 + 1)))
348308, 347breqtrd 3954 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ≤ (((𝐸 / 2) · 𝑃) / (𝑃 + 1)))
349 peano2re 7905 . . . . . . . . . . 11 (𝑃 ∈ ℝ → (𝑃 + 1) ∈ ℝ)
350218, 349syl 14 . . . . . . . . . 10 (𝜑 → (𝑃 + 1) ∈ ℝ)
351218ltp1d 8695 . . . . . . . . . 10 (𝜑𝑃 < (𝑃 + 1))
352218, 350, 97, 351ltmul2dd 9547 . . . . . . . . 9 (𝜑 → ((𝐸 / 2) · 𝑃) < ((𝐸 / 2) · (𝑃 + 1)))
353219, 98, 221ltdivmul2d 9543 . . . . . . . . 9 (𝜑 → ((((𝐸 / 2) · 𝑃) / (𝑃 + 1)) < (𝐸 / 2) ↔ ((𝐸 / 2) · 𝑃) < ((𝐸 / 2) · (𝑃 + 1))))
354352, 353mpbird 166 . . . . . . . 8 (𝜑 → (((𝐸 / 2) · 𝑃) / (𝑃 + 1)) < (𝐸 / 2))
355354adantr 274 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (((𝐸 / 2) · 𝑃) / (𝑃 + 1)) < (𝐸 / 2))
35696, 223, 99, 348, 355lelttrd 7894 . . . . . 6 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < (𝐸 / 2))
35784, 96, 99, 99, 217, 356lt2addd 8336 . . . . 5 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) + Σ𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵))) < ((𝐸 / 2) + (𝐸 / 2)))
35817, 39absmuld 10973 . . . . . . 7 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) = ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)))
359358sumeq2dv 11144 . . . . . 6 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) = Σ𝑗 ∈ (0...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)))
36072zred 9180 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑚𝑠) ∈ ℝ)
361360ltp1d 8695 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (𝑚𝑠) < ((𝑚𝑠) + 1))
362 fzdisj 9839 . . . . . . . 8 ((𝑚𝑠) < ((𝑚𝑠) + 1) → ((0...(𝑚𝑠)) ∩ (((𝑚𝑠) + 1)...𝑚)) = ∅)
363361, 362syl 14 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((0...(𝑚𝑠)) ∩ (((𝑚𝑠) + 1)...𝑚)) = ∅)
364 fzsplit 9838 . . . . . . . 8 ((𝑚𝑠) ∈ (0...𝑚) → (0...𝑚) = ((0...(𝑚𝑠)) ∪ (((𝑚𝑠) + 1)...𝑚)))
36570, 364syl 14 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (0...𝑚) = ((0...(𝑚𝑠)) ∪ (((𝑚𝑠) + 1)...𝑚)))
36682recnd 7801 . . . . . . 7 (((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) ∈ ℂ)
367363, 365, 13, 366fsumsplit 11183 . . . . . 6 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) = (Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) + Σ𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵))))
368359, 367eqtr2d 2173 . . . . 5 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) + Σ𝑗 ∈ (((𝑚𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵))) = Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)))
36945rpcnd 9492 . . . . . . 7 (𝜑𝐸 ∈ ℂ)
370369adantr 274 . . . . . 6 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → 𝐸 ∈ ℂ)
3713702halvesd 8972 . . . . 5 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → ((𝐸 / 2) + (𝐸 / 2)) = 𝐸)
372357, 368, 3713brtr3d 3959 . . . 4 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸)
37342, 44, 47, 48, 372lelttrd 7894 . . 3 ((𝜑𝑚 ∈ (ℤ‘(𝑠 + 𝑡))) → (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸)
374373ralrimiva 2505 . 2 (𝜑 → ∀𝑚 ∈ (ℤ‘(𝑠 + 𝑡))(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸)
375 fveq2 5421 . . . 4 (𝑦 = (𝑠 + 𝑡) → (ℤ𝑦) = (ℤ‘(𝑠 + 𝑡)))
376375raleqdv 2632 . . 3 (𝑦 = (𝑠 + 𝑡) → (∀𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸 ↔ ∀𝑚 ∈ (ℤ‘(𝑠 + 𝑡))(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸))
377376rspcev 2789 . 2 (((𝑠 + 𝑡) ∈ ℕ0 ∧ ∀𝑚 ∈ (ℤ‘(𝑠 + 𝑡))(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸) → ∃𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸)
3789, 374, 377syl2anc 408 1 (𝜑 → ∃𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104  DECID wdc 819   = wceq 1331   ∈ wcel 1480  {cab 2125  ∀wral 2416  ∃wrex 2417   ∪ cun 3069   ∩ cin 3070   ⊆ wss 3071  ∅c0 3363   class class class wbr 3929  dom cdm 4539  ‘cfv 5123  (class class class)co 5774   ≈ cen 6632  Fincfn 6634  ℂcc 7625  ℝcr 7626  0cc0 7627  1c1 7628   + caddc 7630   · cmul 7632   < clt 7807   ≤ cle 7808   − cmin 7940   / cdiv 8439  ℕcn 8727  2c2 8778  ℕ0cn0 8984  ℤcz 9061  ℤ≥cuz 9333  ℝ+crp 9448  ...cfz 9797  seqcseq 10225  ♯chash 10528  abscabs 10776   ⇝ cli 11054  Σcsu 11129 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-nul 4054  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-iinf 4502  ax-cnex 7718  ax-resscn 7719  ax-1cn 7720  ax-1re 7721  ax-icn 7722  ax-addcl 7723  ax-addrcl 7724  ax-mulcl 7725  ax-mulrcl 7726  ax-addcom 7727  ax-mulcom 7728  ax-addass 7729  ax-mulass 7730  ax-distr 7731  ax-i2m1 7732  ax-0lt1 7733  ax-1rid 7734  ax-0id 7735  ax-rnegex 7736  ax-precex 7737  ax-cnre 7738  ax-pre-ltirr 7739  ax-pre-ltwlin 7740  ax-pre-lttrn 7741  ax-pre-apti 7742  ax-pre-ltadd 7743  ax-pre-mulgt0 7744  ax-pre-mulext 7745  ax-arch 7746  ax-caucvg 7747 This theorem depends on definitions:  df-bi 116  df-dc 820  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-nel 2404  df-ral 2421  df-rex 2422  df-reu 2423  df-rmo 2424  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-if 3475  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-tr 4027  df-id 4215  df-po 4218  df-iso 4219  df-iord 4288  df-on 4290  df-ilim 4291  df-suc 4293  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-isom 5132  df-riota 5730  df-ov 5777  df-oprab 5778  df-mpo 5779  df-1st 6038  df-2nd 6039  df-recs 6202  df-irdg 6267  df-frec 6288  df-1o 6313  df-oadd 6317  df-er 6429  df-en 6635  df-dom 6636  df-fin 6637  df-sup 6871  df-pnf 7809  df-mnf 7810  df-xr 7811  df-ltxr 7812  df-le 7813  df-sub 7942  df-neg 7943  df-reap 8344  df-ap 8351  df-div 8440  df-inn 8728  df-2 8786  df-3 8787  df-4 8788  df-n0 8985  df-z 9062  df-uz 9334  df-q 9419  df-rp 9449  df-ico 9684  df-fz 9798  df-fzo 9927  df-seqfrec 10226  df-exp 10300  df-ihash 10529  df-cj 10621  df-re 10622  df-im 10623  df-rsqrt 10777  df-abs 10778  df-clim 11055  df-sumdc 11130 This theorem is referenced by:  mertenslem2  11312
 Copyright terms: Public domain W3C validator