Metamath Proof Explorer

Theorem dgrlb

Description: If all the coefficients above M are zero, then the degree of F is at most M . (Contributed by Mario Carneiro, 22-Jul-2014)

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

Proof

Step Hyp Ref Expression
1 dgrub.1 
 |-  A = ( coeff ` F )
2 dgrub.2 
 |-  N = ( deg ` F )
3 dgrcl 
 |-  ( F e. ( Poly ` S ) -> ( deg ` F ) e. NN0 )
4 2 3 eqeltrid 
 |-  ( F e. ( Poly ` S ) -> N e. NN0 )
5 4 3ad2ant1 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } ) -> N e. NN0 )
6 5 nn0red 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } ) -> N e. RR )
7 simp2 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } ) -> M e. NN0 )
8 7 nn0red 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } ) -> M e. RR )
9 1 dgrlem 
 |-  ( F e. ( Poly ` S ) -> ( A : NN0 --> ( S u. { 0 } ) /\ E. n e. ZZ A. x e. ( `' A " ( CC \ { 0 } ) ) x <_ n ) )
10 9 simpld 
 |-  ( F e. ( Poly ` S ) -> A : NN0 --> ( S u. { 0 } ) )
11 10 3ad2ant1 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } ) -> A : NN0 --> ( S u. { 0 } ) )
12 ffn 
 |-  ( A : NN0 --> ( S u. { 0 } ) -> A Fn NN0 )
13 elpreima 
 |-  ( A Fn NN0 -> ( y e. ( `' A " ( CC \ { 0 } ) ) <-> ( y e. NN0 /\ ( A ` y ) e. ( CC \ { 0 } ) ) ) )
14 11 12 13 3syl 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } ) -> ( y e. ( `' A " ( CC \ { 0 } ) ) <-> ( y e. NN0 /\ ( A ` y ) e. ( CC \ { 0 } ) ) ) )
15 14 biimpa 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } ) /\ y e. ( `' A " ( CC \ { 0 } ) ) ) -> ( y e. NN0 /\ ( A ` y ) e. ( CC \ { 0 } ) ) )
16 15 simpld 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } ) /\ y e. ( `' A " ( CC \ { 0 } ) ) ) -> y e. NN0 )
17 16 nn0red 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } ) /\ y e. ( `' A " ( CC \ { 0 } ) ) ) -> y e. RR )
18 8 adantr 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } ) /\ y e. ( `' A " ( CC \ { 0 } ) ) ) -> M e. RR )
19 eldifsni 
 |-  ( ( A ` y ) e. ( CC \ { 0 } ) -> ( A ` y ) =/= 0 )
20 15 19 simpl2im 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } ) /\ y e. ( `' A " ( CC \ { 0 } ) ) ) -> ( A ` y ) =/= 0 )
21 simp3 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } ) -> ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } )
22 1 coef3 
 |-  ( F e. ( Poly ` S ) -> A : NN0 --> CC )
23 22 3ad2ant1 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } ) -> A : NN0 --> CC )
24 plyco0 
 |-  ( ( M e. NN0 /\ A : NN0 --> CC ) -> ( ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } <-> A. y e. NN0 ( ( A ` y ) =/= 0 -> y <_ M ) ) )
25 7 23 24 syl2anc 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } ) -> ( ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } <-> A. y e. NN0 ( ( A ` y ) =/= 0 -> y <_ M ) ) )
26 21 25 mpbid 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } ) -> A. y e. NN0 ( ( A ` y ) =/= 0 -> y <_ M ) )
27 26 r19.21bi 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } ) /\ y e. NN0 ) -> ( ( A ` y ) =/= 0 -> y <_ M ) )
28 16 27 syldan 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } ) /\ y e. ( `' A " ( CC \ { 0 } ) ) ) -> ( ( A ` y ) =/= 0 -> y <_ M ) )
29 20 28 mpd 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } ) /\ y e. ( `' A " ( CC \ { 0 } ) ) ) -> y <_ M )
30 17 18 29 lensymd 
 |-  ( ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } ) /\ y e. ( `' A " ( CC \ { 0 } ) ) ) -> -. M < y )
31 30 ralrimiva 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } ) -> A. y e. ( `' A " ( CC \ { 0 } ) ) -. M < y )
32 nn0ssre 
 |-  NN0 C_ RR
33 ltso 
 |-  < Or RR
34 soss 
 |-  ( NN0 C_ RR -> ( < Or RR -> < Or NN0 ) )
35 32 33 34 mp2 
 |-  < Or NN0
36 35 a1i 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } ) -> < Or NN0 )
37 0zd 
 |-  ( F e. ( Poly ` S ) -> 0 e. ZZ )
38 cnvimass 
 |-  ( `' A " ( CC \ { 0 } ) ) C_ dom A
39 38 10 fssdm 
 |-  ( F e. ( Poly ` S ) -> ( `' A " ( CC \ { 0 } ) ) C_ NN0 )
40 9 simprd 
 |-  ( F e. ( Poly ` S ) -> E. n e. ZZ A. x e. ( `' A " ( CC \ { 0 } ) ) x <_ n )
41 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
42 41 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 ) ) )
43 37 39 40 42 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 ) ) )
44 43 3ad2ant1 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } ) -> 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 ) ) )
45 36 44 supnub 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } ) -> ( ( M e. NN0 /\ A. y e. ( `' A " ( CC \ { 0 } ) ) -. M < y ) -> -. M < sup ( ( `' A " ( CC \ { 0 } ) ) , NN0 , < ) ) )
46 7 31 45 mp2and 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } ) -> -. M < sup ( ( `' A " ( CC \ { 0 } ) ) , NN0 , < ) )
47 1 dgrval 
 |-  ( F e. ( Poly ` S ) -> ( deg ` F ) = sup ( ( `' A " ( CC \ { 0 } ) ) , NN0 , < ) )
48 2 47 syl5eq 
 |-  ( F e. ( Poly ` S ) -> N = sup ( ( `' A " ( CC \ { 0 } ) ) , NN0 , < ) )
49 48 3ad2ant1 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } ) -> N = sup ( ( `' A " ( CC \ { 0 } ) ) , NN0 , < ) )
50 49 breq2d 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } ) -> ( M < N <-> M < sup ( ( `' A " ( CC \ { 0 } ) ) , NN0 , < ) ) )
51 46 50 mtbird 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } ) -> -. M < N )
52 6 8 51 nltled 
 |-  ( ( F e. ( Poly ` S ) /\ M e. NN0 /\ ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } ) -> N <_ M )