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

Metamath Proof Explorer

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	$⊢ i \in ℂ$
2		cnegex	$⊢ i \in ℂ \to \exists x \in ℂ i + x = 0$
3	1 2	ax-mp	$⊢ \exists x \in ℂ i + x = 0$
4		addcl	$⊢ (i \in ℂ \land x \in ℂ) \to i + x \in ℂ$
5	1 4	mpan	$⊢ x \in ℂ \to i + x \in ℂ$
6		eleq1	$⊢ i + x = 0 \to (i + x \in ℂ \leftrightarrow 0 \in ℂ)$
7	5 6	syl5ibcom	$⊢ x \in ℂ \to (i + x = 0 \to 0 \in ℂ)$
8	7	rexlimiv	$⊢ \exists x \in ℂ i + x = 0 \to 0 \in ℂ$
9	3 8	ax-mp	$⊢ 0 \in ℂ$