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 ffvelrn ( ( 𝐴 : ℕ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 ffvelrnd ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ 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 ‘ 𝑥 ) ↑ 𝑁 ) ) ) )