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

Metamath Proof Explorer

Theorem 0cn

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

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

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