Theorem rpne0

Description: A positive real is nonzero. (Contributed by NM, 18-Jul-2008)

	Ref	Expression
Assertion	rpne0	|- ( A e. RR+ -> A =/= 0 )

Proof

Step	Hyp	Ref	Expression
1		rpregt0	|- ( A e. RR+ -> ( A e. RR /\ 0 < A ) )
2		gt0ne0	|- ( ( A e. RR /\ 0 < A ) -> A =/= 0 )
3	1 2	syl	|- ( A e. RR+ -> A =/= 0 )