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	⊢ ( ( ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( 𝐵 <s 𝐶 ↔ ( 𝐴 ·s 𝐵 ) <s ( 𝐴 ·s 𝐶 ) ) )

Proof

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