Theorem abssid

Description: The absolute value of a non-negative surreal is itself. (Contributed by Scott Fenton, 16-Apr-2025)

	Ref	Expression
Assertion	abssid	$$⊢\left(A\in \mathrm{No}\wedge 0_s{\le }_{s}A\right)\to {abs}_s\left(A\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		abssval	$$⊢A\in \mathrm{No}\to {abs}_s\left(A\right)=if\left(0_s{\le }_{s}A,A,{+}_s\left(A\right)\right)$$
2		iftrue	$$⊢0_s{\le }_{s}A\to if\left(0_s{\le }_{s}A,A,{+}_s\left(A\right)\right)=A$$
3	1 2	sylan9eq	$$⊢\left(A\in \mathrm{No}\wedge 0_s{\le }_{s}A\right)\to {abs}_s\left(A\right)=A$$