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	$$⊢\mathrm{deg}\left(0_{𝑝}\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		df-0p	$$⊢0_{𝑝}=ℂ\times \left\{0\right\}$$
2	1	fveq2i	$$⊢\mathrm{deg}\left(0_{𝑝}\right)=\mathrm{deg}\left(ℂ\times \left\{0\right\}\right)$$
3		0cn	$$⊢0\in ℂ$$
4		0dgr	$$⊢0\in ℂ\to \mathrm{deg}\left(ℂ\times \left\{0\right\}\right)=0$$
5	3 4	ax-mp	$$⊢\mathrm{deg}\left(ℂ\times \left\{0\right\}\right)=0$$
6	2 5	eqtri	$$⊢\mathrm{deg}\left(0_{𝑝}\right)=0$$