Metamath Proof Explorer

Theorem lt0ne0d

Description: Something less than zero is not zero. Deduction form. (Contributed by David Moews, 28-Feb-2017)

Ref Expression
Hypothesis lt0ne0d.1 
|- ( ph -> A < 0 )
Assertion lt0ne0d 
|- ( ph -> A =/= 0 )

Proof

Step Hyp Ref Expression
1 lt0ne0d.1 
 |-  ( ph -> A < 0 )
2 0re 
 |-  0 e. RR
3 2 ltnri 
 |-  -. 0 < 0
4 breq1 
 |-  ( A = 0 -> ( A < 0 <-> 0 < 0 ) )
5 3 4 mtbiri 
 |-  ( A = 0 -> -. A < 0 )
6 5 necon2ai 
 |-  ( A < 0 -> A =/= 0 )
7 1 6 syl 
 |-  ( ph -> A =/= 0 )