Metamath Proof Explorer

Theorem sltmul1d

Description: Multiplication of both sides of surreal less-than by a positive number. (Contributed by Scott Fenton, 10-Mar-2025)

Ref Expression
Hypotheses sltmul12d.1 ⊢ φ → A ∈ No
sltmul12d.2 ⊢ φ → B ∈ No
sltmul12d.3 ⊢ φ → C ∈ No
sltmul12d.4 ⊢ φ → 0 s < s C
Assertion sltmul1d ⊢ φ → A < s B ↔ A ⋅ s C < s B ⋅ s C

Proof

Step Hyp Ref Expression
1 sltmul12d.1 ⊢ φ → A ∈ No
2 sltmul12d.2 ⊢ φ → B ∈ No
3 sltmul12d.3 ⊢ φ → C ∈ No
4 sltmul12d.4 ⊢ φ → 0 s < s C
5 1 2 3 4 sltmul2d ⊢ φ → A < s B ↔ C ⋅ s A < s C ⋅ s B
6 1 3 mulscomd ⊢ φ → A ⋅ s C = C ⋅ s A
7 2 3 mulscomd ⊢ φ → B ⋅ s C = C ⋅ s B
8 6 7 breq12d ⊢ φ → A ⋅ s C < s B ⋅ s C ↔ C ⋅ s A < s C ⋅ s B
9 5 8 bitr4d ⊢ φ → A < s B ↔ A ⋅ s C < s B ⋅ s C