Metamath Proof Explorer


Theorem abelthlem7

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 )
abelthlem6.1 ( 𝜑𝑋 ∈ ( 𝑆 ∖ { 1 } ) )
abelthlem7.2 ( 𝜑𝑅 ∈ ℝ+ )
abelthlem7.3 ( 𝜑𝑁 ∈ ℕ0 )
abelthlem7.4 ( 𝜑 → ∀ 𝑘 ∈ ( ℤ𝑁 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < 𝑅 )
abelthlem7.5 ( 𝜑 → ( abs ‘ ( 1 − 𝑋 ) ) < ( 𝑅 / ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) ) )
Assertion abelthlem7 ( 𝜑 → ( 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 abelthlem6.1 ( 𝜑𝑋 ∈ ( 𝑆 ∖ { 1 } ) )
9 abelthlem7.2 ( 𝜑𝑅 ∈ ℝ+ )
10 abelthlem7.3 ( 𝜑𝑁 ∈ ℕ0 )
11 abelthlem7.4 ( 𝜑 → ∀ 𝑘 ∈ ( ℤ𝑁 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < 𝑅 )
12 abelthlem7.5 ( 𝜑 → ( abs ‘ ( 1 − 𝑋 ) ) < ( 𝑅 / ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) ) )
13 1 2 3 4 5 6 abelthlem4 ( 𝜑𝐹 : 𝑆 ⟶ ℂ )
14 8 eldifad ( 𝜑𝑋𝑆 )
15 13 14 ffvelrnd ( 𝜑 → ( 𝐹𝑋 ) ∈ ℂ )
16 15 abscld ( 𝜑 → ( abs ‘ ( 𝐹𝑋 ) ) ∈ ℝ )
17 ax-1cn 1 ∈ ℂ
18 1 2 3 4 5 6 7 8 abelthlem7a ( 𝜑 → ( 𝑋 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑋 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑋 ) ) ) ) )
19 18 simpld ( 𝜑𝑋 ∈ ℂ )
20 subcl ( ( 1 ∈ ℂ ∧ 𝑋 ∈ ℂ ) → ( 1 − 𝑋 ) ∈ ℂ )
21 17 19 20 sylancr ( 𝜑 → ( 1 − 𝑋 ) ∈ ℂ )
22 fzfid ( 𝜑 → ( 0 ... ( 𝑁 − 1 ) ) ∈ Fin )
23 elfznn0 ( 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑛 ∈ ℕ0 )
24 nn0uz 0 = ( ℤ ‘ 0 )
25 0zd ( 𝜑 → 0 ∈ ℤ )
26 1 ffvelrnda ( ( 𝜑𝑛 ∈ ℕ0 ) → ( 𝐴𝑛 ) ∈ ℂ )
27 24 25 26 serf ( 𝜑 → seq 0 ( + , 𝐴 ) : ℕ0 ⟶ ℂ )
28 27 ffvelrnda ( ( 𝜑𝑛 ∈ ℕ0 ) → ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ∈ ℂ )
29 expcl ( ( 𝑋 ∈ ℂ ∧ 𝑛 ∈ ℕ0 ) → ( 𝑋𝑛 ) ∈ ℂ )
30 19 29 sylan ( ( 𝜑𝑛 ∈ ℕ0 ) → ( 𝑋𝑛 ) ∈ ℂ )
31 28 30 mulcld ( ( 𝜑𝑛 ∈ ℕ0 ) → ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ∈ ℂ )
32 23 31 sylan2 ( ( 𝜑𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ∈ ℂ )
33 22 32 fsumcl ( 𝜑 → Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ∈ ℂ )
34 21 33 mulcld ( 𝜑 → ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ∈ ℂ )
35 34 abscld ( 𝜑 → ( abs ‘ ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ) ∈ ℝ )
36 eqid ( ℤ𝑁 ) = ( ℤ𝑁 )
37 10 nn0zd ( 𝜑𝑁 ∈ ℤ )
38 eluznn0 ( ( 𝑁 ∈ ℕ0𝑛 ∈ ( ℤ𝑁 ) ) → 𝑛 ∈ ℕ0 )
39 10 38 sylan ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → 𝑛 ∈ ℕ0 )
40 fveq2 ( 𝑘 = 𝑛 → ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) = ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) )
41 oveq2 ( 𝑘 = 𝑛 → ( 𝑋𝑘 ) = ( 𝑋𝑛 ) )
42 40 41 oveq12d ( 𝑘 = 𝑛 → ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋𝑘 ) ) = ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) )
43 eqid ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋𝑘 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋𝑘 ) ) )
44 ovex ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ∈ V
45 42 43 44 fvmpt ( 𝑛 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋𝑘 ) ) ) ‘ 𝑛 ) = ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) )
46 39 45 syl ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋𝑘 ) ) ) ‘ 𝑛 ) = ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) )
47 39 31 syldan ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ∈ ℂ )
48 1 2 3 4 5 abelthlem2 ( 𝜑 → ( 1 ∈ 𝑆 ∧ ( 𝑆 ∖ { 1 } ) ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) )
49 48 simprd ( 𝜑 → ( 𝑆 ∖ { 1 } ) ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) )
50 49 8 sseldd ( 𝜑𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) )
51 1 2 3 4 5 6 7 abelthlem5 ( ( 𝜑𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋𝑘 ) ) ) ) ∈ dom ⇝ )
52 50 51 mpdan ( 𝜑 → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋𝑘 ) ) ) ) ∈ dom ⇝ )
53 45 adantl ( ( 𝜑𝑛 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋𝑘 ) ) ) ‘ 𝑛 ) = ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) )
54 53 31 eqeltrd ( ( 𝜑𝑛 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋𝑘 ) ) ) ‘ 𝑛 ) ∈ ℂ )
55 24 10 54 iserex ( 𝜑 → ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋𝑘 ) ) ) ) ∈ dom ⇝ ↔ seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋𝑘 ) ) ) ) ∈ dom ⇝ ) )
56 52 55 mpbid ( 𝜑 → seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋𝑘 ) ) ) ) ∈ dom ⇝ )
57 36 37 46 47 56 isumcl ( 𝜑 → Σ 𝑛 ∈ ( ℤ𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ∈ ℂ )
58 21 57 mulcld ( 𝜑 → ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( ℤ𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ∈ ℂ )
59 58 abscld ( 𝜑 → ( abs ‘ ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( ℤ𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ) ∈ ℝ )
60 35 59 readdcld ( 𝜑 → ( ( abs ‘ ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ) + ( abs ‘ ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( ℤ𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ) ) ∈ ℝ )
61 peano2re ( 𝑀 ∈ ℝ → ( 𝑀 + 1 ) ∈ ℝ )
62 3 61 syl ( 𝜑 → ( 𝑀 + 1 ) ∈ ℝ )
63 9 rpred ( 𝜑𝑅 ∈ ℝ )
64 62 63 remulcld ( 𝜑 → ( ( 𝑀 + 1 ) · 𝑅 ) ∈ ℝ )
65 1 2 3 4 5 6 7 8 abelthlem6 ( 𝜑 → ( 𝐹𝑋 ) = ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) )
66 24 36 10 53 31 52 isumsplit ( 𝜑 → Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) = ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) + Σ 𝑛 ∈ ( ℤ𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) )
67 66 oveq2d ( 𝜑 → ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) = ( ( 1 − 𝑋 ) · ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) + Σ 𝑛 ∈ ( ℤ𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ) )
68 21 33 57 adddid ( 𝜑 → ( ( 1 − 𝑋 ) · ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) + Σ 𝑛 ∈ ( ℤ𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ) = ( ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) + ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( ℤ𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ) )
69 65 67 68 3eqtrd ( 𝜑 → ( 𝐹𝑋 ) = ( ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) + ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( ℤ𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ) )
70 69 fveq2d ( 𝜑 → ( abs ‘ ( 𝐹𝑋 ) ) = ( abs ‘ ( ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) + ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( ℤ𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ) ) )
71 34 58 abstrid ( 𝜑 → ( abs ‘ ( ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) + ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( ℤ𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ) ) ≤ ( ( abs ‘ ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ) + ( abs ‘ ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( ℤ𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ) ) )
72 70 71 eqbrtrd ( 𝜑 → ( abs ‘ ( 𝐹𝑋 ) ) ≤ ( ( abs ‘ ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ) + ( abs ‘ ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( ℤ𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ) ) )
73 3 63 remulcld ( 𝜑 → ( 𝑀 · 𝑅 ) ∈ ℝ )
74 21 abscld ( 𝜑 → ( abs ‘ ( 1 − 𝑋 ) ) ∈ ℝ )
75 28 abscld ( ( 𝜑𝑛 ∈ ℕ0 ) → ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) ∈ ℝ )
76 23 75 sylan2 ( ( 𝜑𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) ∈ ℝ )
77 22 76 fsumrecl ( 𝜑 → Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) ∈ ℝ )
78 peano2re ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) ∈ ℝ → ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) ∈ ℝ )
79 77 78 syl ( 𝜑 → ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) ∈ ℝ )
80 74 79 remulcld ( 𝜑 → ( ( abs ‘ ( 1 − 𝑋 ) ) · ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) ) ∈ ℝ )
81 21 33 absmuld ( 𝜑 → ( abs ‘ ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ) = ( ( abs ‘ ( 1 − 𝑋 ) ) · ( abs ‘ Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ) )
82 33 abscld ( 𝜑 → ( abs ‘ Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ∈ ℝ )
83 21 absge0d ( 𝜑 → 0 ≤ ( abs ‘ ( 1 − 𝑋 ) ) )
84 31 abscld ( ( 𝜑𝑛 ∈ ℕ0 ) → ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ∈ ℝ )
85 23 84 sylan2 ( ( 𝜑𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ∈ ℝ )
86 22 85 fsumrecl ( 𝜑 → Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ∈ ℝ )
87 22 32 fsumabs ( 𝜑 → ( abs ‘ Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ≤ Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) )
88 19 abscld ( 𝜑 → ( abs ‘ 𝑋 ) ∈ ℝ )
89 reexpcl ( ( ( abs ‘ 𝑋 ) ∈ ℝ ∧ 𝑛 ∈ ℕ0 ) → ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ∈ ℝ )
90 88 89 sylan ( ( 𝜑𝑛 ∈ ℕ0 ) → ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ∈ ℝ )
91 1red ( ( 𝜑𝑛 ∈ ℕ0 ) → 1 ∈ ℝ )
92 28 absge0d ( ( 𝜑𝑛 ∈ ℕ0 ) → 0 ≤ ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) )
93 88 adantr ( ( 𝜑𝑛 ∈ ℕ0 ) → ( abs ‘ 𝑋 ) ∈ ℝ )
94 19 absge0d ( 𝜑 → 0 ≤ ( abs ‘ 𝑋 ) )
95 94 adantr ( ( 𝜑𝑛 ∈ ℕ0 ) → 0 ≤ ( abs ‘ 𝑋 ) )
96 0cn 0 ∈ ℂ
97 eqid ( abs ∘ − ) = ( abs ∘ − )
98 97 cnmetdval ( ( 𝑋 ∈ ℂ ∧ 0 ∈ ℂ ) → ( 𝑋 ( abs ∘ − ) 0 ) = ( abs ‘ ( 𝑋 − 0 ) ) )
99 19 96 98 sylancl ( 𝜑 → ( 𝑋 ( abs ∘ − ) 0 ) = ( abs ‘ ( 𝑋 − 0 ) ) )
100 19 subid1d ( 𝜑 → ( 𝑋 − 0 ) = 𝑋 )
101 100 fveq2d ( 𝜑 → ( abs ‘ ( 𝑋 − 0 ) ) = ( abs ‘ 𝑋 ) )
102 99 101 eqtrd ( 𝜑 → ( 𝑋 ( abs ∘ − ) 0 ) = ( abs ‘ 𝑋 ) )
103 cnxmet ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
104 1xr 1 ∈ ℝ*
105 elbl3 ( ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 1 ∈ ℝ* ) ∧ ( 0 ∈ ℂ ∧ 𝑋 ∈ ℂ ) ) → ( 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↔ ( 𝑋 ( abs ∘ − ) 0 ) < 1 ) )
106 103 104 105 mpanl12 ( ( 0 ∈ ℂ ∧ 𝑋 ∈ ℂ ) → ( 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↔ ( 𝑋 ( abs ∘ − ) 0 ) < 1 ) )
107 96 19 106 sylancr ( 𝜑 → ( 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↔ ( 𝑋 ( abs ∘ − ) 0 ) < 1 ) )
108 50 107 mpbid ( 𝜑 → ( 𝑋 ( abs ∘ − ) 0 ) < 1 )
109 102 108 eqbrtrrd ( 𝜑 → ( abs ‘ 𝑋 ) < 1 )
110 1re 1 ∈ ℝ
111 ltle ( ( ( abs ‘ 𝑋 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( abs ‘ 𝑋 ) < 1 → ( abs ‘ 𝑋 ) ≤ 1 ) )
112 88 110 111 sylancl ( 𝜑 → ( ( abs ‘ 𝑋 ) < 1 → ( abs ‘ 𝑋 ) ≤ 1 ) )
113 109 112 mpd ( 𝜑 → ( abs ‘ 𝑋 ) ≤ 1 )
114 113 adantr ( ( 𝜑𝑛 ∈ ℕ0 ) → ( abs ‘ 𝑋 ) ≤ 1 )
115 simpr ( ( 𝜑𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
116 exple1 ( ( ( ( abs ‘ 𝑋 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑋 ) ∧ ( abs ‘ 𝑋 ) ≤ 1 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ≤ 1 )
117 93 95 114 115 116 syl31anc ( ( 𝜑𝑛 ∈ ℕ0 ) → ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ≤ 1 )
118 90 91 75 92 117 lemul2ad ( ( 𝜑𝑛 ∈ ℕ0 ) → ( ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) · ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) ≤ ( ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) · 1 ) )
119 28 30 absmuld ( ( 𝜑𝑛 ∈ ℕ0 ) → ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) = ( ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) · ( abs ‘ ( 𝑋𝑛 ) ) ) )
120 absexp ( ( 𝑋 ∈ ℂ ∧ 𝑛 ∈ ℕ0 ) → ( abs ‘ ( 𝑋𝑛 ) ) = ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) )
121 19 120 sylan ( ( 𝜑𝑛 ∈ ℕ0 ) → ( abs ‘ ( 𝑋𝑛 ) ) = ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) )
122 121 oveq2d ( ( 𝜑𝑛 ∈ ℕ0 ) → ( ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) · ( abs ‘ ( 𝑋𝑛 ) ) ) = ( ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) · ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) )
123 119 122 eqtr2d ( ( 𝜑𝑛 ∈ ℕ0 ) → ( ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) · ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) = ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) )
124 75 recnd ( ( 𝜑𝑛 ∈ ℕ0 ) → ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) ∈ ℂ )
125 124 mulid1d ( ( 𝜑𝑛 ∈ ℕ0 ) → ( ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) · 1 ) = ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) )
126 118 123 125 3brtr3d ( ( 𝜑𝑛 ∈ ℕ0 ) → ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ≤ ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) )
127 23 126 sylan2 ( ( 𝜑𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ≤ ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) )
128 22 85 76 127 fsumle ( 𝜑 → Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ≤ Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) )
129 82 86 77 87 128 letrd ( 𝜑 → ( abs ‘ Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ≤ Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) )
130 77 ltp1d ( 𝜑 → Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) < ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) )
131 82 77 79 129 130 lelttrd ( 𝜑 → ( abs ‘ Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) < ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) )
132 82 79 131 ltled ( 𝜑 → ( abs ‘ Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ≤ ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) )
133 82 79 74 83 132 lemul2ad ( 𝜑 → ( ( abs ‘ ( 1 − 𝑋 ) ) · ( abs ‘ Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ) ≤ ( ( abs ‘ ( 1 − 𝑋 ) ) · ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) ) )
134 81 133 eqbrtrd ( 𝜑 → ( abs ‘ ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ) ≤ ( ( abs ‘ ( 1 − 𝑋 ) ) · ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) ) )
135 0red ( 𝜑 → 0 ∈ ℝ )
136 23 92 sylan2 ( ( 𝜑𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 0 ≤ ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) )
137 22 76 136 fsumge0 ( 𝜑 → 0 ≤ Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) )
138 135 77 79 137 130 lelttrd ( 𝜑 → 0 < ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) )
139 ltmuldiv ( ( ( abs ‘ ( 1 − 𝑋 ) ) ∈ ℝ ∧ 𝑅 ∈ ℝ ∧ ( ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) ∈ ℝ ∧ 0 < ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) ) ) → ( ( ( abs ‘ ( 1 − 𝑋 ) ) · ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) ) < 𝑅 ↔ ( abs ‘ ( 1 − 𝑋 ) ) < ( 𝑅 / ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) ) ) )
140 74 63 79 138 139 syl112anc ( 𝜑 → ( ( ( abs ‘ ( 1 − 𝑋 ) ) · ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) ) < 𝑅 ↔ ( abs ‘ ( 1 − 𝑋 ) ) < ( 𝑅 / ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) ) ) )
141 12 140 mpbird ( 𝜑 → ( ( abs ‘ ( 1 − 𝑋 ) ) · ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) ) < 𝑅 )
142 35 80 63 134 141 lelttrd ( 𝜑 → ( abs ‘ ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ) < 𝑅 )
143 21 57 absmuld ( 𝜑 → ( abs ‘ ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( ℤ𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ) = ( ( abs ‘ ( 1 − 𝑋 ) ) · ( abs ‘ Σ 𝑛 ∈ ( ℤ𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ) )
144 57 abscld ( 𝜑 → ( abs ‘ Σ 𝑛 ∈ ( ℤ𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ∈ ℝ )
145 42 fveq2d ( 𝑘 = 𝑛 → ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋𝑘 ) ) ) = ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) )
146 eqid ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋𝑘 ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋𝑘 ) ) ) )
147 fvex ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ∈ V
148 145 146 147 fvmpt ( 𝑛 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋𝑘 ) ) ) ) ‘ 𝑛 ) = ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) )
149 39 148 syl ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋𝑘 ) ) ) ) ‘ 𝑛 ) = ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) )
150 47 abscld ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ∈ ℝ )
151 uzid ( 𝑁 ∈ ℤ → 𝑁 ∈ ( ℤ𝑁 ) )
152 37 151 syl ( 𝜑𝑁 ∈ ( ℤ𝑁 ) )
153 oveq2 ( 𝑘 = 𝑛 → ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) = ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) )
154 eqid ( 𝑘 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) )
155 ovex ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ∈ V
156 153 154 155 fvmpt ( 𝑛 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ‘ 𝑛 ) = ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) )
157 39 156 syl ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ‘ 𝑛 ) = ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) )
158 39 90 syldan ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ∈ ℝ )
159 157 158 eqeltrd ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ‘ 𝑛 ) ∈ ℝ )
160 150 recnd ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ∈ ℂ )
161 149 160 eqeltrd ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋𝑘 ) ) ) ) ‘ 𝑛 ) ∈ ℂ )
162 88 recnd ( 𝜑 → ( abs ‘ 𝑋 ) ∈ ℂ )
163 absidm ( 𝑋 ∈ ℂ → ( abs ‘ ( abs ‘ 𝑋 ) ) = ( abs ‘ 𝑋 ) )
164 19 163 syl ( 𝜑 → ( abs ‘ ( abs ‘ 𝑋 ) ) = ( abs ‘ 𝑋 ) )
165 164 109 eqbrtrd ( 𝜑 → ( abs ‘ ( abs ‘ 𝑋 ) ) < 1 )
166 162 165 10 157 geolim2 ( 𝜑 → seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ) ⇝ ( ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) / ( 1 − ( abs ‘ 𝑋 ) ) ) )
167 seqex seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ) ∈ V
168 ovex ( ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) / ( 1 − ( abs ‘ 𝑋 ) ) ) ∈ V
169 167 168 breldm ( seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ) ⇝ ( ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) / ( 1 − ( abs ‘ 𝑋 ) ) ) → seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ) ∈ dom ⇝ )
170 166 169 syl ( 𝜑 → seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ) ∈ dom ⇝ )
171 119 122 eqtrd ( ( 𝜑𝑛 ∈ ℕ0 ) → ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) = ( ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) · ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) )
172 39 171 syldan ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) = ( ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) · ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) )
173 39 75 syldan ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) ∈ ℝ )
174 63 adantr ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → 𝑅 ∈ ℝ )
175 88 adantr ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → ( abs ‘ 𝑋 ) ∈ ℝ )
176 94 adantr ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → 0 ≤ ( abs ‘ 𝑋 ) )
177 175 39 176 expge0d ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → 0 ≤ ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) )
178 40 fveq2d ( 𝑘 = 𝑛 → ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) = ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) )
179 178 breq1d ( 𝑘 = 𝑛 → ( ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < 𝑅 ↔ ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) < 𝑅 ) )
180 179 rspccva ( ( ∀ 𝑘 ∈ ( ℤ𝑁 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < 𝑅𝑛 ∈ ( ℤ𝑁 ) ) → ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) < 𝑅 )
181 11 180 sylan ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) < 𝑅 )
182 173 174 181 ltled ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) ≤ 𝑅 )
183 173 174 158 177 182 lemul1ad ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → ( ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) · ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) ≤ ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) )
184 172 183 eqbrtrd ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ≤ ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) )
185 149 fveq2d ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → ( abs ‘ ( ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋𝑘 ) ) ) ) ‘ 𝑛 ) ) = ( abs ‘ ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ) )
186 absidm ( ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ∈ ℂ → ( abs ‘ ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ) = ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) )
187 47 186 syl ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → ( abs ‘ ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ) = ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) )
188 185 187 eqtrd ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → ( abs ‘ ( ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋𝑘 ) ) ) ) ‘ 𝑛 ) ) = ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) )
189 157 oveq2d ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → ( 𝑅 · ( ( 𝑘 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ‘ 𝑛 ) ) = ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) )
190 184 188 189 3brtr4d ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → ( abs ‘ ( ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋𝑘 ) ) ) ) ‘ 𝑛 ) ) ≤ ( 𝑅 · ( ( 𝑘 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ‘ 𝑛 ) ) )
191 36 152 159 161 170 63 190 cvgcmpce ( 𝜑 → seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋𝑘 ) ) ) ) ) ∈ dom ⇝ )
192 36 37 149 150 191 isumrecl ( 𝜑 → Σ 𝑛 ∈ ( ℤ𝑁 ) ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ∈ ℝ )
193 eldifsni ( 𝑋 ∈ ( 𝑆 ∖ { 1 } ) → 𝑋 ≠ 1 )
194 8 193 syl ( 𝜑𝑋 ≠ 1 )
195 194 necomd ( 𝜑 → 1 ≠ 𝑋 )
196 subeq0 ( ( 1 ∈ ℂ ∧ 𝑋 ∈ ℂ ) → ( ( 1 − 𝑋 ) = 0 ↔ 1 = 𝑋 ) )
197 196 necon3bid ( ( 1 ∈ ℂ ∧ 𝑋 ∈ ℂ ) → ( ( 1 − 𝑋 ) ≠ 0 ↔ 1 ≠ 𝑋 ) )
198 17 19 197 sylancr ( 𝜑 → ( ( 1 − 𝑋 ) ≠ 0 ↔ 1 ≠ 𝑋 ) )
199 195 198 mpbird ( 𝜑 → ( 1 − 𝑋 ) ≠ 0 )
200 21 199 absrpcld ( 𝜑 → ( abs ‘ ( 1 − 𝑋 ) ) ∈ ℝ+ )
201 73 200 rerpdivcld ( 𝜑 → ( ( 𝑀 · 𝑅 ) / ( abs ‘ ( 1 − 𝑋 ) ) ) ∈ ℝ )
202 36 37 46 47 56 isumclim2 ( 𝜑 → seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋𝑘 ) ) ) ) ⇝ Σ 𝑛 ∈ ( ℤ𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) )
203 36 37 149 160 191 isumclim2 ( 𝜑 → seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋𝑘 ) ) ) ) ) ⇝ Σ 𝑛 ∈ ( ℤ𝑁 ) ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) )
204 39 54 syldan ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋𝑘 ) ) ) ‘ 𝑛 ) ∈ ℂ )
205 46 fveq2d ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → ( abs ‘ ( ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋𝑘 ) ) ) ‘ 𝑛 ) ) = ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) )
206 149 205 eqtr4d ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋𝑘 ) ) ) ) ‘ 𝑛 ) = ( abs ‘ ( ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋𝑘 ) ) ) ‘ 𝑛 ) ) )
207 36 202 203 37 204 206 iserabs ( 𝜑 → ( abs ‘ Σ 𝑛 ∈ ( ℤ𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ≤ Σ 𝑛 ∈ ( ℤ𝑁 ) ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) )
208 88 10 reexpcld ( 𝜑 → ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) ∈ ℝ )
209 difrp ( ( ( abs ‘ 𝑋 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( abs ‘ 𝑋 ) < 1 ↔ ( 1 − ( abs ‘ 𝑋 ) ) ∈ ℝ+ ) )
210 88 110 209 sylancl ( 𝜑 → ( ( abs ‘ 𝑋 ) < 1 ↔ ( 1 − ( abs ‘ 𝑋 ) ) ∈ ℝ+ ) )
211 109 210 mpbid ( 𝜑 → ( 1 − ( abs ‘ 𝑋 ) ) ∈ ℝ+ )
212 208 211 rerpdivcld ( 𝜑 → ( ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) / ( 1 − ( abs ‘ 𝑋 ) ) ) ∈ ℝ )
213 63 212 remulcld ( 𝜑 → ( 𝑅 · ( ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) / ( 1 − ( abs ‘ 𝑋 ) ) ) ) ∈ ℝ )
214 153 oveq2d ( 𝑘 = 𝑛 → ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) = ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) )
215 eqid ( 𝑘 ∈ ℕ0 ↦ ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) )
216 ovex ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) ∈ V
217 214 215 216 fvmpt ( 𝑛 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ) ‘ 𝑛 ) = ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) )
218 39 217 syl ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ) ‘ 𝑛 ) = ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) )
219 174 158 remulcld ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) ∈ ℝ )
220 9 rpcnd ( 𝜑𝑅 ∈ ℂ )
221 159 recnd ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ‘ 𝑛 ) ∈ ℂ )
222 218 189 eqtr4d ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ) ‘ 𝑛 ) = ( 𝑅 · ( ( 𝑘 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ‘ 𝑛 ) ) )
223 36 37 220 166 221 222 isermulc2 ( 𝜑 → seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ) ) ⇝ ( 𝑅 · ( ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) / ( 1 − ( abs ‘ 𝑋 ) ) ) ) )
224 seqex seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ) ) ∈ V
225 ovex ( 𝑅 · ( ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) / ( 1 − ( abs ‘ 𝑋 ) ) ) ) ∈ V
226 224 225 breldm ( seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ) ) ⇝ ( 𝑅 · ( ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) / ( 1 − ( abs ‘ 𝑋 ) ) ) ) → seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ) ) ∈ dom ⇝ )
227 223 226 syl ( 𝜑 → seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ) ) ∈ dom ⇝ )
228 36 37 149 150 218 219 184 191 227 isumle ( 𝜑 → Σ 𝑛 ∈ ( ℤ𝑁 ) ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ≤ Σ 𝑛 ∈ ( ℤ𝑁 ) ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) )
229 219 recnd ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) ∈ ℂ )
230 36 37 218 229 223 isumclim ( 𝜑 → Σ 𝑛 ∈ ( ℤ𝑁 ) ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) = ( 𝑅 · ( ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) / ( 1 − ( abs ‘ 𝑋 ) ) ) ) )
231 228 230 breqtrd ( 𝜑 → Σ 𝑛 ∈ ( ℤ𝑁 ) ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ≤ ( 𝑅 · ( ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) / ( 1 − ( abs ‘ 𝑋 ) ) ) ) )
232 9 211 rpdivcld ( 𝜑 → ( 𝑅 / ( 1 − ( abs ‘ 𝑋 ) ) ) ∈ ℝ+ )
233 232 rpred ( 𝜑 → ( 𝑅 / ( 1 − ( abs ‘ 𝑋 ) ) ) ∈ ℝ )
234 208 recnd ( 𝜑 → ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) ∈ ℂ )
235 211 rpcnd ( 𝜑 → ( 1 − ( abs ‘ 𝑋 ) ) ∈ ℂ )
236 211 rpne0d ( 𝜑 → ( 1 − ( abs ‘ 𝑋 ) ) ≠ 0 )
237 220 234 235 236 div12d ( 𝜑 → ( 𝑅 · ( ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) / ( 1 − ( abs ‘ 𝑋 ) ) ) ) = ( ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) · ( 𝑅 / ( 1 − ( abs ‘ 𝑋 ) ) ) ) )
238 1red ( 𝜑 → 1 ∈ ℝ )
239 232 rpge0d ( 𝜑 → 0 ≤ ( 𝑅 / ( 1 − ( abs ‘ 𝑋 ) ) ) )
240 exple1 ( ( ( ( abs ‘ 𝑋 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑋 ) ∧ ( abs ‘ 𝑋 ) ≤ 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) ≤ 1 )
241 88 94 113 10 240 syl31anc ( 𝜑 → ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) ≤ 1 )
242 208 238 233 239 241 lemul1ad ( 𝜑 → ( ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) · ( 𝑅 / ( 1 − ( abs ‘ 𝑋 ) ) ) ) ≤ ( 1 · ( 𝑅 / ( 1 − ( abs ‘ 𝑋 ) ) ) ) )
243 232 rpcnd ( 𝜑 → ( 𝑅 / ( 1 − ( abs ‘ 𝑋 ) ) ) ∈ ℂ )
244 243 mulid2d ( 𝜑 → ( 1 · ( 𝑅 / ( 1 − ( abs ‘ 𝑋 ) ) ) ) = ( 𝑅 / ( 1 − ( abs ‘ 𝑋 ) ) ) )
245 242 244 breqtrd ( 𝜑 → ( ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) · ( 𝑅 / ( 1 − ( abs ‘ 𝑋 ) ) ) ) ≤ ( 𝑅 / ( 1 − ( abs ‘ 𝑋 ) ) ) )
246 237 245 eqbrtrd ( 𝜑 → ( 𝑅 · ( ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) / ( 1 − ( abs ‘ 𝑋 ) ) ) ) ≤ ( 𝑅 / ( 1 − ( abs ‘ 𝑋 ) ) ) )
247 18 simprd ( 𝜑 → ( abs ‘ ( 1 − 𝑋 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑋 ) ) ) )
248 resubcl ( ( 1 ∈ ℝ ∧ ( abs ‘ 𝑋 ) ∈ ℝ ) → ( 1 − ( abs ‘ 𝑋 ) ) ∈ ℝ )
249 110 88 248 sylancr ( 𝜑 → ( 1 − ( abs ‘ 𝑋 ) ) ∈ ℝ )
250 3 249 remulcld ( 𝜑 → ( 𝑀 · ( 1 − ( abs ‘ 𝑋 ) ) ) ∈ ℝ )
251 74 250 9 lemul2d ( 𝜑 → ( ( abs ‘ ( 1 − 𝑋 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑋 ) ) ) ↔ ( 𝑅 · ( abs ‘ ( 1 − 𝑋 ) ) ) ≤ ( 𝑅 · ( 𝑀 · ( 1 − ( abs ‘ 𝑋 ) ) ) ) ) )
252 247 251 mpbid ( 𝜑 → ( 𝑅 · ( abs ‘ ( 1 − 𝑋 ) ) ) ≤ ( 𝑅 · ( 𝑀 · ( 1 − ( abs ‘ 𝑋 ) ) ) ) )
253 3 recnd ( 𝜑𝑀 ∈ ℂ )
254 220 253 235 mul12d ( 𝜑 → ( 𝑅 · ( 𝑀 · ( 1 − ( abs ‘ 𝑋 ) ) ) ) = ( 𝑀 · ( 𝑅 · ( 1 − ( abs ‘ 𝑋 ) ) ) ) )
255 220 235 mulcomd ( 𝜑 → ( 𝑅 · ( 1 − ( abs ‘ 𝑋 ) ) ) = ( ( 1 − ( abs ‘ 𝑋 ) ) · 𝑅 ) )
256 255 oveq2d ( 𝜑 → ( 𝑀 · ( 𝑅 · ( 1 − ( abs ‘ 𝑋 ) ) ) ) = ( 𝑀 · ( ( 1 − ( abs ‘ 𝑋 ) ) · 𝑅 ) ) )
257 253 235 220 mul12d ( 𝜑 → ( 𝑀 · ( ( 1 − ( abs ‘ 𝑋 ) ) · 𝑅 ) ) = ( ( 1 − ( abs ‘ 𝑋 ) ) · ( 𝑀 · 𝑅 ) ) )
258 254 256 257 3eqtrd ( 𝜑 → ( 𝑅 · ( 𝑀 · ( 1 − ( abs ‘ 𝑋 ) ) ) ) = ( ( 1 − ( abs ‘ 𝑋 ) ) · ( 𝑀 · 𝑅 ) ) )
259 252 258 breqtrd ( 𝜑 → ( 𝑅 · ( abs ‘ ( 1 − 𝑋 ) ) ) ≤ ( ( 1 − ( abs ‘ 𝑋 ) ) · ( 𝑀 · 𝑅 ) ) )
260 249 73 remulcld ( 𝜑 → ( ( 1 − ( abs ‘ 𝑋 ) ) · ( 𝑀 · 𝑅 ) ) ∈ ℝ )
261 63 260 200 lemuldivd ( 𝜑 → ( ( 𝑅 · ( abs ‘ ( 1 − 𝑋 ) ) ) ≤ ( ( 1 − ( abs ‘ 𝑋 ) ) · ( 𝑀 · 𝑅 ) ) ↔ 𝑅 ≤ ( ( ( 1 − ( abs ‘ 𝑋 ) ) · ( 𝑀 · 𝑅 ) ) / ( abs ‘ ( 1 − 𝑋 ) ) ) ) )
262 259 261 mpbid ( 𝜑𝑅 ≤ ( ( ( 1 − ( abs ‘ 𝑋 ) ) · ( 𝑀 · 𝑅 ) ) / ( abs ‘ ( 1 − 𝑋 ) ) ) )
263 73 recnd ( 𝜑 → ( 𝑀 · 𝑅 ) ∈ ℂ )
264 74 recnd ( 𝜑 → ( abs ‘ ( 1 − 𝑋 ) ) ∈ ℂ )
265 200 rpne0d ( 𝜑 → ( abs ‘ ( 1 − 𝑋 ) ) ≠ 0 )
266 235 263 264 265 divassd ( 𝜑 → ( ( ( 1 − ( abs ‘ 𝑋 ) ) · ( 𝑀 · 𝑅 ) ) / ( abs ‘ ( 1 − 𝑋 ) ) ) = ( ( 1 − ( abs ‘ 𝑋 ) ) · ( ( 𝑀 · 𝑅 ) / ( abs ‘ ( 1 − 𝑋 ) ) ) ) )
267 262 266 breqtrd ( 𝜑𝑅 ≤ ( ( 1 − ( abs ‘ 𝑋 ) ) · ( ( 𝑀 · 𝑅 ) / ( abs ‘ ( 1 − 𝑋 ) ) ) ) )
268 posdif ( ( ( abs ‘ 𝑋 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( abs ‘ 𝑋 ) < 1 ↔ 0 < ( 1 − ( abs ‘ 𝑋 ) ) ) )
269 88 110 268 sylancl ( 𝜑 → ( ( abs ‘ 𝑋 ) < 1 ↔ 0 < ( 1 − ( abs ‘ 𝑋 ) ) ) )
270 109 269 mpbid ( 𝜑 → 0 < ( 1 − ( abs ‘ 𝑋 ) ) )
271 ledivmul ( ( 𝑅 ∈ ℝ ∧ ( ( 𝑀 · 𝑅 ) / ( abs ‘ ( 1 − 𝑋 ) ) ) ∈ ℝ ∧ ( ( 1 − ( abs ‘ 𝑋 ) ) ∈ ℝ ∧ 0 < ( 1 − ( abs ‘ 𝑋 ) ) ) ) → ( ( 𝑅 / ( 1 − ( abs ‘ 𝑋 ) ) ) ≤ ( ( 𝑀 · 𝑅 ) / ( abs ‘ ( 1 − 𝑋 ) ) ) ↔ 𝑅 ≤ ( ( 1 − ( abs ‘ 𝑋 ) ) · ( ( 𝑀 · 𝑅 ) / ( abs ‘ ( 1 − 𝑋 ) ) ) ) ) )
272 63 201 249 270 271 syl112anc ( 𝜑 → ( ( 𝑅 / ( 1 − ( abs ‘ 𝑋 ) ) ) ≤ ( ( 𝑀 · 𝑅 ) / ( abs ‘ ( 1 − 𝑋 ) ) ) ↔ 𝑅 ≤ ( ( 1 − ( abs ‘ 𝑋 ) ) · ( ( 𝑀 · 𝑅 ) / ( abs ‘ ( 1 − 𝑋 ) ) ) ) ) )
273 267 272 mpbird ( 𝜑 → ( 𝑅 / ( 1 − ( abs ‘ 𝑋 ) ) ) ≤ ( ( 𝑀 · 𝑅 ) / ( abs ‘ ( 1 − 𝑋 ) ) ) )
274 213 233 201 246 273 letrd ( 𝜑 → ( 𝑅 · ( ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) / ( 1 − ( abs ‘ 𝑋 ) ) ) ) ≤ ( ( 𝑀 · 𝑅 ) / ( abs ‘ ( 1 − 𝑋 ) ) ) )
275 192 213 201 231 274 letrd ( 𝜑 → Σ 𝑛 ∈ ( ℤ𝑁 ) ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ≤ ( ( 𝑀 · 𝑅 ) / ( abs ‘ ( 1 − 𝑋 ) ) ) )
276 144 192 201 207 275 letrd ( 𝜑 → ( abs ‘ Σ 𝑛 ∈ ( ℤ𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ≤ ( ( 𝑀 · 𝑅 ) / ( abs ‘ ( 1 − 𝑋 ) ) ) )
277 144 73 200 lemuldiv2d ( 𝜑 → ( ( ( abs ‘ ( 1 − 𝑋 ) ) · ( abs ‘ Σ 𝑛 ∈ ( ℤ𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ) ≤ ( 𝑀 · 𝑅 ) ↔ ( abs ‘ Σ 𝑛 ∈ ( ℤ𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ≤ ( ( 𝑀 · 𝑅 ) / ( abs ‘ ( 1 − 𝑋 ) ) ) ) )
278 276 277 mpbird ( 𝜑 → ( ( abs ‘ ( 1 − 𝑋 ) ) · ( abs ‘ Σ 𝑛 ∈ ( ℤ𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ) ≤ ( 𝑀 · 𝑅 ) )
279 143 278 eqbrtrd ( 𝜑 → ( abs ‘ ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( ℤ𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ) ≤ ( 𝑀 · 𝑅 ) )
280 35 59 63 73 142 279 ltleaddd ( 𝜑 → ( ( abs ‘ ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ) + ( abs ‘ ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( ℤ𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ) ) < ( 𝑅 + ( 𝑀 · 𝑅 ) ) )
281 1cnd ( 𝜑 → 1 ∈ ℂ )
282 253 281 220 adddird ( 𝜑 → ( ( 𝑀 + 1 ) · 𝑅 ) = ( ( 𝑀 · 𝑅 ) + ( 1 · 𝑅 ) ) )
283 220 mulid2d ( 𝜑 → ( 1 · 𝑅 ) = 𝑅 )
284 283 oveq2d ( 𝜑 → ( ( 𝑀 · 𝑅 ) + ( 1 · 𝑅 ) ) = ( ( 𝑀 · 𝑅 ) + 𝑅 ) )
285 263 220 addcomd ( 𝜑 → ( ( 𝑀 · 𝑅 ) + 𝑅 ) = ( 𝑅 + ( 𝑀 · 𝑅 ) ) )
286 282 284 285 3eqtrd ( 𝜑 → ( ( 𝑀 + 1 ) · 𝑅 ) = ( 𝑅 + ( 𝑀 · 𝑅 ) ) )
287 280 286 breqtrrd ( 𝜑 → ( ( abs ‘ ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ) + ( abs ‘ ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( ℤ𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋𝑛 ) ) ) ) ) < ( ( 𝑀 + 1 ) · 𝑅 ) )
288 16 60 64 72 287 lelttrd ( 𝜑 → ( abs ‘ ( 𝐹𝑋 ) ) < ( ( 𝑀 + 1 ) · 𝑅 ) )