Metamath Proof Explorer

Theorem ltmuls2

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

Ref Expression
Assertion ltmuls2 ( ( ( 𝐴 ∈ 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 ltsirr ⊢ ( ( 𝐴 ·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 ltsasym ⊢ ( ( ( 𝐴 ·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 ltslin ⊢ ( ( 𝐵 ∈ 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 𝐶 ) ) )