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

Metamath Proof Explorer

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