Theorem abssnid

Description: For a negative surreal, its absolute value is its negation. (Contributed by Scott Fenton, 16-Apr-2025)

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

Proof

Step	Hyp	Ref	Expression
1		0no	$$⊢0_s\in \mathrm{No}$$
2		lesloe	$$⊢\left(A\in \mathrm{No}\wedge 0_s\in \mathrm{No}\right)\to \left(A{\le }_s{0}_s\leftrightarrow \left(A{<}_s{0}_s\vee A=0_s\right)\right)$$
3	1 2	mpan2	$$⊢A\in \mathrm{No}\to \left(A{\le }_s{0}_s\leftrightarrow \left(A{<}_s{0}_s\vee A=0_s\right)\right)$$
4		ltnles	$$⊢\left(A\in \mathrm{No}\wedge 0_s\in \mathrm{No}\right)\to \left(A{<}_s{0}_s\leftrightarrow \neg 0_s{\le }_{s}A\right)$$
5	1 4	mpan2	$$⊢A\in \mathrm{No}\to \left(A{<}_s{0}_s\leftrightarrow \neg 0_s{\le }_{s}A\right)$$
6		abssval	$$⊢A\in \mathrm{No}\to {abs}_s\left(A\right)=if\left(0_s{\le }_{s}A,A,{+}_s\left(A\right)\right)$$
7		iffalse	$$⊢\neg 0_s{\le }_{s}A\to if\left(0_s{\le }_{s}A,A,{+}_s\left(A\right)\right)={+}_s\left(A\right)$$
8	6 7	sylan9eq	$$⊢\left(A\in \mathrm{No}\wedge \neg 0_s{\le }_{s}A\right)\to {abs}_s\left(A\right)={+}_s\left(A\right)$$
9	8	ex	$$⊢A\in \mathrm{No}\to \left(\neg 0_s{\le }_{s}A\to {abs}_s\left(A\right)={+}_s\left(A\right)\right)$$
10	5 9	sylbid	$$⊢A\in \mathrm{No}\to \left(A{<}_s{0}_s\to {abs}_s\left(A\right)={+}_s\left(A\right)\right)$$
11		abs0s	$$⊢{abs}_s\left(0_s\right)=0_s$$
12		neg0s	$$⊢{+}_s\left(0_s\right)=0_s$$
13	11 12	eqtr4i	$$⊢{abs}_s\left(0_s\right)={+}_s\left(0_s\right)$$
14		fveq2	$$⊢A=0_s\to {abs}_s\left(A\right)={abs}_s\left(0_s\right)$$
15		fveq2	$$⊢A=0_s\to {+}_s\left(A\right)={+}_s\left(0_s\right)$$
16	13 14 15	3eqtr4a	$$⊢A=0_s\to {abs}_s\left(A\right)={+}_s\left(A\right)$$
17	16	a1i	$$⊢A\in \mathrm{No}\to \left(A=0_s\to {abs}_s\left(A\right)={+}_s\left(A\right)\right)$$
18	10 17	jaod	$$⊢A\in \mathrm{No}\to \left(\left(A{<}_s{0}_s\vee A=0_s\right)\to {abs}_s\left(A\right)={+}_s\left(A\right)\right)$$
19	3 18	sylbid	$$⊢A\in \mathrm{No}\to \left(A{\le }_s{0}_s\to {abs}_s\left(A\right)={+}_s\left(A\right)\right)$$
20	19	imp	$$⊢\left(A\in \mathrm{No}\wedge A{\le }_s{0}_s\right)\to {abs}_s\left(A\right)={+}_s\left(A\right)$$