Theorem ltnegs

Description: Negative of both sides of surreal less-than. (Contributed by Scott Fenton, 3-Feb-2025)

	Ref	Expression
Assertion	ltnegs	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(A{<}_{s}B\leftrightarrow {+}_s\left(B\right){<}_s{+}_s\left(A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ltnegsim	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(A{<}_{s}B\to {+}_s\left(B\right){<}_s{+}_s\left(A\right)\right)$$
2		negscl	$$⊢B\in \mathrm{No}\to {+}_s\left(B\right)\in \mathrm{No}$$
3		negscl	$$⊢A\in \mathrm{No}\to {+}_s\left(A\right)\in \mathrm{No}$$
4		ltnegsim	$$⊢\left({+}_s\left(B\right)\in \mathrm{No}\wedge {+}_s\left(A\right)\in \mathrm{No}\right)\to \left({+}_s\left(B\right){<}_s{+}_s\left(A\right)\to {+}_s\left({+}_s\left(A\right)\right){<}_s{+}_s\left({+}_s\left(B\right)\right)\right)$$
5	2 3 4	syl2anr	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left({+}_s\left(B\right){<}_s{+}_s\left(A\right)\to {+}_s\left({+}_s\left(A\right)\right){<}_s{+}_s\left({+}_s\left(B\right)\right)\right)$$
6		negnegs	$$⊢A\in \mathrm{No}\to {+}_s\left({+}_s\left(A\right)\right)=A$$
7		negnegs	$$⊢B\in \mathrm{No}\to {+}_s\left({+}_s\left(B\right)\right)=B$$
8	6 7	breqan12d	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left({+}_s\left({+}_s\left(A\right)\right){<}_s{+}_s\left({+}_s\left(B\right)\right)\leftrightarrow A{<}_{s}B\right)$$
9	5 8	sylibd	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left({+}_s\left(B\right){<}_s{+}_s\left(A\right)\to A{<}_{s}B\right)$$
10	1 9	impbid	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(A{<}_{s}B\leftrightarrow {+}_s\left(B\right){<}_s{+}_s\left(A\right)\right)$$