This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 < π$

Step	Hyp	Ref	Expression
1		2pos	$⊢ 0 < 2$
2		pigt2lt4	$⊢ (2 < π \land π < 4)$
3	2	simpli	$⊢ 2 < π$
4		0re	$⊢ 0 \in ℝ$
5		2re	$⊢ 2 \in ℝ$
6		pire	$⊢ π \in ℝ$
7	4 5 6	lttri	$⊢ (0 < 2 \land 2 < π) \to 0 < π$
8	1 3 7	mp2an	$⊢ 0 < π$