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	$$⊢\mathrm{i}\in ℂ$$

Proof

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