Theorem abs0s

Description: The absolute value of surreal zero. (Contributed by Scott Fenton, 16-Apr-2025)

	Ref	Expression
Assertion	abs0s	$$⊢{abs}_s\left(0_s\right)=0_s$$

Proof

Step	Hyp	Ref	Expression
1		0no	$$⊢0_s\in \mathrm{No}$$
2		lesid	$$⊢0_s\in \mathrm{No}\to 0_s{\le }_s{0}_s$$
3	1 2	ax-mp	$$⊢0_s{\le }_s{0}_s$$
4		abssid	$$⊢\left(0_s\in \mathrm{No}\wedge 0_s{\le }_s{0}_s\right)\to {abs}_s\left(0_s\right)=0_s$$
5	1 3 4	mp2an	$$⊢{abs}_s\left(0_s\right)=0_s$$