Description: A positive real is nonzero. (Contributed by NM, 18Jul2008)
Ref  Expression  

Assertion  rpne0   ( A e. RR+ > A =/= 0 ) 
Step  Hyp  Ref  Expression 

1  rpregt0   ( A e. RR+ > ( A e. RR /\ 0 < A ) ) 

2  gt0ne0   ( ( A e. RR /\ 0 < A ) > A =/= 0 ) 

3  1 2  syl   ( A e. RR+ > A =/= 0 ) 