Metamath Proof Explorer

Theorem rpgt0

Description: A positive real is greater than zero. (Contributed by FL, 27-Dec-2007)

Ref Expression
Assertion rpgt0 
|- ( A e. RR+ -> 0 < A )

Proof

Step Hyp Ref Expression
1 elrp 
 |-  ( A e. RR+ <-> ( A e. RR /\ 0 < A ) )
2 1 simprbi 
 |-  ( A e. RR+ -> 0 < A )