Metamath Proof Explorer

Theorem abelthlem8

Description: Lemma for abelth . (Contributed by Mario Carneiro, 2-Apr-2015)

Ref Expression
Hypotheses abelth.1 ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
abelth.2 ⊢ ( 𝜑 → seq 0 ( + , 𝐴 ) ∈ dom ⇝ )
abelth.3 ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
abelth.4 ⊢ ( 𝜑 → 0 ≤ 𝑀 )
abelth.5 ⊢ 𝑆 = { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) }
abelth.6 ⊢ 𝐹 = ( 𝑥 ∈ 𝑆 ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) )
abelth.7 ⊢ ( 𝜑 → seq 0 ( + , 𝐴 ) ⇝ 0 )
Assertion abelthlem8 ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑦 ∈ 𝑆 ( ( abs ‘ ( 1 − 𝑦 ) ) < 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑅 ) )

Proof

Step Hyp Ref Expression
1 abelth.1 ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
2 abelth.2 ⊢ ( 𝜑 → seq 0 ( + , 𝐴 ) ∈ dom ⇝ )
3 abelth.3 ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
4 abelth.4 ⊢ ( 𝜑 → 0 ≤ 𝑀 )
5 abelth.5 ⊢ 𝑆 = { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) }
6 abelth.6 ⊢ 𝐹 = ( 𝑥 ∈ 𝑆 ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) )
7 abelth.7 ⊢ ( 𝜑 → seq 0 ( + , 𝐴 ) ⇝ 0 )
8 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
9 0zd ⊢ ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) → 0 ∈ ℤ )
10 id ⊢ ( 𝑅 ∈ ℝ+ → 𝑅 ∈ ℝ+ )
11 3 4 ge0p1rpd ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℝ+ )
12 rpdivcl ⊢ ( ( 𝑅 ∈ ℝ+ ∧ ( 𝑀 + 1 ) ∈ ℝ+ ) → ( 𝑅 / ( 𝑀 + 1 ) ) ∈ ℝ+ )
13 10 11 12 syl2anr ⊢ ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) → ( 𝑅 / ( 𝑀 + 1 ) ) ∈ ℝ+ )
14 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑘 ∈ ℕ0 ) → ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) = ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) )
15 7 adantr ⊢ ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) → seq 0 ( + , 𝐴 ) ⇝ 0 )
16 8 9 13 14 15 climi0 ⊢ ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) → ∃ 𝑗 ∈ ℕ0 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) )
17 13 adantr ⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ) ) → ( 𝑅 / ( 𝑀 + 1 ) ) ∈ ℝ+ )
18 fzfid ⊢ ( 𝜑 → ( 0 ... ( 𝑗 − 1 ) ) ∈ Fin )
19 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
20 1 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑤 ) ∈ ℂ )
21 8 19 20 serf ⊢ ( 𝜑 → seq 0 ( + , 𝐴 ) : ℕ0 ⟶ ℂ )
22 elfznn0 ⊢ ( 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) → 𝑖 ∈ ℕ0 )
23 ffvelcdm ⊢ ( ( seq 0 ( + , 𝐴 ) : ℕ0 ⟶ ℂ ∧ 𝑖 ∈ ℕ0 ) → ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ∈ ℂ )
24 21 22 23 syl2an ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ) → ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ∈ ℂ )
25 24 abscld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ) → ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) ∈ ℝ )
26 18 25 fsumrecl ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) ∈ ℝ )
27 26 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ) ) → Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) ∈ ℝ )
28 24 absge0d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ) → 0 ≤ ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) )
29 18 25 28 fsumge0 ⊢ ( 𝜑 → 0 ≤ Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) )
30 29 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ) ) → 0 ≤ Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) )
31 27 30 ge0p1rpd ⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ) ) → ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ∈ ℝ+ )
32 17 31 rpdivcld ⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ) ) → ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ) ∈ ℝ+ )
33 1 2 3 4 5 abelthlem2 ⊢ ( 𝜑 → ( 1 ∈ 𝑆 ∧ ( 𝑆 ∖ { 1 } ) ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) )
34 33 simpld ⊢ ( 𝜑 → 1 ∈ 𝑆 )
35 oveq1 ⊢ ( 𝑥 = 1 → ( 𝑥 ↑ 𝑛 ) = ( 1 ↑ 𝑛 ) )
36 nn0z ⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℤ )
37 1exp ⊢ ( 𝑛 ∈ ℤ → ( 1 ↑ 𝑛 ) = 1 )
38 36 37 syl ⊢ ( 𝑛 ∈ ℕ0 → ( 1 ↑ 𝑛 ) = 1 )
39 35 38 sylan9eq ⊢ ( ( 𝑥 = 1 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑥 ↑ 𝑛 ) = 1 )
40 39 oveq2d ⊢ ( ( 𝑥 = 1 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) = ( ( 𝐴 ‘ 𝑛 ) · 1 ) )
41 40 sumeq2dv ⊢ ( 𝑥 = 1 → Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) = Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · 1 ) )
42 sumex ⊢ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · 1 ) ∈ V
43 41 6 42 fvmpt ⊢ ( 1 ∈ 𝑆 → ( 𝐹 ‘ 1 ) = Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · 1 ) )
44 34 43 syl ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · 1 ) )
45 1 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑛 ) ∈ ℂ )
46 45 mulridd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑛 ) · 1 ) = ( 𝐴 ‘ 𝑛 ) )
47 46 eqcomd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑛 ) = ( ( 𝐴 ‘ 𝑛 ) · 1 ) )
48 46 45 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑛 ) · 1 ) ∈ ℂ )
49 8 19 47 48 7 isumclim ⊢ ( 𝜑 → Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · 1 ) = 0 )
50 44 49 eqtrd ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = 0 )
51 50 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( 𝐹 ‘ 1 ) = 0 )
52 51 oveq1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝐹 ‘ 1 ) − ( 𝐹 ‘ 𝑦 ) ) = ( 0 − ( 𝐹 ‘ 𝑦 ) ) )
53 df-neg ⊢ - ( 𝐹 ‘ 𝑦 ) = ( 0 − ( 𝐹 ‘ 𝑦 ) )
54 52 53 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝐹 ‘ 1 ) − ( 𝐹 ‘ 𝑦 ) ) = - ( 𝐹 ‘ 𝑦 ) )
55 54 fveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝐹 ‘ 𝑦 ) ) ) = ( abs ‘ - ( 𝐹 ‘ 𝑦 ) ) )
56 1 2 3 4 5 6 abelthlem4 ⊢ ( 𝜑 → 𝐹 : 𝑆 ⟶ ℂ )
57 56 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℂ )
58 57 absnegd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( abs ‘ - ( 𝐹 ‘ 𝑦 ) ) = ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) )
59 55 58 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝐹 ‘ 𝑦 ) ) ) = ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) )
60 59 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑆 ) → ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝐹 ‘ 𝑦 ) ) ) = ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) )
61 60 ad2ant2r ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ ( abs ‘ ( 1 − 𝑦 ) ) < ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝐹 ‘ 𝑦 ) ) ) = ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) )
62 fveq2 ⊢ ( 𝑦 = 1 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 1 ) )
63 62 50 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑦 = 1 ) → ( 𝐹 ‘ 𝑦 ) = 0 )
64 63 abs00bd ⊢ ( ( 𝜑 ∧ 𝑦 = 1 ) → ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) = 0 )
65 64 ad5ant15 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ ( abs ‘ ( 1 − 𝑦 ) ) < ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ) ) ) ∧ 𝑦 = 1 ) → ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) = 0 )
66 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ ( abs ‘ ( 1 − 𝑦 ) ) < ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ) ) ) → 𝑅 ∈ ℝ+ )
67 66 rpgt0d ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ ( abs ‘ ( 1 − 𝑦 ) ) < ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ) ) ) → 0 < 𝑅 )
68 67 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ ( abs ‘ ( 1 − 𝑦 ) ) < ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ) ) ) ∧ 𝑦 = 1 ) → 0 < 𝑅 )
69 65 68 eqbrtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ ( abs ‘ ( 1 − 𝑦 ) ) < ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ) ) ) ∧ 𝑦 = 1 ) → ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) < 𝑅 )
70 1 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ) ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ ( abs ‘ ( 1 − 𝑦 ) ) < ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ) ) ∧ 𝑦 ≠ 1 ) ) → 𝐴 : ℕ0 ⟶ ℂ )
71 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ) ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ ( abs ‘ ( 1 − 𝑦 ) ) < ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ) ) ∧ 𝑦 ≠ 1 ) ) → seq 0 ( + , 𝐴 ) ∈ dom ⇝ )
72 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ) ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ ( abs ‘ ( 1 − 𝑦 ) ) < ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ) ) ∧ 𝑦 ≠ 1 ) ) → 𝑀 ∈ ℝ )
73 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ) ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ ( abs ‘ ( 1 − 𝑦 ) ) < ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ) ) ∧ 𝑦 ≠ 1 ) ) → 0 ≤ 𝑀 )
74 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ) ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ ( abs ‘ ( 1 − 𝑦 ) ) < ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ) ) ∧ 𝑦 ≠ 1 ) ) → seq 0 ( + , 𝐴 ) ⇝ 0 )
75 simprll ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ) ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ ( abs ‘ ( 1 − 𝑦 ) ) < ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ) ) ∧ 𝑦 ≠ 1 ) ) → 𝑦 ∈ 𝑆 )
76 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ) ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ ( abs ‘ ( 1 − 𝑦 ) ) < ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ) ) ∧ 𝑦 ≠ 1 ) ) → 𝑦 ≠ 1 )
77 eldifsn ⊢ ( 𝑦 ∈ ( 𝑆 ∖ { 1 } ) ↔ ( 𝑦 ∈ 𝑆 ∧ 𝑦 ≠ 1 ) )
78 75 76 77 sylanbrc ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ) ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ ( abs ‘ ( 1 − 𝑦 ) ) < ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ) ) ∧ 𝑦 ≠ 1 ) ) → 𝑦 ∈ ( 𝑆 ∖ { 1 } ) )
79 13 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ) ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ ( abs ‘ ( 1 − 𝑦 ) ) < ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ) ) ∧ 𝑦 ≠ 1 ) ) → ( 𝑅 / ( 𝑀 + 1 ) ) ∈ ℝ+ )
80 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ) ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ ( abs ‘ ( 1 − 𝑦 ) ) < ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ) ) ∧ 𝑦 ≠ 1 ) ) → 𝑗 ∈ ℕ0 )
81 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ) ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ ( abs ‘ ( 1 − 𝑦 ) ) < ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ) ) ∧ 𝑦 ≠ 1 ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) )
82 2fveq3 ⊢ ( 𝑘 = 𝑚 → ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) = ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) )
83 82 breq1d ⊢ ( 𝑘 = 𝑚 → ( ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ↔ ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ) )
84 83 cbvralvw ⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) )
85 81 84 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ) ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ ( abs ‘ ( 1 − 𝑦 ) ) < ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ) ) ∧ 𝑦 ≠ 1 ) ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑚 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) )
86 simprlr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ) ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ ( abs ‘ ( 1 − 𝑦 ) ) < ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ) ) ∧ 𝑦 ≠ 1 ) ) → ( abs ‘ ( 1 − 𝑦 ) ) < ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ) )
87 2fveq3 ⊢ ( 𝑖 = 𝑛 → ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) = ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) )
88 87 cbvsumv ⊢ Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) = Σ 𝑛 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) )
89 88 oveq1i ⊢ ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) = ( Σ 𝑛 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 )
90 89 oveq2i ⊢ ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ) = ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑛 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) )
91 86 90 breqtrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ) ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ ( abs ‘ ( 1 − 𝑦 ) ) < ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ) ) ∧ 𝑦 ≠ 1 ) ) → ( abs ‘ ( 1 − 𝑦 ) ) < ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑛 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) ) )
92 70 71 72 73 5 6 74 78 79 80 85 91 abelthlem7 ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ) ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ ( abs ‘ ( 1 − 𝑦 ) ) < ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ) ) ∧ 𝑦 ≠ 1 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) < ( ( 𝑀 + 1 ) · ( 𝑅 / ( 𝑀 + 1 ) ) ) )
93 rpcn ⊢ ( 𝑅 ∈ ℝ+ → 𝑅 ∈ ℂ )
94 93 adantl ⊢ ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) → 𝑅 ∈ ℂ )
95 11 adantr ⊢ ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) → ( 𝑀 + 1 ) ∈ ℝ+ )
96 95 rpcnd ⊢ ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) → ( 𝑀 + 1 ) ∈ ℂ )
97 95 rpne0d ⊢ ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) → ( 𝑀 + 1 ) ≠ 0 )
98 94 96 97 divcan2d ⊢ ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) → ( ( 𝑀 + 1 ) · ( 𝑅 / ( 𝑀 + 1 ) ) ) = 𝑅 )
99 98 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ) ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ ( abs ‘ ( 1 − 𝑦 ) ) < ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ) ) ∧ 𝑦 ≠ 1 ) ) → ( ( 𝑀 + 1 ) · ( 𝑅 / ( 𝑀 + 1 ) ) ) = 𝑅 )
100 92 99 breqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ) ) ∧ ( ( 𝑦 ∈ 𝑆 ∧ ( abs ‘ ( 1 − 𝑦 ) ) < ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ) ) ∧ 𝑦 ≠ 1 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) < 𝑅 )
101 100 anassrs ⊢ ( ( ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ ( abs ‘ ( 1 − 𝑦 ) ) < ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ) ) ) ∧ 𝑦 ≠ 1 ) → ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) < 𝑅 )
102 69 101 pm2.61dane ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ ( abs ‘ ( 1 − 𝑦 ) ) < ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ) ) ) → ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) < 𝑅 )
103 61 102 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ ( abs ‘ ( 1 − 𝑦 ) ) < ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑅 )
104 103 expr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ) ) ∧ 𝑦 ∈ 𝑆 ) → ( ( abs ‘ ( 1 − 𝑦 ) ) < ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ) → ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑅 ) )
105 104 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ) ) → ∀ 𝑦 ∈ 𝑆 ( ( abs ‘ ( 1 − 𝑦 ) ) < ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ) → ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑅 ) )
106 breq2 ⊢ ( 𝑤 = ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ) → ( ( abs ‘ ( 1 − 𝑦 ) ) < 𝑤 ↔ ( abs ‘ ( 1 − 𝑦 ) ) < ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ) ) )
107 106 rspceaimv ⊢ ( ( ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ) ∈ ℝ+ ∧ ∀ 𝑦 ∈ 𝑆 ( ( abs ‘ ( 1 − 𝑦 ) ) < ( ( 𝑅 / ( 𝑀 + 1 ) ) / ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ) + 1 ) ) → ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑅 ) ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑦 ∈ 𝑆 ( ( abs ‘ ( 1 − 𝑦 ) ) < 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑅 ) )
108 32 105 107 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < ( 𝑅 / ( 𝑀 + 1 ) ) ) ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑦 ∈ 𝑆 ( ( abs ‘ ( 1 − 𝑦 ) ) < 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑅 ) )
109 16 108 rexlimddv ⊢ ( ( 𝜑 ∧ 𝑅 ∈ ℝ+ ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑦 ∈ 𝑆 ( ( abs ‘ ( 1 − 𝑦 ) ) < 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑅 ) )