Metamath Proof Explorer

Theorem ftalem5

Description: Lemma for fta : Main proof. We have already shifted the minimum found in ftalem3 to zero by a change of variables, and now we show that the minimum value is zero. Expanding in a series about the minimum value, let K be the lowest term in the polynomial that is nonzero, and let T be a K -th root of -u F ( 0 ) / A ( K ) . Then an evaluation of F ( T X ) where X is a sufficiently small positive number yields F ( 0 ) for the first term and -u F ( 0 ) x. X ^ K for the K -th term, and all higher terms are bounded because X is small. Thus, abs ( F ( T X ) ) <_ abs ( F ( 0 ) ) ( 1 - X ^ K ) < abs ( F ( 0 ) ) , in contradiction to our choice of F ( 0 ) as the minimum. (Contributed by Mario Carneiro, 14-Sep-2014) (Revised by AV, 28-Sep-2020)

Ref Expression
Hypotheses ftalem.1 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
ftalem.2 ⊢ 𝑁 = ( deg ‘ 𝐹 )
ftalem.3 ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
ftalem.4 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
ftalem4.5 ⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) ≠ 0 )
ftalem4.6 ⊢ 𝐾 = inf ( { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } , ℝ , < )
ftalem4.7 ⊢ 𝑇 = ( - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ 𝐾 ) ) ↑𝑐 ( 1 / 𝐾 ) )
ftalem4.8 ⊢ 𝑈 = ( ( abs ‘ ( 𝐹 ‘ 0 ) ) / ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) + 1 ) )
ftalem4.9 ⊢ 𝑋 = if ( 1 ≤ 𝑈 , 1 , 𝑈 )
Assertion ftalem5 ( 𝜑 → ∃ 𝑥 ∈ ℂ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) < ( abs ‘ ( 𝐹 ‘ 0 ) ) )

Proof

