Metamath Proof Explorer


Theorem slemuld

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 slemuld.1 φ A No
slemuld.2 φ B No
slemuld.3 φ C No
slemuld.4 φ D No
slemuld.5 φ A s B
slemuld.6 φ C s D
Assertion slemuld φ A s D - s A s C s B s D - s B s C

Proof

Step Hyp Ref Expression
1 slemuld.1 φ A No
2 slemuld.2 φ B No
3 slemuld.3 φ C No
4 slemuld.4 φ D No
5 slemuld.5 φ A s B
6 slemuld.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 sltmuld φ 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 sltled φ 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 0sno 0 s No
25 slerflex 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 sleloe 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 slerflex 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 sleloe 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