Database
REAL AND COMPLEX NUMBERS
Derive the basic properties from the field axioms
Some deductions from the field axioms for complex numbers
1cnd
Next ⟩
1ex
Metamath Proof Explorer
Ascii
Unicode
Theorem
1cnd
Description:
One is a complex number, deduction form.
(Contributed by
David A. Wheeler
, 6-Dec-2018)
Ref
Expression
Assertion
1cnd
⊢
φ
→
1
∈
ℂ
Proof
Step
Hyp
Ref
Expression
1
ax-1cn
⊢
1
∈
ℂ
2
1
a1i
⊢
φ
→
1
∈
ℂ