Metamath Proof Explorer

Theorem sgnrrp

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

Ref Expression
Assertion sgnrrp 
|- ( A e. RR+ -> ( sgn ` A ) = 1 )

Proof

Step Hyp Ref Expression
1 rpxr 
 |-  ( A e. RR+ -> A e. RR* )
2 rpgt0 
 |-  ( A e. RR+ -> 0 < A )
3 sgnp 
 |-  ( ( A e. RR* /\ 0 < A ) -> ( sgn ` A ) = 1 )
4 1 2 3 syl2anc 
 |-  ( A e. RR+ -> ( sgn ` A ) = 1 )