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

Proof

Step	Hyp	Ref	Expression
1		ltmulsd.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		ltmulsd.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3		ltmulsd.3	⊢ ( 𝜑 → 𝐶 ∈ No )
4		ltmulsd.4	⊢ ( 𝜑 → 𝐷 ∈ No )
5		ltmulsd.5	⊢ ( 𝜑 → 𝐴 <s 𝐵 )
6		ltmulsd.6	⊢ ( 𝜑 → 𝐶 <s 𝐷 )
7		ltmuls	⊢ ( ( ( 𝐴 ∈ 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 𝐶 ) ) )