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 )