Theorem dgr0

Description: The degree of the zero polynomial is zero. Note: this differs from some other definitions of the degree of the zero polynomial, such as -u 1 , -oo or undefined. But it is convenient for us to define it this way, so that we have dgrcl , dgreq0 and coeid without having to special-case zero, although plydivalg is a little more complicated as a result. (Contributed by Mario Carneiro, 22-Jul-2014)

	Ref	Expression
Assertion	dgr0	|- ( deg ` 0p ) = 0

Proof

Step	Hyp	Ref	Expression
1		df-0p	|- 0p = ( CC X. { 0 } )
2	1	fveq2i	|- ( deg ` 0p ) = ( deg ` ( CC X. { 0 } ) )
3		0cn	|- 0 e. CC
4		0dgr	|- ( 0 e. CC -> ( deg ` ( CC X. { 0 } ) ) = 0 )
5	3 4	ax-mp	|- ( deg ` ( CC X. { 0 } ) ) = 0
6	2 5	eqtri	|- ( deg ` 0p ) = 0