Database
BASIC REAL AND COMPLEX FUNCTIONS
Basic trigonometry
Properties of pi = 3.14159...
neghalfpire
Next ⟩
neghalfpirx
Metamath Proof Explorer
Ascii
Unicode
Theorem
neghalfpire
Description:
-u _pi / 2
is real.
(Contributed by
David A. Wheeler
, 8-Dec-2018)
Ref
Expression
Assertion
neghalfpire
⊢
−
π
2
∈
ℝ
Proof
Step
Hyp
Ref
Expression
1
halfpire
⊢
π
2
∈
ℝ
2
1
renegcli
⊢
−
π
2
∈
ℝ