Metamath Proof Explorer

Theorem slemul1ad

Description: Multiplication of both sides of surreal less-than or equal by a non-negative number. (Contributed by Scott Fenton, 17-Apr-2025)

Ref Expression
Hypotheses slemul1ad.1 ⊢ φ → A ∈ No
slemul1ad.2 ⊢ φ → B ∈ No
slemul1ad.3 ⊢ φ → C ∈ No
slemul1ad.4 ⊢ φ → 0 s ≤ s C
slemul1ad.5 ⊢ φ → A ≤ s B
Assertion slemul1ad ⊢ φ → A ⋅ s C ≤ s B ⋅ s C

Proof

Step Hyp Ref Expression
1 slemul1ad.1 ⊢ φ → A ∈ No
2 slemul1ad.2 ⊢ φ → B ∈ No
3 slemul1ad.3 ⊢ φ → C ∈ No
4 slemul1ad.4 ⊢ φ → 0 s ≤ s C
5 slemul1ad.5 ⊢ φ → A ≤ s B
6 5 adantr ⊢ φ ∧ 0 s < s C → A ≤ s B
7 1 adantr ⊢ φ ∧ 0 s < s C → A ∈ No
8 2 adantr ⊢ φ ∧ 0 s < s C → B ∈ No
9 3 adantr ⊢ φ ∧ 0 s < s C → C ∈ No
10 simpr ⊢ φ ∧ 0 s < s C → 0 s < s C
11 7 8 9 10 slemul1d ⊢ φ ∧ 0 s < s C → A ≤ s B ↔ A ⋅ s C ≤ s B ⋅ s C
12 6 11 mpbid ⊢ φ ∧ 0 s < s C → A ⋅ s C ≤ s B ⋅ s C
13 0sno ⊢ 0 s ∈ No
14 slerflex ⊢ 0 s ∈ No → 0 s ≤ s 0 s
15 13 14 mp1i ⊢ φ → 0 s ≤ s 0 s
16 muls01 ⊢ A ∈ No → A ⋅ s 0 s = 0 s
17 1 16 syl ⊢ φ → A ⋅ s 0 s = 0 s
18 muls01 ⊢ B ∈ No → B ⋅ s 0 s = 0 s
19 2 18 syl ⊢ φ → B ⋅ s 0 s = 0 s
20 15 17 19 3brtr4d ⊢ φ → A ⋅ s 0 s ≤ s B ⋅ s 0 s
21 oveq2 ⊢ 0 s = C → A ⋅ s 0 s = A ⋅ s C
22 oveq2 ⊢ 0 s = C → B ⋅ s 0 s = B ⋅ s C
23 21 22 breq12d ⊢ 0 s = C → A ⋅ s 0 s ≤ s B ⋅ s 0 s ↔ A ⋅ s C ≤ s B ⋅ s C
24 20 23 syl5ibcom ⊢ φ → 0 s = C → A ⋅ s C ≤ s B ⋅ s C
25 24 imp ⊢ φ ∧ 0 s = C → A ⋅ s C ≤ s B ⋅ s C
26 sleloe ⊢ 0 s ∈ No ∧ C ∈ No → 0 s ≤ s C ↔ 0 s < s C ∨ 0 s = C
27 13 3 26 sylancr ⊢ φ → 0 s ≤ s C ↔ 0 s < s C ∨ 0 s = C
28 4 27 mpbid ⊢ φ → 0 s < s C ∨ 0 s = C
29 12 25 28 mpjaodan ⊢ φ → A ⋅ s C ≤ s B ⋅ s C