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 ‘ 0𝑝 ) = 0

Proof

Step	Hyp	Ref	Expression
1		df-0p	⊢ 0𝑝 = ( ℂ × { 0 } )
2	1	fveq2i	⊢ ( deg ‘ 0𝑝 ) = ( deg ‘ ( ℂ × { 0 } ) )
3		0cn	⊢ 0 ∈ ℂ
4		0dgr	⊢ ( 0 ∈ ℂ → ( deg ‘ ( ℂ × { 0 } ) ) = 0 )
5	3 4	ax-mp	⊢ ( deg ‘ ( ℂ × { 0 } ) ) = 0
6	2 5	eqtri	⊢ ( deg ‘ 0𝑝 ) = 0