Theorem sgnrrp

Description: The signum of a positive real is 1. (Contributed by David A. Wheeler, 18-May-2015)

	Ref	Expression
Assertion	sgnrrp	$$⊢A\in {ℝ}^{+}\to \mathrm{sgn}\left(A\right)=1$$

Proof

Step	Hyp	Ref	Expression
1		rpxr	$$⊢A\in {ℝ}^{+}\to A\in {ℝ}^{*}$$
2		rpgt0	$$⊢A\in {ℝ}^{+}\to 0<A$$
3		sgnp	$$⊢\left(A\in {ℝ}^{*}\wedge 0<A\right)\to \mathrm{sgn}\left(A\right)=1$$
4	1 2 3	syl2anc	$$⊢A\in {ℝ}^{+}\to \mathrm{sgn}\left(A\right)=1$$