Metamath Proof Explorer

Theorem ftalem6

Description: Lemma for fta : Discharge the auxiliary variables in ftalem5 . (Contributed by Mario Carneiro, 20-Sep-2014) (Proof shortened 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 )
ftalem6.5 
|- ( ph -> ( F ` 0 ) =/= 0 )
Assertion ftalem6 
|- ( 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 ftalem6.5 
 |-  ( ph -> ( F ` 0 ) =/= 0 )
6 fveq2 
 |-  ( k = n -> ( A ` k ) = ( A ` n ) )
7 6 neeq1d 
 |-  ( k = n -> ( ( A ` k ) =/= 0 <-> ( A ` n ) =/= 0 ) )
8 7 cbvrabv 
 |-  { k e. NN | ( A ` k ) =/= 0 } = { n e. NN | ( A ` n ) =/= 0 }
9 8 infeq1i 
 |-  inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) = inf ( { n e. NN | ( A ` n ) =/= 0 } , RR , < )
10 eqid 
 |-  ( -u ( ( F ` 0 ) / ( A ` inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) ) ^c ( 1 / inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) ) = ( -u ( ( F ` 0 ) / ( A ` inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) ) ^c ( 1 / inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) )
11 fveq2 
 |-  ( r = s -> ( A ` r ) = ( A ` s ) )
12 oveq2 
 |-  ( r = s -> ( ( -u ( ( F ` 0 ) / ( A ` inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) ) ^c ( 1 / inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) ) ^ r ) = ( ( -u ( ( F ` 0 ) / ( A ` inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) ) ^c ( 1 / inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) ) ^ s ) )
13 11 12 oveq12d 
 |-  ( r = s -> ( ( A ` r ) x. ( ( -u ( ( F ` 0 ) / ( A ` inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) ) ^c ( 1 / inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) ) ^ r ) ) = ( ( A ` s ) x. ( ( -u ( ( F ` 0 ) / ( A ` inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) ) ^c ( 1 / inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) ) ^ s ) ) )
14 13 fveq2d 
 |-  ( r = s -> ( abs ` ( ( A ` r ) x. ( ( -u ( ( F ` 0 ) / ( A ` inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) ) ^c ( 1 / inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) ) ^ r ) ) ) = ( abs ` ( ( A ` s ) x. ( ( -u ( ( F ` 0 ) / ( A ` inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) ) ^c ( 1 / inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) ) ^ s ) ) ) )
15 14 cbvsumv 
 |-  sum_ r e. ( ( inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) + 1 ) ... N ) ( abs ` ( ( A ` r ) x. ( ( -u ( ( F ` 0 ) / ( A ` inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) ) ^c ( 1 / inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) ) ^ r ) ) ) = sum_ s e. ( ( inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) + 1 ) ... N ) ( abs ` ( ( A ` s ) x. ( ( -u ( ( F ` 0 ) / ( A ` inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) ) ^c ( 1 / inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) ) ^ s ) ) )
16 15 oveq1i 
 |-  ( sum_ r e. ( ( inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) + 1 ) ... N ) ( abs ` ( ( A ` r ) x. ( ( -u ( ( F ` 0 ) / ( A ` inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) ) ^c ( 1 / inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) ) ^ r ) ) ) + 1 ) = ( sum_ s e. ( ( inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) + 1 ) ... N ) ( abs ` ( ( A ` s ) x. ( ( -u ( ( F ` 0 ) / ( A ` inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) ) ^c ( 1 / inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) ) ^ s ) ) ) + 1 )
17 16 oveq2i 
 |-  ( ( abs ` ( F ` 0 ) ) / ( sum_ r e. ( ( inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) + 1 ) ... N ) ( abs ` ( ( A ` r ) x. ( ( -u ( ( F ` 0 ) / ( A ` inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) ) ^c ( 1 / inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) ) ^ r ) ) ) + 1 ) ) = ( ( abs ` ( F ` 0 ) ) / ( sum_ s e. ( ( inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) + 1 ) ... N ) ( abs ` ( ( A ` s ) x. ( ( -u ( ( F ` 0 ) / ( A ` inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) ) ^c ( 1 / inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) ) ^ s ) ) ) + 1 ) )
18 eqid 
 |-  if ( 1 <_ ( ( abs ` ( F ` 0 ) ) / ( sum_ r e. ( ( inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) + 1 ) ... N ) ( abs ` ( ( A ` r ) x. ( ( -u ( ( F ` 0 ) / ( A ` inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) ) ^c ( 1 / inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) ) ^ r ) ) ) + 1 ) ) , 1 , ( ( abs ` ( F ` 0 ) ) / ( sum_ r e. ( ( inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) + 1 ) ... N ) ( abs ` ( ( A ` r ) x. ( ( -u ( ( F ` 0 ) / ( A ` inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) ) ^c ( 1 / inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) ) ^ r ) ) ) + 1 ) ) ) = if ( 1 <_ ( ( abs ` ( F ` 0 ) ) / ( sum_ r e. ( ( inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) + 1 ) ... N ) ( abs ` ( ( A ` r ) x. ( ( -u ( ( F ` 0 ) / ( A ` inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) ) ^c ( 1 / inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) ) ^ r ) ) ) + 1 ) ) , 1 , ( ( abs ` ( F ` 0 ) ) / ( sum_ r e. ( ( inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) + 1 ) ... N ) ( abs ` ( ( A ` r ) x. ( ( -u ( ( F ` 0 ) / ( A ` inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) ) ^c ( 1 / inf ( { k e. NN | ( A ` k ) =/= 0 } , RR , < ) ) ) ^ r ) ) ) + 1 ) ) )
19 1 2 3 4 5 9 10 17 18 ftalem5 
 |-  ( ph -> E. x e. CC ( abs ` ( F ` x ) ) < ( abs ` ( F ` 0 ) ) )