Theorem ne0gt0

Description: A nonzero nonnegative number is positive. (Contributed by NM, 20-Nov-2007)

	Ref	Expression
Assertion	ne0gt0	|- ( ( A e. RR /\ 0 <_ A ) -> ( A =/= 0 <-> 0 < A ) )

Proof

Step	Hyp	Ref	Expression
1		0re	|- 0 e. RR
2		lttri2	|- ( ( A e. RR /\ 0 e. RR ) -> ( A =/= 0 <-> ( A < 0 \/ 0 < A ) ) )
3	1 2	mpan2	|- ( A e. RR -> ( A =/= 0 <-> ( A < 0 \/ 0 < A ) ) )
4	3	adantr	|- ( ( A e. RR /\ 0 <_ A ) -> ( A =/= 0 <-> ( A < 0 \/ 0 < A ) ) )
5		lenlt	|- ( ( 0 e. RR /\ A e. RR ) -> ( 0 <_ A <-> -. A < 0 ) )
6	1 5	mpan	|- ( A e. RR -> ( 0 <_ A <-> -. A < 0 ) )
7	6	biimpa	|- ( ( A e. RR /\ 0 <_ A ) -> -. A < 0 )
8		biorf	|- ( -. A < 0 -> ( 0 < A <-> ( A < 0 \/ 0 < A ) ) )
9	7 8	syl	|- ( ( A e. RR /\ 0 <_ A ) -> ( 0 < A <-> ( A < 0 \/ 0 < A ) ) )
10	4 9	bitr4d	|- ( ( A e. RR /\ 0 <_ A ) -> ( A =/= 0 <-> 0 < A ) )