Theorem 0cn

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

	Ref	Expression
Assertion	0cn	⊢ 0 ∈ ℂ

Proof

Step	Hyp	Ref	Expression
1		ax-i2m1	⊢ ( ( i · i ) + 1 ) = 0
2		ax-icn	⊢ i ∈ ℂ
3		mulcl	⊢ ( ( i ∈ ℂ ∧ i ∈ ℂ ) → ( i · i ) ∈ ℂ )
4	2 2 3	mp2an	⊢ ( i · i ) ∈ ℂ
5		ax-1cn	⊢ 1 ∈ ℂ
6		addcl	⊢ ( ( ( i · i ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( i · i ) + 1 ) ∈ ℂ )
7	4 5 6	mp2an	⊢ ( ( i · i ) + 1 ) ∈ ℂ
8	1 7	eqeltrri	⊢ 0 ∈ ℂ