Theorem 0cnALT2

Description: Alternate proof of 0cnALT which is shorter, but depends on ax-8 , ax-13 , ax-sep , ax-nul , ax-pow , ax-pr , ax-un , and every complex number axiom except ax-pre-mulgt0 and ax-pre-sup . (Contributed by NM, 19-Feb-2005) (Revised by Mario Carneiro, 27-May-2016) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	0cnALT2	|- 0 e. CC

Proof

Step	Hyp	Ref	Expression
1		ax-icn	|- _i e. CC
2		cnegex	|- ( _i e. CC -> E. x e. CC ( _i + x ) = 0 )
3	1 2	ax-mp	|- E. x e. CC ( _i + x ) = 0
4		addcl	|- ( ( _i e. CC /\ x e. CC ) -> ( _i + x ) e. CC )
5	1 4	mpan	|- ( x e. CC -> ( _i + x ) e. CC )
6		eleq1	|- ( ( _i + x ) = 0 -> ( ( _i + x ) e. CC <-> 0 e. CC ) )
7	5 6	syl5ibcom	|- ( x e. CC -> ( ( _i + x ) = 0 -> 0 e. CC ) )
8	7	rexlimiv	|- ( E. x e. CC ( _i + x ) = 0 -> 0 e. CC )
9	3 8	ax-mp	|- 0 e. CC