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	ffvelcdmd	⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑇 · 𝑋 ) ) ∈ ℂ )
20	19	abscld	⊢ ( 𝜑 → ( abs ‘ ( 𝐹 ‘ ( 𝑇 · 𝑋 ) ) ) ∈ ℝ )
21		0cn	⊢ 0 ∈ ℂ
22		ffvelcdm	⊢ ( ( 𝐹 : ℂ ⟶ ℂ ∧ 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		ffvelcdm	⊢ ( ( 𝐴 : ℕ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	eqtrdi	⊢ ( 𝐹 = 0𝑝 → ( deg ‘ 𝐹 ) = 0 )
72	2 71	eqtrid	⊢ ( 𝐹 = 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	mulridd	⊢ ( 𝜑 → ( ( 𝐹 ‘ 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	eqtr3id	⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 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	eqtrdi	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 1 ... ( 𝐾 − 1 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝑘 ) ) = 0 )
150	12 15 27	mulexpd	⊢ ( 𝜑 → ( ( 𝑇 · 𝑋 ) ↑ 𝐾 ) = ( ( 𝑇 ↑ 𝐾 ) · ( 𝑋 ↑ 𝐾 ) ) )
151	150	oveq2d	⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝐾 ) · ( ( 𝑇 · 𝑋 ) ↑ 𝐾 ) ) = ( ( 𝐴 ‘ 𝐾 ) · ( ( 𝑇 ↑ 𝐾 ) · ( 𝑋 ↑ 𝐾 ) ) ) )
152	33 27	ffvelcdmd	⊢ ( 𝜑 → ( 𝐴 ‘ 𝐾 ) ∈ ℂ )
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	eqtrid	⊢ ( 𝜑 → ( 𝑇 ↑ 𝐾 ) = - ( ( 𝐹 ‘ 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	addlidd	⊢ ( 𝜑 → ( 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	mulridd	⊢ ( 𝜑 → ( ( 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	sselid	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
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 ) ) )