Metamath Proof Explorer

Theorem pige3

Description: _pi is greater than or equal to 3. (Contributed by Mario Carneiro, 21-May-2016)

Ref Expression
Assertion pige3 
|- 3 <_ _pi

Proof

Step Hyp Ref Expression
1 3re 
 |-  3 e. RR
2 pire 
 |-  _pi e. RR
3 pigt3 
 |-  3 < _pi
4 1 2 3 ltleii 
 |-  3 <_ _pi