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