Theorem rpne0

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

	Ref	Expression
Assertion	rpne0	$$⊢A\in {ℝ}^{+}\to A\ne 0$$

Proof

Step	Hyp	Ref	Expression
1		rpregt0	$$⊢A\in {ℝ}^{+}\to \left(A\in ℝ\wedge 0<A\right)$$
2		gt0ne0	$$⊢\left(A\in ℝ\wedge 0<A\right)\to A\ne 0$$
3	1 2	syl	$$⊢A\in {ℝ}^{+}\to A\ne 0$$