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<\mathrm{\pi }$$

Proof

Step	Hyp	Ref	Expression
1		2pos	$$⊢0<2$$
2		pigt2lt4	$$⊢\left(2<\mathrm{\pi }\wedge \mathrm{\pi }<4\right)$$
3	2	simpli	$$⊢2<\mathrm{\pi }$$
4		0re	$$⊢0\in ℝ$$
5		2re	$$⊢2\in ℝ$$
6		pire	$$⊢\mathrm{\pi }\in ℝ$$
7	4 5 6	lttri	$$⊢\left(0<2\wedge 2<\mathrm{\pi }\right)\to 0<\mathrm{\pi }$$
8	1 3 7	mp2an	$$⊢0<\mathrm{\pi }$$