slesubsub3bd

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	slesubsub3bd	$⊢ φ \to ((A -_{s} C) \leq_{s} (B -_{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	2 1 4 3	sltsubsubbd	$⊢ φ \to ((B -_{s} D) <_{s} (A -_{s} C) \leftrightarrow (B -_{s} A) <_{s} (D -_{s} C))$
6	5	notbid	$⊢ φ \to (\neg (B -_{s} D) <_{s} (A -_{s} C) \leftrightarrow \neg (B -_{s} A) <_{s} (D -_{s} C))$
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	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} C) \leq_{s} (B -_{s} D) \leftrightarrow (D -_{s} C) \leq_{s} (B -_{s} A))$

Metamath Proof Explorer