Metamath Proof Explorer

Theorem dgrle

Description: Given an explicit expression for a polynomial, the degree is at most the highest term in the sum. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses dgrle.1 
|- ( ph -> F e. ( Poly ` S ) )
dgrle.2 
|- ( ph -> N e. NN0 )
dgrle.3 
|- ( ( ph /\ k e. ( 0 ... N ) ) -> A e. CC )
dgrle.4 
|- ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( A x. ( z ^ k ) ) ) )
Assertion dgrle 
|- ( ph -> ( deg ` F ) <_ N )

Proof

Step Hyp Ref Expression
1 dgrle.1 
 |-  ( ph -> F e. ( Poly ` S ) )
2 dgrle.2 
 |-  ( ph -> N e. NN0 )
3 dgrle.3 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> A e. CC )
4 dgrle.4 
 |-  ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( A x. ( z ^ k ) ) ) )
5 1 2 3 4 coeeq2 
 |-  ( ph -> ( coeff ` F ) = ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) )
6 5 ad2antrr 
 |-  ( ( ( ph /\ m e. NN0 ) /\ -. m <_ N ) -> ( coeff ` F ) = ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) )
7 6 fveq1d 
 |-  ( ( ( ph /\ m e. NN0 ) /\ -. m <_ N ) -> ( ( coeff ` F ) ` m ) = ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) )
8 nfcv 
 |-  F/_ k m
9 nfv 
 |-  F/ k -. m <_ N
10 nffvmpt1 
 |-  F/_ k ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m )
11 10 nfeq1 
 |-  F/ k ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) = 0
12 9 11 nfim 
 |-  F/ k ( -. m <_ N -> ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) = 0 )
13 breq1 
 |-  ( k = m -> ( k <_ N <-> m <_ N ) )
14 13 notbid 
 |-  ( k = m -> ( -. k <_ N <-> -. m <_ N ) )
15 fveqeq2 
 |-  ( k = m -> ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) = 0 <-> ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) = 0 ) )
16 14 15 imbi12d 
 |-  ( k = m -> ( ( -. k <_ N -> ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) = 0 ) <-> ( -. m <_ N -> ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) = 0 ) ) )
17 iffalse 
 |-  ( -. k <_ N -> if ( k <_ N , A , 0 ) = 0 )
18 17 fveq2d 
 |-  ( -. k <_ N -> ( _I ` if ( k <_ N , A , 0 ) ) = ( _I ` 0 ) )
19 0cn 
 |-  0 e. CC
20 fvi 
 |-  ( 0 e. CC -> ( _I ` 0 ) = 0 )
21 19 20 ax-mp 
 |-  ( _I ` 0 ) = 0
22 18 21 eqtrdi 
 |-  ( -. k <_ N -> ( _I ` if ( k <_ N , A , 0 ) ) = 0 )
23 eqid 
 |-  ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) = ( k e. NN0 |-> if ( k <_ N , A , 0 ) )
24 23 fvmpt2i 
 |-  ( k e. NN0 -> ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) = ( _I ` if ( k <_ N , A , 0 ) ) )
25 24 eqeq1d 
 |-  ( k e. NN0 -> ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) = 0 <-> ( _I ` if ( k <_ N , A , 0 ) ) = 0 ) )
26 22 25 syl5ibr 
 |-  ( k e. NN0 -> ( -. k <_ N -> ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) = 0 ) )
27 8 12 16 26 vtoclgaf 
 |-  ( m e. NN0 -> ( -. m <_ N -> ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) = 0 ) )
28 27 imp 
 |-  ( ( m e. NN0 /\ -. m <_ N ) -> ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) = 0 )
29 28 adantll 
 |-  ( ( ( ph /\ m e. NN0 ) /\ -. m <_ N ) -> ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) = 0 )
30 7 29 eqtrd 
 |-  ( ( ( ph /\ m e. NN0 ) /\ -. m <_ N ) -> ( ( coeff ` F ) ` m ) = 0 )
31 30 ex 
 |-  ( ( ph /\ m e. NN0 ) -> ( -. m <_ N -> ( ( coeff ` F ) ` m ) = 0 ) )
32 31 necon1ad 
 |-  ( ( ph /\ m e. NN0 ) -> ( ( ( coeff ` F ) ` m ) =/= 0 -> m <_ N ) )
33 32 ralrimiva 
 |-  ( ph -> A. m e. NN0 ( ( ( coeff ` F ) ` m ) =/= 0 -> m <_ N ) )
34 eqid 
 |-  ( coeff ` F ) = ( coeff ` F )
35 34 coef3 
 |-  ( F e. ( Poly ` S ) -> ( coeff ` F ) : NN0 --> CC )
36 1 35 syl 
 |-  ( ph -> ( coeff ` F ) : NN0 --> CC )
37 plyco0 
 |-  ( ( N e. NN0 /\ ( coeff ` F ) : NN0 --> CC ) -> ( ( ( coeff ` F ) " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } <-> A. m e. NN0 ( ( ( coeff ` F ) ` m ) =/= 0 -> m <_ N ) ) )
38 2 36 37 syl2anc 
 |-  ( ph -> ( ( ( coeff ` F ) " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } <-> A. m e. NN0 ( ( ( coeff ` F ) ` m ) =/= 0 -> m <_ N ) ) )
39 33 38 mpbird 
 |-  ( ph -> ( ( coeff ` F ) " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
40 eqid 
 |-  ( deg ` F ) = ( deg ` F )
41 34 40 dgrlb 
 |-  ( ( F e. ( Poly ` S ) /\ N e. NN0 /\ ( ( coeff ` F ) " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } ) -> ( deg ` F ) <_ N )
42 1 2 39 41 syl3anc 
 |-  ( ph -> ( deg ` F ) <_ N )