Metamath Proof Explorer


Theorem rpabsid

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

Ref Expression
Assertion rpabsid ( 𝑅 ∈ ℝ+ → ( abs ‘ 𝑅 ) = 𝑅 )

Proof

Step Hyp Ref Expression
1 rpre ( 𝑅 ∈ ℝ+𝑅 ∈ ℝ )
2 rpge0 ( 𝑅 ∈ ℝ+ → 0 ≤ 𝑅 )
3 absid ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( abs ‘ 𝑅 ) = 𝑅 )
4 1 2 3 syl2anc ( 𝑅 ∈ ℝ+ → ( abs ‘ 𝑅 ) = 𝑅 )