Theorem 0cn

Description: Zero is a complex number. See also 0cnALT . (Contributed by NM, 19-Feb-2005)

	Ref	Expression
Assertion	0cn	$$⊢0\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		ax-i2m1	$$⊢\mathrm{i}\mathrm{i}+1=0$$
2		ax-icn	$$⊢\mathrm{i}\in ℂ$$
3		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge \mathrm{i}\in ℂ\right)\to \mathrm{i}\mathrm{i}\in ℂ$$
4	2 2 3	mp2an	$$⊢\mathrm{i}\mathrm{i}\in ℂ$$
5		ax-1cn	$$⊢1\in ℂ$$
6		addcl	$$⊢\left(\mathrm{i}\mathrm{i}\in ℂ\wedge 1\in ℂ\right)\to \mathrm{i}\mathrm{i}+1\in ℂ$$
7	4 5 6	mp2an	$$⊢\mathrm{i}\mathrm{i}+1\in ℂ$$
8	1 7	eqeltrri	$$⊢0\in ℂ$$