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	$$⊢\phi \to A\in \mathrm{No}$$
	slemuld.2	$$⊢\phi \to B\in \mathrm{No}$$
	slemuld.3	$$⊢\phi \to C\in \mathrm{No}$$
	slemuld.4	$$⊢\phi \to D\in \mathrm{No}$$
	slemuld.5	$$⊢\phi \to A{\le }_{s}B$$
	slemuld.6	$$⊢\phi \to C{\le }_{s}D$$
Assertion	slemuld	Could not format assertion : No typesetting found for |- ( ph -> ( ( A x.s D ) -s ( A x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		slemuld.1	$$⊢\phi \to A\in \mathrm{No}$$
2		slemuld.2	$$⊢\phi \to B\in \mathrm{No}$$
3		slemuld.3	$$⊢\phi \to C\in \mathrm{No}$$
4		slemuld.4	$$⊢\phi \to D\in \mathrm{No}$$
5		slemuld.5	$$⊢\phi \to A{\le }_{s}B$$
6		slemuld.6	$$⊢\phi \to C{\le }_{s}D$$
7	1 4	mulscld	Could not format ( ph -> ( A x.s D ) e. No ) : No typesetting found for |- ( ph -> ( A x.s D ) e. No ) with typecode |-
8	1 3	mulscld	Could not format ( ph -> ( A x.s C ) e. No ) : No typesetting found for |- ( ph -> ( A x.s C ) e. No ) with typecode |-
9	7 8	subscld	Could not format ( ph -> ( ( A x.s D ) -s ( A x.s C ) ) e. No ) : No typesetting found for |- ( ph -> ( ( A x.s D ) -s ( A x.s C ) ) e. No ) with typecode |-
10	9	adantr	Could not format ( ( ph /\ ( A ( ( A x.s D ) -s ( A x.s C ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( A ( ( A x.s D ) -s ( A x.s C ) ) e. No ) with typecode |-
11	2 4	mulscld	Could not format ( ph -> ( B x.s D ) e. No ) : No typesetting found for |- ( ph -> ( B x.s D ) e. No ) with typecode |-
12	2 3	mulscld	Could not format ( ph -> ( B x.s C ) e. No ) : No typesetting found for |- ( ph -> ( B x.s C ) e. No ) with typecode |-
13	11 12	subscld	Could not format ( ph -> ( ( B x.s D ) -s ( B x.s C ) ) e. No ) : No typesetting found for |- ( ph -> ( ( B x.s D ) -s ( B x.s C ) ) e. No ) with typecode |-
14	13	adantr	Could not format ( ( ph /\ ( A ( ( B x.s D ) -s ( B x.s C ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( A ( ( B x.s D ) -s ( B x.s C ) ) e. No ) with typecode |-
15	1	adantr	$$⊢\left(\phi \wedge \left(A{<}_{s}B\wedge C{<}_{s}D\right)\right)\to A\in \mathrm{No}$$
16	2	adantr	$$⊢\left(\phi \wedge \left(A{<}_{s}B\wedge C{<}_{s}D\right)\right)\to B\in \mathrm{No}$$
17	3	adantr	$$⊢\left(\phi \wedge \left(A{<}_{s}B\wedge C{<}_{s}D\right)\right)\to C\in \mathrm{No}$$
18	4	adantr	$$⊢\left(\phi \wedge \left(A{<}_{s}B\wedge C{<}_{s}D\right)\right)\to D\in \mathrm{No}$$
19		simprl	$$⊢\left(\phi \wedge \left(A{<}_{s}B\wedge C{<}_{s}D\right)\right)\to A{<}_{s}B$$
20		simprr	$$⊢\left(\phi \wedge \left(A{<}_{s}B\wedge C{<}_{s}D\right)\right)\to C{<}_{s}D$$
21	15 16 17 18 19 20	sltmuld	Could not format ( ( ph /\ ( A ( ( A x.s D ) -s ( A x.s C ) ) ( ( A x.s D ) -s ( A x.s C ) )
22	10 14 21	sltled	Could not format ( ( ph /\ ( A ( ( A x.s D ) -s ( A x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) ) : No typesetting found for |- ( ( ph /\ ( A ( ( A x.s D ) -s ( A x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) ) with typecode |-
23	22	anassrs	Could not format ( ( ( ph /\ A ( ( A x.s D ) -s ( A x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) ) : No typesetting found for |- ( ( ( ph /\ A ( ( A x.s D ) -s ( A x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) ) with typecode |-
24		0sno	Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |-
25		slerflex	Could not format ( 0s e. No -> 0s <_s 0s ) : No typesetting found for |- ( 0s e. No -> 0s <_s 0s ) with typecode |-
26	24 25	mp1i	Could not format ( ph -> 0s <_s 0s ) : No typesetting found for |- ( ph -> 0s <_s 0s ) with typecode |-
27		subsid	Could not format ( ( A x.s D ) e. No -> ( ( A x.s D ) -s ( A x.s D ) ) = 0s ) : No typesetting found for |- ( ( A x.s D ) e. No -> ( ( A x.s D ) -s ( A x.s D ) ) = 0s ) with typecode |-
28	7 27	syl	Could not format ( ph -> ( ( A x.s D ) -s ( A x.s D ) ) = 0s ) : No typesetting found for |- ( ph -> ( ( A x.s D ) -s ( A x.s D ) ) = 0s ) with typecode |-
29		subsid	Could not format ( ( B x.s D ) e. No -> ( ( B x.s D ) -s ( B x.s D ) ) = 0s ) : No typesetting found for |- ( ( B x.s D ) e. No -> ( ( B x.s D ) -s ( B x.s D ) ) = 0s ) with typecode |-
30	11 29	syl	Could not format ( ph -> ( ( B x.s D ) -s ( B x.s D ) ) = 0s ) : No typesetting found for |- ( ph -> ( ( B x.s D ) -s ( B x.s D ) ) = 0s ) with typecode |-
31	26 28 30	3brtr4d	Could not format ( ph -> ( ( A x.s D ) -s ( A x.s D ) ) <_s ( ( B x.s D ) -s ( B x.s D ) ) ) : No typesetting found for |- ( ph -> ( ( A x.s D ) -s ( A x.s D ) ) <_s ( ( B x.s D ) -s ( B x.s D ) ) ) with typecode |-
32		oveq2	Could not format ( C = D -> ( A x.s C ) = ( A x.s D ) ) : No typesetting found for |- ( C = D -> ( A x.s C ) = ( A x.s D ) ) with typecode |-
33	32	oveq2d	Could not format ( C = D -> ( ( A x.s D ) -s ( A x.s C ) ) = ( ( A x.s D ) -s ( A x.s D ) ) ) : No typesetting found for |- ( C = D -> ( ( A x.s D ) -s ( A x.s C ) ) = ( ( A x.s D ) -s ( A x.s D ) ) ) with typecode |-
34		oveq2	Could not format ( C = D -> ( B x.s C ) = ( B x.s D ) ) : No typesetting found for |- ( C = D -> ( B x.s C ) = ( B x.s D ) ) with typecode |-
35	34	oveq2d	Could not format ( C = D -> ( ( B x.s D ) -s ( B x.s C ) ) = ( ( B x.s D ) -s ( B x.s D ) ) ) : No typesetting found for |- ( C = D -> ( ( B x.s D ) -s ( B x.s C ) ) = ( ( B x.s D ) -s ( B x.s D ) ) ) with typecode |-
36	33 35	breq12d	Could not format ( C = D -> ( ( ( A x.s D ) -s ( A x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) <-> ( ( A x.s D ) -s ( A x.s D ) ) <_s ( ( B x.s D ) -s ( B x.s D ) ) ) ) : No typesetting found for |- ( C = D -> ( ( ( A x.s D ) -s ( A x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) <-> ( ( A x.s D ) -s ( A x.s D ) ) <_s ( ( B x.s D ) -s ( B x.s D ) ) ) ) with typecode |-
37	31 36	syl5ibrcom	Could not format ( ph -> ( C = D -> ( ( A x.s D ) -s ( A x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) ) ) : No typesetting found for |- ( ph -> ( C = D -> ( ( A x.s D ) -s ( A x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) ) ) with typecode |-
38	37	imp	Could not format ( ( ph /\ C = D ) -> ( ( A x.s D ) -s ( A x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) ) : No typesetting found for |- ( ( ph /\ C = D ) -> ( ( A x.s D ) -s ( A x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) ) with typecode |-
39	38	adantlr	Could not format ( ( ( ph /\ A ( ( A x.s D ) -s ( A x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) ) : No typesetting found for |- ( ( ( ph /\ A ( ( A x.s D ) -s ( A x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) ) with typecode |-
40		sleloe	$$⊢\left(C\in \mathrm{No}\wedge D\in \mathrm{No}\right)\to \left(C{\le }_{s}D\leftrightarrow \left(C{<}_{s}D\vee C=D\right)\right)$$
41	3 4 40	syl2anc	$$⊢\phi \to \left(C{\le }_{s}D\leftrightarrow \left(C{<}_{s}D\vee C=D\right)\right)$$
42	6 41	mpbid	$$⊢\phi \to \left(C{<}_{s}D\vee C=D\right)$$
43	42	adantr	$$⊢\left(\phi \wedge A{<}_{s}B\right)\to \left(C{<}_{s}D\vee C=D\right)$$
44	23 39 43	mpjaodan	Could not format ( ( ph /\ A ( ( A x.s D ) -s ( A x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) ) : No typesetting found for |- ( ( ph /\ A ( ( A x.s D ) -s ( A x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) ) with typecode |-
45		slerflex	Could not format ( ( ( B x.s D ) -s ( B x.s C ) ) e. No -> ( ( B x.s D ) -s ( B x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) ) : No typesetting found for |- ( ( ( B x.s D ) -s ( B x.s C ) ) e. No -> ( ( B x.s D ) -s ( B x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) ) with typecode |-
46	13 45	syl	Could not format ( ph -> ( ( B x.s D ) -s ( B x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) ) : No typesetting found for |- ( ph -> ( ( B x.s D ) -s ( B x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) ) with typecode |-
47		oveq1	Could not format ( A = B -> ( A x.s D ) = ( B x.s D ) ) : No typesetting found for |- ( A = B -> ( A x.s D ) = ( B x.s D ) ) with typecode |-
48		oveq1	Could not format ( A = B -> ( A x.s C ) = ( B x.s C ) ) : No typesetting found for |- ( A = B -> ( A x.s C ) = ( B x.s C ) ) with typecode |-
49	47 48	oveq12d	Could not format ( A = B -> ( ( A x.s D ) -s ( A x.s C ) ) = ( ( B x.s D ) -s ( B x.s C ) ) ) : No typesetting found for |- ( A = B -> ( ( A x.s D ) -s ( A x.s C ) ) = ( ( B x.s D ) -s ( B x.s C ) ) ) with typecode |-
50	49	breq1d	Could not format ( A = B -> ( ( ( A x.s D ) -s ( A x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) <-> ( ( B x.s D ) -s ( B x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) ) ) : No typesetting found for |- ( A = B -> ( ( ( A x.s D ) -s ( A x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) <-> ( ( B x.s D ) -s ( B x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) ) ) with typecode |-
51	46 50	syl5ibrcom	Could not format ( ph -> ( A = B -> ( ( A x.s D ) -s ( A x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) ) ) : No typesetting found for |- ( ph -> ( A = B -> ( ( A x.s D ) -s ( A x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) ) ) with typecode |-
52	51	imp	Could not format ( ( ph /\ A = B ) -> ( ( A x.s D ) -s ( A x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) ) : No typesetting found for |- ( ( ph /\ A = B ) -> ( ( A x.s D ) -s ( A x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) ) with typecode |-
53		sleloe	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(A{\le }_{s}B\leftrightarrow \left(A{<}_{s}B\vee A=B\right)\right)$$
54	1 2 53	syl2anc	$$⊢\phi \to \left(A{\le }_{s}B\leftrightarrow \left(A{<}_{s}B\vee A=B\right)\right)$$
55	5 54	mpbid	$$⊢\phi \to \left(A{<}_{s}B\vee A=B\right)$$
56	44 52 55	mpjaodan	Could not format ( ph -> ( ( A x.s D ) -s ( A x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) ) : No typesetting found for |- ( ph -> ( ( A x.s D ) -s ( A x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) ) with typecode |-