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 Poly S A 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 Poly S k 0 A k 0 k N
4 3 3expia F Poly S k 0 A k 0 k N
5 4 ralrimiva F Poly S k 0 A k 0 k N
6 dgrcl F Poly S deg F 0
7 2 6 eqeltrid F Poly S N 0
8 1 coef3 F Poly S A : 0
9 plyco0 N 0 A : 0 A N + 1 = 0 k 0 A k 0 k N
10 7 8 9 syl2anc F Poly S A N + 1 = 0 k 0 A k 0 k N
11 5 10 mpbird F Poly S A N + 1 = 0