Theorem absnegs

Description: Surreal absolute value of the negative. (Contributed by Scott Fenton, 16-Apr-2025)

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

Proof

Step	Hyp	Ref	Expression
1		negnegs	$$⊢A\in \mathrm{No}\to {+}_s\left({+}_s\left(A\right)\right)=A$$
2	1	adantr	$$⊢\left(A\in \mathrm{No}\wedge 0_s{\le }_{s}A\right)\to {+}_s\left({+}_s\left(A\right)\right)=A$$
3		negscl	$$⊢A\in \mathrm{No}\to {+}_s\left(A\right)\in \mathrm{No}$$
4		0no	$$⊢0_s\in \mathrm{No}$$
5	4	a1i	$$⊢A\in \mathrm{No}\to 0_s\in \mathrm{No}$$
6		id	$$⊢A\in \mathrm{No}\to A\in \mathrm{No}$$
7	5 6	lenegsd	$$⊢A\in \mathrm{No}\to \left(0_s{\le }_{s}A\leftrightarrow {+}_s\left(A\right){\le }_s{+}_s\left(0_s\right)\right)$$
8		neg0s	$$⊢{+}_s\left(0_s\right)=0_s$$
9	8	breq2i	$$⊢{+}_s\left(A\right){\le }_s{+}_s\left(0_s\right)\leftrightarrow {+}_s\left(A\right){\le }_s{0}_s$$
10	7 9	bitrdi	$$⊢A\in \mathrm{No}\to \left(0_s{\le }_{s}A\leftrightarrow {+}_s\left(A\right){\le }_s{0}_s\right)$$
11	10	biimpa	$$⊢\left(A\in \mathrm{No}\wedge 0_s{\le }_{s}A\right)\to {+}_s\left(A\right){\le }_s{0}_s$$
12		abssnid	$$⊢\left({+}_s\left(A\right)\in \mathrm{No}\wedge {+}_s\left(A\right){\le }_s{0}_s\right)\to {abs}_s\left({+}_s\left(A\right)\right)={+}_s\left({+}_s\left(A\right)\right)$$
13	3 11 12	syl2an2r	$$⊢\left(A\in \mathrm{No}\wedge 0_s{\le }_{s}A\right)\to {abs}_s\left({+}_s\left(A\right)\right)={+}_s\left({+}_s\left(A\right)\right)$$
14		abssid	$$⊢\left(A\in \mathrm{No}\wedge 0_s{\le }_{s}A\right)\to {abs}_s\left(A\right)=A$$
15	2 13 14	3eqtr4d	$$⊢\left(A\in \mathrm{No}\wedge 0_s{\le }_{s}A\right)\to {abs}_s\left({+}_s\left(A\right)\right)={abs}_s\left(A\right)$$
16	6 5	lenegsd	$$⊢A\in \mathrm{No}\to \left(A{\le }_s{0}_s\leftrightarrow {+}_s\left(0_s\right){\le }_s{+}_s\left(A\right)\right)$$
17	8	breq1i	$$⊢{+}_s\left(0_s\right){\le }_s{+}_s\left(A\right)\leftrightarrow 0_s{\le }_s{+}_s\left(A\right)$$
18	16 17	bitrdi	$$⊢A\in \mathrm{No}\to \left(A{\le }_s{0}_s\leftrightarrow 0_s{\le }_s{+}_s\left(A\right)\right)$$
19	18	biimpa	$$⊢\left(A\in \mathrm{No}\wedge A{\le }_s{0}_s\right)\to 0_s{\le }_s{+}_s\left(A\right)$$
20		abssid	$$⊢\left({+}_s\left(A\right)\in \mathrm{No}\wedge 0_s{\le }_s{+}_s\left(A\right)\right)\to {abs}_s\left({+}_s\left(A\right)\right)={+}_s\left(A\right)$$
21	3 19 20	syl2an2r	$$⊢\left(A\in \mathrm{No}\wedge A{\le }_s{0}_s\right)\to {abs}_s\left({+}_s\left(A\right)\right)={+}_s\left(A\right)$$
22		abssnid	$$⊢\left(A\in \mathrm{No}\wedge A{\le }_s{0}_s\right)\to {abs}_s\left(A\right)={+}_s\left(A\right)$$
23	21 22	eqtr4d	$$⊢\left(A\in \mathrm{No}\wedge A{\le }_s{0}_s\right)\to {abs}_s\left({+}_s\left(A\right)\right)={abs}_s\left(A\right)$$
24		lestric	$$⊢\left(0_s\in \mathrm{No}\wedge A\in \mathrm{No}\right)\to \left(0_s{\le }_{s}A\vee A{\le }_s{0}_s\right)$$
25	4 24	mpan	$$⊢A\in \mathrm{No}\to \left(0_s{\le }_{s}A\vee A{\le }_s{0}_s\right)$$
26	15 23 25	mpjaodan	$$⊢A\in \mathrm{No}\to {abs}_s\left({+}_s\left(A\right)\right)={abs}_s\left(A\right)$$