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\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		ax-icn	$$⊢\mathrm{i}\in ℂ$$
2		cnegex	$$⊢\mathrm{i}\in ℂ\to \exists x\in ℂ\mathrm{i}+x=0$$
3	1 2	ax-mp	$$⊢\exists x\in ℂ\mathrm{i}+x=0$$
4		addcl	$$⊢\left(\mathrm{i}\in ℂ\wedge x\in ℂ\right)\to \mathrm{i}+x\in ℂ$$
5	1 4	mpan	$$⊢x\in ℂ\to \mathrm{i}+x\in ℂ$$
6		eleq1	$$⊢\mathrm{i}+x=0\to \left(\mathrm{i}+x\in ℂ\leftrightarrow 0\in ℂ\right)$$
7	5 6	syl5ibcom	$$⊢x\in ℂ\to \left(\mathrm{i}+x=0\to 0\in ℂ\right)$$
8	7	rexlimiv	$$⊢\exists x\in ℂ\mathrm{i}+x=0\to 0\in ℂ$$
9	3 8	ax-mp	$$⊢0\in ℂ$$