Metamath Proof Explorer

Theorem ltmuls

Description: An ordering relationship for surreal multiplication. Compare theorem 8(iii) of Conway p. 19. (Contributed by Scott Fenton, 5-Mar-2025)

Ref Expression
Assertion ltmuls ⊢ 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

Proof

Step Hyp Ref Expression
1 0no ⊢ 0 s ∈ No
2 1 1 pm3.2i ⊢ 0 s ∈ No ∧ 0 s ∈ No
3 mulsprop ⊢ 0 s ∈ No ∧ 0 s ∈ No ∧ A ∈ No ∧ B ∈ No ∧ C ∈ No ∧ D ∈ No → 0 s ⋅ s 0 s ∈ No ∧ A < s B ∧ C < s D → A ⋅ s D - s A ⋅ s C < s B ⋅ s D - s B ⋅ s C
4 2 3 mp3an1 ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No ∧ D ∈ No → 0 s ⋅ s 0 s ∈ No ∧ A < s B ∧ C < s D → A ⋅ s D - s A ⋅ s C < s B ⋅ s D - s B ⋅ s C
5 4 simprd ⊢ 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