Database
REAL AND COMPLEX NUMBERS
Integer sets
Some properties of specific numbers
neg1rr
Next ⟩
neg1ne0
Metamath Proof Explorer
Ascii
Structured
Theorem
neg1rr
Description:
-1 is a real number.
(Contributed by
David A. Wheeler
, 5-Dec-2018)
Ref
Expression
Assertion
neg1rr
⊢
- 1 ∈ ℝ
Proof
Step
Hyp
Ref
Expression
1
1re
⊢
1 ∈ ℝ
2
1
renegcli
⊢
- 1 ∈ ℝ