Description: 1 is a complex number. Axiom 2 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1cn . (Contributed by NM, 12-Apr-2007) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | ax1cn | ⊢ 1 ∈ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | axresscn | ⊢ ℝ ⊆ ℂ | |
2 | df-1 | ⊢ 1 = ⟨ 1R , 0R ⟩ | |
3 | 1sr | ⊢ 1R ∈ R | |
4 | opelreal | ⊢ ( ⟨ 1R , 0R ⟩ ∈ ℝ ↔ 1R ∈ R ) | |
5 | 3 4 | mpbir | ⊢ ⟨ 1R , 0R ⟩ ∈ ℝ |
6 | 2 5 | eqeltri | ⊢ 1 ∈ ℝ |
7 | 1 6 | sselii | ⊢ 1 ∈ ℂ |