Database
REAL AND COMPLEX NUMBERS
Derive the basic properties from the field axioms
Some deductions from the field axioms for complex numbers
1ex
Next ⟩
cnre
Metamath Proof Explorer
Ascii
Unicode
Theorem
1ex
Description:
One is a set.
(Contributed by
David A. Wheeler
, 7-Jul-2016)
Ref
Expression
Assertion
1ex
⊢
1
∈
V
Proof
Step
Hyp
Ref
Expression
1
ax-1cn
⊢
1
∈
ℂ
2
1
elexi
⊢
1
∈
V