Metamath Proof Explorer

Theorem rpabsid

Description: A positive real is its own absolute value. (Contributed by SN, 1-Oct-2025)

Ref Expression
Assertion rpabsid 
|- ( R e. RR+ -> ( abs ` R ) = R )

Proof

Step Hyp Ref Expression
1 rpre 
 |-  ( R e. RR+ -> R e. RR )
2 rpge0 
 |-  ( R e. RR+ -> 0 <_ R )
3 absid 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( abs ` R ) = R )
4 1 2 3 syl2anc 
 |-  ( R e. RR+ -> ( abs ` R ) = R )