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	|- ( ( ( A e. No /\ 0s ( B ( A x.s B )

Proof

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