Description: A positive real is its own absolute value. (Contributed by SN, 1-Oct-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | rpabsid | ⊢ ( 𝑅 ∈ ℝ+ → ( abs ‘ 𝑅 ) = 𝑅 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rpre | ⊢ ( 𝑅 ∈ ℝ+ → 𝑅 ∈ ℝ ) | |
| 2 | rpge0 | ⊢ ( 𝑅 ∈ ℝ+ → 0 ≤ 𝑅 ) | |
| 3 | absid | ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( abs ‘ 𝑅 ) = 𝑅 ) | |
| 4 | 1 2 3 | syl2anc | ⊢ ( 𝑅 ∈ ℝ+ → ( abs ‘ 𝑅 ) = 𝑅 ) |