Theorem pipos

Description: _pi is positive. (Contributed by Paul Chapman, 23-Jan-2008) (Revised by Mario Carneiro, 9-May-2014)

	Ref	Expression
Assertion	pipos	⊢ 0 < π

Proof

Step	Hyp	Ref	Expression
1		2pos	⊢ 0 < 2
2		pigt2lt4	⊢ ( 2 < π ∧ π < 4 )
3	2	simpli	⊢ 2 < π
4		0re	⊢ 0 ∈ ℝ
5		2re	⊢ 2 ∈ ℝ
6		pire	⊢ π ∈ ℝ
7	4 5 6	lttri	⊢ ( ( 0 < 2 ∧ 2 < π ) → 0 < π )
8	1 3 7	mp2an	⊢ 0 < π