Metamath Proof Explorer

Theorem gt0ne0i

Description: Positive means nonzero (useful for ordering theorems involving division). (Contributed by NM, 16-Sep-1999)

Ref Expression
Hypothesis lt2.1 
|- A e. RR
Assertion gt0ne0i 
|- ( 0 < A -> A =/= 0 )

Proof

Step Hyp Ref Expression
1 lt2.1 
 |-  A e. RR
2 0re 
 |-  0 e. RR
3 2 1 ltnei 
 |-  ( 0 < A -> A =/= 0 )