Theorem 0cn

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

	Ref	Expression
Assertion	0cn	|- 0 e. CC

Proof

Step	Hyp	Ref	Expression
1		ax-i2m1	|- ( ( _i x. _i ) + 1 ) = 0
2		ax-icn	|- _i e. CC
3		mulcl	|- ( ( _i e. CC /\ _i e. CC ) -> ( _i x. _i ) e. CC )
4	2 2 3	mp2an	|- ( _i x. _i ) e. CC
5		ax-1cn	|- 1 e. CC
6		addcl	|- ( ( ( _i x. _i ) e. CC /\ 1 e. CC ) -> ( ( _i x. _i ) + 1 ) e. CC )
7	4 5 6	mp2an	|- ( ( _i x. _i ) + 1 ) e. CC
8	1 7	eqeltrri	|- 0 e. CC