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 ‘ 𝑅 ) = 𝑅 ) |