slesubsubbd

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

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	2 1 4 3	sltsubsub3bd	$⊢ φ \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		slenlt	$⊢ (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		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))$
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