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 syl5eq
 |-  ( 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 ffvelrnd
 |-  ( ( 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 )