lesubsubsbd

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	lesubsubsbd	$⊢ φ \to ((A -_{s} C) \leq_{s} (B -_{s} D) \leftrightarrow (A -_{s} B) \leq_{s} (C -_{s} D))$

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	2 1 4 3	ltsubsubs3bd	$⊢ φ \to ((B -_{s} D) <_{s} (A -_{s} C) \leftrightarrow (C -_{s} D) <_{s} (A -_{s} B))$
6	5	notbid	$⊢ φ \to (\neg (B -_{s} D) <_{s} (A -_{s} C) \leftrightarrow \neg (C -_{s} D) <_{s} (A -_{s} B))$
7	1 3	subscld	$⊢ φ \to A -_{s} C \in No$
8	2 4	subscld	$⊢ φ \to B -_{s} D \in No$
9		lenlts	$⊢ (A -_{s} C \in No \land B -_{s} D \in No) \to ((A -_{s} C) \leq_{s} (B -_{s} D) \leftrightarrow \neg (B -_{s} D) <_{s} (A -_{s} C))$
10	7 8 9	syl2anc	$⊢ φ \to ((A -_{s} C) \leq_{s} (B -_{s} D) \leftrightarrow \neg (B -_{s} D) <_{s} (A -_{s} C))$
11	1 2	subscld	$⊢ φ \to A -_{s} B \in No$
12	3 4	subscld	$⊢ φ \to C -_{s} D \in No$
13		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))$
14	11 12 13	syl2anc	$⊢ φ \to ((A -_{s} B) \leq_{s} (C -_{s} D) \leftrightarrow \neg (C -_{s} D) <_{s} (A -_{s} B))$
15	6 10 14	3bitr4d	$⊢ φ \to ((A -_{s} C) \leq_{s} (B -_{s} D) \leftrightarrow (A -_{s} B) \leq_{s} (C -_{s} D))$

Metamath Proof Explorer