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 ⊢A=coeff⁡F
ftalem.2 ⊢N=deg⁡F
ftalem.3 ⊢φ→F∈Poly⁡S
ftalem.4 ⊢φ→N∈ℕ
ftalem1.5 ⊢φ→E∈ℝ+
ftalem1.6 ⊢T=∑k=0N−1A⁡kE
Assertion ftalem1 ⊢φ→∃r∈ℝ∀x∈ℂr<x→F⁡x−A⁡N⁢xN<E⁢xN

Proof

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