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 ) · 𝑅 ) )