Metamath Proof Explorer
Description: Positive implies nonzero. (Contributed by NM, 3Oct1999) (Proof
shortened by Mario Carneiro, 27May2016)


Ref 
Expression 

Assertion 
gt0ne0 
$${\u22a2}\left({A}\in \mathbb{R}\wedge 0<{A}\right)\to {A}\ne 0$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

0red 
$${\u22a2}{A}\in \mathbb{R}\to 0\in \mathbb{R}$$ 
2 

ltne 
$${\u22a2}\left(0\in \mathbb{R}\wedge 0<{A}\right)\to {A}\ne 0$$ 
3 
1 2

sylan 
$${\u22a2}\left({A}\in \mathbb{R}\wedge 0<{A}\right)\to {A}\ne 0$$ 