Theorem absscl

Description: Closure law for surreal absolute value. (Contributed by Scott Fenton, 16-Apr-2025)

	Ref	Expression
Assertion	absscl	$$⊢A\in \mathrm{No}\to {abs}_s\left(A\right)\in \mathrm{No}$$

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		id	$$⊢A\in \mathrm{No}\to A\in \mathrm{No}$$
3		negscl	$$⊢A\in \mathrm{No}\to {+}_s\left(A\right)\in \mathrm{No}$$
4	2 3	ifcld	$$⊢A\in \mathrm{No}\to if\left(0_s{\le }_{s}A,A,{+}_s\left(A\right)\right)\in \mathrm{No}$$
5	1 4	eqeltrd	$$⊢A\in \mathrm{No}\to {abs}_s\left(A\right)\in \mathrm{No}$$