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 | ||
sltmuld.2 | |||
sltmuld.3 | |||
sltmuld.4 | |||
sltmuld.5 | |||
sltmuld.6 | |||
Assertion | sltmuld |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sltmuld.1 | ||
2 | sltmuld.2 | ||
3 | sltmuld.3 | ||
4 | sltmuld.4 | ||
5 | sltmuld.5 | ||
6 | sltmuld.6 | ||
7 | sltmul | ||
8 | 1 2 3 4 7 | syl22anc | |
9 | 5 6 8 | mp2and |