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

Metamath Proof Explorer

Theorem axicn

Description: _i is a complex number. Axiom 3 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-icn . (Contributed by NM, 23-Feb-1996) (New usage is discouraged.)

		Ref	Expression
	Assertion	axicn	$⊢ i \in ℂ$

Proof

Step	Hyp	Ref	Expression
1		0r	$⊢ 0_{𝑹} \in 𝑹$
2		1sr	$⊢ 1_{𝑹} \in 𝑹$
3		df-i	$⊢ i = ⟨0_{𝑹}, 1_{𝑹}⟩$
4	3	eleq1i	$⊢ i \in ℂ \leftrightarrow ⟨0_{𝑹}, 1_{𝑹}⟩ \in ℂ$
5		opelcn	$⊢ ⟨0_{𝑹}, 1_{𝑹}⟩ \in ℂ \leftrightarrow (0_{𝑹} \in 𝑹 \land 1_{𝑹} \in 𝑹)$
6	4 5	bitri	$⊢ i \in ℂ \leftrightarrow (0_{𝑹} \in 𝑹 \land 1_{𝑹} \in 𝑹)$
7	1 2 6	mpbir2an	$⊢ i \in ℂ$