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 e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( deg ` ( F oF x. G ) ) <_ ( M + N ) ) |
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 e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( coeff ` ( F oF x. G ) ) = ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( ( coeff ` F ) ` k ) x. ( ( coeff ` G ) ` ( n - k ) ) ) ) /\ ( deg ` ( F oF x. G ) ) <_ ( M + N ) ) ) |
6 | 5 | simprd | |- ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( deg ` ( F oF x. G ) ) <_ ( M + N ) ) |