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

Theorem mertenslem2 11576
Description: Lemma for mertensabs 11577. (Contributed by Mario Carneiro, 28-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))))
Assertion
Ref Expression
mertenslem2 (𝜑 → ∃𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸)
Distinct variable groups:   𝑗,𝑚,𝑛,𝑠,𝑦,𝑧,𝐵   𝑗,𝑘,𝐺,𝑚,𝑛,𝑠,𝑦,𝑧   𝜑,𝑗,𝑘,𝑚,𝑦,𝑧   𝐴,𝑘,𝑚,𝑛,𝑠,𝑦   𝑗,𝐸,𝑘,𝑚,𝑛,𝑠,𝑦,𝑧   𝑗,𝐾,𝑘,𝑚,𝑛,𝑠,𝑦,𝑧   𝑗,𝐹,𝑚,𝑛,𝑦   𝜓,𝑗,𝑘,𝑚,𝑛,𝑦,𝑧   𝑇,𝑗,𝑘,𝑚,𝑛,𝑦,𝑧   𝑘,𝐻,𝑚,𝑦   𝜑,𝑛,𝑠
Allowed substitution hints:   𝜓(𝑠)   𝐴(𝑧,𝑗)   𝐵(𝑘)   𝑇(𝑠)   𝐹(𝑧,𝑘,𝑠)   𝐻(𝑧,𝑗,𝑛,𝑠)

