This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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_{𝑝} = ℂ \times \{0\}$
2	1	fveq2i	$⊢ \deg (0_{𝑝}) = \deg (ℂ \times \{0\})$
3		0cn	$⊢ 0 \in ℂ$
4		0dgr	$⊢ 0 \in ℂ \to \deg (ℂ \times \{0\}) = 0$
5	3 4	ax-mp	$⊢ \deg (ℂ \times \{0\}) = 0$
6	2 5	eqtri	$⊢ \deg (0_{𝑝}) = 0$