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	⊢ ( 𝜑 → 𝐴 ∈ No )
	sltmuld.2	⊢ ( 𝜑 → 𝐵 ∈ No )
	sltmuld.3	⊢ ( 𝜑 → 𝐶 ∈ No )
	sltmuld.4	⊢ ( 𝜑 → 𝐷 ∈ No )
	sltmuld.5	⊢ ( 𝜑 → 𝐴 <s 𝐵 )
	sltmuld.6	⊢ ( 𝜑 → 𝐶 <s 𝐷 )
Assertion	sltmuld	⊢ ( 𝜑 → ( ( 𝐴 ·s 𝐷 ) -s ( 𝐴 ·s 𝐶 ) ) <s ( ( 𝐵 ·s 𝐷 ) -s ( 𝐵 ·s 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sltmuld.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		sltmuld.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3		sltmuld.3	⊢ ( 𝜑 → 𝐶 ∈ No )
4		sltmuld.4	⊢ ( 𝜑 → 𝐷 ∈ No )
5		sltmuld.5	⊢ ( 𝜑 → 𝐴 <s 𝐵 )
6		sltmuld.6	⊢ ( 𝜑 → 𝐶 <s 𝐷 )
7		sltmul	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝐶 ∈ No ∧ 𝐷 ∈ No ) ) → ( ( 𝐴 <s 𝐵 ∧ 𝐶 <s 𝐷 ) → ( ( 𝐴 ·s 𝐷 ) -s ( 𝐴 ·s 𝐶 ) ) <s ( ( 𝐵 ·s 𝐷 ) -s ( 𝐵 ·s 𝐶 ) ) ) )
8	1 2 3 4 7	syl22anc	⊢ ( 𝜑 → ( ( 𝐴 <s 𝐵 ∧ 𝐶 <s 𝐷 ) → ( ( 𝐴 ·s 𝐷 ) -s ( 𝐴 ·s 𝐶 ) ) <s ( ( 𝐵 ·s 𝐷 ) -s ( 𝐵 ·s 𝐶 ) ) ) )
9	5 6 8	mp2and	⊢ ( 𝜑 → ( ( 𝐴 ·s 𝐷 ) -s ( 𝐴 ·s 𝐶 ) ) <s ( ( 𝐵 ·s 𝐷 ) -s ( 𝐵 ·s 𝐶 ) ) )