Metamath Proof Explorer

Theorem ftalem4

Description: Lemma for fta : Closure of the auxiliary variables for ftalem5 . (Contributed by Mario Carneiro, 20-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 ftalem4 
|- ( ph -> ( ( K e. NN /\ ( A ` K ) =/= 0 ) /\ ( T e. CC /\ U e. RR+ /\ X e. RR+ ) ) )

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 ssrab2 
 |-  { n e. NN | ( A ` n ) =/= 0 } C_ NN
11 nnuz 
 |-  NN = ( ZZ>= ` 1 )
12 10 11 sseqtri 
 |-  { n e. NN | ( A ` n ) =/= 0 } C_ ( ZZ>= ` 1 )
13 fveq2 
 |-  ( n = N -> ( A ` n ) = ( A ` N ) )
14 13 neeq1d 
 |-  ( n = N -> ( ( A ` n ) =/= 0 <-> ( A ` N ) =/= 0 ) )
15 4 nnne0d 
 |-  ( ph -> N =/= 0 )
16 2 1 dgreq0 
 |-  ( F e. ( Poly ` S ) -> ( F = 0p <-> ( A ` N ) = 0 ) )
17 3 16 syl 
 |-  ( ph -> ( F = 0p <-> ( A ` N ) = 0 ) )
18 fveq2 
 |-  ( F = 0p -> ( deg ` F ) = ( deg ` 0p ) )
19 dgr0 
 |-  ( deg ` 0p ) = 0
20 18 19 eqtrdi 
 |-  ( F = 0p -> ( deg ` F ) = 0 )
21 2 20 eqtrid 
 |-  ( F = 0p -> N = 0 )
22 17 21 syl6bir 
 |-  ( ph -> ( ( A ` N ) = 0 -> N = 0 ) )
23 22 necon3d 
 |-  ( ph -> ( N =/= 0 -> ( A ` N ) =/= 0 ) )
24 15 23 mpd 
 |-  ( ph -> ( A ` N ) =/= 0 )
25 14 4 24 elrabd 
 |-  ( ph -> N e. { n e. NN | ( A ` n ) =/= 0 } )
26 25 ne0d 
 |-  ( ph -> { n e. NN | ( A ` n ) =/= 0 } =/= (/) )
27 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 } )
28 12 26 27 sylancr 
 |-  ( ph -> inf ( { n e. NN | ( A ` n ) =/= 0 } , RR , < ) e. { n e. NN | ( A ` n ) =/= 0 } )
29 6 28 eqeltrid 
 |-  ( ph -> K e. { n e. NN | ( A ` n ) =/= 0 } )
30 fveq2 
 |-  ( n = K -> ( A ` n ) = ( A ` K ) )
31 30 neeq1d 
 |-  ( n = K -> ( ( A ` n ) =/= 0 <-> ( A ` K ) =/= 0 ) )
32 31 elrab 
 |-  ( K e. { n e. NN | ( A ` n ) =/= 0 } <-> ( K e. NN /\ ( A ` K ) =/= 0 ) )
33 29 32 sylib 
 |-  ( ph -> ( K e. NN /\ ( A ` K ) =/= 0 ) )
34 plyf 
 |-  ( F e. ( Poly ` S ) -> F : CC --> CC )
35 3 34 syl 
 |-  ( ph -> F : CC --> CC )
36 0cn 
 |-  0 e. CC
37 ffvelrn 
 |-  ( ( F : CC --> CC /\ 0 e. CC ) -> ( F ` 0 ) e. CC )
38 35 36 37 sylancl 
 |-  ( ph -> ( F ` 0 ) e. CC )
39 1 coef3 
 |-  ( F e. ( Poly ` S ) -> A : NN0 --> CC )
40 3 39 syl 
 |-  ( ph -> A : NN0 --> CC )
41 33 simpld 
 |-  ( ph -> K e. NN )
42 41 nnnn0d 
 |-  ( ph -> K e. NN0 )
43 40 42 ffvelrnd 
 |-  ( ph -> ( A ` K ) e. CC )
44 33 simprd 
 |-  ( ph -> ( A ` K ) =/= 0 )
45 38 43 44 divcld 
 |-  ( ph -> ( ( F ` 0 ) / ( A ` K ) ) e. CC )
46 45 negcld 
 |-  ( ph -> -u ( ( F ` 0 ) / ( A ` K ) ) e. CC )
47 41 nnrecred 
 |-  ( ph -> ( 1 / K ) e. RR )
48 47 recnd 
 |-  ( ph -> ( 1 / K ) e. CC )
49 46 48 cxpcld 
 |-  ( ph -> ( -u ( ( F ` 0 ) / ( A ` K ) ) ^c ( 1 / K ) ) e. CC )
50 7 49 eqeltrid 
 |-  ( ph -> T e. CC )
51 38 5 absrpcld 
 |-  ( ph -> ( abs ` ( F ` 0 ) ) e. RR+ )
52 fzfid 
 |-  ( ph -> ( ( K + 1 ) ... N ) e. Fin )
53 peano2nn0 
 |-  ( K e. NN0 -> ( K + 1 ) e. NN0 )
54 42 53 syl 
 |-  ( ph -> ( K + 1 ) e. NN0 )
55 elfzuz 
 |-  ( k e. ( ( K + 1 ) ... N ) -> k e. ( ZZ>= ` ( K + 1 ) ) )
56 eluznn0 
 |-  ( ( ( K + 1 ) e. NN0 /\ k e. ( ZZ>= ` ( K + 1 ) ) ) -> k e. NN0 )
57 54 55 56 syl2an 
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> k e. NN0 )
58 40 ffvelrnda 
 |-  ( ( ph /\ k e. NN0 ) -> ( A ` k ) e. CC )
59 57 58 syldan 
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( A ` k ) e. CC )
60 expcl 
 |-  ( ( T e. CC /\ k e. NN0 ) -> ( T ^ k ) e. CC )
61 50 57 60 syl2an2r 
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( T ^ k ) e. CC )
62 59 61 mulcld 
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( ( A ` k ) x. ( T ^ k ) ) e. CC )
63 62 abscld 
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) e. RR )
64 52 63 fsumrecl 
 |-  ( ph -> sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) e. RR )
65 62 absge0d 
 |-  ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> 0 <_ ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) )
66 52 63 65 fsumge0 
 |-  ( ph -> 0 <_ sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) )
67 64 66 ge0p1rpd 
 |-  ( ph -> ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) + 1 ) e. RR+ )
68 51 67 rpdivcld 
 |-  ( ph -> ( ( abs ` ( F ` 0 ) ) / ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) + 1 ) ) e. RR+ )
69 8 68 eqeltrid 
 |-  ( ph -> U e. RR+ )
70 1rp 
 |-  1 e. RR+
71 ifcl 
 |-  ( ( 1 e. RR+ /\ U e. RR+ ) -> if ( 1 <_ U , 1 , U ) e. RR+ )
72 70 69 71 sylancr 
 |-  ( ph -> if ( 1 <_ U , 1 , U ) e. RR+ )
73 9 72 eqeltrid 
 |-  ( ph -> X e. RR+ )
74 50 69 73 3jca 
 |-  ( ph -> ( T e. CC /\ U e. RR+ /\ X e. RR+ ) )
75 33 74 jca 
 |-  ( ph -> ( ( K e. NN /\ ( A ` K ) =/= 0 ) /\ ( T e. CC /\ U e. RR+ /\ X e. RR+ ) ) )