Metamath Proof Explorer

Theorem ftalem1

Description: Lemma for fta : "growth lemma". There exists some r such that F is arbitrarily close in proportion to its dominant term. (Contributed by Mario Carneiro, 14-Sep-2014)

Ref Expression
Hypotheses ftalem.1 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
ftalem.2 ⊢ 𝑁 = ( deg ‘ 𝐹 )
ftalem.3 ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
ftalem.4 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
ftalem1.5 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
ftalem1.6 ⊢ 𝑇 = ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) / 𝐸 )
Assertion ftalem1 ( 𝜑 → ∃ 𝑟 ∈ ℝ ∀ 𝑥 ∈ ℂ ( 𝑟 < ( abs ‘ 𝑥 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( ( 𝐴 ‘ 𝑁 ) · ( 𝑥 ↑ 𝑁 ) ) ) ) < ( 𝐸 · ( ( abs ‘ 𝑥 ) ↑ 𝑁 ) ) ) )

Proof

Step Hyp Ref Expression
1 ftalem.1 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
2 ftalem.2 ⊢ 𝑁 = ( deg ‘ 𝐹 )
3 ftalem.3 ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
4 ftalem.4 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
5 ftalem1.5 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
6 ftalem1.6 ⊢ 𝑇 = ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) / 𝐸 )
7 fzfid ⊢ ( 𝜑 → ( 0 ... ( 𝑁 − 1 ) ) ∈ Fin )
8 1 coef3 ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐴 : ℕ0 ⟶ ℂ )
9 3 8 syl ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
10 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ℕ0 )
11 ffvelcdm ⊢ ( ( 𝐴 : ℕ0 ⟶ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
12 9 10 11 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
13 12 abscld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) ∈ ℝ )
14 7 13 fsumrecl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) ∈ ℝ )
15 14 5 rerpdivcld ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) / 𝐸 ) ∈ ℝ )
16 6 15 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
17 1re ⊢ 1 ∈ ℝ
18 ifcl ⊢ ( ( 𝑇 ∈ ℝ ∧ 1 ∈ ℝ ) → if ( 1 ≤ 𝑇 , 𝑇 , 1 ) ∈ ℝ )
19 16 17 18 sylancl ⊢ ( 𝜑 → if ( 1 ≤ 𝑇 , 𝑇 , 1 ) ∈ ℝ )
20 fzfid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( 0 ... ( 𝑁 − 1 ) ) ∈ Fin )
21 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 𝐴 : ℕ0 ⟶ ℂ )
22 21 11 sylan ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
23 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 𝑥 ∈ ℂ )
24 expcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑥 ↑ 𝑘 ) ∈ ℂ )
25 23 24 sylan ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑥 ↑ 𝑘 ) ∈ ℂ )
26 22 25 mulcld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ∈ ℂ )
27 10 26 sylan2 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ∈ ℂ )
28 20 27 fsumcl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ∈ ℂ )
29 4 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
30 29 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 𝑁 ∈ ℕ0 )
31 21 30 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( 𝐴 ‘ 𝑁 ) ∈ ℂ )
32 23 30 expcld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( 𝑥 ↑ 𝑁 ) ∈ ℂ )
33 31 32 mulcld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( ( 𝐴 ‘ 𝑁 ) · ( 𝑥 ↑ 𝑁 ) ) ∈ ℂ )
34 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
35 1 2 coeid2 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑥 ∈ ℂ ) → ( 𝐹 ‘ 𝑥 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) )
36 34 23 35 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( 𝐹 ‘ 𝑥 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) )
37 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
38 30 37 eleqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
39 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
40 39 26 sylan2 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ∈ ℂ )
41 fveq2 ⊢ ( 𝑘 = 𝑁 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑁 ) )
42 oveq2 ⊢ ( 𝑘 = 𝑁 → ( 𝑥 ↑ 𝑘 ) = ( 𝑥 ↑ 𝑁 ) )
43 41 42 oveq12d ⊢ ( 𝑘 = 𝑁 → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) = ( ( 𝐴 ‘ 𝑁 ) · ( 𝑥 ↑ 𝑁 ) ) )
44 38 40 43 fsumm1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) = ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) + ( ( 𝐴 ‘ 𝑁 ) · ( 𝑥 ↑ 𝑁 ) ) ) )
45 36 44 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( 𝐹 ‘ 𝑥 ) = ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) + ( ( 𝐴 ‘ 𝑁 ) · ( 𝑥 ↑ 𝑁 ) ) ) )
46 28 33 45 mvrraddd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) − ( ( 𝐴 ‘ 𝑁 ) · ( 𝑥 ↑ 𝑁 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) )
47 46 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( ( 𝐴 ‘ 𝑁 ) · ( 𝑥 ↑ 𝑁 ) ) ) ) = ( abs ‘ Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ) )
48 28 abscld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( abs ‘ Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ) ∈ ℝ )
49 27 abscld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ) ∈ ℝ )
50 20 49 fsumrecl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ) ∈ ℝ )
51 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 𝐸 ∈ ℝ+ )
52 51 rpred ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 𝐸 ∈ ℝ )
53 23 abscld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( abs ‘ 𝑥 ) ∈ ℝ )
54 53 30 reexpcld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( ( abs ‘ 𝑥 ) ↑ 𝑁 ) ∈ ℝ )
55 52 54 remulcld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( 𝐸 · ( ( abs ‘ 𝑥 ) ↑ 𝑁 ) ) ∈ ℝ )
56 20 27 fsumabs ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( abs ‘ Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ) ≤ Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ) )
57 14 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) ∈ ℝ )
58 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 𝑁 ∈ ℕ )
59 nnm1nn0 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
60 58 59 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( 𝑁 − 1 ) ∈ ℕ0 )
61 53 60 reexpcld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ∈ ℝ )
62 57 61 remulcld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ∈ ℝ )
63 13 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) ∈ ℝ )
64 61 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ∈ ℝ )
65 63 64 remulcld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ∈ ℝ )
66 22 25 absmuld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ℕ0 ) → ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ) = ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( abs ‘ ( 𝑥 ↑ 𝑘 ) ) ) )
67 10 66 sylan2 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ) = ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( abs ‘ ( 𝑥 ↑ 𝑘 ) ) ) )
68 10 25 sylan2 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑥 ↑ 𝑘 ) ∈ ℂ )
69 68 abscld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( abs ‘ ( 𝑥 ↑ 𝑘 ) ) ∈ ℝ )
70 10 22 sylan2 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
71 70 absge0d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 0 ≤ ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) )
72 absexp ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( abs ‘ ( 𝑥 ↑ 𝑘 ) ) = ( ( abs ‘ 𝑥 ) ↑ 𝑘 ) )
73 23 10 72 syl2an ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( abs ‘ ( 𝑥 ↑ 𝑘 ) ) = ( ( abs ‘ 𝑥 ) ↑ 𝑘 ) )
74 53 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( abs ‘ 𝑥 ) ∈ ℝ )
75 17 a1i ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 1 ∈ ℝ )
76 19 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → if ( 1 ≤ 𝑇 , 𝑇 , 1 ) ∈ ℝ )
77 max1 ⊢ ( ( 1 ∈ ℝ ∧ 𝑇 ∈ ℝ ) → 1 ≤ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) )
78 17 16 77 sylancr ⊢ ( 𝜑 → 1 ≤ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) )
79 78 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 1 ≤ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) )
80 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) )
81 75 76 53 79 80 lelttrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 1 < ( abs ‘ 𝑥 ) )
82 75 53 81 ltled ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 1 ≤ ( abs ‘ 𝑥 ) )
83 82 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 1 ≤ ( abs ‘ 𝑥 ) )
84 elfzuz3 ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑘 ) )
85 84 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑘 ) )
86 74 83 85 leexp2ad ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( abs ‘ 𝑥 ) ↑ 𝑘 ) ≤ ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) )
87 73 86 eqbrtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( abs ‘ ( 𝑥 ↑ 𝑘 ) ) ≤ ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) )
88 69 64 63 71 87 lemul2ad ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( abs ‘ ( 𝑥 ↑ 𝑘 ) ) ) ≤ ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) )
89 67 88 eqbrtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ) ≤ ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) )
90 20 49 65 89 fsumle ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ) ≤ Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) )
91 61 recnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ∈ ℂ )
92 63 recnd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) ∈ ℂ )
93 20 91 92 fsummulc1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) )
94 90 93 breqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ) ≤ ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) )
95 16 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 𝑇 ∈ ℝ )
96 max2 ⊢ ( ( 1 ∈ ℝ ∧ 𝑇 ∈ ℝ ) → 𝑇 ≤ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) )
97 17 16 96 sylancr ⊢ ( 𝜑 → 𝑇 ≤ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) )
98 97 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 𝑇 ≤ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) )
99 95 76 53 98 80 lelttrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 𝑇 < ( abs ‘ 𝑥 ) )
100 6 99 eqbrtrrid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) / 𝐸 ) < ( abs ‘ 𝑥 ) )
101 57 53 51 ltdivmuld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) / 𝐸 ) < ( abs ‘ 𝑥 ) ↔ Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) < ( 𝐸 · ( abs ‘ 𝑥 ) ) ) )
102 100 101 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) < ( 𝐸 · ( abs ‘ 𝑥 ) ) )
103 52 53 remulcld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( 𝐸 · ( abs ‘ 𝑥 ) ) ∈ ℝ )
104 60 nn0zd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( 𝑁 − 1 ) ∈ ℤ )
105 0red ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 0 ∈ ℝ )
106 0lt1 ⊢ 0 < 1
107 106 a1i ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 0 < 1 )
108 105 75 53 107 81 lttrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 0 < ( abs ‘ 𝑥 ) )
109 expgt0 ⊢ ( ( ( abs ‘ 𝑥 ) ∈ ℝ ∧ ( 𝑁 − 1 ) ∈ ℤ ∧ 0 < ( abs ‘ 𝑥 ) ) → 0 < ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) )
110 53 104 108 109 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 0 < ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) )
111 ltmul1 ⊢ ( ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) ∈ ℝ ∧ ( 𝐸 · ( abs ‘ 𝑥 ) ) ∈ ℝ ∧ ( ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ∈ ℝ ∧ 0 < ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ) → ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) < ( 𝐸 · ( abs ‘ 𝑥 ) ) ↔ ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) < ( ( 𝐸 · ( abs ‘ 𝑥 ) ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ) )
112 57 103 61 110 111 syl112anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) < ( 𝐸 · ( abs ‘ 𝑥 ) ) ↔ ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) < ( ( 𝐸 · ( abs ‘ 𝑥 ) ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ) )
113 102 112 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) < ( ( 𝐸 · ( abs ‘ 𝑥 ) ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) )
114 53 recnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( abs ‘ 𝑥 ) ∈ ℂ )
115 expm1t ⊢ ( ( ( abs ‘ 𝑥 ) ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( abs ‘ 𝑥 ) ↑ 𝑁 ) = ( ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) · ( abs ‘ 𝑥 ) ) )
116 114 58 115 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( ( abs ‘ 𝑥 ) ↑ 𝑁 ) = ( ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) · ( abs ‘ 𝑥 ) ) )
117 91 114 mulcomd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) · ( abs ‘ 𝑥 ) ) = ( ( abs ‘ 𝑥 ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) )
118 116 117 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( ( abs ‘ 𝑥 ) ↑ 𝑁 ) = ( ( abs ‘ 𝑥 ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) )
119 118 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( 𝐸 · ( ( abs ‘ 𝑥 ) ↑ 𝑁 ) ) = ( 𝐸 · ( ( abs ‘ 𝑥 ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ) )
120 52 recnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 𝐸 ∈ ℂ )
121 120 114 91 mulassd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( ( 𝐸 · ( abs ‘ 𝑥 ) ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) = ( 𝐸 · ( ( abs ‘ 𝑥 ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ) )
122 119 121 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( 𝐸 · ( ( abs ‘ 𝑥 ) ↑ 𝑁 ) ) = ( ( 𝐸 · ( abs ‘ 𝑥 ) ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) )
123 113 122 breqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) < ( 𝐸 · ( ( abs ‘ 𝑥 ) ↑ 𝑁 ) ) )
124 50 62 55 94 123 lelttrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ) < ( 𝐸 · ( ( abs ‘ 𝑥 ) ↑ 𝑁 ) ) )
125 48 50 55 56 124 lelttrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( abs ‘ Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ) < ( 𝐸 · ( ( abs ‘ 𝑥 ) ↑ 𝑁 ) ) )
126 47 125 eqbrtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( ( 𝐴 ‘ 𝑁 ) · ( 𝑥 ↑ 𝑁 ) ) ) ) < ( 𝐸 · ( ( abs ‘ 𝑥 ) ↑ 𝑁 ) ) )
127 126 expr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( ( 𝐴 ‘ 𝑁 ) · ( 𝑥 ↑ 𝑁 ) ) ) ) < ( 𝐸 · ( ( abs ‘ 𝑥 ) ↑ 𝑁 ) ) ) )
128 127 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℂ ( if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( ( 𝐴 ‘ 𝑁 ) · ( 𝑥 ↑ 𝑁 ) ) ) ) < ( 𝐸 · ( ( abs ‘ 𝑥 ) ↑ 𝑁 ) ) ) )
129 breq1 ⊢ ( 𝑟 = if ( 1 ≤ 𝑇 , 𝑇 , 1 ) → ( 𝑟 < ( abs ‘ 𝑥 ) ↔ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) )
130 129 rspceaimv ⊢ ( ( if ( 1 ≤ 𝑇 , 𝑇 , 1 ) ∈ ℝ ∧ ∀ 𝑥 ∈ ℂ ( if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( ( 𝐴 ‘ 𝑁 ) · ( 𝑥 ↑ 𝑁 ) ) ) ) < ( 𝐸 · ( ( abs ‘ 𝑥 ) ↑ 𝑁 ) ) ) ) → ∃ 𝑟 ∈ ℝ ∀ 𝑥 ∈ ℂ ( 𝑟 < ( abs ‘ 𝑥 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( ( 𝐴 ‘ 𝑁 ) · ( 𝑥 ↑ 𝑁 ) ) ) ) < ( 𝐸 · ( ( abs ‘ 𝑥 ) ↑ 𝑁 ) ) ) )
131 19 128 130 syl2anc ⊢ ( 𝜑 → ∃ 𝑟 ∈ ℝ ∀ 𝑥 ∈ ℂ ( 𝑟 < ( abs ‘ 𝑥 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( ( 𝐴 ‘ 𝑁 ) · ( 𝑥 ↑ 𝑁 ) ) ) ) < ( 𝐸 · ( ( abs ‘ 𝑥 ) ↑ 𝑁 ) ) ) )