Step Hyp Ref Expression
1 ftalem.1 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
2 ftalem.2 ⊢ 𝑁 = ( deg ‘ 𝐹 )
3 ftalem.3 ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
4 ftalem.4 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
5 ftalem4.5 ⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) ≠ 0 )
6 ftalem4.6 ⊢ 𝐾 = inf ( { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } , ℝ , < )
7 ftalem4.7 ⊢ 𝑇 = ( - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ 𝐾 ) ) ↑𝑐 ( 1 / 𝐾 ) )
8 ftalem4.8 ⊢ 𝑈 = ( ( abs ‘ ( 𝐹 ‘ 0 ) ) / ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) + 1 ) )
9 ftalem4.9 ⊢ 𝑋 = if ( 1 ≤ 𝑈 , 1 , 𝑈 )
10 1 2 3 4 5 6 7 8 9 ftalem4 ⊢ ( 𝜑 → ( ( 𝐾 ∈ ℕ ∧ ( 𝐴 ‘ 𝐾 ) ≠ 0 ) ∧ ( 𝑇 ∈ ℂ ∧ 𝑈 ∈ ℝ+ ∧ 𝑋 ∈ ℝ+ ) ) )
11 10 simprd ⊢ ( 𝜑 → ( 𝑇 ∈ ℂ ∧ 𝑈 ∈ ℝ+ ∧ 𝑋 ∈ ℝ+ ) )
12 11 simp1d ⊢ ( 𝜑 → 𝑇 ∈ ℂ )
13 11 simp3d ⊢ ( 𝜑 → 𝑋 ∈ ℝ+ )
14 13 rpred ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
15 14 recnd ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
16 12 15 mulcld ⊢ ( 𝜑 → ( 𝑇 · 𝑋 ) ∈ ℂ )
17 plyf ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 : ℂ ⟶ ℂ )
18 3 17 syl ⊢ ( 𝜑 → 𝐹 : ℂ ⟶ ℂ )
19 18 16 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑇 · 𝑋 ) ) ∈ ℂ )
20 19 abscld ⊢ ( 𝜑 → ( abs ‘ ( 𝐹 ‘ ( 𝑇 · 𝑋 ) ) ) ∈ ℝ )
21 0cn ⊢ 0 ∈ ℂ
22 ffvelrn ⊢ ( ( 𝐹 : ℂ ⟶ ℂ ∧ 0 ∈ ℂ ) → ( 𝐹 ‘ 0 ) ∈ ℂ )
23 18 21 22 sylancl ⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) ∈ ℂ )
24 23 abscld ⊢ ( 𝜑 → ( abs ‘ ( 𝐹 ‘ 0 ) ) ∈ ℝ )
25 10 simpld ⊢ ( 𝜑 → ( 𝐾 ∈ ℕ ∧ ( 𝐴 ‘ 𝐾 ) ≠ 0 ) )
26 25 simpld ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
27 26 nnnn0d ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
28 14 27 reexpcld ⊢ ( 𝜑 → ( 𝑋 ↑ 𝐾 ) ∈ ℝ )
29 24 28 remulcld ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐹 ‘ 0 ) ) · ( 𝑋 ↑ 𝐾 ) ) ∈ ℝ )
30 24 29 resubcld ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐹 ‘ 0 ) ) − ( ( abs ‘ ( 𝐹 ‘ 0 ) ) · ( 𝑋 ↑ 𝐾 ) ) ) ∈ ℝ )
31 fzfid ⊢ ( 𝜑 → ( ( 𝐾 + 1 ) ... 𝑁 ) ∈ Fin )
32 1 coef3 ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐴 : ℕ0 ⟶ ℂ )
33 3 32 syl ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
34 peano2nn0 ⊢ ( 𝐾 ∈ ℕ0 → ( 𝐾 + 1 ) ∈ ℕ0 )
35 27 34 syl ⊢ ( 𝜑 → ( 𝐾 + 1 ) ∈ ℕ0 )
36 elfzuz ⊢ ( 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) → 𝑘 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) )
37 eluznn0 ⊢ ( ( ( 𝐾 + 1 ) ∈ ℕ0 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) ) → 𝑘 ∈ ℕ0 )
38 35 36 37 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → 𝑘 ∈ ℕ0 )
39 ffvelrn ⊢ ( ( 𝐴 : ℕ0 ⟶ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
40 33 38 39 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
41 16 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( 𝑇 · 𝑋 ) ∈ ℂ )
42 41 38 expcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ∈ ℂ )
43 40 42 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ∈ ℂ )
44 31 43 fsumcl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ∈ ℂ )
45 44 abscld ⊢ ( 𝜑 → ( abs ‘ Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ) ∈ ℝ )
46 30 45 readdcld ⊢ ( 𝜑 → ( ( ( abs ‘ ( 𝐹 ‘ 0 ) ) − ( ( abs ‘ ( 𝐹 ‘ 0 ) ) · ( 𝑋 ↑ 𝐾 ) ) ) + ( abs ‘ Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ) ) ∈ ℝ )
47 fzfid ⊢ ( 𝜑 → ( 0 ... 𝐾 ) ∈ Fin )
48 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝐾 ) → 𝑘 ∈ ℕ0 )
49 33 48 39 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
50 expcl ⊢ ( ( ( 𝑇 · 𝑋 ) ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ∈ ℂ )
51 16 48 50 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ∈ ℂ )
52 49 51 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝐾 ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ∈ ℂ )
53 47 52 fsumcl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 𝐾 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ∈ ℂ )
54 53 44 abstrid ⊢ ( 𝜑 → ( abs ‘ ( Σ 𝑘 ∈ ( 0 ... 𝐾 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) + Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ) ) ≤ ( ( abs ‘ Σ 𝑘 ∈ ( 0 ... 𝐾 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ) + ( abs ‘ Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ) ) )
55 1 2 coeid2 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑇 · 𝑋 ) ∈ ℂ ) → ( 𝐹 ‘ ( 𝑇 · 𝑋 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) )
56 3 16 55 syl2anc ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑇 · 𝑋 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) )
57 26 nnred ⊢ ( 𝜑 → 𝐾 ∈ ℝ )
58 57 ltp1d ⊢ ( 𝜑 → 𝐾 < ( 𝐾 + 1 ) )
59 fzdisj ⊢ ( 𝐾 < ( 𝐾 + 1 ) → ( ( 0 ... 𝐾 ) ∩ ( ( 𝐾 + 1 ) ... 𝑁 ) ) = ∅ )
60 58 59 syl ⊢ ( 𝜑 → ( ( 0 ... 𝐾 ) ∩ ( ( 𝐾 + 1 ) ... 𝑁 ) ) = ∅ )
61 ssrab2 ⊢ { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } ⊆ ℕ
62 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
63 61 62 sseqtri ⊢ { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } ⊆ ( ℤ≥ ‘ 1 )
64 fveq2 ⊢ ( 𝑛 = 𝑁 → ( 𝐴 ‘ 𝑛 ) = ( 𝐴 ‘ 𝑁 ) )
65 64 neeq1d ⊢ ( 𝑛 = 𝑁 → ( ( 𝐴 ‘ 𝑛 ) ≠ 0 ↔ ( 𝐴 ‘ 𝑁 ) ≠ 0 ) )
66 4 nnne0d ⊢ ( 𝜑 → 𝑁 ≠ 0 )
67 2 1 dgreq0 ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝐹 = 0𝑝 ↔ ( 𝐴 ‘ 𝑁 ) = 0 ) )
68 3 67 syl ⊢ ( 𝜑 → ( 𝐹 = 0𝑝 ↔ ( 𝐴 ‘ 𝑁 ) = 0 ) )
69 fveq2 ⊢ ( 𝐹 = 0𝑝 → ( deg ‘ 𝐹 ) = ( deg ‘ 0𝑝 ) )
70 dgr0 ⊢ ( deg ‘ 0𝑝 ) = 0
71 69 70 syl6eq ⊢ ( 𝐹 = 0𝑝 → ( deg ‘ 𝐹 ) = 0 )
72 2 71 syl5eq ⊢ ( 𝐹 = 0𝑝 → 𝑁 = 0 )
73 68 72 syl6bir ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑁 ) = 0 → 𝑁 = 0 ) )
74 73 necon3d ⊢ ( 𝜑 → ( 𝑁 ≠ 0 → ( 𝐴 ‘ 𝑁 ) ≠ 0 ) )
75 66 74 mpd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑁 ) ≠ 0 )
76 65 4 75 elrabd ⊢ ( 𝜑 → 𝑁 ∈ { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } )
77 infssuzle ⊢ ( ( { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } ⊆ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } ) → inf ( { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } , ℝ , < ) ≤ 𝑁 )
78 63 76 77 sylancr ⊢ ( 𝜑 → inf ( { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } , ℝ , < ) ≤ 𝑁 )
79 6 78 eqbrtrid ⊢ ( 𝜑 → 𝐾 ≤ 𝑁 )
80 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
81 27 80 eleqtrdi ⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 0 ) )
82 4 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
83 elfz5 ⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ( 0 ... 𝑁 ) ↔ 𝐾 ≤ 𝑁 ) )
84 81 82 83 syl2anc ⊢ ( 𝜑 → ( 𝐾 ∈ ( 0 ... 𝑁 ) ↔ 𝐾 ≤ 𝑁 ) )
85 79 84 mpbird ⊢ ( 𝜑 → 𝐾 ∈ ( 0 ... 𝑁 ) )
86 fzsplit ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 0 ... 𝑁 ) = ( ( 0 ... 𝐾 ) ∪ ( ( 𝐾 + 1 ) ... 𝑁 ) ) )
87 85 86 syl ⊢ ( 𝜑 → ( 0 ... 𝑁 ) = ( ( 0 ... 𝐾 ) ∪ ( ( 𝐾 + 1 ) ... 𝑁 ) ) )
88 fzfid ⊢ ( 𝜑 → ( 0 ... 𝑁 ) ∈ Fin )
89 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
90 33 89 39 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
91 16 89 50 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ∈ ℂ )
92 90 91 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ∈ ℂ )
93 60 87 88 92 fsumsplit ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) = ( Σ 𝑘 ∈ ( 0 ... 𝐾 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) + Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ) )
94 56 93 eqtrd ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑇 · 𝑋 ) ) = ( Σ 𝑘 ∈ ( 0 ... 𝐾 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) + Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ) )
95 94 fveq2d ⊢ ( 𝜑 → ( abs ‘ ( 𝐹 ‘ ( 𝑇 · 𝑋 ) ) ) = ( abs ‘ ( Σ 𝑘 ∈ ( 0 ... 𝐾 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) + Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ) ) )
96 1 coefv0 ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝐹 ‘ 0 ) = ( 𝐴 ‘ 0 ) )
97 3 96 syl ⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) = ( 𝐴 ‘ 0 ) )
98 97 eqcomd ⊢ ( 𝜑 → ( 𝐴 ‘ 0 ) = ( 𝐹 ‘ 0 ) )
99 16 exp0d ⊢ ( 𝜑 → ( ( 𝑇 · 𝑋 ) ↑ 0 ) = 1 )
100 98 99 oveq12d ⊢ ( 𝜑 → ( ( 𝐴 ‘ 0 ) · ( ( 𝑇 · 𝑋 ) ↑ 0 ) ) = ( ( 𝐹 ‘ 0 ) · 1 ) )
101 23 mulid1d ⊢ ( 𝜑 → ( ( 𝐹 ‘ 0 ) · 1 ) = ( 𝐹 ‘ 0 ) )
102 100 101 eqtrd ⊢ ( 𝜑 → ( ( 𝐴 ‘ 0 ) · ( ( 𝑇 · 𝑋 ) ↑ 0 ) ) = ( 𝐹 ‘ 0 ) )
103 1e0p1 ⊢ 1 = ( 0 + 1 )
104 103 oveq1i ⊢ ( 1 ... 𝐾 ) = ( ( 0 + 1 ) ... 𝐾 )
105 104 sumeq1i ⊢ Σ 𝑘 ∈ ( 1 ... 𝐾 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( ( 0 + 1 ) ... 𝐾 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) )
106 26 62 eleqtrdi ⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 1 ) )
107 elfznn ⊢ ( 𝑘 ∈ ( 1 ... 𝐾 ) → 𝑘 ∈ ℕ )
108 107 nnnn0d ⊢ ( 𝑘 ∈ ( 1 ... 𝐾 ) → 𝑘 ∈ ℕ0 )
109 33 108 39 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝐾 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
110 16 108 50 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝐾 ) ) → ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ∈ ℂ )
111 109 110 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝐾 ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ∈ ℂ )
112 fveq2 ⊢ ( 𝑘 = 𝐾 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝐾 ) )
113 oveq2 ⊢ ( 𝑘 = 𝐾 → ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) = ( ( 𝑇 · 𝑋 ) ↑ 𝐾 ) )
114 112 113 oveq12d ⊢ ( 𝑘 = 𝐾 → ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) = ( ( 𝐴 ‘ 𝐾 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝐾 ) ) )
115 106 111 114 fsumm1 ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 1 ... 𝐾 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) = ( Σ 𝑘 ∈ ( 1 ... ( 𝐾 − 1 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) + ( ( 𝐴 ‘ 𝐾 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝐾 ) ) ) )
116 105 115 syl5eqr ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 0 + 1 ) ... 𝐾 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) = ( Σ 𝑘 ∈ ( 1 ... ( 𝐾 − 1 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) + ( ( 𝐴 ‘ 𝐾 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝐾 ) ) ) )
117 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( 𝐾 − 1 ) ) → 𝑘 ∈ ℕ )
118 117 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → 𝑘 ∈ ℕ )
119 118 nnred ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → 𝑘 ∈ ℝ )
120 57 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → 𝐾 ∈ ℝ )
121 peano2rem ⊢ ( 𝐾 ∈ ℝ → ( 𝐾 − 1 ) ∈ ℝ )
122 120 121 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( 𝐾 − 1 ) ∈ ℝ )
123 elfzle2 ⊢ ( 𝑘 ∈ ( 1 ... ( 𝐾 − 1 ) ) → 𝑘 ≤ ( 𝐾 − 1 ) )
124 123 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → 𝑘 ≤ ( 𝐾 − 1 ) )
125 120 ltm1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( 𝐾 − 1 ) < 𝐾 )
126 119 122 120 124 125 lelttrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → 𝑘 < 𝐾 )
127 119 120 ltnled ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( 𝑘 < 𝐾 ↔ ¬ 𝐾 ≤ 𝑘 ) )
128 126 127 mpbid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ¬ 𝐾 ≤ 𝑘 )
129 infssuzle ⊢ ( ( { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } ⊆ ( ℤ≥ ‘ 1 ) ∧ 𝑘 ∈ { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } ) → inf ( { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } , ℝ , < ) ≤ 𝑘 )
130 6 129 eqbrtrid ⊢ ( ( { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } ⊆ ( ℤ≥ ‘ 1 ) ∧ 𝑘 ∈ { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } ) → 𝐾 ≤ 𝑘 )
131 63 130 mpan ⊢ ( 𝑘 ∈ { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } → 𝐾 ≤ 𝑘 )
132 128 131 nsyl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ¬ 𝑘 ∈ { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } )
133 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐴 ‘ 𝑛 ) = ( 𝐴 ‘ 𝑘 ) )
134 133 neeq1d ⊢ ( 𝑛 = 𝑘 → ( ( 𝐴 ‘ 𝑛 ) ≠ 0 ↔ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) )
135 134 elrab3 ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 ∈ { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } ↔ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) )
136 118 135 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( 𝑘 ∈ { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } ↔ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) )
137 136 necon2bbid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) = 0 ↔ ¬ 𝑘 ∈ { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } ) )
138 132 137 mpbird ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( 𝐴 ‘ 𝑘 ) = 0 )
139 138 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) = ( 0 · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) )
140 117 nnnn0d ⊢ ( 𝑘 ∈ ( 1 ... ( 𝐾 − 1 ) ) → 𝑘 ∈ ℕ0 )
141 16 140 50 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ∈ ℂ )
142 141 mul02d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( 0 · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) = 0 )
143 139 142 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) = 0 )
144 143 sumeq2dv ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 1 ... ( 𝐾 − 1 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 1 ... ( 𝐾 − 1 ) ) 0 )
145 fzfi ⊢ ( 1 ... ( 𝐾 − 1 ) ) ∈ Fin
146 145 olci ⊢ ( ( 1 ... ( 𝐾 − 1 ) ) ⊆ ( ℤ≥ ‘ 1 ) ∨ ( 1 ... ( 𝐾 − 1 ) ) ∈ Fin )
147 sumz ⊢ ( ( ( 1 ... ( 𝐾 − 1 ) ) ⊆ ( ℤ≥ ‘ 1 ) ∨ ( 1 ... ( 𝐾 − 1 ) ) ∈ Fin ) → Σ 𝑘 ∈ ( 1 ... ( 𝐾 − 1 ) ) 0 = 0 )
148 146 147 ax-mp ⊢ Σ 𝑘 ∈ ( 1 ... ( 𝐾 − 1 ) ) 0 = 0
149 144 148 syl6eq ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 1 ... ( 𝐾 − 1 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) = 0 )
150 12 15 27 mulexpd ⊢ ( 𝜑 → ( ( 𝑇 · 𝑋 ) ↑ 𝐾 ) = ( ( 𝑇 ↑ 𝐾 ) · ( 𝑋 ↑ 𝐾 ) ) )
151 150 oveq2d ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝐾 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝐾 ) ) = ( ( 𝐴 ‘ 𝐾 ) · ( ( 𝑇 ↑ 𝐾 ) · ( 𝑋 ↑ 𝐾 ) ) ) )
152 33 27 ffvelrnd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐾 ) ∈ ℂ )
153 12 27 expcld ⊢ ( 𝜑 → ( 𝑇 ↑ 𝐾 ) ∈ ℂ )
154 28 recnd ⊢ ( 𝜑 → ( 𝑋 ↑ 𝐾 ) ∈ ℂ )
155 152 153 154 mulassd ⊢ ( 𝜑 → ( ( ( 𝐴 ‘ 𝐾 ) · ( 𝑇 ↑ 𝐾 ) ) · ( 𝑋 ↑ 𝐾 ) ) = ( ( 𝐴 ‘ 𝐾 ) · ( ( 𝑇 ↑ 𝐾 ) · ( 𝑋 ↑ 𝐾 ) ) ) )
156 151 155 eqtr4d ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝐾 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝐾 ) ) = ( ( ( 𝐴 ‘ 𝐾 ) · ( 𝑇 ↑ 𝐾 ) ) · ( 𝑋 ↑ 𝐾 ) ) )
157 7 oveq1i ⊢ ( 𝑇 ↑ 𝐾 ) = ( ( - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ 𝐾 ) ) ↑𝑐 ( 1 / 𝐾 ) ) ↑ 𝐾 )
158 57 recnd ⊢ ( 𝜑 → 𝐾 ∈ ℂ )
159 26 nnne0d ⊢ ( 𝜑 → 𝐾 ≠ 0 )
160 158 159 recid2d ⊢ ( 𝜑 → ( ( 1 / 𝐾 ) · 𝐾 ) = 1 )
161 160 oveq2d ⊢ ( 𝜑 → ( - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ 𝐾 ) ) ↑𝑐 ( ( 1 / 𝐾 ) · 𝐾 ) ) = ( - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ 𝐾 ) ) ↑𝑐 1 ) )
162 25 simprd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐾 ) ≠ 0 )
163 23 152 162 divcld ⊢ ( 𝜑 → ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ 𝐾 ) ) ∈ ℂ )
164 163 negcld ⊢ ( 𝜑 → - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ 𝐾 ) ) ∈ ℂ )
165 26 nnrecred ⊢ ( 𝜑 → ( 1 / 𝐾 ) ∈ ℝ )
166 165 recnd ⊢ ( 𝜑 → ( 1 / 𝐾 ) ∈ ℂ )
167 164 166 27 cxpmul2d ⊢ ( 𝜑 → ( - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ 𝐾 ) ) ↑𝑐 ( ( 1 / 𝐾 ) · 𝐾 ) ) = ( ( - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ 𝐾 ) ) ↑𝑐 ( 1 / 𝐾 ) ) ↑ 𝐾 ) )
168 164 cxp1d ⊢ ( 𝜑 → ( - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ 𝐾 ) ) ↑𝑐 1 ) = - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ 𝐾 ) ) )
169 161 167 168 3eqtr3d ⊢ ( 𝜑 → ( ( - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ 𝐾 ) ) ↑𝑐 ( 1 / 𝐾 ) ) ↑ 𝐾 ) = - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ 𝐾 ) ) )
170 157 169 syl5eq ⊢ ( 𝜑 → ( 𝑇 ↑ 𝐾 ) = - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ 𝐾 ) ) )
171 170 oveq2d ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝐾 ) · ( 𝑇 ↑ 𝐾 ) ) = ( ( 𝐴 ‘ 𝐾 ) · - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ 𝐾 ) ) ) )
172 152 163 mulneg2d ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝐾 ) · - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ 𝐾 ) ) ) = - ( ( 𝐴 ‘ 𝐾 ) · ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ 𝐾 ) ) ) )
173 23 152 162 divcan2d ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝐾 ) · ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ 𝐾 ) ) ) = ( 𝐹 ‘ 0 ) )
174 173 negeqd ⊢ ( 𝜑 → - ( ( 𝐴 ‘ 𝐾 ) · ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ 𝐾 ) ) ) = - ( 𝐹 ‘ 0 ) )
175 171 172 174 3eqtrd ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝐾 ) · ( 𝑇 ↑ 𝐾 ) ) = - ( 𝐹 ‘ 0 ) )
176 175 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐴 ‘ 𝐾 ) · ( 𝑇 ↑ 𝐾 ) ) · ( 𝑋 ↑ 𝐾 ) ) = ( - ( 𝐹 ‘ 0 ) · ( 𝑋 ↑ 𝐾 ) ) )
177 23 154 mulneg1d ⊢ ( 𝜑 → ( - ( 𝐹 ‘ 0 ) · ( 𝑋 ↑ 𝐾 ) ) = - ( ( 𝐹 ‘ 0 ) · ( 𝑋 ↑ 𝐾 ) ) )
178 156 176 177 3eqtrd ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝐾 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝐾 ) ) = - ( ( 𝐹 ‘ 0 ) · ( 𝑋 ↑ 𝐾 ) ) )
179 149 178 oveq12d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 1 ... ( 𝐾 − 1 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) + ( ( 𝐴 ‘ 𝐾 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝐾 ) ) ) = ( 0 + - ( ( 𝐹 ‘ 0 ) · ( 𝑋 ↑ 𝐾 ) ) ) )
180 23 154 mulcld ⊢ ( 𝜑 → ( ( 𝐹 ‘ 0 ) · ( 𝑋 ↑ 𝐾 ) ) ∈ ℂ )
181 180 negcld ⊢ ( 𝜑 → - ( ( 𝐹 ‘ 0 ) · ( 𝑋 ↑ 𝐾 ) ) ∈ ℂ )
182 181 addid2d ⊢ ( 𝜑 → ( 0 + - ( ( 𝐹 ‘ 0 ) · ( 𝑋 ↑ 𝐾 ) ) ) = - ( ( 𝐹 ‘ 0 ) · ( 𝑋 ↑ 𝐾 ) ) )
183 116 179 182 3eqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 0 + 1 ) ... 𝐾 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) = - ( ( 𝐹 ‘ 0 ) · ( 𝑋 ↑ 𝐾 ) ) )
184 102 183 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐴 ‘ 0 ) · ( ( 𝑇 · 𝑋 ) ↑ 0 ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... 𝐾 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ) = ( ( 𝐹 ‘ 0 ) + - ( ( 𝐹 ‘ 0 ) · ( 𝑋 ↑ 𝐾 ) ) ) )
185 fveq2 ⊢ ( 𝑘 = 0 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 0 ) )
186 oveq2 ⊢ ( 𝑘 = 0 → ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) = ( ( 𝑇 · 𝑋 ) ↑ 0 ) )
187 185 186 oveq12d ⊢ ( 𝑘 = 0 → ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) = ( ( 𝐴 ‘ 0 ) · ( ( 𝑇 · 𝑋 ) ↑ 0 ) ) )
188 81 52 187 fsum1p ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 𝐾 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) = ( ( ( 𝐴 ‘ 0 ) · ( ( 𝑇 · 𝑋 ) ↑ 0 ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... 𝐾 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ) )
189 101 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 0 ) · 1 ) − ( ( 𝐹 ‘ 0 ) · ( 𝑋 ↑ 𝐾 ) ) ) = ( ( 𝐹 ‘ 0 ) − ( ( 𝐹 ‘ 0 ) · ( 𝑋 ↑ 𝐾 ) ) ) )
190 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
191 23 190 154 subdid ⊢ ( 𝜑 → ( ( 𝐹 ‘ 0 ) · ( 1 − ( 𝑋 ↑ 𝐾 ) ) ) = ( ( ( 𝐹 ‘ 0 ) · 1 ) − ( ( 𝐹 ‘ 0 ) · ( 𝑋 ↑ 𝐾 ) ) ) )
192 23 180 negsubd ⊢ ( 𝜑 → ( ( 𝐹 ‘ 0 ) + - ( ( 𝐹 ‘ 0 ) · ( 𝑋 ↑ 𝐾 ) ) ) = ( ( 𝐹 ‘ 0 ) − ( ( 𝐹 ‘ 0 ) · ( 𝑋 ↑ 𝐾 ) ) ) )
193 189 191 192 3eqtr4d ⊢ ( 𝜑 → ( ( 𝐹 ‘ 0 ) · ( 1 − ( 𝑋 ↑ 𝐾 ) ) ) = ( ( 𝐹 ‘ 0 ) + - ( ( 𝐹 ‘ 0 ) · ( 𝑋 ↑ 𝐾 ) ) ) )
194 184 188 193 3eqtr4d ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 𝐾 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) = ( ( 𝐹 ‘ 0 ) · ( 1 − ( 𝑋 ↑ 𝐾 ) ) ) )
195 194 fveq2d ⊢ ( 𝜑 → ( abs ‘ Σ 𝑘 ∈ ( 0 ... 𝐾 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 0 ) · ( 1 − ( 𝑋 ↑ 𝐾 ) ) ) ) )
196 1re ⊢ 1 ∈ ℝ
197 resubcl ⊢ ( ( 1 ∈ ℝ ∧ ( 𝑋 ↑ 𝐾 ) ∈ ℝ ) → ( 1 − ( 𝑋 ↑ 𝐾 ) ) ∈ ℝ )
198 196 28 197 sylancr ⊢ ( 𝜑 → ( 1 − ( 𝑋 ↑ 𝐾 ) ) ∈ ℝ )
199 198 recnd ⊢ ( 𝜑 → ( 1 − ( 𝑋 ↑ 𝐾 ) ) ∈ ℂ )
200 23 199 absmuld ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐹 ‘ 0 ) · ( 1 − ( 𝑋 ↑ 𝐾 ) ) ) ) = ( ( abs ‘ ( 𝐹 ‘ 0 ) ) · ( abs ‘ ( 1 − ( 𝑋 ↑ 𝐾 ) ) ) ) )
201 13 rpge0d ⊢ ( 𝜑 → 0 ≤ 𝑋 )
202 11 simp2d ⊢ ( 𝜑 → 𝑈 ∈ ℝ+ )
203 202 rpred ⊢ ( 𝜑 → 𝑈 ∈ ℝ )
204 min1 ⊢ ( ( 1 ∈ ℝ ∧ 𝑈 ∈ ℝ ) → if ( 1 ≤ 𝑈 , 1 , 𝑈 ) ≤ 1 )
205 196 203 204 sylancr ⊢ ( 𝜑 → if ( 1 ≤ 𝑈 , 1 , 𝑈 ) ≤ 1 )
206 9 205 eqbrtrid ⊢ ( 𝜑 → 𝑋 ≤ 1 )
207 exple1 ⊢ ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ∧ 𝑋 ≤ 1 ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝑋 ↑ 𝐾 ) ≤ 1 )
208 14 201 206 27 207 syl31anc ⊢ ( 𝜑 → ( 𝑋 ↑ 𝐾 ) ≤ 1 )
209 subge0 ⊢ ( ( 1 ∈ ℝ ∧ ( 𝑋 ↑ 𝐾 ) ∈ ℝ ) → ( 0 ≤ ( 1 − ( 𝑋 ↑ 𝐾 ) ) ↔ ( 𝑋 ↑ 𝐾 ) ≤ 1 ) )
210 196 28 209 sylancr ⊢ ( 𝜑 → ( 0 ≤ ( 1 − ( 𝑋 ↑ 𝐾 ) ) ↔ ( 𝑋 ↑ 𝐾 ) ≤ 1 ) )
211 208 210 mpbird ⊢ ( 𝜑 → 0 ≤ ( 1 − ( 𝑋 ↑ 𝐾 ) ) )
212 198 211 absidd ⊢ ( 𝜑 → ( abs ‘ ( 1 − ( 𝑋 ↑ 𝐾 ) ) ) = ( 1 − ( 𝑋 ↑ 𝐾 ) ) )
213 212 oveq2d ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐹 ‘ 0 ) ) · ( abs ‘ ( 1 − ( 𝑋 ↑ 𝐾 ) ) ) ) = ( ( abs ‘ ( 𝐹 ‘ 0 ) ) · ( 1 − ( 𝑋 ↑ 𝐾 ) ) ) )
214 24 recnd ⊢ ( 𝜑 → ( abs ‘ ( 𝐹 ‘ 0 ) ) ∈ ℂ )
215 214 190 154 subdid ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐹 ‘ 0 ) ) · ( 1 − ( 𝑋 ↑ 𝐾 ) ) ) = ( ( ( abs ‘ ( 𝐹 ‘ 0 ) ) · 1 ) − ( ( abs ‘ ( 𝐹 ‘ 0 ) ) · ( 𝑋 ↑ 𝐾 ) ) ) )
216 214 mulid1d ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐹 ‘ 0 ) ) · 1 ) = ( abs ‘ ( 𝐹 ‘ 0 ) ) )
217 216 oveq1d ⊢ ( 𝜑 → ( ( ( abs ‘ ( 𝐹 ‘ 0 ) ) · 1 ) − ( ( abs ‘ ( 𝐹 ‘ 0 ) ) · ( 𝑋 ↑ 𝐾 ) ) ) = ( ( abs ‘ ( 𝐹 ‘ 0 ) ) − ( ( abs ‘ ( 𝐹 ‘ 0 ) ) · ( 𝑋 ↑ 𝐾 ) ) ) )
218 213 215 217 3eqtrd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐹 ‘ 0 ) ) · ( abs ‘ ( 1 − ( 𝑋 ↑ 𝐾 ) ) ) ) = ( ( abs ‘ ( 𝐹 ‘ 0 ) ) − ( ( abs ‘ ( 𝐹 ‘ 0 ) ) · ( 𝑋 ↑ 𝐾 ) ) ) )
219 195 200 218 3eqtrrd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐹 ‘ 0 ) ) − ( ( abs ‘ ( 𝐹 ‘ 0 ) ) · ( 𝑋 ↑ 𝐾 ) ) ) = ( abs ‘ Σ 𝑘 ∈ ( 0 ... 𝐾 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ) )
220 219 oveq1d ⊢ ( 𝜑 → ( ( ( abs ‘ ( 𝐹 ‘ 0 ) ) − ( ( abs ‘ ( 𝐹 ‘ 0 ) ) · ( 𝑋 ↑ 𝐾 ) ) ) + ( abs ‘ Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ) ) = ( ( abs ‘ Σ 𝑘 ∈ ( 0 ... 𝐾 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ) + ( abs ‘ Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ) ) )
221 54 95 220 3brtr4d ⊢ ( 𝜑 → ( abs ‘ ( 𝐹 ‘ ( 𝑇 · 𝑋 ) ) ) ≤ ( ( ( abs ‘ ( 𝐹 ‘ 0 ) ) − ( ( abs ‘ ( 𝐹 ‘ 0 ) ) · ( 𝑋 ↑ 𝐾 ) ) ) + ( abs ‘ Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ) ) )
222 43 abscld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ) ∈ ℝ )
223 31 222 fsumrecl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ) ∈ ℝ )
224 31 43 fsumabs ⊢ ( 𝜑 → ( abs ‘ Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ) ≤ Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ) )
225 expcl ⊢ ( ( 𝑇 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑇 ↑ 𝑘 ) ∈ ℂ )
226 12 38 225 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( 𝑇 ↑ 𝑘 ) ∈ ℂ )
227 40 226 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ∈ ℂ )
228 227 abscld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) ∈ ℝ )
229 31 228 fsumrecl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) ∈ ℝ )
230 14 35 reexpcld ⊢ ( 𝜑 → ( 𝑋 ↑ ( 𝐾 + 1 ) ) ∈ ℝ )
231 229 230 remulcld ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) · ( 𝑋 ↑ ( 𝐾 + 1 ) ) ) ∈ ℝ )
232 230 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( 𝑋 ↑ ( 𝐾 + 1 ) ) ∈ ℝ )
233 228 232 remulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) · ( 𝑋 ↑ ( 𝐾 + 1 ) ) ) ∈ ℝ )
234 12 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → 𝑇 ∈ ℂ )
235 15 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → 𝑋 ∈ ℂ )
236 234 235 38 mulexpd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) = ( ( 𝑇 ↑ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) )
237 236 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) = ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 ↑ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) )
238 14 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → 𝑋 ∈ ℝ )
239 238 38 reexpcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( 𝑋 ↑ 𝑘 ) ∈ ℝ )
240 239 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( 𝑋 ↑ 𝑘 ) ∈ ℂ )
241 40 226 240 mulassd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) · ( 𝑋 ↑ 𝑘 ) ) = ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 ↑ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) )
242 237 241 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) = ( ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) · ( 𝑋 ↑ 𝑘 ) ) )
243 242 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ) = ( abs ‘ ( ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) · ( 𝑋 ↑ 𝑘 ) ) ) )
244 227 240 absmuld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( abs ‘ ( ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) · ( 𝑋 ↑ 𝑘 ) ) ) = ( ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) · ( abs ‘ ( 𝑋 ↑ 𝑘 ) ) ) )
245 elfzelz ⊢ ( 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) → 𝑘 ∈ ℤ )
246 rpexpcl ⊢ ( ( 𝑋 ∈ ℝ+ ∧ 𝑘 ∈ ℤ ) → ( 𝑋 ↑ 𝑘 ) ∈ ℝ+ )
247 13 245 246 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( 𝑋 ↑ 𝑘 ) ∈ ℝ+ )
248 247 rpge0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → 0 ≤ ( 𝑋 ↑ 𝑘 ) )
249 239 248 absidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( abs ‘ ( 𝑋 ↑ 𝑘 ) ) = ( 𝑋 ↑ 𝑘 ) )
250 249 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) · ( abs ‘ ( 𝑋 ↑ 𝑘 ) ) ) = ( ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) · ( 𝑋 ↑ 𝑘 ) ) )
251 243 244 250 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ) = ( ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) · ( 𝑋 ↑ 𝑘 ) ) )
252 227 absge0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → 0 ≤ ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) )
253 35 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( 𝐾 + 1 ) ∈ ℕ0 )
254 36 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → 𝑘 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) )
255 201 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → 0 ≤ 𝑋 )
256 206 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → 𝑋 ≤ 1 )
257 238 253 254 255 256 leexp2rd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( 𝑋 ↑ 𝑘 ) ≤ ( 𝑋 ↑ ( 𝐾 + 1 ) ) )
258 239 232 228 252 257 lemul2ad ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) · ( 𝑋 ↑ 𝑘 ) ) ≤ ( ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) · ( 𝑋 ↑ ( 𝐾 + 1 ) ) ) )
259 251 258 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ) ≤ ( ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) · ( 𝑋 ↑ ( 𝐾 + 1 ) ) ) )
260 31 222 233 259 fsumle ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ) ≤ Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) · ( 𝑋 ↑ ( 𝐾 + 1 ) ) ) )
261 230 recnd ⊢ ( 𝜑 → ( 𝑋 ↑ ( 𝐾 + 1 ) ) ∈ ℂ )
262 228 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) ∈ ℂ )
263 31 261 262 fsummulc1 ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) · ( 𝑋 ↑ ( 𝐾 + 1 ) ) ) = Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) · ( 𝑋 ↑ ( 𝐾 + 1 ) ) ) )
264 260 263 breqtrrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ) ≤ ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) · ( 𝑋 ↑ ( 𝐾 + 1 ) ) ) )
265 15 27 expp1d ⊢ ( 𝜑 → ( 𝑋 ↑ ( 𝐾 + 1 ) ) = ( ( 𝑋 ↑ 𝐾 ) · 𝑋 ) )
266 154 15 mulcomd ⊢ ( 𝜑 → ( ( 𝑋 ↑ 𝐾 ) · 𝑋 ) = ( 𝑋 · ( 𝑋 ↑ 𝐾 ) ) )
267 265 266 eqtrd ⊢ ( 𝜑 → ( 𝑋 ↑ ( 𝐾 + 1 ) ) = ( 𝑋 · ( 𝑋 ↑ 𝐾 ) ) )
268 267 oveq2d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) · ( 𝑋 ↑ ( 𝐾 + 1 ) ) ) = ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) · ( 𝑋 · ( 𝑋 ↑ 𝐾 ) ) ) )
269 229 recnd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) ∈ ℂ )
270 269 15 154 mulassd ⊢ ( 𝜑 → ( ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) · 𝑋 ) · ( 𝑋 ↑ 𝐾 ) ) = ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) · ( 𝑋 · ( 𝑋 ↑ 𝐾 ) ) ) )
271 268 270 eqtr4d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) · ( 𝑋 ↑ ( 𝐾 + 1 ) ) ) = ( ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) · 𝑋 ) · ( 𝑋 ↑ 𝐾 ) ) )
272 229 14 remulcld ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) · 𝑋 ) ∈ ℝ )
273 nnssz ⊢ ℕ ⊆ ℤ
274 61 273 sstri ⊢ { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } ⊆ ℤ
275 76 ne0d ⊢ ( 𝜑 → { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } ≠ ∅ )
276 infssuzcl ⊢ ( ( { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } ⊆ ( ℤ≥ ‘ 1 ) ∧ { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } ≠ ∅ ) → inf ( { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } , ℝ , < ) ∈ { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } )
277 63 275 276 sylancr ⊢ ( 𝜑 → inf ( { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } , ℝ , < ) ∈ { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } )
278 6 277 eqeltrid ⊢ ( 𝜑 → 𝐾 ∈ { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } )
279 274 278 sseldi ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
280 13 279 rpexpcld ⊢ ( 𝜑 → ( 𝑋 ↑ 𝐾 ) ∈ ℝ+ )
281 peano2re ⊢ ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) ∈ ℝ → ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) + 1 ) ∈ ℝ )
282 229 281 syl ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) + 1 ) ∈ ℝ )
283 282 14 remulcld ⊢ ( 𝜑 → ( ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) + 1 ) · 𝑋 ) ∈ ℝ )
284 229 ltp1d ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) < ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) + 1 ) )
285 229 282 13 284 ltmul1dd ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) · 𝑋 ) < ( ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) + 1 ) · 𝑋 ) )
286 min2 ⊢ ( ( 1 ∈ ℝ ∧ 𝑈 ∈ ℝ ) → if ( 1 ≤ 𝑈 , 1 , 𝑈 ) ≤ 𝑈 )
287 196 203 286 sylancr ⊢ ( 𝜑 → if ( 1 ≤ 𝑈 , 1 , 𝑈 ) ≤ 𝑈 )
288 9 287 eqbrtrid ⊢ ( 𝜑 → 𝑋 ≤ 𝑈 )
289 288 8 breqtrdi ⊢ ( 𝜑 → 𝑋 ≤ ( ( abs ‘ ( 𝐹 ‘ 0 ) ) / ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) + 1 ) ) )
290 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
291 31 228 252 fsumge0 ⊢ ( 𝜑 → 0 ≤ Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) )
292 290 229 282 291 284 lelttrd ⊢ ( 𝜑 → 0 < ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) + 1 ) )
293 lemuldiv2 ⊢ ( ( 𝑋 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 0 ) ) ∈ ℝ ∧ ( ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) + 1 ) ∈ ℝ ∧ 0 < ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) + 1 ) ) ) → ( ( ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) + 1 ) · 𝑋 ) ≤ ( abs ‘ ( 𝐹 ‘ 0 ) ) ↔ 𝑋 ≤ ( ( abs ‘ ( 𝐹 ‘ 0 ) ) / ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) + 1 ) ) ) )
294 14 24 282 292 293 syl112anc ⊢ ( 𝜑 → ( ( ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) + 1 ) · 𝑋 ) ≤ ( abs ‘ ( 𝐹 ‘ 0 ) ) ↔ 𝑋 ≤ ( ( abs ‘ ( 𝐹 ‘ 0 ) ) / ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) + 1 ) ) ) )
295 289 294 mpbird ⊢ ( 𝜑 → ( ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) + 1 ) · 𝑋 ) ≤ ( abs ‘ ( 𝐹 ‘ 0 ) ) )
296 272 283 24 285 295 ltletrd ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) · 𝑋 ) < ( abs ‘ ( 𝐹 ‘ 0 ) ) )
297 272 24 280 296 ltmul1dd ⊢ ( 𝜑 → ( ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) · 𝑋 ) · ( 𝑋 ↑ 𝐾 ) ) < ( ( abs ‘ ( 𝐹 ‘ 0 ) ) · ( 𝑋 ↑ 𝐾 ) ) )
298 271 297 eqbrtrd ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) · ( 𝑋 ↑ ( 𝐾 + 1 ) ) ) < ( ( abs ‘ ( 𝐹 ‘ 0 ) ) · ( 𝑋 ↑ 𝐾 ) ) )
299 223 231 29 264 298 lelttrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ) < ( ( abs ‘ ( 𝐹 ‘ 0 ) ) · ( 𝑋 ↑ 𝐾 ) ) )
300 45 223 29 224 299 lelttrd ⊢ ( 𝜑 → ( abs ‘ Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ) < ( ( abs ‘ ( 𝐹 ‘ 0 ) ) · ( 𝑋 ↑ 𝐾 ) ) )
301 45 29 24 300 ltsub2dd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐹 ‘ 0 ) ) − ( ( abs ‘ ( 𝐹 ‘ 0 ) ) · ( 𝑋 ↑ 𝐾 ) ) ) < ( ( abs ‘ ( 𝐹 ‘ 0 ) ) − ( abs ‘ Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ) ) )
302 30 45 24 ltaddsubd ⊢ ( 𝜑 → ( ( ( ( abs ‘ ( 𝐹 ‘ 0 ) ) − ( ( abs ‘ ( 𝐹 ‘ 0 ) ) · ( 𝑋 ↑ 𝐾 ) ) ) + ( abs ‘ Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ) ) < ( abs ‘ ( 𝐹 ‘ 0 ) ) ↔ ( ( abs ‘ ( 𝐹 ‘ 0 ) ) − ( ( abs ‘ ( 𝐹 ‘ 0 ) ) · ( 𝑋 ↑ 𝐾 ) ) ) < ( ( abs ‘ ( 𝐹 ‘ 0 ) ) − ( abs ‘ Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ) ) ) )
303 301 302 mpbird ⊢ ( 𝜑 → ( ( ( abs ‘ ( 𝐹 ‘ 0 ) ) − ( ( abs ‘ ( 𝐹 ‘ 0 ) ) · ( 𝑋 ↑ 𝐾 ) ) ) + ( abs ‘ Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) ) ) < ( abs ‘ ( 𝐹 ‘ 0 ) ) )
304 20 46 24 221 303 lelttrd ⊢ ( 𝜑 → ( abs ‘ ( 𝐹 ‘ ( 𝑇 · 𝑋 ) ) ) < ( abs ‘ ( 𝐹 ‘ 0 ) ) )
305 2fveq3 ⊢ ( 𝑥 = ( 𝑇 · 𝑋 ) → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) = ( abs ‘ ( 𝐹 ‘ ( 𝑇 · 𝑋 ) ) ) )
306 305 breq1d ⊢ ( 𝑥 = ( 𝑇 · 𝑋 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) < ( abs ‘ ( 𝐹 ‘ 0 ) ) ↔ ( abs ‘ ( 𝐹 ‘ ( 𝑇 · 𝑋 ) ) ) < ( abs ‘ ( 𝐹 ‘ 0 ) ) ) )
307 306 rspcev ⊢ ( ( ( 𝑇 · 𝑋 ) ∈ ℂ ∧ ( abs ‘ ( 𝐹 ‘ ( 𝑇 · 𝑋 ) ) ) < ( abs ‘ ( 𝐹 ‘ 0 ) ) ) → ∃ 𝑥 ∈ ℂ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) < ( abs ‘ ( 𝐹 ‘ 0 ) ) )
308 16 304 307 syl2anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℂ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) < ( abs ‘ ( 𝐹 ‘ 0 ) ) )