Theorem negpilt0

Description: Negative _pi is negative. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	negpilt0	⊢ - π < 0

Proof

Step	Hyp	Ref	Expression
1		pipos	⊢ 0 < π
2		pire	⊢ π ∈ ℝ
3		lt0neg2	⊢ ( π ∈ ℝ → ( 0 < π ↔ - π < 0 ) )
4	2 3	ax-mp	⊢ ( 0 < π ↔ - π < 0 )
5	1 4	mpbi	⊢ - π < 0