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 } )