Theorem sq0

Description: The square of 0 is 0. (Contributed by NM, 6-Jun-2006)

	Ref	Expression
Assertion	sq0	$$⊢0^2=0$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢0=0$$
2		0cn	$$⊢0\in ℂ$$
3	2	sqeq0i	$$⊢0^2=0\leftrightarrow 0=0$$
4	1 3	mpbir	$$⊢0^2=0$$