Metamath Proof Explorer

Theorem ltmulnegs1d

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

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

Proof

Step Hyp Ref Expression
1 ltmulnegs.1 ⊢ φ → A ∈ No
2 ltmulnegs.2 ⊢ φ → B ∈ No
3 ltmulnegs.3 ⊢ φ → C ∈ No
4 ltmulnegs.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 neg0s ⊢ + s ⁡ 0 s = 0 s
10 0no ⊢ 0 s ∈ No
11 10 a1i ⊢ φ → 0 s ∈ No
12 3 11 ltnegsd ⊢ φ → 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 ltmuls1d ⊢ φ → 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 ltnegsd ⊢ φ → 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