Metamath Proof Explorer

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 < _pi

Proof

Step Hyp Ref Expression
1 2pos 
 |-  0 < 2
2 pigt2lt4 
 |-  ( 2 < _pi /\ _pi < 4 )
3 2 simpli 
 |-  2 < _pi
4 0re 
 |-  0 e. RR
5 2re 
 |-  2 e. RR
6 pire 
 |-  _pi e. RR
7 4 5 6 lttri 
 |-  ( ( 0 < 2 /\ 2 < _pi ) -> 0 < _pi )
8 1 3 7 mp2an 
 |-  0 < _pi