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	⊢ - π ∈ ℂ