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

Proof

Step Hyp Ref Expression
1 2pos 0 < 2
2 pigt2lt4 2 < π π < 4
3 2 simpli 2 < π
4 0re 0
5 2re 2
6 pire π
7 4 5 6 lttri 0 < 2 2 < π 0 < π
8 1 3 7 mp2an 0 < π