Theorem sltmul2

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

	Ref	Expression
Assertion	sltmul2	Could not format assertion : No typesetting found for |- ( ( ( A e. No /\ 0s ( B ( A x.s B )

Proof

Step	Hyp	Ref	Expression
1		simpl1l	Could not format ( ( ( ( A e. No /\ 0s A e. No ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s A e. No ) with typecode |-
2		simpl3	Could not format ( ( ( ( A e. No /\ 0s C e. No ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s C e. No ) with typecode |-
3		simpl2	Could not format ( ( ( ( A e. No /\ 0s B e. No ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s B e. No ) with typecode |-
4	2 3	subscld	Could not format ( ( ( ( A e. No /\ 0s ( C -s B ) e. No ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s ( C -s B ) e. No ) with typecode |-
5		simpl1r	Could not format ( ( ( ( A e. No /\ 0s 0s 0s
6		simp2	Could not format ( ( ( A e. No /\ 0s B e. No ) : No typesetting found for |- ( ( ( A e. No /\ 0s B e. No ) with typecode |-
7		simp3	Could not format ( ( ( A e. No /\ 0s C e. No ) : No typesetting found for |- ( ( ( A e. No /\ 0s C e. No ) with typecode |-
8	6 7	posdifsd	Could not format ( ( ( A e. No /\ 0s ( B 0s ( B 0s
9	8	biimpa	Could not format ( ( ( ( A e. No /\ 0s 0s 0s
10	1 4 5 9	mulsgt0d	Could not format ( ( ( ( A e. No /\ 0s 0s 0s
11	1 2 3	subsdid	Could not format ( ( ( ( A e. No /\ 0s ( A x.s ( C -s B ) ) = ( ( A x.s C ) -s ( A x.s B ) ) ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s ( A x.s ( C -s B ) ) = ( ( A x.s C ) -s ( A x.s B ) ) ) with typecode |-
12	10 11	breqtrd	Could not format ( ( ( ( A e. No /\ 0s 0s 0s
13	1 3	mulscld	Could not format ( ( ( ( A e. No /\ 0s ( A x.s B ) e. No ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s ( A x.s B ) e. No ) with typecode |-
14	1 2	mulscld	Could not format ( ( ( ( A e. No /\ 0s ( A x.s C ) e. No ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s ( A x.s C ) e. No ) with typecode |-
15	13 14	posdifsd	Could not format ( ( ( ( A e. No /\ 0s ( ( A x.s B ) 0s ( ( A x.s B ) 0s
16	12 15	mpbird	Could not format ( ( ( ( A e. No /\ 0s ( A x.s B ) ( A x.s B )
17		simp1l	Could not format ( ( ( A e. No /\ 0s A e. No ) : No typesetting found for |- ( ( ( A e. No /\ 0s A e. No ) with typecode |-
18	17 7	mulscld	Could not format ( ( ( A e. No /\ 0s ( A x.s C ) e. No ) : No typesetting found for |- ( ( ( A e. No /\ 0s ( A x.s C ) e. No ) with typecode |-
19		sltirr	Could not format ( ( A x.s C ) e. No -> -. ( A x.s C ) -. ( A x.s C )
20	18 19	syl	Could not format ( ( ( A e. No /\ 0s -. ( A x.s C ) -. ( A x.s C )
21		oveq2	Could not format ( B = C -> ( A x.s B ) = ( A x.s C ) ) : No typesetting found for |- ( B = C -> ( A x.s B ) = ( A x.s C ) ) with typecode |-
22	21	breq1d	Could not format ( B = C -> ( ( A x.s B ) ( A x.s C ) ( ( A x.s B ) ( A x.s C )
23	22	notbid	Could not format ( B = C -> ( -. ( A x.s B ) -. ( A x.s C ) ( -. ( A x.s B ) -. ( A x.s C )
24	20 23	syl5ibrcom	Could not format ( ( ( A e. No /\ 0s ( B = C -> -. ( A x.s B ) ( B = C -> -. ( A x.s B )
25	24	con2d	Could not format ( ( ( A e. No /\ 0s ( ( A x.s B ) -. B = C ) ) : No typesetting found for |- ( ( ( A e. No /\ 0s ( ( A x.s B ) -. B = C ) ) with typecode |-
26	25	imp	Could not format ( ( ( ( A e. No /\ 0s -. B = C ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s -. B = C ) with typecode |-
27	17 6	mulscld	Could not format ( ( ( A e. No /\ 0s ( A x.s B ) e. No ) : No typesetting found for |- ( ( ( A e. No /\ 0s ( A x.s B ) e. No ) with typecode |-
28		sltasym	Could not format ( ( ( A x.s B ) e. No /\ ( A x.s C ) e. No ) -> ( ( A x.s B ) -. ( A x.s C ) ( ( A x.s B ) -. ( A x.s C )
29	27 18 28	syl2anc	Could not format ( ( ( A e. No /\ 0s ( ( A x.s B ) -. ( A x.s C ) ( ( A x.s B ) -. ( A x.s C )
30	29	imp	Could not format ( ( ( ( A e. No /\ 0s -. ( A x.s C ) -. ( A x.s C )
31		simpl1l	Could not format ( ( ( ( A e. No /\ 0s A e. No ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s A e. No ) with typecode |-
32	31	adantr	Could not format ( ( ( ( ( A e. No /\ 0s A e. No ) : No typesetting found for |- ( ( ( ( ( A e. No /\ 0s A e. No ) with typecode |-
33		simpll2	Could not format ( ( ( ( ( A e. No /\ 0s B e. No ) : No typesetting found for |- ( ( ( ( ( A e. No /\ 0s B e. No ) with typecode |-
34		simpll3	Could not format ( ( ( ( ( A e. No /\ 0s C e. No ) : No typesetting found for |- ( ( ( ( ( A e. No /\ 0s C e. No ) with typecode |-
35	33 34	subscld	Could not format ( ( ( ( ( A e. No /\ 0s ( B -s C ) e. No ) : No typesetting found for |- ( ( ( ( ( A e. No /\ 0s ( B -s C ) e. No ) with typecode |-
36		simpl1r	Could not format ( ( ( ( A e. No /\ 0s 0s 0s
37	36	adantr	Could not format ( ( ( ( ( A e. No /\ 0s 0s 0s
38		simpr	Could not format ( ( ( ( ( A e. No /\ 0s 0s 0s
39	32 35 37 38	mulsgt0d	Could not format ( ( ( ( ( A e. No /\ 0s 0s 0s
40	32 33 34	subsdid	Could not format ( ( ( ( ( A e. No /\ 0s ( A x.s ( B -s C ) ) = ( ( A x.s B ) -s ( A x.s C ) ) ) : No typesetting found for |- ( ( ( ( ( A e. No /\ 0s ( A x.s ( B -s C ) ) = ( ( A x.s B ) -s ( A x.s C ) ) ) with typecode |-
41	40	breq2d	Could not format ( ( ( ( ( A e. No /\ 0s ( 0s 0s ( 0s 0s
42	18	ad2antrr	Could not format ( ( ( ( ( A e. No /\ 0s ( A x.s C ) e. No ) : No typesetting found for |- ( ( ( ( ( A e. No /\ 0s ( A x.s C ) e. No ) with typecode |-
43	27	ad2antrr	Could not format ( ( ( ( ( A e. No /\ 0s ( A x.s B ) e. No ) : No typesetting found for |- ( ( ( ( ( A e. No /\ 0s ( A x.s B ) e. No ) with typecode |-
44	42 43	posdifsd	Could not format ( ( ( ( ( A e. No /\ 0s ( ( A x.s C ) 0s ( ( A x.s C ) 0s
45	41 44	bitr4d	Could not format ( ( ( ( ( A e. No /\ 0s ( 0s ( A x.s C ) ( 0s ( A x.s C )
46	39 45	mpbid	Could not format ( ( ( ( ( A e. No /\ 0s ( A x.s C ) ( A x.s C )
47	30 46	mtand	Could not format ( ( ( ( A e. No /\ 0s -. 0s -. 0s
48		simpl3	Could not format ( ( ( ( A e. No /\ 0s C e. No ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s C e. No ) with typecode |-
49		simpl2	Could not format ( ( ( ( A e. No /\ 0s B e. No ) : No typesetting found for |- ( ( ( ( A e. No /\ 0s B e. No ) with typecode |-
50	48 49	posdifsd	Could not format ( ( ( ( A e. No /\ 0s ( C 0s ( C 0s
51	47 50	mtbird	Could not format ( ( ( ( A e. No /\ 0s -. C -. C
52		sltlin	$$⊢\left(B\in \mathrm{No}\wedge C\in \mathrm{No}\right)\to \left(B{<}_{s}C\vee B=C\vee C{<}_{s}B\right)$$
53	49 48 52	syl2anc	Could not format ( ( ( ( A e. No /\ 0s ( B ( B
54	26 51 53	ecase23d	Could not format ( ( ( ( A e. No /\ 0s B B
55	16 54	impbida	Could not format ( ( ( A e. No /\ 0s ( B ( A x.s B ) ( B ( A x.s B )