Theorem rpabsid

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

	Ref	Expression
Assertion	rpabsid	$$⊢R\in {ℝ}^{+}\to \left|R\right|=R$$

Proof

Step	Hyp	Ref	Expression
1		rpre	$$⊢R\in {ℝ}^{+}\to R\in ℝ$$
2		rpge0	$$⊢R\in {ℝ}^{+}\to 0\le R$$
3		absid	$$⊢\left(R\in ℝ\wedge 0\le R\right)\to \left|R\right|=R$$
4	1 2 3	syl2anc	$$⊢R\in {ℝ}^{+}\to \left|R\right|=R$$