Metamath Proof Explorer

Theorem lemuls1d

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 ltmuls12d.1 ⊢ φ → A ∈ No
ltmuls12d.2 ⊢ φ → B ∈ No
ltmuls12d.3 ⊢ φ → C ∈ No
ltmuls12d.4 ⊢ φ → 0 s < s C
Assertion lemuls1d ⊢ φ → A ≤ s B ↔ A ⋅ s C ≤ s B ⋅ s C

Proof

Step Hyp Ref Expression
1 ltmuls12d.1 ⊢ φ → A ∈ No
2 ltmuls12d.2 ⊢ φ → B ∈ No
3 ltmuls12d.3 ⊢ φ → C ∈ No
4 ltmuls12d.4 ⊢ φ → 0 s < s C
5 2 1 3 4 ltmuls1d ⊢ φ → B < s A ↔ B ⋅ s C < s A ⋅ s C
6 5 notbid ⊢ φ → ¬ B < s A ↔ ¬ B ⋅ s C < s A ⋅ s C
7 lenlts ⊢ A ∈ No ∧ B ∈ No → A ≤ s B ↔ ¬ B < s A
8 1 2 7 syl2anc ⊢ φ → A ≤ s B ↔ ¬ B < s A
9 1 3 mulscld ⊢ φ → A ⋅ s C ∈ No
10 2 3 mulscld ⊢ φ → B ⋅ s C ∈ No
11 lenlts ⊢ A ⋅ s C ∈ No ∧ B ⋅ s C ∈ No → A ⋅ s C ≤ s B ⋅ s C ↔ ¬ B ⋅ s C < s A ⋅ s C
12 9 10 11 syl2anc ⊢ φ → A ⋅ s C ≤ s B ⋅ s C ↔ ¬ B ⋅ s C < s A ⋅ s C
13 6 8 12 3bitr4d ⊢ φ → A ≤ s B ↔ A ⋅ s C ≤ s B ⋅ s C