Metamath Proof Explorer


Theorem dgrmul2

Description: The degree of a product of polynomials is at most the sum of degrees. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses dgradd.1 M = deg F
dgradd.2 N = deg G
Assertion dgrmul2 F Poly S G Poly S deg F × f G M + N

Proof

Step Hyp Ref Expression
1 dgradd.1 M = deg F
2 dgradd.2 N = deg G
3 eqid coeff F = coeff F
4 eqid coeff G = coeff G
5 3 4 1 2 coemullem F Poly S G Poly S coeff F × f G = n 0 k = 0 n coeff F k coeff G n k deg F × f G M + N
6 5 simprd F Poly S G Poly S deg F × f G M + N