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 ⊢ ( 𝜑 → 𝐴 ∈ No )
lemulsd.2 ⊢ ( 𝜑 → 𝐵 ∈ No )
lemulsd.3 ⊢ ( 𝜑 → 𝐶 ∈ No )
lemulsd.4 ⊢ ( 𝜑 → 𝐷 ∈ No )
lemulsd.5 ⊢ ( 𝜑 → 𝐴 ≤s 𝐵 )
lemulsd.6 ⊢ ( 𝜑 → 𝐶 ≤s 𝐷 )
Assertion lemulsd ( 𝜑 → ( ( 𝐴 ·s 𝐷 ) -s ( 𝐴 ·s 𝐶 ) ) ≤s ( ( 𝐵 ·s 𝐷 ) -s ( 𝐵 ·s 𝐶 ) ) )

Proof

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