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 ) |
| 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 ) |