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 ∈ ℂ

Proof

Step Hyp Ref Expression
1 0r ⊢ 0R ∈ R
2 1sr ⊢ 1R ∈ R
3 df-i ⊢ i = ⟨ 0R , 1R ⟩
4 3 eleq1i ⊢ ( i ∈ ℂ ↔ ⟨ 0R , 1R ⟩ ∈ ℂ )
5 opelcn ⊢ ( ⟨ 0R , 1R ⟩ ∈ ℂ ↔ ( 0R ∈ R ∧ 1R ∈ R ) )
6 4 5 bitri ⊢ ( i ∈ ℂ ↔ ( 0R ∈ R ∧ 1R ∈ R ) )
7 1 2 6 mpbir2an ⊢ i ∈ ℂ