Metamath Proof Explorer

Theorem lemulsd

Description: An ordering relationship for surreal multiplication. Compare theorem 8(iii) of Conway p. 19. (Contributed by Scott Fenton, 7-Mar-2025)

Ref Expression
Hypotheses lemulsd.1 ⊢ φ → A ∈ No
lemulsd.2 ⊢ φ → B ∈ No
lemulsd.3 ⊢ φ → C ∈ No
lemulsd.4 ⊢ φ → D ∈ No
lemulsd.5 ⊢ φ → A ≤ s B
lemulsd.6 ⊢ φ → C ≤ s D
Assertion lemulsd ⊢ φ → A ⋅ s D - s A ⋅ s C ≤ s B ⋅ s D - s B ⋅ s C

Proof

Step Hyp Ref Expression
1 lemulsd.1 ⊢ φ → A ∈ No
2 lemulsd.2 ⊢ φ → B ∈ No
3 lemulsd.3 ⊢ φ → C ∈ No
4 lemulsd.4 ⊢ φ → D ∈ No
5 lemulsd.5 ⊢ φ → A ≤ s B
6 lemulsd.6 ⊢ φ → C ≤ s D
7 1 4 mulscld ⊢ φ → A ⋅ s D ∈ No
8 1 3 mulscld ⊢ φ → A ⋅ s C ∈ No
9 7 8 subscld ⊢ φ → A ⋅ s D - s A ⋅ s C ∈ No
10 9 adantr ⊢ φ ∧ A < s B ∧ C < s D → A ⋅ s D - s A ⋅ s C ∈ No
11 2 4 mulscld ⊢ φ → B ⋅ s D ∈ No
12 2 3 mulscld ⊢ φ → B ⋅ s C ∈ No
13 11 12 subscld ⊢ φ → B ⋅ s D - s B ⋅ s C ∈ No
14 13 adantr ⊢ φ ∧ A < s B ∧ C < s D → B ⋅ s D - s B ⋅ s C ∈ No
15 1 adantr ⊢ φ ∧ A < s B ∧ C < s D → A ∈ No
16 2 adantr ⊢ φ ∧ A < s B ∧ C < s D → B ∈ No
17 3 adantr ⊢ φ ∧ A < s B ∧ C < s D → C ∈ No
18 4 adantr ⊢ φ ∧ A < s B ∧ C < s D → D ∈ No
19 simprl ⊢ φ ∧ A < s B ∧ C < s D → A < s B
20 simprr ⊢ φ ∧ A < s B ∧ C < s D → C < s D
21 15 16 17 18 19 20 ltmulsd ⊢ φ ∧ A < s B ∧ C < s D → A ⋅ s D - s A ⋅ s C < s B ⋅ s D - s B ⋅ s C
22 10 14 21 ltlesd ⊢ φ ∧ A < s B ∧ C < s D → A ⋅ s D - s A ⋅ s C ≤ s B ⋅ s D - s B ⋅ s C
23 22 anassrs ⊢ φ ∧ A < s B ∧ C < s D → A ⋅ s D - s A ⋅ s C ≤ s B ⋅ s D - s B ⋅ s C
24 0no ⊢ 0 s ∈ No
25 lesid ⊢ 0 s ∈ No → 0 s ≤ s 0 s
26 24 25 mp1i ⊢ φ → 0 s ≤ s 0 s
27 subsid ⊢ A ⋅ s D ∈ No → A ⋅ s D - s A ⋅ s D = 0 s
28 7 27 syl ⊢ φ → A ⋅ s D - s A ⋅ s D = 0 s
29 subsid ⊢ B ⋅ s D ∈ No → B ⋅ s D - s B ⋅ s D = 0 s
30 11 29 syl ⊢ φ → B ⋅ s D - s B ⋅ s D = 0 s
31 26 28 30 3brtr4d ⊢ φ → A ⋅ s D - s A ⋅ s D ≤ s B ⋅ s D - s B ⋅ s D
32 oveq2 ⊢ C = D → A ⋅ s C = A ⋅ s D
33 32 oveq2d ⊢ C = D → A ⋅ s D - s A ⋅ s C = A ⋅ s D - s A ⋅ s D
34 oveq2 ⊢ C = D → B ⋅ s C = B ⋅ s D
35 34 oveq2d ⊢ C = D → B ⋅ s D - s B ⋅ s C = B ⋅ s D - s B ⋅ s D
36 33 35 breq12d ⊢ C = D → A ⋅ s D - s A ⋅ s C ≤ s B ⋅ s D - s B ⋅ s C ↔ A ⋅ s D - s A ⋅ s D ≤ s B ⋅ s D - s B ⋅ s D
37 31 36 syl5ibrcom ⊢ φ → C = D → A ⋅ s D - s A ⋅ s C ≤ s B ⋅ s D - s B ⋅ s C
38 37 imp ⊢ φ ∧ C = D → A ⋅ s D - s A ⋅ s C ≤ s B ⋅ s D - s B ⋅ s C
39 38 adantlr ⊢ φ ∧ A < s B ∧ C = D → A ⋅ s D - s A ⋅ s C ≤ s B ⋅ s D - s B ⋅ s C
40 lesloe ⊢ C ∈ No ∧ D ∈ No → C ≤ s D ↔ C < s D ∨ C = D
41 3 4 40 syl2anc ⊢ φ → C ≤ s D ↔ C < s D ∨ C = D
42 6 41 mpbid ⊢ φ → C < s D ∨ C = D
43 42 adantr ⊢ φ ∧ A < s B → C < s D ∨ C = D
44 23 39 43 mpjaodan ⊢ φ ∧ A < s B → A ⋅ s D - s A ⋅ s C ≤ s B ⋅ s D - s B ⋅ s C
45 lesid ⊢ B ⋅ s D - s B ⋅ s C ∈ No → B ⋅ s D - s B ⋅ s C ≤ s B ⋅ s D - s B ⋅ s C
46 13 45 syl ⊢ φ → B ⋅ s D - s B ⋅ s C ≤ s B ⋅ s D - s B ⋅ s C
47 oveq1 ⊢ A = B → A ⋅ s D = B ⋅ s D
48 oveq1 ⊢ A = B → A ⋅ s C = B ⋅ s C
49 47 48 oveq12d ⊢ A = B → A ⋅ s D - s A ⋅ s C = B ⋅ s D - s B ⋅ s C
50 49 breq1d ⊢ A = B → A ⋅ s D - s A ⋅ s C ≤ s B ⋅ s D - s B ⋅ s C ↔ B ⋅ s D - s B ⋅ s C ≤ s B ⋅ s D - s B ⋅ s C
51 46 50 syl5ibrcom ⊢ φ → A = B → A ⋅ s D - s A ⋅ s C ≤ s B ⋅ s D - s B ⋅ s C
52 51 imp ⊢ φ ∧ A = B → A ⋅ s D - s A ⋅ s C ≤ s B ⋅ s D - s B ⋅ s C
53 lesloe ⊢ A ∈ No ∧ B ∈ No → A ≤ s B ↔ A < s B ∨ A = B
54 1 2 53 syl2anc ⊢ φ → A ≤ s B ↔ A < s B ∨ A = B
55 5 54 mpbid ⊢ φ → A < s B ∨ A = B
56 44 52 55 mpjaodan ⊢ φ → A ⋅ s D - s A ⋅ s C ≤ s B ⋅ s D - s B ⋅ s C