Metamath Proof Explorer

Theorem sltmulneg1d

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

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

Proof

Step Hyp Ref Expression
1 sltmulneg.1 ⊢ φ → A ∈ No
2 sltmulneg.2 ⊢ φ → B ∈ No
3 sltmulneg.3 ⊢ φ → C ∈ No
4 sltmulneg.4 ⊢ φ → C < s 0 s
5 1 3 mulnegs2d ⊢ φ → A ⋅ s + s ⁡ C = + s ⁡ A ⋅ s C
6 2 3 mulnegs2d ⊢ φ → B ⋅ s + s ⁡ C = + s ⁡ B ⋅ s C
7 5 6 breq12d ⊢ φ → A ⋅ s + s ⁡ C < s B ⋅ s + s ⁡ C ↔ + s ⁡ A ⋅ s C < s + s ⁡ B ⋅ s C
8 3 negscld ⊢ φ → + s ⁡ C ∈ No
9 negs0s ⊢ + s ⁡ 0 s = 0 s
10 0sno ⊢ 0 s ∈ No
11 10 a1i ⊢ φ → 0 s ∈ No
12 3 11 sltnegd ⊢ φ → C < s 0 s ↔ + s ⁡ 0 s < s + s ⁡ C
13 4 12 mpbid ⊢ φ → + s ⁡ 0 s < s + s ⁡ C
14 9 13 eqbrtrrid ⊢ φ → 0 s < s + s ⁡ C
15 1 2 8 14 sltmul1d ⊢ φ → A < s B ↔ A ⋅ s + s ⁡ C < s B ⋅ s + s ⁡ C
16 2 3 mulscld ⊢ φ → B ⋅ s C ∈ No
17 1 3 mulscld ⊢ φ → A ⋅ s C ∈ No
18 16 17 sltnegd ⊢ φ → B ⋅ s C < s A ⋅ s C ↔ + s ⁡ A ⋅ s C < s + s ⁡ B ⋅ s C
19 7 15 18 3bitr4d ⊢ φ → A < s B ↔ B ⋅ s C < s A ⋅ s C