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 )