This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mertenslem2

Description: Lemma for mertens . (Contributed by Mario Carneiro, 28-Apr-2014)

Ref Expression
Hypotheses mertens.1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑗 ) = 𝐴 )
mertens.2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐾 ‘ 𝑗 ) = ( abs ‘ 𝐴 ) )
mertens.3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
mertens.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑘 ) = 𝐵 )
mertens.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐵 ∈ ℂ )
mertens.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐻 ‘ 𝑘 ) = Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( 𝐴 · ( 𝐺 ‘ ( 𝑘 − 𝑗 ) ) ) )
mertens.7 ⊢ ( 𝜑 → seq 0 ( + , 𝐾 ) ∈ dom ⇝ )
mertens.8 ⊢ ( 𝜑 → seq 0 ( + , 𝐺 ) ∈ dom ⇝ )
mertens.9 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
mertens.10 ⊢ 𝑇 = { 𝑧 ∣ ∃ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) 𝑧 = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) }
mertens.11 ⊢ ( 𝜓 ↔ ( 𝑠 ∈ ℕ ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑠 ) ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ) )
Assertion mertenslem2 ( 𝜑 → ∃ 𝑦 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) ) < 𝐸 )

Proof

Step Hyp Ref Expression
1 mertens.1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑗 ) = 𝐴 )
2 mertens.2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐾 ‘ 𝑗 ) = ( abs ‘ 𝐴 ) )
3 mertens.3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
4 mertens.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑘 ) = 𝐵 )
5 mertens.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐵 ∈ ℂ )
6 mertens.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐻 ‘ 𝑘 ) = Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( 𝐴 · ( 𝐺 ‘ ( 𝑘 − 𝑗 ) ) ) )
7 mertens.7 ⊢ ( 𝜑 → seq 0 ( + , 𝐾 ) ∈ dom ⇝ )
8 mertens.8 ⊢ ( 𝜑 → seq 0 ( + , 𝐺 ) ∈ dom ⇝ )
9 mertens.9 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
10 mertens.10 ⊢ 𝑇 = { 𝑧 ∣ ∃ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) 𝑧 = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) }
11 mertens.11 ⊢ ( 𝜓 ↔ ( 𝑠 ∈ ℕ ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑠 ) ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ) )
12 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
13 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
14 9 rphalfcld ⊢ ( 𝜑 → ( 𝐸 / 2 ) ∈ ℝ+ )
15 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
16 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
17 eqidd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐾 ‘ 𝑗 ) = ( 𝐾 ‘ 𝑗 ) )
18 3 abscld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( abs ‘ 𝐴 ) ∈ ℝ )
19 2 18 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐾 ‘ 𝑗 ) ∈ ℝ )
20 15 16 17 19 7 isumrecl ⊢ ( 𝜑 → Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) ∈ ℝ )
21 3 absge0d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → 0 ≤ ( abs ‘ 𝐴 ) )
22 21 2 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → 0 ≤ ( 𝐾 ‘ 𝑗 ) )
23 15 16 17 19 7 22 isumge0 ⊢ ( 𝜑 → 0 ≤ Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) )
24 20 23 ge0p1rpd ⊢ ( 𝜑 → ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ∈ ℝ+ )
25 14 24 rpdivcld ⊢ ( 𝜑 → ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ∈ ℝ+ )
26 eqidd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) = ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) )
27 15 16 4 5 8 isumclim2 ⊢ ( 𝜑 → seq 0 ( + , 𝐺 ) ⇝ Σ 𝑘 ∈ ℕ0 𝐵 )
28 12 13 25 26 27 climi2 ⊢ ( 𝜑 → ∃ 𝑠 ∈ ℕ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑠 ) ( abs ‘ ( ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) − Σ 𝑘 ∈ ℕ0 𝐵 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) )
29 eluznn ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑠 ) ) → 𝑚 ∈ ℕ )
30 4 5 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
31 15 16 30 serf ⊢ ( 𝜑 → seq 0 ( + , 𝐺 ) : ℕ0 ⟶ ℂ )
32 nnnn0 ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℕ0 )
33 ffvelcdm ⊢ ( ( seq 0 ( + , 𝐺 ) : ℕ0 ⟶ ℂ ∧ 𝑚 ∈ ℕ0 ) → ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) ∈ ℂ )
34 31 32 33 syl2an ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) ∈ ℂ )
35 15 16 4 5 8 isumcl ⊢ ( 𝜑 → Σ 𝑘 ∈ ℕ0 𝐵 ∈ ℂ )
36 35 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → Σ 𝑘 ∈ ℕ0 𝐵 ∈ ℂ )
37 34 36 abssubd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( abs ‘ ( ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) − Σ 𝑘 ∈ ℕ0 𝐵 ) ) = ( abs ‘ ( Σ 𝑘 ∈ ℕ0 𝐵 − ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) ) ) )
38 eqid ⊢ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) = ( ℤ≥ ‘ ( 𝑚 + 1 ) )
39 32 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℕ0 )
40 peano2nn0 ⊢ ( 𝑚 ∈ ℕ0 → ( 𝑚 + 1 ) ∈ ℕ0 )
41 39 40 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑚 + 1 ) ∈ ℕ0 )
42 41 nn0zd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑚 + 1 ) ∈ ℤ )
43 simpll ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) → 𝜑 )
44 eluznn0 ⊢ ( ( ( 𝑚 + 1 ) ∈ ℕ0 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) → 𝑘 ∈ ℕ0 )
45 41 44 sylan ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) → 𝑘 ∈ ℕ0 )
46 43 45 4 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) → ( 𝐺 ‘ 𝑘 ) = 𝐵 )
47 43 45 5 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) → 𝐵 ∈ ℂ )
48 8 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → seq 0 ( + , 𝐺 ) ∈ dom ⇝ )
49 30 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
50 15 41 49 iserex ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( seq 0 ( + , 𝐺 ) ∈ dom ⇝ ↔ seq ( 𝑚 + 1 ) ( + , 𝐺 ) ∈ dom ⇝ ) )
51 48 50 mpbid ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → seq ( 𝑚 + 1 ) ( + , 𝐺 ) ∈ dom ⇝ )
52 38 42 46 47 51 isumcl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) 𝐵 ∈ ℂ )
53 34 52 pncan2d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) 𝐵 ) − ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) ) = Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) 𝐵 )
54 4 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑘 ) = 𝐵 )
55 5 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ℕ0 ) → 𝐵 ∈ ℂ )
56 15 38 41 54 55 48 isumsplit ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → Σ 𝑘 ∈ ℕ0 𝐵 = ( Σ 𝑘 ∈ ( 0 ... ( ( 𝑚 + 1 ) − 1 ) ) 𝐵 + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) 𝐵 ) )
57 nncn ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℂ )
58 57 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℂ )
59 ax-1cn ⊢ 1 ∈ ℂ
60 pncan ⊢ ( ( 𝑚 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑚 + 1 ) − 1 ) = 𝑚 )
61 58 59 60 sylancl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑚 + 1 ) − 1 ) = 𝑚 )
62 61 oveq2d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 0 ... ( ( 𝑚 + 1 ) − 1 ) ) = ( 0 ... 𝑚 ) )
63 62 sumeq1d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → Σ 𝑘 ∈ ( 0 ... ( ( 𝑚 + 1 ) − 1 ) ) 𝐵 = Σ 𝑘 ∈ ( 0 ... 𝑚 ) 𝐵 )
64 simpl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝜑 )
65 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑚 ) → 𝑘 ∈ ℕ0 )
66 64 65 4 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ... 𝑚 ) ) → ( 𝐺 ‘ 𝑘 ) = 𝐵 )
67 39 15 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ( ℤ≥ ‘ 0 ) )
68 64 65 5 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ... 𝑚 ) ) → 𝐵 ∈ ℂ )
69 66 67 68 fsumser ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → Σ 𝑘 ∈ ( 0 ... 𝑚 ) 𝐵 = ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) )
70 63 69 eqtrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → Σ 𝑘 ∈ ( 0 ... ( ( 𝑚 + 1 ) − 1 ) ) 𝐵 = ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) )
71 70 oveq1d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( Σ 𝑘 ∈ ( 0 ... ( ( 𝑚 + 1 ) − 1 ) ) 𝐵 + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) 𝐵 ) = ( ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) 𝐵 ) )
72 56 71 eqtrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → Σ 𝑘 ∈ ℕ0 𝐵 = ( ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) 𝐵 ) )
73 72 oveq1d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( Σ 𝑘 ∈ ℕ0 𝐵 − ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) ) = ( ( ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) 𝐵 ) − ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) ) )
74 46 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ( 𝐺 ‘ 𝑘 ) = Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) 𝐵 )
75 53 73 74 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( Σ 𝑘 ∈ ℕ0 𝐵 − ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) ) = Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ( 𝐺 ‘ 𝑘 ) )
76 75 fveq2d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( abs ‘ ( Σ 𝑘 ∈ ℕ0 𝐵 − ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) ) ) = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) )
77 37 76 eqtrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( abs ‘ ( ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) − Σ 𝑘 ∈ ℕ0 𝐵 ) ) = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) )
78 77 breq1d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( abs ‘ ( ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) − Σ 𝑘 ∈ ℕ0 𝐵 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ↔ ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ) )
79 29 78 sylan2 ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑠 ) ) ) → ( ( abs ‘ ( ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) − Σ 𝑘 ∈ ℕ0 𝐵 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ↔ ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ) )
80 79 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑠 ) ) → ( ( abs ‘ ( ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) − Σ 𝑘 ∈ ℕ0 𝐵 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ↔ ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ) )
81 80 ralbidva ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑠 ) ( abs ‘ ( ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) − Σ 𝑘 ∈ ℕ0 𝐵 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑠 ) ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ) )
82 fvoveq1 ⊢ ( 𝑚 = 𝑛 → ( ℤ≥ ‘ ( 𝑚 + 1 ) ) = ( ℤ≥ ‘ ( 𝑛 + 1 ) ) )
83 82 sumeq1d ⊢ ( 𝑚 = 𝑛 → Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ( 𝐺 ‘ 𝑘 ) = Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) )
84 83 fveq2d ⊢ ( 𝑚 = 𝑛 → ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) )
85 84 breq1d ⊢ ( 𝑚 = 𝑛 → ( ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ↔ ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ) )
86 85 cbvralvw ⊢ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑠 ) ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ↔ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑠 ) ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) )
87 81 86 bitrdi ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑠 ) ( abs ‘ ( ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) − Σ 𝑘 ∈ ℕ0 𝐵 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ↔ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑠 ) ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ) )
88 0zd ⊢ ( ( 𝜑 ∧ 𝜓 ) → 0 ∈ ℤ )
89 14 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐸 / 2 ) ∈ ℝ+ )
90 11 simplbi ⊢ ( 𝜓 → 𝑠 ∈ ℕ )
91 90 adantl ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑠 ∈ ℕ )
92 91 nnrpd ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑠 ∈ ℝ+ )
93 89 92 rpdivcld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝐸 / 2 ) / 𝑠 ) ∈ ℝ+ )
94 eqid ⊢ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) = ( ℤ≥ ‘ ( 𝑛 + 1 ) )
95 elfznn0 ⊢ ( 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) → 𝑛 ∈ ℕ0 )
96 95 adantl ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → 𝑛 ∈ ℕ0 )
97 peano2nn0 ⊢ ( 𝑛 ∈ ℕ0 → ( 𝑛 + 1 ) ∈ ℕ0 )
98 96 97 syl ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → ( 𝑛 + 1 ) ∈ ℕ0 )
99 98 nn0zd ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → ( 𝑛 + 1 ) ∈ ℤ )
100 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
101 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) → 𝜑 )
102 eluznn0 ⊢ ( ( ( 𝑛 + 1 ) ∈ ℕ0 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) → 𝑘 ∈ ℕ0 )
103 98 102 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) → 𝑘 ∈ ℕ0 )
104 101 103 30 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
105 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → seq 0 ( + , 𝐺 ) ∈ dom ⇝ )
106 30 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
107 15 98 106 iserex ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → ( seq 0 ( + , 𝐺 ) ∈ dom ⇝ ↔ seq ( 𝑛 + 1 ) ( + , 𝐺 ) ∈ dom ⇝ ) )
108 105 107 mpbid ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → seq ( 𝑛 + 1 ) ( + , 𝐺 ) ∈ dom ⇝ )
109 94 99 100 104 108 isumcl ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
110 109 abscld ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) ∈ ℝ )
111 eleq1a ⊢ ( ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) ∈ ℝ → ( 𝑧 = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) → 𝑧 ∈ ℝ ) )
112 110 111 syl ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → ( 𝑧 = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) → 𝑧 ∈ ℝ ) )
113 112 rexlimdva ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ∃ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) 𝑧 = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) → 𝑧 ∈ ℝ ) )
114 113 abssdv ⊢ ( ( 𝜑 ∧ 𝜓 ) → { 𝑧 ∣ ∃ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) 𝑧 = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) } ⊆ ℝ )
115 10 114 eqsstrid ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑇 ⊆ ℝ )
116 fzfid ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 0 ... ( 𝑠 − 1 ) ) ∈ Fin )
117 abrexfi ⊢ ( ( 0 ... ( 𝑠 − 1 ) ) ∈ Fin → { 𝑧 ∣ ∃ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) 𝑧 = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) } ∈ Fin )
118 116 117 syl ⊢ ( ( 𝜑 ∧ 𝜓 ) → { 𝑧 ∣ ∃ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) 𝑧 = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) } ∈ Fin )
119 10 118 eqeltrid ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑇 ∈ Fin )
120 nnm1nn0 ⊢ ( 𝑠 ∈ ℕ → ( 𝑠 − 1 ) ∈ ℕ0 )
121 91 120 syl ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑠 − 1 ) ∈ ℕ0 )
122 121 15 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑠 − 1 ) ∈ ( ℤ≥ ‘ 0 ) )
123 eluzfz1 ⊢ ( ( 𝑠 − 1 ) ∈ ( ℤ≥ ‘ 0 ) → 0 ∈ ( 0 ... ( 𝑠 − 1 ) ) )
124 122 123 syl ⊢ ( ( 𝜑 ∧ 𝜓 ) → 0 ∈ ( 0 ... ( 𝑠 − 1 ) ) )
125 nnnn0 ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
126 125 4 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) = 𝐵 )
127 126 sumeq2dv ⊢ ( 𝜑 → Σ 𝑘 ∈ ℕ ( 𝐺 ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ 𝐵 )
128 127 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → Σ 𝑘 ∈ ℕ ( 𝐺 ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ 𝐵 )
129 128 fveq2d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( abs ‘ Σ 𝑘 ∈ ℕ ( 𝐺 ‘ 𝑘 ) ) = ( abs ‘ Σ 𝑘 ∈ ℕ 𝐵 ) )
130 129 eqcomd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( abs ‘ Σ 𝑘 ∈ ℕ 𝐵 ) = ( abs ‘ Σ 𝑘 ∈ ℕ ( 𝐺 ‘ 𝑘 ) ) )
131 fv0p1e1 ⊢ ( 𝑛 = 0 → ( ℤ≥ ‘ ( 𝑛 + 1 ) ) = ( ℤ≥ ‘ 1 ) )
132 131 12 eqtr4di ⊢ ( 𝑛 = 0 → ( ℤ≥ ‘ ( 𝑛 + 1 ) ) = ℕ )
133 132 sumeq1d ⊢ ( 𝑛 = 0 → Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ ( 𝐺 ‘ 𝑘 ) )
134 133 fveq2d ⊢ ( 𝑛 = 0 → ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) = ( abs ‘ Σ 𝑘 ∈ ℕ ( 𝐺 ‘ 𝑘 ) ) )
135 134 rspceeqv ⊢ ( ( 0 ∈ ( 0 ... ( 𝑠 − 1 ) ) ∧ ( abs ‘ Σ 𝑘 ∈ ℕ 𝐵 ) = ( abs ‘ Σ 𝑘 ∈ ℕ ( 𝐺 ‘ 𝑘 ) ) ) → ∃ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ( abs ‘ Σ 𝑘 ∈ ℕ 𝐵 ) = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) )
136 124 130 135 syl2anc ⊢ ( ( 𝜑 ∧ 𝜓 ) → ∃ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ( abs ‘ Σ 𝑘 ∈ ℕ 𝐵 ) = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) )
137 fvex ⊢ ( abs ‘ Σ 𝑘 ∈ ℕ 𝐵 ) ∈ V
138 eqeq1 ⊢ ( 𝑧 = ( abs ‘ Σ 𝑘 ∈ ℕ 𝐵 ) → ( 𝑧 = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) ↔ ( abs ‘ Σ 𝑘 ∈ ℕ 𝐵 ) = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) ) )
139 138 rexbidv ⊢ ( 𝑧 = ( abs ‘ Σ 𝑘 ∈ ℕ 𝐵 ) → ( ∃ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) 𝑧 = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) ↔ ∃ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ( abs ‘ Σ 𝑘 ∈ ℕ 𝐵 ) = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) ) )
140 137 139 10 elab2 ⊢ ( ( abs ‘ Σ 𝑘 ∈ ℕ 𝐵 ) ∈ 𝑇 ↔ ∃ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ( abs ‘ Σ 𝑘 ∈ ℕ 𝐵 ) = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) )
141 136 140 sylibr ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( abs ‘ Σ 𝑘 ∈ ℕ 𝐵 ) ∈ 𝑇 )
142 141 ne0d ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑇 ≠ ∅ )
143 ltso ⊢ < Or ℝ
144 fisupcl ⊢ ( ( < Or ℝ ∧ ( 𝑇 ∈ Fin ∧ 𝑇 ≠ ∅ ∧ 𝑇 ⊆ ℝ ) ) → sup ( 𝑇 , ℝ , < ) ∈ 𝑇 )
145 143 144 mpan ⊢ ( ( 𝑇 ∈ Fin ∧ 𝑇 ≠ ∅ ∧ 𝑇 ⊆ ℝ ) → sup ( 𝑇 , ℝ , < ) ∈ 𝑇 )
146 119 142 115 145 syl3anc ⊢ ( ( 𝜑 ∧ 𝜓 ) → sup ( 𝑇 , ℝ , < ) ∈ 𝑇 )
147 115 146 sseldd ⊢ ( ( 𝜑 ∧ 𝜓 ) → sup ( 𝑇 , ℝ , < ) ∈ ℝ )
148 0red ⊢ ( ( 𝜑 ∧ 𝜓 ) → 0 ∈ ℝ )
149 125 5 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐵 ∈ ℂ )
150 1nn0 ⊢ 1 ∈ ℕ0
151 150 a1i ⊢ ( 𝜑 → 1 ∈ ℕ0 )
152 15 151 30 iserex ⊢ ( 𝜑 → ( seq 0 ( + , 𝐺 ) ∈ dom ⇝ ↔ seq 1 ( + , 𝐺 ) ∈ dom ⇝ ) )
153 8 152 mpbid ⊢ ( 𝜑 → seq 1 ( + , 𝐺 ) ∈ dom ⇝ )
154 12 13 126 149 153 isumcl ⊢ ( 𝜑 → Σ 𝑘 ∈ ℕ 𝐵 ∈ ℂ )
155 154 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → Σ 𝑘 ∈ ℕ 𝐵 ∈ ℂ )
156 155 abscld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( abs ‘ Σ 𝑘 ∈ ℕ 𝐵 ) ∈ ℝ )
157 155 absge0d ⊢ ( ( 𝜑 ∧ 𝜓 ) → 0 ≤ ( abs ‘ Σ 𝑘 ∈ ℕ 𝐵 ) )
158 fimaxre2 ⊢ ( ( 𝑇 ⊆ ℝ ∧ 𝑇 ∈ Fin ) → ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ 𝑇 𝑤 ≤ 𝑧 )
159 115 119 158 syl2anc ⊢ ( ( 𝜑 ∧ 𝜓 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ 𝑇 𝑤 ≤ 𝑧 )
160 115 142 159 141 suprubd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( abs ‘ Σ 𝑘 ∈ ℕ 𝐵 ) ≤ sup ( 𝑇 , ℝ , < ) )
161 148 156 147 157 160 letrd ⊢ ( ( 𝜑 ∧ 𝜓 ) → 0 ≤ sup ( 𝑇 , ℝ , < ) )
162 147 161 ge0p1rpd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( sup ( 𝑇 , ℝ , < ) + 1 ) ∈ ℝ+ )
163 93 162 rpdivcld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ∈ ℝ+ )
164 fveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝐾 ‘ 𝑛 ) = ( 𝐾 ‘ 𝑚 ) )
165 eqid ⊢ ( 𝑛 ∈ ℕ0 ↦ ( 𝐾 ‘ 𝑛 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝐾 ‘ 𝑛 ) )
166 fvex ⊢ ( 𝐾 ‘ 𝑚 ) ∈ V
167 164 165 166 fvmpt ⊢ ( 𝑚 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐾 ‘ 𝑛 ) ) ‘ 𝑚 ) = ( 𝐾 ‘ 𝑚 ) )
168 167 adantl ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐾 ‘ 𝑛 ) ) ‘ 𝑚 ) = ( 𝐾 ‘ 𝑚 ) )
169 nn0ex ⊢ ℕ0 ∈ V
170 169 mptex ⊢ ( 𝑛 ∈ ℕ0 ↦ ( 𝐾 ‘ 𝑛 ) ) ∈ V
171 170 a1i ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ0 ↦ ( 𝐾 ‘ 𝑛 ) ) ∈ V )
172 elnn0uz ⊢ ( 𝑗 ∈ ℕ0 ↔ 𝑗 ∈ ( ℤ≥ ‘ 0 ) )
173 fveq2 ⊢ ( 𝑛 = 𝑗 → ( 𝐾 ‘ 𝑛 ) = ( 𝐾 ‘ 𝑗 ) )
174 fvex ⊢ ( 𝐾 ‘ 𝑗 ) ∈ V
175 173 165 174 fvmpt ⊢ ( 𝑗 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐾 ‘ 𝑛 ) ) ‘ 𝑗 ) = ( 𝐾 ‘ 𝑗 ) )
176 175 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐾 ‘ 𝑛 ) ) ‘ 𝑗 ) = ( 𝐾 ‘ 𝑗 ) )
177 172 176 sylan2br ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 0 ) ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐾 ‘ 𝑛 ) ) ‘ 𝑗 ) = ( 𝐾 ‘ 𝑗 ) )
178 16 177 seqfeq ⊢ ( 𝜑 → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( 𝐾 ‘ 𝑛 ) ) ) = seq 0 ( + , 𝐾 ) )
179 178 7 eqeltrd ⊢ ( 𝜑 → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( 𝐾 ‘ 𝑛 ) ) ) ∈ dom ⇝ )
180 176 2 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐾 ‘ 𝑛 ) ) ‘ 𝑗 ) = ( abs ‘ 𝐴 ) )
181 180 18 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐾 ‘ 𝑛 ) ) ‘ 𝑗 ) ∈ ℝ )
182 181 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐾 ‘ 𝑛 ) ) ‘ 𝑗 ) ∈ ℂ )
183 15 16 171 179 182 serf0 ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ0 ↦ ( 𝐾 ‘ 𝑛 ) ) ⇝ 0 )
184 183 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑛 ∈ ℕ0 ↦ ( 𝐾 ‘ 𝑛 ) ) ⇝ 0 )
185 15 88 163 168 184 climi0 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ∃ 𝑡 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑡 ) ( abs ‘ ( 𝐾 ‘ 𝑚 ) ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) )
186 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑡 ∈ ℕ0 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑡 ) ) → 𝜑 )
187 eluznn0 ⊢ ( ( 𝑡 ∈ ℕ0 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑡 ) ) → 𝑚 ∈ ℕ0 )
188 187 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑡 ∈ ℕ0 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑡 ) ) → 𝑚 ∈ ℕ0 )
189 19 22 absidd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( abs ‘ ( 𝐾 ‘ 𝑗 ) ) = ( 𝐾 ‘ 𝑗 ) )
190 189 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ ℕ0 ( abs ‘ ( 𝐾 ‘ 𝑗 ) ) = ( 𝐾 ‘ 𝑗 ) )
191 fveq2 ⊢ ( 𝑗 = 𝑚 → ( 𝐾 ‘ 𝑗 ) = ( 𝐾 ‘ 𝑚 ) )
192 191 fveq2d ⊢ ( 𝑗 = 𝑚 → ( abs ‘ ( 𝐾 ‘ 𝑗 ) ) = ( abs ‘ ( 𝐾 ‘ 𝑚 ) ) )
193 192 191 eqeq12d ⊢ ( 𝑗 = 𝑚 → ( ( abs ‘ ( 𝐾 ‘ 𝑗 ) ) = ( 𝐾 ‘ 𝑗 ) ↔ ( abs ‘ ( 𝐾 ‘ 𝑚 ) ) = ( 𝐾 ‘ 𝑚 ) ) )
194 193 rspccva ⊢ ( ( ∀ 𝑗 ∈ ℕ0 ( abs ‘ ( 𝐾 ‘ 𝑗 ) ) = ( 𝐾 ‘ 𝑗 ) ∧ 𝑚 ∈ ℕ0 ) → ( abs ‘ ( 𝐾 ‘ 𝑚 ) ) = ( 𝐾 ‘ 𝑚 ) )
195 190 194 sylan ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( abs ‘ ( 𝐾 ‘ 𝑚 ) ) = ( 𝐾 ‘ 𝑚 ) )
196 186 188 195 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑡 ∈ ℕ0 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑡 ) ) → ( abs ‘ ( 𝐾 ‘ 𝑚 ) ) = ( 𝐾 ‘ 𝑚 ) )
197 196 breq1d ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑡 ∈ ℕ0 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑡 ) ) → ( ( abs ‘ ( 𝐾 ‘ 𝑚 ) ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ↔ ( 𝐾 ‘ 𝑚 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) )
198 197 ralbidva ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑡 ∈ ℕ0 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑡 ) ( abs ‘ ( 𝐾 ‘ 𝑚 ) ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑚 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) )
199 164 breq1d ⊢ ( 𝑛 = 𝑚 → ( ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ↔ ( 𝐾 ‘ 𝑚 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) )
200 199 cbvralvw ⊢ ( ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑚 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) )
201 198 200 bitr4di ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑡 ∈ ℕ0 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑡 ) ( abs ‘ ( 𝐾 ‘ 𝑚 ) ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ↔ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) )
202 1 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) ∧ 𝑗 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑗 ) = 𝐴 )
203 2 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) ∧ 𝑗 ∈ ℕ0 ) → ( 𝐾 ‘ 𝑗 ) = ( abs ‘ 𝐴 ) )
204 3 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) ∧ 𝑗 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
205 4 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑘 ) = 𝐵 )
206 5 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝐵 ∈ ℂ )
207 6 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐻 ‘ 𝑘 ) = Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( 𝐴 · ( 𝐺 ‘ ( 𝑘 − 𝑗 ) ) ) )
208 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) → seq 0 ( + , 𝐾 ) ∈ dom ⇝ )
209 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) → seq 0 ( + , 𝐺 ) ∈ dom ⇝ )
210 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) → 𝐸 ∈ ℝ+ )
211 200 anbi2i ⊢ ( ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ↔ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑚 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) )
212 211 anbi2i ⊢ ( ( 𝜓 ∧ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) ↔ ( 𝜓 ∧ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑚 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) )
213 212 biimpi ⊢ ( ( 𝜓 ∧ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) → ( 𝜓 ∧ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑚 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) )
214 213 adantll ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) → ( 𝜓 ∧ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑚 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) )
215 115 142 159 3jca ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ 𝑇 𝑤 ≤ 𝑧 ) )
216 161 215 jca ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 0 ≤ sup ( 𝑇 , ℝ , < ) ∧ ( 𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ 𝑇 𝑤 ≤ 𝑧 ) ) )
217 216 adantr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) → ( 0 ≤ sup ( 𝑇 , ℝ , < ) ∧ ( 𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ 𝑇 𝑤 ≤ 𝑧 ) ) )
218 202 203 204 205 206 207 208 209 210 10 11 214 217 mertenslem1 ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) ) < 𝐸 )
219 218 expr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑡 ∈ ℕ0 ) → ( ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) ) < 𝐸 ) )
220 201 219 sylbid ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑡 ∈ ℕ0 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑡 ) ( abs ‘ ( 𝐾 ‘ 𝑚 ) ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) ) < 𝐸 ) )
221 220 rexlimdva ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ∃ 𝑡 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑡 ) ( abs ‘ ( 𝐾 ‘ 𝑚 ) ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) ) < 𝐸 ) )
222 185 221 mpd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) ) < 𝐸 )
223 222 ex ⊢ ( 𝜑 → ( 𝜓 → ∃ 𝑦 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) ) < 𝐸 ) )
224 11 223 biimtrrid ⊢ ( 𝜑 → ( ( 𝑠 ∈ ℕ ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑠 ) ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) ) < 𝐸 ) )
225 224 expdimp ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ ) → ( ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑠 ) ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) ) < 𝐸 ) )
226 87 225 sylbid ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑠 ) ( abs ‘ ( ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) − Σ 𝑘 ∈ ℕ0 𝐵 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) ) < 𝐸 ) )
227 226 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑠 ∈ ℕ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑠 ) ( abs ‘ ( ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) − Σ 𝑘 ∈ ℕ0 𝐵 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) ) < 𝐸 ) )
228 28 227 mpd ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) ) < 𝐸 )