Metamath Proof Explorer

Theorem gt0ne0d

Description: Positive implies nonzero. (Contributed by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 gt0ne0d.1 
 |-  ( ph -> 0 < A )
2 0re 
 |-  0 e. RR
3 ltne 
 |-  ( ( 0 e. RR /\ 0 < A ) -> A =/= 0 )
4 2 1 3 sylancr 
 |-  ( ph -> A =/= 0 )