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

Theorem mertenslem2 11337
Description: Lemma for mertensabs 11338. (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 9385 . . 3 ℕ = (ℤ‘1)
2 1zzd 9105 . . 3 (𝜑 → 1 ∈ ℤ)
3 mertens.9 . . . . 5 (𝜑𝐸 ∈ ℝ+)
43rphalfcld 9526 . . . 4 (𝜑 → (𝐸 / 2) ∈ ℝ+)
5 nn0uz 9384 . . . . . 6 0 = (ℤ‘0)
6 0zd 9090 . . . . . 6 (𝜑 → 0 ∈ ℤ)
7 eqidd 2141 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → (𝐾𝑗) = (𝐾𝑗))
8 mertens.2 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → (𝐾𝑗) = (abs‘𝐴))
9 mertens.3 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → 𝐴 ∈ ℂ)
109abscld 10985 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → (abs‘𝐴) ∈ ℝ)
118, 10eqeltrd 2217 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → (𝐾𝑗) ∈ ℝ)
12 mertens.7 . . . . . 6 (𝜑 → seq0( + , 𝐾) ∈ dom ⇝ )
135, 6, 7, 11, 12isumrecl 11230 . . . . 5 (𝜑 → Σ𝑗 ∈ ℕ0 (𝐾𝑗) ∈ ℝ)
149absge0d 10988 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → 0 ≤ (abs‘𝐴))
1514, 8breqtrrd 3964 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → 0 ≤ (𝐾𝑗))
165, 6, 7, 11, 12, 15isumge0 11231 . . . . 5 (𝜑 → 0 ≤ Σ𝑗 ∈ ℕ0 (𝐾𝑗))
1713, 16ge0p1rpd 9544 . . . 4 (𝜑 → (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1) ∈ ℝ+)
184, 17rpdivcld 9531 . . 3 (𝜑 → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) ∈ ℝ+)
19 eqidd 2141 . . 3 ((𝜑𝑚 ∈ ℕ) → (seq0( + , 𝐺)‘𝑚) = (seq0( + , 𝐺)‘𝑚))
20 mertens.4 . . . 4 ((𝜑𝑘 ∈ ℕ0) → (𝐺𝑘) = 𝐵)
21 mertens.5 . . . 4 ((𝜑𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)
22 mertens.8 . . . 4 (𝜑 → seq0( + , 𝐺) ∈ dom ⇝ )
235, 6, 20, 21, 22isumclim2 11223 . . 3 (𝜑 → seq0( + , 𝐺) ⇝ Σ𝑘 ∈ ℕ0 𝐵)
241, 2, 18, 19, 23climi2 11089 . 2 (𝜑 → ∃𝑠 ∈ ℕ ∀𝑚 ∈ (ℤ𝑠)(abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
25 eluznn 9421 . . . . . . . 8 ((𝑠 ∈ ℕ ∧ 𝑚 ∈ (ℤ𝑠)) → 𝑚 ∈ ℕ)
2620, 21eqeltrd 2217 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → (𝐺𝑘) ∈ ℂ)
275, 6, 26serf 10278 . . . . . . . . . . . 12 (𝜑 → seq0( + , 𝐺):ℕ0⟶ℂ)
28 nnnn0 9008 . . . . . . . . . . . 12 (𝑚 ∈ ℕ → 𝑚 ∈ ℕ0)
29 ffvelrn 5561 . . . . . . . . . . . 12 ((seq0( + , 𝐺):ℕ0⟶ℂ ∧ 𝑚 ∈ ℕ0) → (seq0( + , 𝐺)‘𝑚) ∈ ℂ)
3027, 28, 29syl2an 287 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (seq0( + , 𝐺)‘𝑚) ∈ ℂ)
315, 6, 20, 21, 22isumcl 11226 . . . . . . . . . . . 12 (𝜑 → Σ𝑘 ∈ ℕ0 𝐵 ∈ ℂ)
3231adantr 274 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → Σ𝑘 ∈ ℕ0 𝐵 ∈ ℂ)
3330, 32abssubd 10997 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → (abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) = (abs‘(Σ𝑘 ∈ ℕ0 𝐵 − (seq0( + , 𝐺)‘𝑚))))
34 eqid 2140 . . . . . . . . . . . . . 14 (ℤ‘(𝑚 + 1)) = (ℤ‘(𝑚 + 1))
3528adantl 275 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ ℕ) → 𝑚 ∈ ℕ0)
36 peano2nn0 9041 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ℕ0 → (𝑚 + 1) ∈ ℕ0)
3735, 36syl 14 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → (𝑚 + 1) ∈ ℕ0)
3837nn0zd 9195 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → (𝑚 + 1) ∈ ℤ)
39 simpll 519 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (ℤ‘(𝑚 + 1))) → 𝜑)
40 eluznn0 9420 . . . . . . . . . . . . . . . 16 (((𝑚 + 1) ∈ ℕ0𝑘 ∈ (ℤ‘(𝑚 + 1))) → 𝑘 ∈ ℕ0)
4137, 40sylan 281 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (ℤ‘(𝑚 + 1))) → 𝑘 ∈ ℕ0)
4239, 41, 20syl2anc 409 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (ℤ‘(𝑚 + 1))) → (𝐺𝑘) = 𝐵)
4339, 41, 21syl2anc 409 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (ℤ‘(𝑚 + 1))) → 𝐵 ∈ ℂ)
4422adantr 274 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → seq0( + , 𝐺) ∈ dom ⇝ )
4526adantlr 469 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) ∈ ℂ)
465, 37, 45iserex 11140 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → (seq0( + , 𝐺) ∈ dom ⇝ ↔ seq(𝑚 + 1)( + , 𝐺) ∈ dom ⇝ ))
4744, 46mpbid 146 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → seq(𝑚 + 1)( + , 𝐺) ∈ dom ⇝ )
4834, 38, 42, 43, 47isumcl 11226 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → Σ𝑘 ∈ (ℤ‘(𝑚 + 1))𝐵 ∈ ℂ)
4930, 48pncan2d 8099 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → (((seq0( + , 𝐺)‘𝑚) + Σ𝑘 ∈ (ℤ‘(𝑚 + 1))𝐵) − (seq0( + , 𝐺)‘𝑚)) = Σ𝑘 ∈ (ℤ‘(𝑚 + 1))𝐵)
5020adantlr 469 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) = 𝐵)
5121adantlr 469 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)
525, 34, 37, 50, 51, 44isumsplit 11292 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → Σ𝑘 ∈ ℕ0 𝐵 = (Σ𝑘 ∈ (0...((𝑚 + 1) − 1))𝐵 + Σ𝑘 ∈ (ℤ‘(𝑚 + 1))𝐵))
53 nncn 8752 . . . . . . . . . . . . . . . . . . . 20 (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
5453adantl 275 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ ℕ) → 𝑚 ∈ ℂ)
55 ax-1cn 7737 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℂ
56 pncan 7992 . . . . . . . . . . . . . . . . . . 19 ((𝑚 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑚 + 1) − 1) = 𝑚)
5754, 55, 56sylancl 410 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ ℕ) → ((𝑚 + 1) − 1) = 𝑚)
5857oveq2d 5798 . . . . . . . . . . . . . . . . 17 ((𝜑𝑚 ∈ ℕ) → (0...((𝑚 + 1) − 1)) = (0...𝑚))
5958sumeq1d 11167 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ ℕ) → Σ𝑘 ∈ (0...((𝑚 + 1) − 1))𝐵 = Σ𝑘 ∈ (0...𝑚)𝐵)
60 elnn0uz 9387 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℕ0𝑘 ∈ (ℤ‘0))
6160, 50sylan2br 286 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (ℤ‘0)) → (𝐺𝑘) = 𝐵)
6235, 5eleqtrdi 2233 . . . . . . . . . . . . . . . . 17 ((𝜑𝑚 ∈ ℕ) → 𝑚 ∈ (ℤ‘0))
6360, 51sylan2br 286 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℕ) ∧ 𝑘 ∈ (ℤ‘0)) → 𝐵 ∈ ℂ)
6461, 62, 63fsum3ser 11198 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ ℕ) → Σ𝑘 ∈ (0...𝑚)𝐵 = (seq0( + , 𝐺)‘𝑚))
6559, 64eqtrd 2173 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → Σ𝑘 ∈ (0...((𝑚 + 1) − 1))𝐵 = (seq0( + , 𝐺)‘𝑚))
6665oveq1d 5797 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → (Σ𝑘 ∈ (0...((𝑚 + 1) − 1))𝐵 + Σ𝑘 ∈ (ℤ‘(𝑚 + 1))𝐵) = ((seq0( + , 𝐺)‘𝑚) + Σ𝑘 ∈ (ℤ‘(𝑚 + 1))𝐵))
6752, 66eqtrd 2173 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → Σ𝑘 ∈ ℕ0 𝐵 = ((seq0( + , 𝐺)‘𝑚) + Σ𝑘 ∈ (ℤ‘(𝑚 + 1))𝐵))
6867oveq1d 5797 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → (Σ𝑘 ∈ ℕ0 𝐵 − (seq0( + , 𝐺)‘𝑚)) = (((seq0( + , 𝐺)‘𝑚) + Σ𝑘 ∈ (ℤ‘(𝑚 + 1))𝐵) − (seq0( + , 𝐺)‘𝑚)))
6942sumeq2dv 11169 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → Σ𝑘 ∈ (ℤ‘(𝑚 + 1))(𝐺𝑘) = Σ𝑘 ∈ (ℤ‘(𝑚 + 1))𝐵)
7049, 68, 693eqtr4d 2183 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (Σ𝑘 ∈ ℕ0 𝐵 − (seq0( + , 𝐺)‘𝑚)) = Σ𝑘 ∈ (ℤ‘(𝑚 + 1))(𝐺𝑘))
7170fveq2d 5433 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → (abs‘(Σ𝑘 ∈ ℕ0 𝐵 − (seq0( + , 𝐺)‘𝑚))) = (abs‘Σ𝑘 ∈ (ℤ‘(𝑚 + 1))(𝐺𝑘)))
7233, 71eqtrd 2173 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → (abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) = (abs‘Σ𝑘 ∈ (ℤ‘(𝑚 + 1))(𝐺𝑘)))
7372breq1d 3947 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → ((abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) ↔ (abs‘Σ𝑘 ∈ (ℤ‘(𝑚 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
7425, 73sylan2 284 . . . . . . 7 ((𝜑 ∧ (𝑠 ∈ ℕ ∧ 𝑚 ∈ (ℤ𝑠))) → ((abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) ↔ (abs‘Σ𝑘 ∈ (ℤ‘(𝑚 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
7574anassrs 398 . . . . . 6 (((𝜑𝑠 ∈ ℕ) ∧ 𝑚 ∈ (ℤ𝑠)) → ((abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) ↔ (abs‘Σ𝑘 ∈ (ℤ‘(𝑚 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
7675ralbidva 2434 . . . . 5 ((𝜑𝑠 ∈ ℕ) → (∀𝑚 ∈ (ℤ𝑠)(abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) ↔ ∀𝑚 ∈ (ℤ𝑠)(abs‘Σ𝑘 ∈ (ℤ‘(𝑚 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
77 fvoveq1 5805 . . . . . . . . 9 (𝑚 = 𝑛 → (ℤ‘(𝑚 + 1)) = (ℤ‘(𝑛 + 1)))
7877sumeq1d 11167 . . . . . . . 8 (𝑚 = 𝑛 → Σ𝑘 ∈ (ℤ‘(𝑚 + 1))(𝐺𝑘) = Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘))
7978fveq2d 5433 . . . . . . 7 (𝑚 = 𝑛 → (abs‘Σ𝑘 ∈ (ℤ‘(𝑚 + 1))(𝐺𝑘)) = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)))
8079breq1d 3947 . . . . . 6 (𝑚 = 𝑛 → ((abs‘Σ𝑘 ∈ (ℤ‘(𝑚 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) ↔ (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
8180cbvralv 2657 . . . . 5 (∀𝑚 ∈ (ℤ𝑠)(abs‘Σ𝑘 ∈ (ℤ‘(𝑚 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) ↔ ∀𝑛 ∈ (ℤ𝑠)(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
8276, 81syl6bb 195 . . . 4 ((𝜑𝑠 ∈ ℕ) → (∀𝑚 ∈ (ℤ𝑠)(abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) ↔ ∀𝑛 ∈ (ℤ𝑠)(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
83 mertens.11 . . . . . 6 (𝜓 ↔ (𝑠 ∈ ℕ ∧ ∀𝑛 ∈ (ℤ𝑠)(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
84 0zd 9090 . . . . . . . . . 10 ((𝜑𝜓) → 0 ∈ ℤ)
854adantr 274 . . . . . . . . . . . 12 ((𝜑𝜓) → (𝐸 / 2) ∈ ℝ+)
8683simplbi 272 . . . . . . . . . . . . . 14 (𝜓𝑠 ∈ ℕ)
8786adantl 275 . . . . . . . . . . . . 13 ((𝜑𝜓) → 𝑠 ∈ ℕ)
8887nnrpd 9511 . . . . . . . . . . . 12 ((𝜑𝜓) → 𝑠 ∈ ℝ+)
8985, 88rpdivcld 9531 . . . . . . . . . . 11 ((𝜑𝜓) → ((𝐸 / 2) / 𝑠) ∈ ℝ+)
9087nnzd 9196 . . . . . . . . . . . . . . 15 ((𝜑𝜓) → 𝑠 ∈ ℤ)
91 1zzd 9105 . . . . . . . . . . . . . . 15 ((𝜑𝜓) → 1 ∈ ℤ)
9290, 91zsubcld 9202 . . . . . . . . . . . . . 14 ((𝜑𝜓) → (𝑠 − 1) ∈ ℤ)
9384, 92fzfigd 10235 . . . . . . . . . . . . 13 ((𝜑𝜓) → (0...(𝑠 − 1)) ∈ Fin)
94 eqid 2140 . . . . . . . . . . . . . . 15 (ℤ‘(𝑛 + 1)) = (ℤ‘(𝑛 + 1))
95 elfznn0 9925 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (0...(𝑠 − 1)) → 𝑛 ∈ ℕ0)
9695adantl 275 . . . . . . . . . . . . . . . . 17 (((𝜑𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → 𝑛 ∈ ℕ0)
97 peano2nn0 9041 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ0 → (𝑛 + 1) ∈ ℕ0)
9896, 97syl 14 . . . . . . . . . . . . . . . 16 (((𝜑𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → (𝑛 + 1) ∈ ℕ0)
9998nn0zd 9195 . . . . . . . . . . . . . . 15 (((𝜑𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → (𝑛 + 1) ∈ ℤ)
100 eqidd 2141 . . . . . . . . . . . . . . 15 ((((𝜑𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) ∧ 𝑘 ∈ (ℤ‘(𝑛 + 1))) → (𝐺𝑘) = (𝐺𝑘))
101 simplll 523 . . . . . . . . . . . . . . . 16 ((((𝜑𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) ∧ 𝑘 ∈ (ℤ‘(𝑛 + 1))) → 𝜑)
102 eluznn0 9420 . . . . . . . . . . . . . . . . 17 (((𝑛 + 1) ∈ ℕ0𝑘 ∈ (ℤ‘(𝑛 + 1))) → 𝑘 ∈ ℕ0)
10398, 102sylan 281 . . . . . . . . . . . . . . . 16 ((((𝜑𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) ∧ 𝑘 ∈ (ℤ‘(𝑛 + 1))) → 𝑘 ∈ ℕ0)
104101, 103, 26syl2anc 409 . . . . . . . . . . . . . . 15 ((((𝜑𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) ∧ 𝑘 ∈ (ℤ‘(𝑛 + 1))) → (𝐺𝑘) ∈ ℂ)
10522ad2antrr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → seq0( + , 𝐺) ∈ dom ⇝ )
106 simpll 519 . . . . . . . . . . . . . . . . . 18 (((𝜑𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → 𝜑)
107106, 26sylan 281 . . . . . . . . . . . . . . . . 17 ((((𝜑𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) ∈ ℂ)
1085, 98, 107iserex 11140 . . . . . . . . . . . . . . . 16 (((𝜑𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → (seq0( + , 𝐺) ∈ dom ⇝ ↔ seq(𝑛 + 1)( + , 𝐺) ∈ dom ⇝ ))
109105, 108mpbid 146 . . . . . . . . . . . . . . 15 (((𝜑𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → seq(𝑛 + 1)( + , 𝐺) ∈ dom ⇝ )
11094, 99, 100, 104, 109isumcl 11226 . . . . . . . . . . . . . 14 (((𝜑𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘) ∈ ℂ)
111110abscld 10985 . . . . . . . . . . . . 13 (((𝜑𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) ∈ ℝ)
11293, 111fsumrecl 11202 . . . . . . . . . . . 12 ((𝜑𝜓) → Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) ∈ ℝ)
113 0red 7791 . . . . . . . . . . . . 13 ((𝜑𝜓) → 0 ∈ ℝ)
114 nnnn0 9008 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
115114, 20sylan2 284 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (𝐺𝑘) = 𝐵)
116114, 21sylan2 284 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → 𝐵 ∈ ℂ)
117 1nn0 9017 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℕ0
118117a1i 9 . . . . . . . . . . . . . . . . . 18 (𝜑 → 1 ∈ ℕ0)
1195, 118, 26iserex 11140 . . . . . . . . . . . . . . . . 17 (𝜑 → (seq0( + , 𝐺) ∈ dom ⇝ ↔ seq1( + , 𝐺) ∈ dom ⇝ ))
12022, 119mpbid 146 . . . . . . . . . . . . . . . 16 (𝜑 → seq1( + , 𝐺) ∈ dom ⇝ )
1211, 2, 115, 116, 120isumcl 11226 . . . . . . . . . . . . . . 15 (𝜑 → Σ𝑘 ∈ ℕ 𝐵 ∈ ℂ)
122121adantr 274 . . . . . . . . . . . . . 14 ((𝜑𝜓) → Σ𝑘 ∈ ℕ 𝐵 ∈ ℂ)
123122abscld 10985 . . . . . . . . . . . . 13 ((𝜑𝜓) → (abs‘Σ𝑘 ∈ ℕ 𝐵) ∈ ℝ)
124122absge0d 10988 . . . . . . . . . . . . 13 ((𝜑𝜓) → 0 ≤ (abs‘Σ𝑘 ∈ ℕ 𝐵))
12520adantlr 469 . . . . . . . . . . . . . 14 (((𝜑𝜓) ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) = 𝐵)
12621adantlr 469 . . . . . . . . . . . . . 14 (((𝜑𝜓) ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)
12722adantr 274 . . . . . . . . . . . . . 14 ((𝜑𝜓) → seq0( + , 𝐺) ∈ dom ⇝ )
128 mertens.10 . . . . . . . . . . . . . 14 𝑇 = {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘))}
129 nnm1nn0 9042 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ ℕ → (𝑠 − 1) ∈ ℕ0)
13087, 129syl 14 . . . . . . . . . . . . . . . . . 18 ((𝜑𝜓) → (𝑠 − 1) ∈ ℕ0)
131130, 5eleqtrdi 2233 . . . . . . . . . . . . . . . . 17 ((𝜑𝜓) → (𝑠 − 1) ∈ (ℤ‘0))
132 eluzfz1 9842 . . . . . . . . . . . . . . . . 17 ((𝑠 − 1) ∈ (ℤ‘0) → 0 ∈ (0...(𝑠 − 1)))
133131, 132syl 14 . . . . . . . . . . . . . . . 16 ((𝜑𝜓) → 0 ∈ (0...(𝑠 − 1)))
134115sumeq2dv 11169 . . . . . . . . . . . . . . . . . . 19 (𝜑 → Σ𝑘 ∈ ℕ (𝐺𝑘) = Σ𝑘 ∈ ℕ 𝐵)
135134adantr 274 . . . . . . . . . . . . . . . . . 18 ((𝜑𝜓) → Σ𝑘 ∈ ℕ (𝐺𝑘) = Σ𝑘 ∈ ℕ 𝐵)
136135fveq2d 5433 . . . . . . . . . . . . . . . . 17 ((𝜑𝜓) → (abs‘Σ𝑘 ∈ ℕ (𝐺𝑘)) = (abs‘Σ𝑘 ∈ ℕ 𝐵))
137136eqcomd 2146 . . . . . . . . . . . . . . . 16 ((𝜑𝜓) → (abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈ ℕ (𝐺𝑘)))
138 fv0p1e1 8859 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 0 → (ℤ‘(𝑛 + 1)) = (ℤ‘1))
139138, 1eqtr4di 2191 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 0 → (ℤ‘(𝑛 + 1)) = ℕ)
140139sumeq1d 11167 . . . . . . . . . . . . . . . . . 18 (𝑛 = 0 → Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘) = Σ𝑘 ∈ ℕ (𝐺𝑘))
141140fveq2d 5433 . . . . . . . . . . . . . . . . 17 (𝑛 = 0 → (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) = (abs‘Σ𝑘 ∈ ℕ (𝐺𝑘)))
142141rspceeqv 2811 . . . . . . . . . . . . . . . 16 ((0 ∈ (0...(𝑠 − 1)) ∧ (abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈ ℕ (𝐺𝑘))) → ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)))
143133, 137, 142syl2anc 409 . . . . . . . . . . . . . . 15 ((𝜑𝜓) → ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)))
144 eqeq1 2147 . . . . . . . . . . . . . . . . . 18 (𝑧 = (abs‘Σ𝑘 ∈ ℕ 𝐵) → (𝑧 = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) ↔ (abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘))))
145144rexbidv 2439 . . . . . . . . . . . . . . . . 17 (𝑧 = (abs‘Σ𝑘 ∈ ℕ 𝐵) → (∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) ↔ ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘))))
146145, 128elab2g 2835 . . . . . . . . . . . . . . . 16 ((abs‘Σ𝑘 ∈ ℕ 𝐵) ∈ ℝ → ((abs‘Σ𝑘 ∈ ℕ 𝐵) ∈ 𝑇 ↔ ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘))))
147123, 146syl 14 . . . . . . . . . . . . . . 15 ((𝜑𝜓) → ((abs‘Σ𝑘 ∈ ℕ 𝐵) ∈ 𝑇 ↔ ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘))))
148143, 147mpbird 166 . . . . . . . . . . . . . 14 ((𝜑𝜓) → (abs‘Σ𝑘 ∈ ℕ 𝐵) ∈ 𝑇)
149125, 126, 127, 128, 148, 87mertenslemub 11335 . . . . . . . . . . . . 13 ((𝜑𝜓) → (abs‘Σ𝑘 ∈ ℕ 𝐵) ≤ Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)))
150113, 123, 112, 124, 149letrd 7910 . . . . . . . . . . . 12 ((𝜑𝜓) → 0 ≤ Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)))
151112, 150ge0p1rpd 9544 . . . . . . . . . . 11 ((𝜑𝜓) → (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) + 1) ∈ ℝ+)
15289, 151rpdivcld 9531 . . . . . . . . . 10 ((𝜑𝜓) → (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) + 1)) ∈ ℝ+)
153 simpr 109 . . . . . . . . . . 11 (((𝜑𝜓) ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈ ℕ0)
154 fveq2 5429 . . . . . . . . . . . . 13 (𝑗 = 𝑚 → (𝐾𝑗) = (𝐾𝑚))
155154eleq1d 2209 . . . . . . . . . . . 12 (𝑗 = 𝑚 → ((𝐾𝑗) ∈ ℝ ↔ (𝐾𝑚) ∈ ℝ))
15611ralrimiva 2508 . . . . . . . . . . . . 13 (𝜑 → ∀𝑗 ∈ ℕ0 (𝐾𝑗) ∈ ℝ)
157156ad2antrr 480 . . . . . . . . . . . 12 (((𝜑𝜓) ∧ 𝑚 ∈ ℕ0) → ∀𝑗 ∈ ℕ0 (𝐾𝑗) ∈ ℝ)
158155, 157, 153rspcdva 2798 . . . . . . . . . . 11 (((𝜑𝜓) ∧ 𝑚 ∈ ℕ0) → (𝐾𝑚) ∈ ℝ)
159 fveq2 5429 . . . . . . . . . . . 12 (𝑛 = 𝑚 → (𝐾𝑛) = (𝐾𝑚))
160 eqid 2140 . . . . . . . . . . . 12 (𝑛 ∈ ℕ0 ↦ (𝐾𝑛)) = (𝑛 ∈ ℕ0 ↦ (𝐾𝑛))
161159, 160fvmptg 5505 . . . . . . . . . . 11 ((𝑚 ∈ ℕ0 ∧ (𝐾𝑚) ∈ ℝ) → ((𝑛 ∈ ℕ0 ↦ (𝐾𝑛))‘𝑚) = (𝐾𝑚))
162153, 158, 161syl2anc 409 . . . . . . . . . 10 (((𝜑𝜓) ∧ 𝑚 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (𝐾𝑛))‘𝑚) = (𝐾𝑚))
163 nn0ex 9007 . . . . . . . . . . . . . 14 0 ∈ V
164163mptex 5654 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ0 ↦ (𝐾𝑛)) ∈ V
165164a1i 9 . . . . . . . . . . . 12 (𝜑 → (𝑛 ∈ ℕ0 ↦ (𝐾𝑛)) ∈ V)
16660biimpri 132 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (ℤ‘0) → 𝑘 ∈ ℕ0)
167 fveq2 5429 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑘 → (𝐾𝑗) = (𝐾𝑘))
168167eleq1d 2209 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑘 → ((𝐾𝑗) ∈ ℝ ↔ (𝐾𝑘) ∈ ℝ))
169156adantr 274 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ0) → ∀𝑗 ∈ ℕ0 (𝐾𝑗) ∈ ℝ)
170 simpr 109 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
171168, 169, 170rspcdva 2798 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ℕ0) → (𝐾𝑘) ∈ ℝ)
17260, 171sylan2br 286 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (ℤ‘0)) → (𝐾𝑘) ∈ ℝ)
173 fveq2 5429 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑘 → (𝐾𝑛) = (𝐾𝑘))
174173, 160fvmptg 5505 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ0 ∧ (𝐾𝑘) ∈ ℝ) → ((𝑛 ∈ ℕ0 ↦ (𝐾𝑛))‘𝑘) = (𝐾𝑘))
175166, 172, 174syl2an2 584 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (ℤ‘0)) → ((𝑛 ∈ ℕ0 ↦ (𝐾𝑛))‘𝑘) = (𝐾𝑘))
176175, 172eqeltrd 2217 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (ℤ‘0)) → ((𝑛 ∈ ℕ0 ↦ (𝐾𝑛))‘𝑘) ∈ ℝ)
177 elnn0uz 9387 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ0𝑗 ∈ (ℤ‘0))
178 simpr 109 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ0) → 𝑗 ∈ ℕ0)
179 fveq2 5429 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑗 → (𝐾𝑛) = (𝐾𝑗))
180179, 160fvmptg 5505 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ ℕ0 ∧ (𝐾𝑗) ∈ ℝ) → ((𝑛 ∈ ℕ0 ↦ (𝐾𝑛))‘𝑗) = (𝐾𝑗))
181178, 11, 180syl2anc 409 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (𝐾𝑛))‘𝑗) = (𝐾𝑗))
182177, 181sylan2br 286 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℤ‘0)) → ((𝑛 ∈ ℕ0 ↦ (𝐾𝑛))‘𝑗) = (𝐾𝑗))
183 readdcl 7770 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑘 + 𝑦) ∈ ℝ)
184183adantl 275 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑘 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑘 + 𝑦) ∈ ℝ)
1856, 176, 182, 184seq3feq 10276 . . . . . . . . . . . . 13 (𝜑 → seq0( + , (𝑛 ∈ ℕ0 ↦ (𝐾𝑛))) = seq0( + , 𝐾))
186185, 12eqeltrd 2217 . . . . . . . . . . . 12 (𝜑 → seq0( + , (𝑛 ∈ ℕ0 ↦ (𝐾𝑛))) ∈ dom ⇝ )
187181, 11eqeltrd 2217 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (𝐾𝑛))‘𝑗) ∈ ℝ)
188187recnd 7818 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (𝐾𝑛))‘𝑗) ∈ ℂ)
1895, 6, 165, 186, 188serf0 11153 . . . . . . . . . . 11 (𝜑 → (𝑛 ∈ ℕ0 ↦ (𝐾𝑛)) ⇝ 0)
190189adantr 274 . . . . . . . . . 10 ((𝜑𝜓) → (𝑛 ∈ ℕ0 ↦ (𝐾𝑛)) ⇝ 0)
1915, 84, 152, 162, 190climi0 11090 . . . . . . . . 9 ((𝜑𝜓) → ∃𝑡 ∈ ℕ0𝑚 ∈ (ℤ𝑡)(abs‘(𝐾𝑚)) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) + 1)))
192 fveq2 5429 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑎 → (𝐺𝑘) = (𝐺𝑎))
193192cbvsumv 11162 . . . . . . . . . . . . . . . . 17 Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘) = Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)
194193fveq2i 5432 . . . . . . . . . . . . . . . 16 (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) = (abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎))
195194a1i 9 . . . . . . . . . . . . . . 15 (𝑛 ∈ (0...(𝑠 − 1)) → (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) = (abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)))
196195sumeq2i 11165 . . . . . . . . . . . . . 14 Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) = Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎))
197196oveq1i 5792 . . . . . . . . . . . . 13 𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) + 1) = (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)
198197oveq2i 5793 . . . . . . . . . . . 12 (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) + 1)) = (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1))
199198breq2i 3945 . . . . . . . . . . 11 ((abs‘(𝐾𝑚)) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) + 1)) ↔ (abs‘(𝐾𝑚)) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))
200199ralbii 2444 . . . . . . . . . 10 (∀𝑚 ∈ (ℤ𝑡)(abs‘(𝐾𝑚)) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) + 1)) ↔ ∀𝑚 ∈ (ℤ𝑡)(abs‘(𝐾𝑚)) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))
201200rexbii 2445 . . . . . . . . 9 (∃𝑡 ∈ ℕ0𝑚 ∈ (ℤ𝑡)(abs‘(𝐾𝑚)) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) + 1)) ↔ ∃𝑡 ∈ ℕ0𝑚 ∈ (ℤ𝑡)(abs‘(𝐾𝑚)) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))
202191, 201sylib 121 . . . . . . . 8 ((𝜑𝜓) → ∃𝑡 ∈ ℕ0𝑚 ∈ (ℤ𝑡)(abs‘(𝐾𝑚)) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))
203 simplll 523 . . . . . . . . . . . . . 14 ((((𝜑𝜓) ∧ 𝑡 ∈ ℕ0) ∧ 𝑚 ∈ (ℤ𝑡)) → 𝜑)
204 eluznn0 9420 . . . . . . . . . . . . . . 15 ((𝑡 ∈ ℕ0𝑚 ∈ (ℤ𝑡)) → 𝑚 ∈ ℕ0)
205204adantll 468 . . . . . . . . . . . . . 14 ((((𝜑𝜓) ∧ 𝑡 ∈ ℕ0) ∧ 𝑚 ∈ (ℤ𝑡)) → 𝑚 ∈ ℕ0)
20611, 15absidd 10971 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ0) → (abs‘(𝐾𝑗)) = (𝐾𝑗))
207206ralrimiva 2508 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑗 ∈ ℕ0 (abs‘(𝐾𝑗)) = (𝐾𝑗))
208154fveq2d 5433 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑚 → (abs‘(𝐾𝑗)) = (abs‘(𝐾𝑚)))
209208, 154eqeq12d 2155 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑚 → ((abs‘(𝐾𝑗)) = (𝐾𝑗) ↔ (abs‘(𝐾𝑚)) = (𝐾𝑚)))
210209rspccva 2792 . . . . . . . . . . . . . . 15 ((∀𝑗 ∈ ℕ0 (abs‘(𝐾𝑗)) = (𝐾𝑗) ∧ 𝑚 ∈ ℕ0) → (abs‘(𝐾𝑚)) = (𝐾𝑚))
211207, 210sylan 281 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ0) → (abs‘(𝐾𝑚)) = (𝐾𝑚))
212203, 205, 211syl2anc 409 . . . . . . . . . . . . 13 ((((𝜑𝜓) ∧ 𝑡 ∈ ℕ0) ∧ 𝑚 ∈ (ℤ𝑡)) → (abs‘(𝐾𝑚)) = (𝐾𝑚))
213212breq1d 3947 . . . . . . . . . . . 12 ((((𝜑𝜓) ∧ 𝑡 ∈ ℕ0) ∧ 𝑚 ∈ (ℤ𝑡)) → ((abs‘(𝐾𝑚)) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)) ↔ (𝐾𝑚) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1))))
214213ralbidva 2434 . . . . . . . . . . 11 (((𝜑𝜓) ∧ 𝑡 ∈ ℕ0) → (∀𝑚 ∈ (ℤ𝑡)(abs‘(𝐾𝑚)) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)) ↔ ∀𝑚 ∈ (ℤ𝑡)(𝐾𝑚) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1))))
215 nfv 1509 . . . . . . . . . . . 12 𝑚(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1))
216 nfcv 2282 . . . . . . . . . . . . 13 𝑛(𝐾𝑚)
217 nfcv 2282 . . . . . . . . . . . . 13 𝑛 <
218 nfcv 2282 . . . . . . . . . . . . . 14 𝑛((𝐸 / 2) / 𝑠)
219 nfcv 2282 . . . . . . . . . . . . . 14 𝑛 /
220 nfcv 2282 . . . . . . . . . . . . . . . 16 𝑛(0...(𝑠 − 1))
221220nfsum1 11157 . . . . . . . . . . . . . . 15 𝑛Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎))
222 nfcv 2282 . . . . . . . . . . . . . . 15 𝑛 +
223 nfcv 2282 . . . . . . . . . . . . . . 15 𝑛1
224221, 222, 223nfov 5809 . . . . . . . . . . . . . 14 𝑛𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)
225218, 219, 224nfov 5809 . . . . . . . . . . . . 13 𝑛(((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1))
226216, 217, 225nfbr 3982 . . . . . . . . . . . 12 𝑛(𝐾𝑚) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1))
227159breq1d 3947 . . . . . . . . . . . 12 (𝑛 = 𝑚 → ((𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)) ↔ (𝐾𝑚) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1))))
228215, 226, 227cbvral 2653 . . . . . . . . . . 11 (∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)) ↔ ∀𝑚 ∈ (ℤ𝑡)(𝐾𝑚) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))
229214, 228syl6bbr 197 . . . . . . . . . 10 (((𝜑𝜓) ∧ 𝑡 ∈ ℕ0) → (∀𝑚 ∈ (ℤ𝑡)(abs‘(𝐾𝑚)) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)) ↔ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1))))
230 simpll 519 . . . . . . . . . . . . 13 (((𝜑𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))) → 𝜑)
231 mertens.1 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ0) → (𝐹𝑗) = 𝐴)
232230, 231sylan 281 . . . . . . . . . . . 12 ((((𝜑𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))) ∧ 𝑗 ∈ ℕ0) → (𝐹𝑗) = 𝐴)
233230, 8sylan 281 . . . . . . . . . . . 12 ((((𝜑𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))) ∧ 𝑗 ∈ ℕ0) → (𝐾𝑗) = (abs‘𝐴))
234230, 9sylan 281 . . . . . . . . . . . 12 ((((𝜑𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))) ∧ 𝑗 ∈ ℕ0) → 𝐴 ∈ ℂ)
235230, 20sylan 281 . . . . . . . . . . . 12 ((((𝜑𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))) ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) = 𝐵)
236230, 21sylan 281 . . . . . . . . . . . 12 ((((𝜑𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))) ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)
237 mertens.6 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → (𝐻𝑘) = Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘𝑗))))
238230, 237sylan 281 . . . . . . . . . . . 12 ((((𝜑𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))) ∧ 𝑘 ∈ ℕ0) → (𝐻𝑘) = Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘𝑗))))
23912ad2antrr 480 . . . . . . . . . . . 12 (((𝜑𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))) → seq0( + , 𝐾) ∈ dom ⇝ )
24022ad2antrr 480 . . . . . . . . . . . 12 (((𝜑𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))) → seq0( + , 𝐺) ∈ dom ⇝ )
2413ad2antrr 480 . . . . . . . . . . . 12 (((𝜑𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))) → 𝐸 ∈ ℝ+)
242196, 112eqeltrrid 2228 . . . . . . . . . . . . 13 ((𝜑𝜓) → Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) ∈ ℝ)
243242adantr 274 . . . . . . . . . . . 12 (((𝜑𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))) → Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) ∈ ℝ)
244228anbi2i 453 . . . . . . . . . . . . . . 15 ((𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1))) ↔ (𝑡 ∈ ℕ0 ∧ ∀𝑚 ∈ (ℤ𝑡)(𝐾𝑚) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1))))
245244anbi2i 453 . . . . . . . . . . . . . 14 ((𝜓 ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))) ↔ (𝜓 ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑚 ∈ (ℤ𝑡)(𝐾𝑚) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))))
246245biimpi 119 . . . . . . . . . . . . 13 ((𝜓 ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))) → (𝜓 ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑚 ∈ (ℤ𝑡)(𝐾𝑚) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))))
247246adantll 468 . . . . . . . . . . . 12 (((𝜑𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))) → (𝜓 ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑚 ∈ (ℤ𝑡)(𝐾𝑚) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))))
248150, 196breqtrdi 3977 . . . . . . . . . . . . 13 ((𝜑𝜓) → 0 ≤ Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)))
249248adantr 274 . . . . . . . . . . . 12 (((𝜑𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))) → 0 ≤ Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)))
250 simpr 109 . . . . . . . . . . . . . . . 16 ((((𝜑𝜓) ∧ 𝑤𝑇) ∧ 𝑎 ∈ ℕ0) → 𝑎 ∈ ℕ0)
25120ralrimiva 2508 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑘 ∈ ℕ0 (𝐺𝑘) = 𝐵)
252251ad3antrrr 484 . . . . . . . . . . . . . . . 16 ((((𝜑𝜓) ∧ 𝑤𝑇) ∧ 𝑎 ∈ ℕ0) → ∀𝑘 ∈ ℕ0 (𝐺𝑘) = 𝐵)
253 nfcsb1v 3040 . . . . . . . . . . . . . . . . . 18 𝑘𝑎 / 𝑘𝐵
254253nfeq2 2294 . . . . . . . . . . . . . . . . 17 𝑘(𝐺𝑎) = 𝑎 / 𝑘𝐵
255 csbeq1a 3016 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑎𝐵 = 𝑎 / 𝑘𝐵)
256192, 255eqeq12d 2155 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑎 → ((𝐺𝑘) = 𝐵 ↔ (𝐺𝑎) = 𝑎 / 𝑘𝐵))
257254, 256rspc 2787 . . . . . . . . . . . . . . . 16 (𝑎 ∈ ℕ0 → (∀𝑘 ∈ ℕ0 (𝐺𝑘) = 𝐵 → (𝐺𝑎) = 𝑎 / 𝑘𝐵))
258250, 252, 257sylc 62 . . . . . . . . . . . . . . 15 ((((𝜑𝜓) ∧ 𝑤𝑇) ∧ 𝑎 ∈ ℕ0) → (𝐺𝑎) = 𝑎 / 𝑘𝐵)
25921ralrimiva 2508 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑘 ∈ ℕ0 𝐵 ∈ ℂ)
260259ad3antrrr 484 . . . . . . . . . . . . . . . 16 ((((𝜑𝜓) ∧ 𝑤𝑇) ∧ 𝑎 ∈ ℕ0) → ∀𝑘 ∈ ℕ0 𝐵 ∈ ℂ)
261253nfel1 2293 . . . . . . . . . . . . . . . . 17 𝑘𝑎 / 𝑘𝐵 ∈ ℂ
262255eleq1d 2209 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑎 → (𝐵 ∈ ℂ ↔ 𝑎 / 𝑘𝐵 ∈ ℂ))
263261, 262rspc 2787 . . . . . . . . . . . . . . . 16 (𝑎 ∈ ℕ0 → (∀𝑘 ∈ ℕ0 𝐵 ∈ ℂ → 𝑎 / 𝑘𝐵 ∈ ℂ))
264250, 260, 263sylc 62 . . . . . . . . . . . . . . 15 ((((𝜑𝜓) ∧ 𝑤𝑇) ∧ 𝑎 ∈ ℕ0) → 𝑎 / 𝑘𝐵 ∈ ℂ)
26522ad2antrr 480 . . . . . . . . . . . . . . 15 (((𝜑𝜓) ∧ 𝑤𝑇) → seq0( + , 𝐺) ∈ dom ⇝ )
266194eqeq2i 2151 . . . . . . . . . . . . . . . . . 18 (𝑧 = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) ↔ 𝑧 = (abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)))
267266rexbii 2445 . . . . . . . . . . . . . . . . 17 (∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) ↔ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)))
268267abbii 2256 . . . . . . . . . . . . . . . 16 {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘))} = {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎))}
269128, 268eqtri 2161 . . . . . . . . . . . . . . 15 𝑇 = {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎))}
270 simpr 109 . . . . . . . . . . . . . . 15 (((𝜑𝜓) ∧ 𝑤𝑇) → 𝑤𝑇)
27187adantr 274 . . . . . . . . . . . . . . 15 (((𝜑𝜓) ∧ 𝑤𝑇) → 𝑠 ∈ ℕ)
272258, 264, 265, 269, 270, 271mertenslemub 11335 . . . . . . . . . . . . . 14 (((𝜑𝜓) ∧ 𝑤𝑇) → 𝑤 ≤ Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)))
273272ralrimiva 2508 . . . . . . . . . . . . 13 ((𝜑𝜓) → ∀𝑤𝑇 𝑤 ≤ Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)))
274273adantr 274 . . . . . . . . . . . 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 11336 . . . . . . . . . . 11 (((𝜑𝜓) ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)))) → ∃𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸)
276275expr 373 . . . . . . . . . 10 (((𝜑𝜓) ∧ 𝑡 ∈ ℕ0) → (∀𝑛 ∈ (ℤ𝑡)(𝐾𝑛) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)) → ∃𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸))
277229, 276sylbid 149 . . . . . . . . 9 (((𝜑𝜓) ∧ 𝑡 ∈ ℕ0) → (∀𝑚 ∈ (ℤ𝑡)(abs‘(𝐾𝑚)) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)) → ∃𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸))
278277rexlimdva 2552 . . . . . . . 8 ((𝜑𝜓) → (∃𝑡 ∈ ℕ0𝑚 ∈ (ℤ𝑡)(abs‘(𝐾𝑚)) < (((𝐸 / 2) / 𝑠) / (Σ𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑎 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑎)) + 1)) → ∃𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸))
279202, 278mpd 13 . . . . . . 7 ((𝜑𝜓) → ∃𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸)
280279ex 114 . . . . . 6 (𝜑 → (𝜓 → ∃𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸))
28183, 280syl5bir 152 . . . . 5 (𝜑 → ((𝑠 ∈ ℕ ∧ ∀𝑛 ∈ (ℤ𝑠)(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))) → ∃𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸))
282281expdimp 257 . . . 4 ((𝜑𝑠 ∈ ℕ) → (∀𝑛 ∈ (ℤ𝑠)(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) → ∃𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸))
28382, 282sylbid 149 . . 3 ((𝜑𝑠 ∈ ℕ) → (∀𝑚 ∈ (ℤ𝑠)(abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) → ∃𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝐸))
284283rexlimdva 2552 . 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 103  wb 104   = wceq 1332  wcel 1481  {cab 2126  wral 2417  wrex 2418  Vcvv 2689  csb 3007   class class class wbr 3937  cmpt 3997  dom cdm 4547  wf 5127  cfv 5131  (class class class)co 5782  cc 7642  cr 7643  0cc0 7644  1c1 7645   + caddc 7647   · cmul 7649   < clt 7824  cle 7825  cmin 7957   / cdiv 8456  cn 8744  2c2 8795  0cn0 9001  cuz 9350  +crp 9470  ...cfz 9821  seqcseq 10249  abscabs 10801  cli 11079  Σcsu 11154
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 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4051  ax-sep 4054  ax-nul 4062  ax-pow 4106  ax-pr 4139  ax-un 4363  ax-setind 4460  ax-iinf 4510  ax-cnex 7735  ax-resscn 7736  ax-1cn 7737  ax-1re 7738  ax-icn 7739  ax-addcl 7740  ax-addrcl 7741  ax-mulcl 7742  ax-mulrcl 7743  ax-addcom 7744  ax-mulcom 7745  ax-addass 7746  ax-mulass 7747  ax-distr 7748  ax-i2m1 7749  ax-0lt1 7750  ax-1rid 7751  ax-0id 7752  ax-rnegex 7753  ax-precex 7754  ax-cnre 7755  ax-pre-ltirr 7756  ax-pre-ltwlin 7757  ax-pre-lttrn 7758  ax-pre-apti 7759  ax-pre-ltadd 7760  ax-pre-mulgt0 7761  ax-pre-mulext 7762  ax-arch 7763  ax-caucvg 7764
This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-nel 2405  df-ral 2422  df-rex 2423  df-reu 2424  df-rmo 2425  df-rab 2426  df-v 2691  df-sbc 2914  df-csb 3008  df-dif 3078  df-un 3080  df-in 3082  df-ss 3089  df-nul 3369  df-if 3480  df-pw 3517  df-sn 3538  df-pr 3539  df-op 3541  df-uni 3745  df-int 3780  df-iun 3823  df-br 3938  df-opab 3998  df-mpt 3999  df-tr 4035  df-id 4223  df-po 4226  df-iso 4227  df-iord 4296  df-on 4298  df-ilim 4299  df-suc 4301  df-iom 4513  df-xp 4553  df-rel 4554  df-cnv 4555  df-co 4556  df-dm 4557  df-rn 4558  df-res 4559  df-ima 4560  df-iota 5096  df-fun 5133  df-fn 5134  df-f 5135  df-f1 5136  df-fo 5137  df-f1o 5138  df-fv 5139  df-isom 5140  df-riota 5738  df-ov 5785  df-oprab 5786  df-mpo 5787  df-1st 6046  df-2nd 6047  df-recs 6210  df-irdg 6275  df-frec 6296  df-1o 6321  df-oadd 6325  df-er 6437  df-en 6643  df-dom 6644  df-fin 6645  df-sup 6879  df-pnf 7826  df-mnf 7827  df-xr 7828  df-ltxr 7829  df-le 7830  df-sub 7959  df-neg 7960  df-reap 8361  df-ap 8368  df-div 8457  df-inn 8745  df-2 8803  df-3 8804  df-4 8805  df-n0 9002  df-z 9079  df-uz 9351  df-q 9439  df-rp 9471  df-ico 9707  df-fz 9822  df-fzo 9951  df-seqfrec 10250  df-exp 10324  df-ihash 10554  df-cj 10646  df-re 10647  df-im 10648  df-rsqrt 10802  df-abs 10803  df-clim 11080  df-sumdc 11155
This theorem is referenced by:  mertensabs  11338
  Copyright terms: Public domain W3C validator