slesubsub2bd

Description: Equivalence for the surreal less-than or equal relationship between differences. (Contributed by Scott Fenton, 7-Mar-2025)

	Ref	Expression
Hypotheses	sltsubsubbd.1	$⊢ φ \to A \in No$
	sltsubsubbd.2	$⊢ φ \to B \in No$
	sltsubsubbd.3	$⊢ φ \to C \in No$
	sltsubsubbd.4	$⊢ φ \to D \in No$
Assertion	slesubsub2bd	$⊢ φ \to ((A -_{s} B) \leq_{s} (C -_{s} D) \leftrightarrow (D -_{s} C) \leq_{s} (B -_{s} A))$

Step	Hyp	Ref	Expression
1		sltsubsubbd.1	$⊢ φ \to A \in No$
2		sltsubsubbd.2	$⊢ φ \to B \in No$
3		sltsubsubbd.3	$⊢ φ \to C \in No$
4		sltsubsubbd.4	$⊢ φ \to D \in No$
5	3 4 1 2	sltsubsub2bd	$⊢ φ \to ((C -_{s} D) <_{s} (A -_{s} B) \leftrightarrow (B -_{s} A) <_{s} (D -_{s} C))$
6	5	notbid	$⊢ φ \to (\neg (C -_{s} D) <_{s} (A -_{s} B) \leftrightarrow \neg (B -_{s} A) <_{s} (D -_{s} C))$
7	1 2	subscld	$⊢ φ \to A -_{s} B \in No$
8	3 4	subscld	$⊢ φ \to C -_{s} D \in No$
9		slenlt	$⊢ (A -_{s} B \in No \land C -_{s} D \in No) \to ((A -_{s} B) \leq_{s} (C -_{s} D) \leftrightarrow \neg (C -_{s} D) <_{s} (A -_{s} B))$
10	7 8 9	syl2anc	$⊢ φ \to ((A -_{s} B) \leq_{s} (C -_{s} D) \leftrightarrow \neg (C -_{s} D) <_{s} (A -_{s} B))$
11	4 3	subscld	$⊢ φ \to D -_{s} C \in No$
12	2 1	subscld	$⊢ φ \to B -_{s} A \in No$
13		slenlt	$⊢ (D -_{s} C \in No \land B -_{s} A \in No) \to ((D -_{s} C) \leq_{s} (B -_{s} A) \leftrightarrow \neg (B -_{s} A) <_{s} (D -_{s} C))$
14	11 12 13	syl2anc	$⊢ φ \to ((D -_{s} C) \leq_{s} (B -_{s} A) \leftrightarrow \neg (B -_{s} A) <_{s} (D -_{s} C))$
15	6 10 14	3bitr4d	$⊢ φ \to ((A -_{s} B) \leq_{s} (C -_{s} D) \leftrightarrow (D -_{s} C) \leq_{s} (B -_{s} A))$

Metamath Proof Explorer