Theorem sgnrrp

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

	Ref	Expression
Assertion	sgnrrp	⊢ ( 𝐴 ∈ ℝ+ → ( sgn ‘ 𝐴 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		rpxr	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ* )
2		rpgt0	⊢ ( 𝐴 ∈ ℝ+ → 0 < 𝐴 )
3		sgnp	⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ( sgn ‘ 𝐴 ) = 1 )
4	1 2 3	syl2anc	⊢ ( 𝐴 ∈ ℝ+ → ( sgn ‘ 𝐴 ) = 1 )