Proof of Theorem mertenslem2
Dummy variables 𝑡 𝑤 𝑎 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnuz 9593 . . 3 ℕ = (ℤ‘1)
2 1zzd 9310 . . 3 (𝜑 → 1 ∈ ℤ)
3 mertens.9 . . . . 5 (𝜑𝐸 ∈ ℝ+)
43rphalfcld 9739 . . . 4 (𝜑 → (𝐸 / 2) ∈ ℝ+)
5 nn0uz 9592 . . . . . 6 0 = (ℤ‘0)
6 0zd 9295 . . . . . 6 (𝜑 → 0 ∈ ℤ)
7 eqidd 2190 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → (𝐾𝑗) = (𝐾𝑗))
8 mertens.2 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → (𝐾𝑗) = (abs‘𝐴))
9 mertens.3 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → 𝐴 ∈ ℂ)
109abscld 11222 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → (abs‘𝐴) ∈ ℝ)
118, 10eqeltrd 2266 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → (𝐾𝑗) ∈ ℝ)
12 mertens.7 . . . . . 6 (𝜑 → seq0( + , 𝐾) ∈ dom ⇝ )
135, 6, 7, 11, 12isumrecl 11469 . . . . 5 (𝜑 → Σ𝑗 ∈ ℕ0 (𝐾𝑗) ∈ ℝ)
149absge0d 11225 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → 0 ≤ (abs‘𝐴))
1514, 8breqtrrd 4046 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → 0 ≤ (𝐾𝑗))
165, 6, 7, 11, 12, 15isumge0 11470 . . . . 5 (𝜑 → 0 ≤ Σ𝑗 ∈ ℕ0 (𝐾𝑗))
1713, 16ge0p1rpd 9757 . . . 4 (𝜑 → (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ∈ ℝ+)
184, 17rpdivcld 9744 . . 3 (𝜑 → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) ∈ ℝ+)
19 eqidd 2190 . . 3 ((𝜑𝑚 ∈ ℕ) → (seq0( + , 𝐺)‘𝑚) = (seq0( + , 𝐺)‘𝑚))
20 mertens.4 . . . 4 ((𝜑𝑘 ∈ ℕ0) → (𝐺𝑘) = 𝐵)
21 mertens.5 . . . 4 ((𝜑𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)
22 mertens.8 . . . 4 (𝜑 → seq0( + , 𝐺) ∈ dom ⇝ )
235, 6, 20, 21, 22isumclim2 11462 . . 3 (𝜑 → seq0( + , 𝐺) ⇝ Σ𝑘 ∈ ℕ0 𝐵)
241, 2, 18, 19, 23climi2 11328 . 2 (𝜑 → ∃𝑠 ∈ ℕ ∀𝑚 ∈ (ℤ𝑠)(abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
25 eluznn 9630 . . . . . . . 8 ((𝑠 ∈ ℕ ∧ 𝑚 ∈ (ℤ𝑠)) → 𝑚 ∈ ℕ)
2620, 21eqeltrd 2266 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → (𝐺𝑘) ∈ ℂ)
275, 6, 26serf 10505 . . . . . . . . . . . 12 (𝜑 → seq0( + , 𝐺):ℕ0⟶ℂ)
28 nnnn0 9213 . . . . . . . . . . . 12 (𝑚 ∈ ℕ → 𝑚 ∈ ℕ0)
29 ffvelcdm 5670 . . . . . . . . . . . 12 ((seq0( + , 𝐺):ℕ0⟶ℂ ∧ 𝑚 ∈ ℕ0) → (seq0( + , 𝐺)‘𝑚) ∈ ℂ)
3027, 28, 29syl2an 289 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (seq0( + , 𝐺)‘𝑚) ∈ ℂ)
315, 6, 20, 21, 22isumcl 11465 . . . . . . . . . . . 12 (𝜑 → Σ𝑘 ∈ ℕ0 𝐵 ∈ ℂ)
3231adantr 276 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → Σ𝑘 ∈ ℕ0 𝐵 ∈ ℂ)
3330, 32abssubd 11234 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → (abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) = (abs‘(Σ𝑘 ∈ ℕ0 𝐵 − (seq0( + , 𝐺)‘𝑚))))
34 eqid 2189 . . . . . . . . . . . . . 14 (ℤ‘(𝑚 + 1)) = (ℤ‘(𝑚 + 1))
3528adantl 277 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ ℕ) → 𝑚 ∈ ℕ0)
36 peano2nn0 9246 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ℕ0 → (𝑚 + 1) ∈ ℕ0)
3735, 36syl 14 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → (𝑚 + 1) ∈ ℕ0)
3837nn0zd 9403 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → (𝑚 + 1) ∈ ℤ)
39 simpll 527 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (ℤ‘(𝑚 + 1))) → 𝜑)
40 eluznn0 9629 . . . . . . . . . . . . . . . 16 (((𝑚 + 1) ∈ ℕ0𝑘 ∈ (ℤ‘(𝑚 + 1))) → 𝑘 ∈ ℕ0)
4137, 40sylan 283 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (ℤ‘(𝑚 + 1))) → 𝑘 ∈ ℕ0)
4239, 41, 20syl2anc 411 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (ℤ‘(𝑚 + 1))) → (𝐺𝑘) = 𝐵)
4339, 41, 21syl2anc 411 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (ℤ‘(𝑚 + 1))) → 𝐵 ∈ ℂ)
4422adantr 276 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → seq0( + , 𝐺) ∈ dom ⇝ )
4526adantlr 477 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) ∈ ℂ)
465, 37, 45iserex 11379 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → (seq0( + , 𝐺) ∈ dom ⇝ ↔ seq(𝑚 + 1)( + , 𝐺) ∈ dom ⇝ ))
4744, 46mpbid 147 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → seq(𝑚 + 1)( + , 𝐺) ∈ dom ⇝ )
4834, 38, 42, 43, 47isumcl 11465 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → Σ𝑘 ∈ (ℤ‘(𝑚 + 1))𝐵 ∈ ℂ)
4930, 48pncan2d 8300 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → (((seq0( + , 𝐺)‘𝑚) + Σ𝑘 ∈ (ℤ‘(𝑚 + 1))𝐵) − (seq0( + , 𝐺)‘𝑚)) = Σ𝑘 ∈ (ℤ‘(𝑚 + 1))𝐵)
5020adantlr 477 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) = 𝐵)
5121adantlr 477 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)
525, 34, 37, 50, 51, 44isumsplit 11531 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → Σ𝑘 ∈ ℕ0 𝐵 = (Σ𝑘 ∈ (0...((𝑚 + 1) − 1))𝐵 + Σ𝑘 ∈ (ℤ‘(𝑚 + 1))𝐵))
53 nncn 8957 . . . . . . . . . . . . . . . . . . . 20 (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
5453adantl 277 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ ℕ) → 𝑚 ∈ ℂ)
55 ax-1cn 7934 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℂ
56 pncan 8193 . . . . . . . . . . . . . . . . . . 19 ((𝑚 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑚 + 1) − 1) = 𝑚)
5754, 55, 56sylancl 413 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ ℕ) → ((𝑚 + 1) − 1) = 𝑚)
5857oveq2d 5912 . . . . . . . . . . . . . . . . 17 ((𝜑𝑚 ∈ ℕ) → (0...((𝑚 + 1) − 1)) = (0...𝑚))
5958sumeq1d 11406 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ ℕ) → Σ𝑘 ∈ (0...((𝑚 + 1) − 1))𝐵 = Σ𝑘 ∈ (0...𝑚)𝐵)
60 elnn0uz 9595 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℕ0𝑘 ∈ (ℤ‘0))
6160, 50sylan2br 288 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (ℤ‘0)) → (𝐺𝑘) = 𝐵)
6235, 5eleqtrdi 2282 . . . . . . . . . . . . . . . . 17 ((𝜑𝑚 ∈ ℕ) → 𝑚 ∈ (ℤ‘0))
6360, 51sylan2br 288 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (ℤ‘0)) → 𝐵 ∈ ℂ)
6461, 62, 63fsum3ser 11437 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ ℕ) → Σ𝑘 ∈ (0...𝑚)𝐵 = (seq0( + , 𝐺)‘𝑚))
6559, 64eqtrd 2222 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → Σ𝑘 ∈ (0...((𝑚 + 1) − 1))𝐵 = (seq0( + , 𝐺)‘𝑚))
6665oveq1d 5911 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → (Σ𝑘 ∈ (0...((𝑚 + 1) − 1))𝐵 + Σ𝑘 ∈ (ℤ‘(𝑚 + 1))𝐵) = ((seq0( + , 𝐺)‘𝑚) + Σ𝑘 ∈ (ℤ‘(𝑚 + 1))𝐵))
6752, 66eqtrd 2222 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → Σ𝑘 ∈ ℕ0 𝐵 = ((seq0( + , 𝐺)‘𝑚) + Σ𝑘 ∈ (ℤ‘(𝑚 + 1))𝐵))
6867oveq1d 5911 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → (Σ𝑘 ∈ ℕ0 𝐵 − (seq0( + , 𝐺)‘𝑚)) = (((seq0( + , 𝐺)‘𝑚) + Σ𝑘 ∈ (ℤ‘(𝑚 + 1))𝐵) − (seq0( + , 𝐺)‘𝑚)))
6942sumeq2dv 11408 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → Σ𝑘 ∈ (ℤ‘(𝑚 + 1))(𝐺𝑘) = Σ𝑘 ∈ (ℤ‘(𝑚 + 1))𝐵)
7049, 68, 693eqtr4d 2232 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (Σ𝑘 ∈ ℕ0 𝐵 − (seq0( + , 𝐺)‘𝑚)) = Σ𝑘 ∈ (ℤ‘(𝑚 + 1))(𝐺𝑘))
7170fveq2d 5538 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → (abs‘(Σ𝑘 ∈ ℕ0 𝐵 − (seq0( + , 𝐺)‘𝑚))) = (abs‘Σ𝑘 ∈ (ℤ‘(𝑚 + 1))(𝐺𝑘)))
7233, 71eqtrd 2222 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → (abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) = (abs‘Σ𝑘 ∈ (ℤ‘(𝑚 + 1))(𝐺𝑘)))
7372breq1d 4028 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → ((abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) ↔ (abs‘Σ𝑘 ∈ (ℤ‘(𝑚 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
7425, 73sylan2 286 . . . . . . 7 ((𝜑 ∧ (𝑠 ∈ ℕ ∧ 𝑚 ∈ (ℤ𝑠))) → ((abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) ↔ (abs‘Σ𝑘 ∈ (ℤ‘(𝑚 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
7574anassrs 400 . . . . . 6 (((𝜑𝑠 ∈ ℕ) ∧ 𝑚 ∈ (ℤ𝑠)) → ((abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) ↔ (abs‘Σ𝑘 ∈ (ℤ‘(𝑚 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
7675ralbidva 2486 . . . . 5 ((𝜑𝑠 ∈ ℕ) → (∀𝑚 ∈ (ℤ𝑠)(abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) ↔ ∀𝑚 ∈ (ℤ𝑠)(abs‘Σ𝑘 ∈ (ℤ‘(𝑚 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
77 fvoveq1 5919 . . . . . . . . 9 (𝑚 = 𝑛 → (ℤ‘(𝑚 + 1)) = (ℤ‘(𝑛 + 1)))
7877sumeq1d 11406 . . . . . . . 8 (𝑚 = 𝑛 → Σ𝑘 ∈ (ℤ‘(𝑚 + 1))(𝐺𝑘) = Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘))
7978fveq2d 5538 . . . . . . 7 (𝑚 = 𝑛 → (abs‘Σ𝑘 ∈ (ℤ‘(𝑚 + 1))(𝐺𝑘)) = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)))
8079breq1d 4028 . . . . . 6 (𝑚 = 𝑛 → ((abs‘Σ𝑘 ∈ (ℤ‘(𝑚 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) ↔ (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
8180cbvralv 2718 . . . . 5 (∀𝑚 ∈ (ℤ𝑠)(abs‘Σ𝑘 ∈ (ℤ‘(𝑚 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) ↔ ∀𝑛 ∈ (ℤ𝑠)(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
8276, 81bitrdi 196 . . . 4 ((𝜑𝑠 ∈ ℕ) → (∀𝑚 ∈ (ℤ𝑠)(abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) ↔ ∀𝑛 ∈ (ℤ𝑠)(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
83 mertens.11 . . . . . 6 (𝜓 ↔ (𝑠 ∈ ℕ ∧ ∀𝑛 ∈ (ℤ𝑠)(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
84 0zd 9295 . . . . . . . . . 10 ((𝜑𝜓) → 0 ∈ ℤ)
854adantr 276 . . . . . . . . . . . 12 ((𝜑𝜓) → (𝐸 / 2) ∈ ℝ+)
8683simplbi 274 . . . . . . . . . . . . . 14 (𝜓𝑠 ∈ ℕ)
8786adantl 277 . . . . . . . . . . . . 13 ((𝜑𝜓) → 𝑠 ∈ ℕ)
8887nnrpd 9724 . . . . . . . . . . . 12 ((𝜑𝜓) → 𝑠 ∈ ℝ+)
8985, 88rpdivcld 9744 . . . . . . . . . . 11 ((𝜑𝜓) → ((𝐸 / 2) / 𝑠) ∈ ℝ+)
9087nnzd 9404 . . . . . . . . . . . . . . 15 ((𝜑𝜓) → 𝑠 ∈ ℤ)
91 1zzd 9310 . . . . . . . . . . . . . . 15 ((𝜑𝜓) → 1 ∈ ℤ)
9290, 91zsubcld 9410 . . . . . . . . . . . . . 14 ((𝜑𝜓) → (𝑠 − 1) ∈ ℤ)
9384, 92fzfigd 10462 . . . . . . . . . . . . 13 ((𝜑𝜓) → (0...(𝑠 − 1)) ∈ Fin)
94 eqid 2189 . . . . . . . . . . . . . . 15 (ℤ‘(𝑛 + 1)) = (ℤ‘(𝑛 + 1))
95 elfznn0 10144 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (0...(𝑠 − 1)) → 𝑛 ∈ ℕ0)
9695adantl 277 . . . . . . . . . . . . . . . . 17 (((𝜑𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → 𝑛 ∈ ℕ0)
97 peano2nn0 9246 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ0 → (𝑛 + 1) ∈ ℕ0)
9896, 97syl 14 . . . . . . . . . . . . . . . 16 (((𝜑𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → (𝑛 + 1) ∈ ℕ0)
9998nn0zd 9403 . . . . . . . . . . . . . . 15 (((𝜑𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → (𝑛 + 1) ∈ ℤ)
100 eqidd 2190 . . . . . . . . . . . . . . 15 ((((𝜑𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) ∧ 𝑘 ∈ (ℤ‘(𝑛 + 1))) → (𝐺𝑘) = (𝐺𝑘))
101 simplll 533 . . . . . . . . . . . . . . . 16 ((((𝜑𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) ∧ 𝑘 ∈ (ℤ‘(𝑛 + 1))) → 𝜑)
102 eluznn0 9629 . . . . . . . . . . . . . . . . 17 (((𝑛 + 1) ∈ ℕ0𝑘 ∈ (ℤ‘(𝑛 + 1))) → 𝑘 ∈ ℕ0)
10398, 102sylan 283 . . . . . . . . . . . . . . . 16 ((((𝜑𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) ∧ 𝑘 ∈ (ℤ‘(𝑛 + 1))) → 𝑘 ∈ ℕ0)
104101, 103, 26syl2anc 411 . . . . . . . . . . . . . . 15 ((((𝜑𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) ∧ 𝑘 ∈ (ℤ‘(𝑛 + 1))) → (𝐺𝑘) ∈ ℂ)
10522ad2antrr 488 . . . . . . . . . . . . . . . 16 (((𝜑𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → seq0( + , 𝐺) ∈ dom ⇝ )
106 simpll 527 . . . . . . . . . . . . . . . . . 18 (((𝜑𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → 𝜑)
107106, 26sylan 283 . . . . . . . . . . . . . . . . 17 ((((𝜑𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) ∈ ℂ)
1085, 98, 107iserex 11379 . . . . . . . . . . . . . . . 16 (((𝜑𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → (seq0( + , 𝐺) ∈ dom ⇝ ↔ seq(𝑛 + 1)( + , 𝐺) ∈ dom ⇝ ))
109105, 108mpbid 147 . . . . . . . . . . . . . . 15 (((𝜑𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → seq(𝑛 + 1)( + , 𝐺) ∈ dom ⇝ )
11094, 99, 100, 104, 109isumcl 11465 . . . . . . . . . . . . . 14 (((𝜑𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘) ∈ ℂ)
111110abscld 11222 . . . . . . . . . . . . 13 (((𝜑𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) ∈ ℝ)
11293, 111fsumrecl 11441 . . . . . . . . . . . 12 ((𝜑𝜓) → Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) ∈ ℝ)
113 0red 7988 . . . . . . . . . . . . 13 ((𝜑𝜓) → 0 ∈ ℝ)
114 nnnn0 9213 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
115114, 20sylan2 286 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (𝐺𝑘) = 𝐵)
116114, 21sylan2 286 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → 𝐵 ∈ ℂ)
117 1nn0 9222 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℕ0
118117a1i 9 . . . . . . . . . . . . . . . . . 18 (𝜑 → 1 ∈ ℕ0)
1195, 118, 26iserex 11379 . . . . . . . . . . . . . . . . 17 (𝜑 → (seq0( + , 𝐺) ∈ dom ⇝ ↔ seq1( + , 𝐺) ∈ dom ⇝ ))
12022, 119mpbid 147 . . . . . . . . . . . . . . . 16 (𝜑 → seq1( + , 𝐺) ∈ dom ⇝ )
1211, 2, 115, 116, 120isumcl 11465 . . . . . . . . . . . . . . 15 (𝜑 → Σ𝑘 ∈ ℕ 𝐵 ∈ ℂ)
122121adantr 276 . . . . . . . . . . . . . 14 ((𝜑𝜓) → Σ𝑘 ∈ ℕ 𝐵 ∈ ℂ)
123122abscld 11222 . . . . . . . . . . . . 13 ((𝜑𝜓) → (abs‘Σ𝑘 ∈ ℕ 𝐵) ∈ ℝ)
124122absge0d 11225 . . . . . . . . . . . . 13 ((𝜑𝜓) → 0 ≤ (abs‘Σ𝑘 ∈ ℕ 𝐵))
12520adantlr 477 . . . . . . . . . . . . . 14 (((𝜑𝜓) ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) = 𝐵)
12621adantlr 477 . . . . . . . . . . . . . 14 (((𝜑𝜓) ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)
12722adantr 276 . . . . . . . . . . . . . 14 ((𝜑𝜓) → seq0( + , 𝐺) ∈ dom ⇝ )
128 mertens.10 . . . . . . . . . . . . . 14 𝑇 = {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘))}
129 nnm1nn0 9247 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ ℕ → (𝑠 − 1) ∈ ℕ0)
13087, 129syl 14 . . . . . . . . . . . . . . . . . 18 ((𝜑𝜓) → (𝑠 − 1) ∈ ℕ0)
131130, 5eleqtrdi 2282 . . . . . . . . . . . . . . . . 17 ((𝜑𝜓) → (𝑠 − 1) ∈ (ℤ‘0))
132 eluzfz1 10061 . . . . . . . . . . . . . . . . 17 ((𝑠 − 1) ∈ (ℤ‘0) → 0 ∈ (0...(𝑠 − 1)))
133131, 132syl 14 . . . . . . . . . . . . . . . 16 ((𝜑𝜓) → 0 ∈ (0...(𝑠 − 1)))
134115sumeq2dv 11408 . . . . . . . . . . . . . . . . . . 19 (𝜑 → Σ𝑘 ∈ ℕ (𝐺𝑘) = Σ𝑘 ∈ ℕ 𝐵)
135134adantr 276 . . . . . . . . . . . . . . . . . 18 ((𝜑𝜓) → Σ𝑘 ∈ ℕ (𝐺𝑘) = Σ𝑘 ∈ ℕ 𝐵)
136135fveq2d 5538 . . . . . . . . . . . . . . . . 17 ((𝜑𝜓) → (abs‘Σ𝑘 ∈ ℕ (𝐺𝑘)) = (abs‘Σ𝑘 ∈ ℕ 𝐵))
137136eqcomd 2195 . . . . . . . . . . . . . . . 16 ((𝜑𝜓) → (abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈ ℕ (𝐺𝑘)))
138 fv0p1e1 9064 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 0 → (ℤ‘(𝑛 + 1)) = (ℤ‘1))
139138, 1eqtr4di 2240 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 0 → (ℤ‘(𝑛 + 1)) = ℕ)
140139sumeq1d 11406 . . . . . . . . . . . . . . . . . 18 (𝑛 = 0 → Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘) = Σ𝑘 ∈ ℕ (𝐺𝑘))
141140fveq2d 5538 . . . . . . . . . . . . . . . . 17 (𝑛 = 0 → (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) = (abs‘Σ𝑘 ∈ ℕ (𝐺𝑘)))
142141rspceeqv 2874 . . . . . . . . . . . . . . . 16 ((0 ∈ (0...(𝑠 − 1)) ∧ (abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈ ℕ (𝐺𝑘))) → ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)))
143133, 137, 142syl2anc 411 . . . . . . . . . . . . . . 15 ((𝜑𝜓) → ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)))
144 eqeq1 2196 . . . . . . . . . . . . . . . . . 18 (𝑧 = (abs‘Σ𝑘 ∈ ℕ 𝐵) → (𝑧 = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) ↔ (abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘))))
145144rexbidv 2491 . . . . . . . . . . . . . . . . 17 (𝑧 = (abs‘Σ𝑘 ∈ ℕ 𝐵) → (∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) ↔ ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘))))
146145, 128elab2g 2899 . . . . . . . . . . . . . . . 16 ((abs‘Σ𝑘 ∈ ℕ 𝐵) ∈ ℝ → ((abs‘Σ𝑘 ∈ ℕ 𝐵) ∈ 𝑇 ↔ ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘))))
147123, 146syl 14 . . . . . . . . . . . . . . 15 ((𝜑𝜓) → ((abs‘Σ𝑘 ∈ ℕ 𝐵) ∈ 𝑇 ↔ ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘))))
148143, 147mpbird 167 . . . . . . . . . . . . . 14 ((𝜑𝜓) → (abs‘Σ𝑘 ∈ ℕ 𝐵) ∈ 𝑇)
149125, 126, 127, 128, 148, 87mertenslemub 11574 . . . . . . . . . . . . 13 ((𝜑𝜓) → (abs‘Σ𝑘 ∈ ℕ 𝐵) ≤ Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)))
150113, 123, 112, 124, 149letrd 8111 . . . . . . . . . . . 12 ((𝜑𝜓) → 0 ≤ Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)))
151112, 150ge0p1rpd 9757 . . . . . . . . . . 11 ((𝜑𝜓) → (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) + 1) ∈ ℝ+)
15289, 151rpdivcld 9744 . . . . . . . . . 10 ((𝜑𝜓) → (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) + 1)) ∈ ℝ+)
153 simpr 110 . . . . . . . . . . 11 (((𝜑𝜓) ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈ ℕ0)
154 fveq2 5534 . . . . . . . . . . . . 13 (𝑗 = 𝑚 → (𝐾𝑗) = (𝐾𝑚))
155154eleq1d 2258 . . . . . . . . . . . 12 (𝑗 = 𝑚 → ((𝐾𝑗) ∈ ℝ ↔ (𝐾𝑚) ∈ ℝ))
15611ralrimiva 2563 . . . . . . . . . . . . 13 (𝜑 → ∀𝑗 ∈ ℕ0 (𝐾𝑗) ∈ ℝ)
157156ad2antrr 488 . . . . . . . . . . . 12 (((𝜑𝜓) ∧ 𝑚 ∈ ℕ0) → ∀𝑗 ∈ ℕ0 (𝐾𝑗) ∈ ℝ)
158155, 157, 153rspcdva 2861 . . . . . . . . . . 11 (((𝜑𝜓) ∧ 𝑚 ∈ ℕ0) → (𝐾𝑚) ∈ ℝ)
159 fveq2 5534 . . . . . . . . . . . 12 (𝑛 = 𝑚 → (𝐾𝑛) = (𝐾𝑚))
160 eqid 2189 . . . . . . . . . . . 12 (𝑛 ∈ ℕ0 ↦ (𝐾𝑛)) = (𝑛 ∈ ℕ0 ↦ (𝐾𝑛))
161159, 160fvmptg 5613 . . . . . . . . . . 11 ((𝑚 ∈ ℕ0 ∧ (𝐾𝑚) ∈ ℝ) → ((𝑛 ∈ ℕ0 ↦ (𝐾𝑛))‘𝑚) = (𝐾𝑚))
162153, 158, 161syl2anc 411 . . . . . . . . . 10 (((𝜑𝜓) ∧ 𝑚 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (𝐾𝑛))‘𝑚) = (𝐾𝑚))
163 nn0ex 9212 . . . . . . . . . . . . . 14 0 ∈ V
164163mptex 5763 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ0 ↦ (𝐾𝑛)) ∈ V
165164a1i 9 . . . . . . . . . . . 12 (𝜑 → (𝑛 ∈ ℕ0 ↦ (𝐾𝑛)) ∈ V)
16660biimpri 133 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (ℤ‘0) → 𝑘 ∈ ℕ0)
167 fveq2 5534 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑘 → (𝐾𝑗) = (𝐾𝑘))
168167eleq1d 2258 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑘 → ((𝐾𝑗) ∈ ℝ ↔ (𝐾𝑘) ∈ ℝ))
169156adantr 276 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ0) → ∀𝑗 ∈ ℕ0 (𝐾𝑗) ∈ ℝ)
170 simpr 110 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
171168, 169, 170rspcdva 2861 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ℕ0) → (𝐾𝑘) ∈ ℝ)
17260, 171sylan2br 288 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (ℤ‘0)) → (𝐾𝑘) ∈ ℝ)
173 fveq2 5534 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑘 → (𝐾𝑛) = (𝐾𝑘))
174173, 160fvmptg 5613 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ0 ∧ (𝐾𝑘) ∈ ℝ) → ((𝑛 ∈ ℕ0 ↦ (𝐾𝑛))‘𝑘) = (𝐾𝑘))
175166, 172, 174syl2an2 594 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (ℤ‘0)) → ((𝑛 ∈ ℕ0 ↦ (𝐾𝑛))‘𝑘) = (𝐾𝑘))
176175, 172eqeltrd 2266 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (ℤ‘0)) → ((𝑛 ∈ ℕ0 ↦ (𝐾𝑛))‘𝑘) ∈ ℝ)
177 elnn0uz 9595 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ0𝑗 ∈ (ℤ‘0))
178 simpr 110 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ0) → 𝑗 ∈ ℕ0)
179 fveq2 5534 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑗 → (𝐾𝑛) = (𝐾𝑗))
180179, 160fvmptg 5613 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ ℕ0 ∧ (𝐾𝑗) ∈ ℝ) → ((𝑛 ∈ ℕ0 ↦ (𝐾𝑛))‘𝑗) = (𝐾𝑗))
181178, 11, 180syl2anc 411 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (𝐾𝑛))‘𝑗) = (𝐾𝑗))
182177, 181sylan2br 288 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℤ‘0)) → ((𝑛 ∈ ℕ0 ↦ (𝐾𝑛))‘𝑗) = (𝐾𝑗))
183 readdcl 7967 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑘 + 𝑦) ∈ ℝ)
184183adantl 277 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑘 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑘 + 𝑦) ∈ ℝ)
1856, 176, 182, 184seq3feq 10503 . . . . . . . . . . . . 13 (𝜑 → seq0( + , (𝑛 ∈ ℕ0 ↦ (𝐾𝑛))) = seq0( + , 𝐾))
186185, 12eqeltrd 2266 . . . . . . . . . . . 12 (𝜑 → seq0( + , (𝑛 ∈ ℕ0 ↦ (𝐾𝑛))) ∈ dom ⇝ )
187181, 11eqeltrd 2266 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (𝐾𝑛))‘𝑗) ∈ ℝ)
188187recnd 8016 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (𝐾𝑛))‘𝑗) ∈ ℂ)
1895, 6, 165, 186, 188serf0 11392 . . . . . . . . . . 11 (𝜑 → (𝑛 ∈ ℕ0 ↦ (𝐾𝑛)) ⇝ 0)
190189adantr 276 . . . . . . . . . 10 ((𝜑𝜓) → (𝑛 ∈ ℕ0 ↦ (𝐾𝑛)) ⇝ 0)
1915, 84, 152, 162, 190climi0 11329 . . . . . . . . 9 ((𝜑𝜓) → ∃𝑡 ∈ ℕ0𝑚 ∈ (ℤ𝑡)(abs‘(𝐾𝑚)) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) + 1)))
192 fveq2 5534 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑎 → (𝐺𝑘) = (𝐺𝑎))
193192cbvsumv 11401 . . . . . . . . . . . . . . . . 17 Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘) = Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)
194193fveq2i 5537 . . . . . . . . . . . . . . . 16 (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) = (abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎))
195194a1i 9 . . . . . . . . . . . . . . 15 (𝑛 ∈ (0...(𝑠 − 1)) → (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) = (abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)))
196195sumeq2i 11404 . . . . . . . . . . . . . 14 Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) = Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎))
197196oveq1i 5906 . . . . . . . . . . . . 13 𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) + 1) = (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)
198197oveq2i 5907 . . . . . . . . . . . 12 (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) + 1)) = (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1))
199198breq2i 4026 . . . . . . . . . . 11 ((abs‘(𝐾𝑚)) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) + 1)) ↔ (abs‘(𝐾𝑚)) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))
200199ralbii 2496 . . . . . . . . . 10 (∀𝑚 ∈ (ℤ𝑡)(abs‘(𝐾𝑚)) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) + 1)) ↔ ∀𝑚 ∈ (ℤ𝑡)(abs‘(𝐾𝑚)) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))
201200rexbii 2497 . . . . . . . . 9 (∃𝑡 ∈ ℕ0𝑚 ∈ (ℤ𝑡)(abs‘(𝐾𝑚)) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) + 1)) ↔ ∃𝑡 ∈ ℕ0𝑚 ∈ (ℤ𝑡)(abs‘(𝐾𝑚)) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))
202191, 201sylib 122 . . . . . . . 8 ((𝜑𝜓) → ∃𝑡 ∈ ℕ0𝑚 ∈ (ℤ𝑡)(abs‘(𝐾𝑚)) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))
203 simplll 533 . . . . . . . . . . . . . 14 ((((𝜑𝜓) ∧ 𝑡 ∈ ℕ0) ∧ 𝑚 ∈ (ℤ𝑡)) → 𝜑)
204 eluznn0 9629 . . . . . . . . . . . . . . 15 ((𝑡 ∈ ℕ0𝑚 ∈ (ℤ𝑡)) → 𝑚 ∈ ℕ0)
205204adantll 476 . . . . . . . . . . . . . 14 ((((𝜑𝜓) ∧ 𝑡 ∈ ℕ0) ∧ 𝑚 ∈ (ℤ𝑡)) → 𝑚 ∈ ℕ0)
20611, 15absidd 11208 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ0) → (abs‘(𝐾𝑗)) = (𝐾𝑗))
207206ralrimiva 2563 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑗 ∈ ℕ0 (abs‘(𝐾𝑗)) = (𝐾𝑗))
208154fveq2d 5538 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑚 → (abs‘(𝐾𝑗)) = (abs‘(𝐾𝑚)))
209208, 154eqeq12d 2204 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑚 → ((abs‘(𝐾𝑗)) = (𝐾𝑗) ↔ (abs‘(𝐾𝑚)) = (𝐾𝑚)))
210209rspccva 2855 . . . . . . . . . . . . . . 15 ((∀𝑗 ∈ ℕ0 (abs‘(𝐾𝑗)) = (𝐾𝑗) ∧ 𝑚 ∈ ℕ0) → (abs‘(𝐾𝑚)) = (𝐾𝑚))
211207, 210sylan 283 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ0) → (abs‘(𝐾𝑚)) = (𝐾𝑚))
212203, 205, 211syl2anc 411 . . . . . . . . . . . . 13 ((((𝜑𝜓) ∧ 𝑡 ∈ ℕ0) ∧ 𝑚 ∈ (ℤ𝑡)) → (abs‘(𝐾𝑚)) = (𝐾𝑚))
213212breq1d 4028 . . . . . . . . . . . 12 ((((𝜑𝜓) ∧ 𝑡 ∈ ℕ0) ∧ 𝑚 ∈ (ℤ𝑡)) → ((abs‘(𝐾𝑚)) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)) ↔ (𝐾𝑚) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1))))
214213ralbidva 2486 . . . . . . . . . . 11 (((𝜑𝜓) ∧ 𝑡 ∈ ℕ0) → (∀𝑚 ∈ (ℤ𝑡)(abs‘(𝐾𝑚)) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)) ↔ ∀𝑚 ∈ (ℤ𝑡)(𝐾𝑚) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1))))
215 nfv 1539 . . . . . . . . . . . 12 𝑚(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1))
216 nfcv 2332 . . . . . . . . . . . . 13 𝑛(𝐾𝑚)
217 nfcv 2332 . . . . . . . . . . . . 13 𝑛 <
218 nfcv 2332 . . . . . . . . . . . . . 14 𝑛((𝐸 / 2) / 𝑠)
219 nfcv 2332 . . . . . . . . . . . . . 14 𝑛 /
220 nfcv 2332 . . . . . . . . . . . . . . . 16 𝑛(0...(𝑠 − 1))
221220nfsum1 11396 . . . . . . . . . . . . . . 15 𝑛Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎))
222 nfcv 2332 . . . . . . . . . . . . . . 15 𝑛 +
223 nfcv 2332 . . . . . . . . . . . . . . 15 𝑛1
224221, 222, 223nfov 5926 . . . . . . . . . . . . . 14 𝑛𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)
225218, 219, 224nfov 5926 . . . . . . . . . . . . 13 𝑛(((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1))
226216, 217, 225nfbr 4064 . . . . . . . . . . . 12 𝑛(𝐾𝑚) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1))
227159breq1d 4028 . . . . . . . . . . . 12 (𝑛 = 𝑚 → ((𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)) ↔ (𝐾𝑚) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1))))
228215, 226, 227cbvral 2714 . . . . . . . . . . 11 (∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)) ↔ ∀𝑚 ∈ (ℤ𝑡)(𝐾𝑚) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))
229214, 228bitr4di 198 . . . . . . . . . 10 (((𝜑𝜓) ∧ 𝑡 ∈ ℕ0) → (∀𝑚 ∈ (ℤ𝑡)(abs‘(𝐾𝑚)) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)) ↔ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1))))
230 simpll 527 . . . . . . . . . . . . 13 (((𝜑𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))) → 𝜑)
231 mertens.1 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ0) → (𝐹𝑗) = 𝐴)
232230, 231sylan 283 . . . . . . . . . . . 12 ((((𝜑𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))) ∧ 𝑗 ∈ ℕ0) → (𝐹𝑗) = 𝐴)
233230, 8sylan 283 . . . . . . . . . . . 12 ((((𝜑𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))) ∧ 𝑗 ∈ ℕ0) → (𝐾𝑗) = (abs‘𝐴))
234230, 9sylan 283 . . . . . . . . . . . 12 ((((𝜑𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))) ∧ 𝑗 ∈ ℕ0) → 𝐴 ∈ ℂ)
235230, 20sylan 283 . . . . . . . . . . . 12 ((((𝜑𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))) ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) = 𝐵)
236230, 21sylan 283 . . . . . . . . . . . 12 ((((𝜑𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))) ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)
237 mertens.6 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → (𝐻𝑘) = Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘𝑗))))
238230, 237sylan 283 . . . . . . . . . . . 12 ((((𝜑𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))) ∧ 𝑘 ∈ ℕ0) → (𝐻𝑘) = Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘𝑗))))
23912ad2antrr 488 . . . . . . . . . . . 12 (((𝜑𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))) → seq0( + , 𝐾) ∈ dom ⇝ )
24022ad2antrr 488 . . . . . . . . . . . 12 (((𝜑𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))) → seq0( + , 𝐺) ∈ dom ⇝ )
2413ad2antrr 488 . . . . . . . . . . . 12 (((𝜑𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))) → 𝐸 ∈ ℝ+)
242196, 112eqeltrrid 2277 . . . . . . . . . . . . 13 ((𝜑𝜓) → Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) ∈ ℝ)
243242adantr 276 . . . . . . . . . . . 12 (((𝜑𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))) → Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) ∈ ℝ)
244228anbi2i 457 . . . . . . . . . . . . . . 15 ((𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1))) ↔ (𝑡 ∈ ℕ0 ∧ ∀𝑚 ∈ (ℤ𝑡)(𝐾𝑚) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1))))
245244anbi2i 457 . . . . . . . . . . . . . 14 ((𝜓 ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))) ↔ (𝜓 ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑚 ∈ (ℤ𝑡)(𝐾𝑚) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))))
246245biimpi 120 . . . . . . . . . . . . 13 ((𝜓 ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))) → (𝜓 ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑚 ∈ (ℤ𝑡)(𝐾𝑚) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))))
247246adantll 476 . . . . . . . . . . . 12 (((𝜑𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))) → (𝜓 ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑚 ∈ (ℤ𝑡)(𝐾𝑚) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))))
248150, 196breqtrdi 4059 . . . . . . . . . . . . 13 ((𝜑𝜓) → 0 ≤ Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)))
249248adantr 276 . . . . . . . . . . . 12 (((𝜑𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))) → 0 ≤ Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)))
250 simpr 110 . . . . . . . . . . . . . . . 16 ((((𝜑𝜓) ∧ 𝑤𝑇) ∧ 𝑎 ∈ ℕ0) → 𝑎 ∈ ℕ0)
25120ralrimiva 2563 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑘 ∈ ℕ0 (𝐺𝑘) = 𝐵)
252251ad3antrrr 492 . . . . . . . . . . . . . . . 16 ((((𝜑𝜓) ∧ 𝑤𝑇) ∧ 𝑎 ∈ ℕ0) → ∀𝑘 ∈ ℕ0 (𝐺𝑘) = 𝐵)
253 nfcsb1v 3105 . . . . . . . . . . . . . . . . . 18 𝑘𝑎 / 𝑘𝐵
254253nfeq2 2344 . . . . . . . . . . . . . . . . 17 𝑘(𝐺𝑎) = 𝑎 / 𝑘𝐵
255 csbeq1a 3081 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑎𝐵 = 𝑎 / 𝑘𝐵)
256192, 255eqeq12d 2204 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑎 → ((𝐺𝑘) = 𝐵 ↔ (𝐺𝑎) = 𝑎 / 𝑘𝐵))
257254, 256rspc 2850 . . . . . . . . . . . . . . . 16 (𝑎 ∈ ℕ0 → (∀𝑘 ∈ ℕ0 (𝐺𝑘) = 𝐵 → (𝐺𝑎) = 𝑎 / 𝑘𝐵))
258250, 252, 257sylc 62 . . . . . . . . . . . . . . 15 ((((𝜑𝜓) ∧ 𝑤𝑇) ∧ 𝑎 ∈ ℕ0) → (𝐺𝑎) = 𝑎 / 𝑘𝐵)
25921ralrimiva 2563 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑘 ∈ ℕ0 𝐵 ∈ ℂ)
260259ad3antrrr 492 . . . . . . . . . . . . . . . 16 ((((𝜑𝜓) ∧ 𝑤𝑇) ∧ 𝑎 ∈ ℕ0) → ∀𝑘 ∈ ℕ0 𝐵 ∈ ℂ)
261253nfel1 2343 . . . . . . . . . . . . . . . . 17 𝑘𝑎 / 𝑘𝐵 ∈ ℂ
262255eleq1d 2258 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑎 → (𝐵 ∈ ℂ ↔ 𝑎 / 𝑘𝐵 ∈ ℂ))
263261, 262rspc 2850 . . . . . . . . . . . . . . . 16 (𝑎 ∈ ℕ0 → (∀𝑘 ∈ ℕ0 𝐵 ∈ ℂ → 𝑎 / 𝑘𝐵 ∈ ℂ))
264250, 260, 263sylc 62 . . . . . . . . . . . . . . 15 ((((𝜑𝜓) ∧ 𝑤𝑇) ∧ 𝑎 ∈ ℕ0) → 𝑎 / 𝑘𝐵 ∈ ℂ)
26522ad2antrr 488 . . . . . . . . . . . . . . 15 (((𝜑𝜓) ∧ 𝑤𝑇) → seq0( + , 𝐺) ∈ dom ⇝ )
266194eqeq2i 2200 . . . . . . . . . . . . . . . . . 18 (𝑧 = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) ↔ 𝑧 = (abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)))
267266rexbii 2497 . . . . . . . . . . . . . . . . 17 (∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) ↔ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)))
268267abbii 2305 . . . . . . . . . . . . . . . 16 {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘))} = {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎))}
269128, 268eqtri 2210 . . . . . . . . . . . . . . 15 𝑇 = {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎))}
270 simpr 110 . . . . . . . . . . . . . . 15 (((𝜑𝜓) ∧ 𝑤𝑇) → 𝑤𝑇)
27187adantr 276 . . . . . . . . . . . . . . 15 (((𝜑𝜓) ∧ 𝑤𝑇) → 𝑠 ∈ ℕ)
272258, 264, 265, 269, 270, 271mertenslemub 11574 . . . . . . . . . . . . . 14 (((𝜑𝜓) ∧ 𝑤𝑇) → 𝑤 ≤ Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)))
273272ralrimiva 2563 . . . . . . . . . . . . 13 ((𝜑𝜓) → ∀𝑤𝑇 𝑤 ≤ Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)))
274273adantr 276 . . . . . . . . . . . 12 (((𝜑𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))) → ∀𝑤𝑇 𝑤 ≤ Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)))
275232, 233, 234, 235, 236, 238, 239, 240, 241, 128, 83, 243, 247, 249, 274mertenslemi1 11575 . . . . . . . . . . 11 (((𝜑𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))) → ∃𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸)
276275expr 375 . . . . . . . . . 10 (((𝜑𝜓) ∧ 𝑡 ∈ ℕ0) → (∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)) → ∃𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸))
277229, 276sylbid 150 . . . . . . . . 9 (((𝜑𝜓) ∧ 𝑡 ∈ ℕ0) → (∀𝑚 ∈ (ℤ𝑡)(abs‘(𝐾𝑚)) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)) → ∃𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸))
278277rexlimdva 2607 . . . . . . . 8 ((𝜑𝜓) → (∃𝑡 ∈ ℕ0𝑚 ∈ (ℤ𝑡)(abs‘(𝐾𝑚)) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)) → ∃𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸))
279202, 278mpd 13 . . . . . . 7 ((𝜑𝜓) → ∃𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸)
280279ex 115 . . . . . 6 (𝜑 → (𝜓 → ∃𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸))
28183, 280biimtrrid 153 . . . . 5 (𝜑 → ((𝑠 ∈ ℕ ∧ ∀𝑛 ∈ (ℤ𝑠)(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))) → ∃𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸))
282281expdimp 259 . . . 4 ((𝜑𝑠 ∈ ℕ) → (∀𝑛 ∈ (ℤ𝑠)(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) → ∃𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸))
28382, 282sylbid 150 . . 3 ((𝜑𝑠 ∈ ℕ) → (∀𝑚 ∈ (ℤ𝑠)(abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) → ∃𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸))
284283rexlimdva 2607 . 2 (𝜑 → (∃𝑠 ∈ ℕ ∀𝑚 ∈ (ℤ𝑠)(abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) → ∃𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸))
28524, 284mpd 13 1 (𝜑 → ∃𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105   = wceq 1364  wcel 2160  {cab 2175  wral 2468  wrex 2469  Vcvv 2752  csb 3072   class class class wbr 4018  cmpt 4079  dom cdm 4644  wf 5231  cfv 5235  (class class class)co 5896  cc 7839  cr 7840  0cc0 7841  1c1 7842   + caddc 7844   · cmul 7846   < clt 8022  cle 8023  cmin 8158   / cdiv 8659  cn 8949  2c2 9000  0cn0 9206  cuz 9558  +crp 9683  ...cfz 10038  seqcseq 10476  abscabs 11038  cli 11318  Σcsu 11393
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 7932  ax-resscn 7933  ax-1cn 7934  ax-1re 7935  ax-icn 7936  ax-addcl 7937  ax-addrcl 7938  ax-mulcl 7939  ax-mulrcl 7940  ax-addcom 7941  ax-mulcom 7942  ax-addass 7943  ax-mulass 7944  ax-distr 7945  ax-i2m1 7946  ax-0lt1 7947  ax-1rid 7948  ax-0id 7949  ax-rnegex 7950  ax-precex 7951  ax-cnre 7952  ax-pre-ltirr 7953  ax-pre-ltwlin 7954  ax-pre-lttrn 7955  ax-pre-apti 7956  ax-pre-ltadd 7957  ax-pre-mulgt0 7958  ax-pre-mulext 7959  ax-arch 7960  ax-caucvg 7961
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 5852  df-ov 5899  df-oprab 5900  df-mpo 5901  df-1st 6165  df-2nd 6166  df-recs 6330  df-irdg 6395  df-frec 6416  df-1o 6441  df-oadd 6445  df-er 6559  df-en 6767  df-dom 6768  df-fin 6769  df-sup 7013  df-pnf 8024  df-mnf 8025  df-xr 8026  df-ltxr 8027  df-le 8028  df-sub 8160  df-neg 8161  df-reap 8562  df-ap 8569  df-div 8660  df-inn 8950  df-2 9008  df-3 9009  df-4 9010  df-n0 9207  df-z 9284  df-uz 9559  df-q 9650  df-rp 9684  df-ico 9924  df-fz 10039  df-fzo 10173  df-seqfrec 10477  df-exp 10551  df-ihash 10788  df-cj 10883  df-re 10884  df-im 10885  df-rsqrt 11039  df-abs 11040  df-clim 11319  df-sumdc 11394
This theorem is referenced by:  mertensabs  11577
  Copyright terms: Public domain W3C validator