Database
BASIC REAL AND COMPLEX FUNCTIONS
Basic trigonometry
Properties of pi = 3.14159...
negpicn
Next ⟩
sinhalfpilem
Metamath Proof Explorer
Ascii
Unicode
Theorem
negpicn
Description:
-u _pi
is a real number.
(Contributed by
David A. Wheeler
, 8-Dec-2018)
Ref
Expression
Assertion
negpicn
⊢
−
π
∈
ℂ
Proof
Step
Hyp
Ref
Expression
1
picn
⊢
π
∈
ℂ
2
1
negcli
⊢
−
π
∈
ℂ