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	⊢ ( 2 < π ∧ π < 4 )

Proof

Step	Hyp	Ref	Expression
1		pilem3	⊢ ( π ∈ ( 2 (,) 4 ) ∧ ( sin ‘ π ) = 0 )
2	1	simpli	⊢ π ∈ ( 2 (,) 4 )
3		eliooord	⊢ ( π ∈ ( 2 (,) 4 ) → ( 2 < π ∧ π < 4 ) )
4	2 3	ax-mp	⊢ ( 2 < π ∧ π < 4 )