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 φ A No
sltmuld.2 φ B No
sltmuld.3 φ C No
sltmuld.4 φ D No
sltmuld.5 φ A < s B
sltmuld.6 φ C < s D
Assertion sltmuld φ A s D - s A s C < s B s D - s B s C

Proof

Step Hyp Ref Expression
1 sltmuld.1 φ A No
2 sltmuld.2 φ B No
3 sltmuld.3 φ C No
4 sltmuld.4 φ D No
5 sltmuld.5 φ A < s B
6 sltmuld.6 φ C < s D
7 sltmul A No B No C No D No A < s B C < s D A s D - s A s C < s B s D - s B s C
8 1 2 3 4 7 syl22anc φ A < s B C < s D A s D - s A s C < s B s D - s B s C
9 5 6 8 mp2and φ A s D - s A s C < s B s D - s B s C