0cnALT

Description: Alternate proof of 0cn which does not reference ax-1cn . (Contributed by NM, 19-Feb-2005) (Revised by Mario Carneiro, 27-May-2016) Reduce dependencies on axioms. (Revised by Steven Nguyen, 7-Jan-2022) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	0cnALT	$⊢ 0 \in ℂ$

Proof

Step	Hyp	Ref	Expression
1		ax-icn	$⊢ i \in ℂ$
2		cnre	$⊢ i \in ℂ \to \exists x \in ℝ \exists y \in ℝ i = x + i y$
3		ax-rnegex	$⊢ x \in ℝ \to \exists z \in ℝ x + z = 0$
4		readdcl	$⊢ (x \in ℝ \land z \in ℝ) \to x + z \in ℝ$
5		eleq1	$⊢ x + z = 0 \to (x + z \in ℝ \leftrightarrow 0 \in ℝ)$
6	4 5	syl5ibcom	$⊢ (x \in ℝ \land z \in ℝ) \to (x + z = 0 \to 0 \in ℝ)$
7	6	rexlimdva	$⊢ x \in ℝ \to (\exists z \in ℝ x + z = 0 \to 0 \in ℝ)$
8	3 7	mpd	$⊢ x \in ℝ \to 0 \in ℝ$
9	8	adantr	$⊢ (x \in ℝ \land \exists y \in ℝ i = x + i y) \to 0 \in ℝ$
10	9	rexlimiva	$⊢ \exists x \in ℝ \exists y \in ℝ i = x + i y \to 0 \in ℝ$
11	1 2 10	mp2b	$⊢ 0 \in ℝ$
12	11	recni	$⊢ 0 \in ℂ$

Metamath Proof Explorer

Theorem 0cnALT

Proof