Theorem pigt2lt4

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

	Ref	Expression
Assertion	pigt2lt4	$$⊢\left(2<\mathrm{\pi }\wedge \mathrm{\pi }<4\right)$$

Proof

Step	Hyp	Ref	Expression
1		pilem3	$$⊢\left(\mathrm{\pi }\in \left(2,4\right)\wedge \sin \mathrm{\pi }=0\right)$$
2	1	simpli	$$⊢\mathrm{\pi }\in \left(2,4\right)$$
3		eliooord	$$⊢\mathrm{\pi }\in \left(2,4\right)\to \left(2<\mathrm{\pi }\wedge \mathrm{\pi }<4\right)$$
4	2 3	ax-mp	$$⊢\left(2<\mathrm{\pi }\wedge \mathrm{\pi }<4\right)$$