lesubsubs2bd

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

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

Step	Hyp	Ref	Expression
1		ltsubsubsbd.1	$⊢ φ \to A \in No$
2		ltsubsubsbd.2	$⊢ φ \to B \in No$
3		ltsubsubsbd.3	$⊢ φ \to C \in No$
4		ltsubsubsbd.4	$⊢ φ \to D \in No$
5	3 4 1 2	ltsubsubs2bd	$⊢ φ \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		lenlts	$⊢ (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		lenlts	$⊢ (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