Metamath Proof Explorer

Theorem lt0ne0

Description: A number which is less than zero is not zero. (Contributed by Stefan O'Rear, 13-Sep-2014)

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

Proof

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