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