This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dgrub2

Description: All the coefficients above the degree of F are zero. (Contributed by Mario Carneiro, 23-Jul-2014)

Ref Expression
Hypotheses dgrub.1 
|- A = ( coeff ` F )
dgrub.2 
|- N = ( deg ` F )
Assertion dgrub2 
|- ( F e. ( Poly ` S ) -> ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )

Proof

Step Hyp Ref Expression
1 dgrub.1 
 |-  A = ( coeff ` F )
2 dgrub.2 
 |-  N = ( deg ` F )
3 1 2 dgrub 
 |-  ( ( F e. ( Poly ` S ) /\ k e. NN0 /\ ( A ` k ) =/= 0 ) -> k <_ N )
4 3 3expia 
 |-  ( ( F e. ( Poly ` S ) /\ k e. NN0 ) -> ( ( A ` k ) =/= 0 -> k <_ N ) )
5 4 ralrimiva 
 |-  ( F e. ( Poly ` S ) -> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) )
6 dgrcl 
 |-  ( F e. ( Poly ` S ) -> ( deg ` F ) e. NN0 )
7 2 6 eqeltrid 
 |-  ( F e. ( Poly ` S ) -> N e. NN0 )
8 1 coef3 
 |-  ( F e. ( Poly ` S ) -> A : NN0 --> CC )
9 plyco0 
 |-  ( ( N e. NN0 /\ A : NN0 --> CC ) -> ( ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } <-> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) ) )
10 7 8 9 syl2anc 
 |-  ( F e. ( Poly ` S ) -> ( ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } <-> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) ) )
11 5 10 mpbird 
 |-  ( F e. ( Poly ` S ) -> ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )