Database
REAL AND COMPLEX NUMBERS
Derive the basic properties from the field axioms
Some deductions from the field axioms for complex numbers
1elpr01
Next ⟩
cnre
Metamath Proof Explorer
Ascii
Unicode
Theorem
1elpr01
Description:
1 is an element of
{ 0 , 1 }
.
(Contributed by
Umit Teoman Dogan
, 10-Jun-2026)
Ref
Expression
Assertion
1elpr01
⊢
1
∈
0
1
Proof
Step
Hyp
Ref
Expression
1
1ex
⊢
1
∈
V
2
1
prid2
⊢
1
∈
0
1