Metamath Proof Explorer

Theorem sltmuld

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	sltmuld.1	$⊢ φ \to A \in No$
		sltmuld.2	$⊢ φ \to B \in No$
		sltmuld.3	$⊢ φ \to C \in No$
		sltmuld.4	$⊢ φ \to D \in No$
		sltmuld.5	$⊢ φ \to A <_{s} B$
		sltmuld.6	$⊢ φ \to C <_{s} D$
	Assertion	sltmuld	$⊢ φ \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		sltmuld.1	$⊢ φ \to A \in No$
2		sltmuld.2	$⊢ φ \to B \in No$
3		sltmuld.3	$⊢ φ \to C \in No$
4		sltmuld.4	$⊢ φ \to D \in No$
5		sltmuld.5	$⊢ φ \to A <_{s} B$
6		sltmuld.6	$⊢ φ \to C <_{s} D$
7		sltmul	$⊢ ((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))$