Metamath Proof Explorer

Theorem dgrub

Description: If the M -th coefficient of F is nonzero, then the degree of F is at least M . (Contributed by Mario Carneiro, 22-Jul-2014)

Ref Expression
Hypotheses dgrub.1 
|- A = ( coeff ` F )
dgrub.2 
|- N = ( deg ` F )
Assertion dgrub 
|- ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A ` M ) =/= 0 ) -> M <_ N )

Proof

Step Hyp Ref Expression
1 dgrub.1 
 |-  A = ( coeff ` F )
2 dgrub.2 
 |-  N = ( deg ` F )
3 simp2 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A ` M ) =/= 0 ) -> M e. NN0 )
4 3 nn0red 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A ` M ) =/= 0 ) -> M e. RR )
5 simp1 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A ` M ) =/= 0 ) -> F e. ( Poly ` S ) )
6 dgrcl 
 |-  ( F e. ( Poly ` S ) -> ( deg ` F ) e. NN0 )
7 2 6 eqeltrid 
 |-  ( F e. ( Poly ` S ) -> N e. NN0 )
8 5 7 syl 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A ` M ) =/= 0 ) -> N e. NN0 )
9 8 nn0red 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A ` M ) =/= 0 ) -> N e. RR )
10 1 dgrval 
 |-  ( F e. ( Poly ` S ) -> ( deg ` F ) = sup ( ( `' A " ( CC \ { 0 } ) ) , NN0 , < ) )
11 2 10 eqtrid 
 |-  ( F e. ( Poly ` S ) -> N = sup ( ( `' A " ( CC \ { 0 } ) ) , NN0 , < ) )
12 5 11 syl 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A ` M ) =/= 0 ) -> N = sup ( ( `' A " ( CC \ { 0 } ) ) , NN0 , < ) )
13 1 coef3 
 |-  ( F e. ( Poly ` S ) -> A : NN0 --> CC )
14 5 13 syl 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A ` M ) =/= 0 ) -> A : NN0 --> CC )
15 14 3 ffvelcdmd 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A ` M ) =/= 0 ) -> ( A ` M ) e. CC )
16 simp3 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A ` M ) =/= 0 ) -> ( A ` M ) =/= 0 )
17 eldifsn 
 |-  ( ( A ` M ) e. ( CC \ { 0 } ) <-> ( ( A ` M ) e. CC /\ ( A ` M ) =/= 0 ) )
18 15 16 17 sylanbrc 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A ` M ) =/= 0 ) -> ( A ` M ) e. ( CC \ { 0 } ) )
19 1 coef 
 |-  ( F e. ( Poly ` S ) -> A : NN0 --> ( S u. { 0 } ) )
20 ffn 
 |-  ( A : NN0 --> ( S u. { 0 } ) -> A Fn NN0 )
21 elpreima 
 |-  ( A Fn NN0 -> ( M e. ( `' A " ( CC \ { 0 } ) ) <-> ( M e. NN0 /\ ( A ` M ) e. ( CC \ { 0 } ) ) ) )
22 5 19 20 21 4syl 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A ` M ) =/= 0 ) -> ( M e. ( `' A " ( CC \ { 0 } ) ) <-> ( M e. NN0 /\ ( A ` M ) e. ( CC \ { 0 } ) ) ) )
23 3 18 22 mpbir2and 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A ` M ) =/= 0 ) -> M e. ( `' A " ( CC \ { 0 } ) ) )
24 nn0ssre 
 |-  NN0 C_ RR
25 ltso 
 |-  < Or RR
26 soss 
 |-  ( NN0 C_ RR -> ( < Or RR -> < Or NN0 ) )
27 24 25 26 mp2 
 |-  < Or NN0
28 27 a1i 
 |-  ( F e. ( Poly ` S ) -> < Or NN0 )
29 0zd 
 |-  ( F e. ( Poly ` S ) -> 0 e. ZZ )
30 cnvimass 
 |-  ( `' A " ( CC \ { 0 } ) ) C_ dom A
31 30 19 fssdm 
 |-  ( F e. ( Poly ` S ) -> ( `' A " ( CC \ { 0 } ) ) C_ NN0 )
32 1 dgrlem 
 |-  ( F e. ( Poly ` S ) -> ( A : NN0 --> ( S u. { 0 } ) /\ E. n e. ZZ A. x e. ( `' A " ( CC \ { 0 } ) ) x <_ n ) )
33 32 simprd 
 |-  ( F e. ( Poly ` S ) -> E. n e. ZZ A. x e. ( `' A " ( CC \ { 0 } ) ) x <_ n )
34 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
35 34 uzsupss 
 |-  ( ( 0 e. ZZ /\ ( `' A " ( CC \ { 0 } ) ) C_ NN0 /\ E. n e. ZZ A. x e. ( `' A " ( CC \ { 0 } ) ) x <_ n ) -> E. n e. NN0 ( A. x e. ( `' A " ( CC \ { 0 } ) ) -. n < x /\ A. x e. NN0 ( x < n -> E. y e. ( `' A " ( CC \ { 0 } ) ) x < y ) ) )
36 29 31 33 35 syl3anc 
 |-  ( F e. ( Poly ` S ) -> E. n e. NN0 ( A. x e. ( `' A " ( CC \ { 0 } ) ) -. n < x /\ A. x e. NN0 ( x < n -> E. y e. ( `' A " ( CC \ { 0 } ) ) x < y ) ) )
37 28 36 supub 
 |-  ( F e. ( Poly ` S ) -> ( M e. ( `' A " ( CC \ { 0 } ) ) -> -. sup ( ( `' A " ( CC \ { 0 } ) ) , NN0 , < ) < M ) )
38 5 23 37 sylc 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A ` M ) =/= 0 ) -> -. sup ( ( `' A " ( CC \ { 0 } ) ) , NN0 , < ) < M )
39 12 38 eqnbrtrd 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A ` M ) =/= 0 ) -> -. N < M )
40 4 9 39 nltled 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A ` M ) =/= 0 ) -> M <_ N )