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	\|- A = ( coeff ` F )
	ftalem.2	\|- N = ( deg ` F )
	ftalem.3	\|- ( ph -> F e. ( Poly ` S ) )
	ftalem.4	\|- ( ph -> N e. NN )
	ftalem4.5	\|- ( ph -> ( F ` 0 ) =/= 0 )
	ftalem4.6	\|- K = inf ( { n e. NN \| ( A ` n ) =/= 0 } , RR , < )
	ftalem4.7	\|- T = ( -u ( ( F ` 0 ) / ( A ` K ) ) ^c ( 1 / K ) )
	ftalem4.8	\|- U = ( ( abs ` ( F ` 0 ) ) / ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) + 1 ) )
	ftalem4.9	\|- X = if ( 1 <_ U , 1 , U )
Assertion	ftalem5	\|- ( ph -> E. x e. CC ( abs ` ( F ` x ) ) < ( abs ` ( F ` 0 ) ) )

Proof

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

Metamath Proof Explorer

Theorem ftalem5

Proof