Metamath Proof Explorer

Theorem gt0ne0

Description: Positive implies nonzero. (Contributed by NM, 3-Oct-1999) (Proof shortened by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion gt0ne0 
|- ( ( A e. RR /\ 0 < A ) -> A =/= 0 )

Proof

Step Hyp Ref Expression
1 0red 
 |-  ( A e. RR -> 0 e. RR )
2 ltne 
 |-  ( ( 0 e. RR /\ 0 < A ) -> A =/= 0 )
3 1 2 sylan 
 |-  ( ( A e. RR /\ 0 < A ) -> A =/= 0 )