Metamath Proof Explorer

Theorem ltmuls2

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

Ref Expression
Assertion ltmuls2 ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No → B < s C ↔ A ⋅ s B < s A ⋅ s C

Proof

Step Hyp Ref Expression
1 simpl1l ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ B < s C → A ∈ No
2 simpl3 ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ B < s C → C ∈ No
3 simpl2 ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ B < s C → B ∈ No
4 2 3 subscld ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ B < s C → C - s B ∈ No
5 simpl1r ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ B < s C → 0 s < s A
6 simp2 ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No → B ∈ No
7 simp3 ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No → C ∈ No
8 6 7 posdifsd ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No → B < s C ↔ 0 s < s C - s B
9 8 biimpa ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ B < s C → 0 s < s C - s B
10 1 4 5 9 mulsgt0d ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ B < s C → 0 s < s A ⋅ s C - s B
11 1 2 3 subsdid ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ B < s C → A ⋅ s C - s B = A ⋅ s C - s A ⋅ s B
12 10 11 breqtrd ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ B < s C → 0 s < s A ⋅ s C - s A ⋅ s B
13 1 3 mulscld ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ B < s C → A ⋅ s B ∈ No
14 1 2 mulscld ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ B < s C → A ⋅ s C ∈ No
15 13 14 posdifsd ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ B < s C → A ⋅ s B < s A ⋅ s C ↔ 0 s < s A ⋅ s C - s A ⋅ s B
16 12 15 mpbird ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ B < s C → A ⋅ s B < s A ⋅ s C
17 simp1l ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No → A ∈ No
18 17 7 mulscld ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No → A ⋅ s C ∈ No
19 ltsirr ⊢ A ⋅ s C ∈ No → ¬ A ⋅ s C < s A ⋅ s C
20 18 19 syl ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No → ¬ A ⋅ s C < s A ⋅ s C
21 oveq2 ⊢ B = C → A ⋅ s B = A ⋅ s C
22 21 breq1d ⊢ B = C → A ⋅ s B < s A ⋅ s C ↔ A ⋅ s C < s A ⋅ s C
23 22 notbid ⊢ B = C → ¬ A ⋅ s B < s A ⋅ s C ↔ ¬ A ⋅ s C < s A ⋅ s C
24 20 23 syl5ibrcom ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No → B = C → ¬ A ⋅ s B < s A ⋅ s C
25 24 con2d ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No → A ⋅ s B < s A ⋅ s C → ¬ B = C
26 25 imp ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ A ⋅ s B < s A ⋅ s C → ¬ B = C
27 17 6 mulscld ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No → A ⋅ s B ∈ No
28 ltsasym ⊢ A ⋅ s B ∈ No ∧ A ⋅ s C ∈ No → A ⋅ s B < s A ⋅ s C → ¬ A ⋅ s C < s A ⋅ s B
29 27 18 28 syl2anc ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No → A ⋅ s B < s A ⋅ s C → ¬ A ⋅ s C < s A ⋅ s B
30 29 imp ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ A ⋅ s B < s A ⋅ s C → ¬ A ⋅ s C < s A ⋅ s B
31 simpl1l ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ A ⋅ s B < s A ⋅ s C → A ∈ No
32 31 adantr ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ A ⋅ s B < s A ⋅ s C ∧ 0 s < s B - s C → A ∈ No
33 simpll2 ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ A ⋅ s B < s A ⋅ s C ∧ 0 s < s B - s C → B ∈ No
34 simpll3 ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ A ⋅ s B < s A ⋅ s C ∧ 0 s < s B - s C → C ∈ No
35 33 34 subscld ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ A ⋅ s B < s A ⋅ s C ∧ 0 s < s B - s C → B - s C ∈ No
36 simpl1r ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ A ⋅ s B < s A ⋅ s C → 0 s < s A
37 36 adantr ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ A ⋅ s B < s A ⋅ s C ∧ 0 s < s B - s C → 0 s < s A
38 simpr ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ A ⋅ s B < s A ⋅ s C ∧ 0 s < s B - s C → 0 s < s B - s C
39 32 35 37 38 mulsgt0d ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ A ⋅ s B < s A ⋅ s C ∧ 0 s < s B - s C → 0 s < s A ⋅ s B - s C
40 32 33 34 subsdid ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ A ⋅ s B < s A ⋅ s C ∧ 0 s < s B - s C → A ⋅ s B - s C = A ⋅ s B - s A ⋅ s C
41 40 breq2d ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ A ⋅ s B < s A ⋅ s C ∧ 0 s < s B - s C → 0 s < s A ⋅ s B - s C ↔ 0 s < s A ⋅ s B - s A ⋅ s C
42 18 ad2antrr ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ A ⋅ s B < s A ⋅ s C ∧ 0 s < s B - s C → A ⋅ s C ∈ No
43 27 ad2antrr ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ A ⋅ s B < s A ⋅ s C ∧ 0 s < s B - s C → A ⋅ s B ∈ No
44 42 43 posdifsd ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ A ⋅ s B < s A ⋅ s C ∧ 0 s < s B - s C → A ⋅ s C < s A ⋅ s B ↔ 0 s < s A ⋅ s B - s A ⋅ s C
45 41 44 bitr4d ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ A ⋅ s B < s A ⋅ s C ∧ 0 s < s B - s C → 0 s < s A ⋅ s B - s C ↔ A ⋅ s C < s A ⋅ s B
46 39 45 mpbid ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ A ⋅ s B < s A ⋅ s C ∧ 0 s < s B - s C → A ⋅ s C < s A ⋅ s B
47 30 46 mtand ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ A ⋅ s B < s A ⋅ s C → ¬ 0 s < s B - s C
48 simpl3 ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ A ⋅ s B < s A ⋅ s C → C ∈ No
49 simpl2 ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ A ⋅ s B < s A ⋅ s C → B ∈ No
50 48 49 posdifsd ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ A ⋅ s B < s A ⋅ s C → C < s B ↔ 0 s < s B - s C
51 47 50 mtbird ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ A ⋅ s B < s A ⋅ s C → ¬ C < s B
52 ltslin ⊢ B ∈ No ∧ C ∈ No → B < s C ∨ B = C ∨ C < s B
53 49 48 52 syl2anc ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ A ⋅ s B < s A ⋅ s C → B < s C ∨ B = C ∨ C < s B
54 26 51 53 ecase23d ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No ∧ A ⋅ s B < s A ⋅ s C → B < s C
55 16 54 impbida ⊢ A ∈ No ∧ 0 s < s A ∧ B ∈ No ∧ C ∈ No → B < s C ↔ A ⋅ s B < s A ⋅ s C