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 < _pi /\ _pi < 4 )

Proof

Step Hyp Ref Expression
1 pilem3 
 |-  ( _pi e. ( 2 (,) 4 ) /\ ( sin ` _pi ) = 0 )
2 1 simpli 
 |-  _pi e. ( 2 (,) 4 )
3 eliooord 
 |-  ( _pi e. ( 2 (,) 4 ) -> ( 2 < _pi /\ _pi < 4 ) )
4 2 3 ax-mp 
 |-  ( 2 < _pi /\ _pi < 4 )