Database
REAL AND COMPLEX NUMBERS
Integer sets
Some properties of specific numbers
neg1cn
Next ⟩
neg1rr
Metamath Proof Explorer
Ascii
Unicode
Theorem
neg1cn
Description:
-1 is a complex number.
(Contributed by
David A. Wheeler
, 7-Jul-2016)
Ref
Expression
Assertion
neg1cn
⊢
−
1
∈
ℂ
Proof
Step
Hyp
Ref
Expression
1
ax-1cn
⊢
1
∈
ℂ
2
1
negcli
⊢
−
1
∈
ℂ