Metamath Proof Explorer

Theorem 0nrp

Description: Zero is not a positive real. Axiom 9 of Apostol p. 20. (Contributed by NM, 27-Oct-2007)

Ref Expression
Assertion 0nrp 
|- -. 0 e. RR+

Proof

Step Hyp Ref Expression
1 0re 
 |-  0 e. RR
2 1 ltnri 
 |-  -. 0 < 0
3 rpgt0 
 |-  ( 0 e. RR+ -> 0 < 0 )
4 2 3 mto 
 |-  -. 0 e. RR+