Metamath Proof Explorer

Theorem ltmulsd

Description: An ordering relationship for surreal multiplication. Compare theorem 8(iii) of Conway p. 19. (Contributed by Scott Fenton, 6-Mar-2025)

		Ref	Expression
	Hypotheses	ltmulsd.1	$⊢ φ \to A \in No$
		ltmulsd.2	$⊢ φ \to B \in No$
		ltmulsd.3	$⊢ φ \to C \in No$
		ltmulsd.4	$⊢ φ \to D \in No$
		ltmulsd.5	$⊢ φ \to A <_{s} B$
		ltmulsd.6	$⊢ φ \to C <_{s} D$
	Assertion	ltmulsd	$⊢ φ \to ((A \cdot_{s} D) -_{s} (A \cdot_{s} C)) <_{s} ((B \cdot_{s} D) -_{s} (B \cdot_{s} C))$

Proof

Step	Hyp	Ref	Expression
1		ltmulsd.1	$⊢ φ \to A \in No$
2		ltmulsd.2	$⊢ φ \to B \in No$
3		ltmulsd.3	$⊢ φ \to C \in No$
4		ltmulsd.4	$⊢ φ \to D \in No$
5		ltmulsd.5	$⊢ φ \to A <_{s} B$
6		ltmulsd.6	$⊢ φ \to C <_{s} D$
7		ltmuls	$⊢ ((A \in No \land B \in No) \land (C \in No \land D \in No)) \to ((A <_{s} B \land C <_{s} D) \to ((A \cdot_{s} D) -_{s} (A \cdot_{s} C)) <_{s} ((B \cdot_{s} D) -_{s} (B \cdot_{s} C)))$
8	1 2 3 4 7	syl22anc	$⊢ φ \to ((A <_{s} B \land C <_{s} D) \to ((A \cdot_{s} D) -_{s} (A \cdot_{s} C)) <_{s} ((B \cdot_{s} D) -_{s} (B \cdot_{s} C)))$
9	5 6 8	mp2and	$⊢ φ \to ((A \cdot_{s} D) -_{s} (A \cdot_{s} C)) <_{s} ((B \cdot_{s} D) -_{s} (B \cdot_{s} C))$