Metamath Proof Explorer

Theorem slemul2d

Description: Multiplication of both sides of surreal less-than or equal 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 slemul2d ⊢ φ → A ≤ s B ↔ C ⋅ s A ≤ s C ⋅ s B

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 2 1 3 4 sltmul2d ⊢ φ → B < s A ↔ C ⋅ s B < s C ⋅ s A
6 5 notbid ⊢ φ → ¬ B < s A ↔ ¬ C ⋅ s B < s C ⋅ s A
7 slenlt ⊢ A ∈ No ∧ B ∈ No → A ≤ s B ↔ ¬ B < s A
8 1 2 7 syl2anc ⊢ φ → A ≤ s B ↔ ¬ B < s A
9 3 1 mulscld ⊢ φ → C ⋅ s A ∈ No
10 3 2 mulscld ⊢ φ → C ⋅ s B ∈ No
11 slenlt ⊢ C ⋅ s A ∈ No ∧ C ⋅ s B ∈ No → C ⋅ s A ≤ s C ⋅ s B ↔ ¬ C ⋅ s B < s C ⋅ s A
12 9 10 11 syl2anc ⊢ φ → C ⋅ s A ≤ s C ⋅ s B ↔ ¬ C ⋅ s B < s C ⋅ s A
13 6 8 12 3bitr4d ⊢ φ → A ≤ s B ↔ C ⋅ s A ≤ s C ⋅ s B