P. 281 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28001-28100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	posdifsd 28001	Comparison of two surreals whose difference is positive. (Contributed by Scott Fenton, 10-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ 0s <s (𝐵 -s 𝐴)))
Theorem	sltsubposd 28002	Subtraction of a positive number decreases the sum. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → ( 0s <s 𝐴 ↔ (𝐵 -s 𝐴) <s 𝐵))
Theorem	subsge0d 28003	Non-negative subtraction. (Contributed by Scott Fenton, 26-May-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → ( 0s ≤s (𝐴 -s 𝐵) ↔ 𝐵 ≤s 𝐴))
Theorem	addsubs4d 28004	Rearrangement of four terms in mixed addition and subtraction. Surreal version. (Contributed by Scott Fenton, 25-Jul-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐷 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 +s 𝐵) -s (𝐶 +s 𝐷)) = ((𝐴 -s 𝐶) +s (𝐵 -s 𝐷)))
Theorem	sltm1d 28005	A surreal is greater than itself minus one. (Contributed by Scott Fenton, 20-Aug-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 -s 1s ) <s 𝐴)
Theorem	subscan1d 28006	Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐶 -s 𝐴) = (𝐶 -s 𝐵) ↔ 𝐴 = 𝐵))
Theorem	subscan2d 28007	Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 -s 𝐶) = (𝐵 -s 𝐶) ↔ 𝐴 = 𝐵))
Theorem	subseq0d 28008	The difference between two surreals is zero iff they are equal. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 -s 𝐵) = 0s ↔ 𝐴 = 𝐵))
15.5.3  Multiplication
Syntax	cmuls 28009	Set up the syntax for surreal multiplication.
class ·s
Definition	df-muls 28010*	Define surreal multiplication. Definition from [Conway] p. 5. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ·s = norec2 ((𝑧 ∈ V, 𝑚 ∈ V ↦ ⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd ‘𝑧) / 𝑦⦌(({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝑥)∃𝑞 ∈ ( L ‘𝑦)𝑎 = (((𝑝𝑚𝑦) +s (𝑥𝑚𝑞)) -s (𝑝𝑚𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ ( R ‘𝑥)∃𝑠 ∈ ( R ‘𝑦)𝑏 = (((𝑟𝑚𝑦) +s (𝑥𝑚𝑠)) -s (𝑟𝑚𝑠))}) |s ({𝑐 ∣ ∃𝑡 ∈ ( L ‘𝑥)∃𝑢 ∈ ( R ‘𝑦)𝑐 = (((𝑡𝑚𝑦) +s (𝑥𝑚𝑢)) -s (𝑡𝑚𝑢))} ∪ {𝑑 ∣ ∃𝑣 ∈ ( R ‘𝑥)∃𝑤 ∈ ( L ‘𝑦)𝑑 = (((𝑣𝑚𝑦) +s (𝑥𝑚𝑤)) -s (𝑣𝑚𝑤))}))))
Theorem	mulsfn 28011	Surreal multiplication is a function over surreals. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ·s Fn ( No × No )
Theorem	mulsval 28012*	The value of surreal multiplication. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 ·s 𝐵) = (({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)∃𝑞 ∈ ( L ‘𝐵)𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ ( R ‘𝐴)∃𝑠 ∈ ( R ‘𝐵)𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) |s ({𝑐 ∣ ∃𝑡 ∈ ( L ‘𝐴)∃𝑢 ∈ ( R ‘𝐵)𝑐 = (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑑 ∣ ∃𝑣 ∈ ( R ‘𝐴)∃𝑤 ∈ ( L ‘𝐵)𝑑 = (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤))})))
Theorem	mulsval2lem 28013*	Lemma for mulsval2 28014. Change bound variables in one of the cases. (Contributed by Scott Fenton, 8-Mar-2025.)
⊢ {𝑎 ∣ ∃𝑝 ∈ 𝑋 ∃𝑞 ∈ 𝑌 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} = {𝑏 ∣ ∃𝑟 ∈ 𝑋 ∃𝑠 ∈ 𝑌 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}
Theorem	mulsval2 28014*	The value of surreal multiplication, expressed with fewer distinct variable conditions. (Contributed by Scott Fenton, 8-Mar-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 ·s 𝐵) = (({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)∃𝑞 ∈ ( L ‘𝐵)𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ ( R ‘𝐴)∃𝑠 ∈ ( R ‘𝐵)𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) |s ({𝑐 ∣ ∃𝑡 ∈ ( L ‘𝐴)∃𝑢 ∈ ( R ‘𝐵)𝑐 = (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑑 ∣ ∃𝑣 ∈ ( R ‘𝐴)∃𝑤 ∈ ( L ‘𝐵)𝑑 = (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤))})))
Theorem	muls01 28015	Surreal multiplication by zero. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ (𝐴 ∈ No → (𝐴 ·s 0s ) = 0s )
Theorem	mulsrid 28016	Surreal one is a right identity element for multiplication. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ (𝐴 ∈ No → (𝐴 ·s 1s ) = 𝐴)
Theorem	mulsridd 28017	Surreal one is a right identity element for multiplication. (Contributed by Scott Fenton, 14-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 ·s 1s ) = 𝐴)
Theorem	mulsproplemcbv 28018*	Lemma for surreal multiplication. Change some bound variables for later use. (Contributed by Scott Fenton, 5-Mar-2025.)
⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))    ⇒   ⊢ (𝜑 → ∀𝑔 ∈ No ∀ℎ ∈ No ∀𝑖 ∈ No ∀𝑗 ∈ No ∀𝑘 ∈ No ∀𝑙 ∈ No (((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))))
Theorem	mulsproplem1 28019*	Lemma for surreal multiplication. Instantiate some variables. (Contributed by Scott Fenton, 4-Mar-2025.)
⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))    &   ⊢ (𝜑 → 𝑋 ∈ No )    &   ⊢ (𝜑 → 𝑌 ∈ No )    &   ⊢ (𝜑 → 𝑍 ∈ No )    &   ⊢ (𝜑 → 𝑊 ∈ No )    &   ⊢ (𝜑 → 𝑇 ∈ No )    &   ⊢ (𝜑 → 𝑈 ∈ No )    &   ⊢ (𝜑 → ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (((( bday ‘𝑍) +no ( bday ‘𝑇)) ∪ (( bday ‘𝑊) +no ( bday ‘𝑈))) ∪ ((( bday ‘𝑍) +no ( bday ‘𝑈)) ∪ (( bday ‘𝑊) +no ( bday ‘𝑇))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))))    ⇒   ⊢ (𝜑 → ((𝑋 ·s 𝑌) ∈ No ∧ ((𝑍 <s 𝑊 ∧ 𝑇 <s 𝑈) → ((𝑍 ·s 𝑈) -s (𝑍 ·s 𝑇)) <s ((𝑊 ·s 𝑈) -s (𝑊 ·s 𝑇)))))
Theorem	mulsproplem2 28020*	Lemma for surreal multiplication. Under the inductive hypothesis, the product of a member of the old set of 𝐴 and 𝐵 itself is a surreal number. (Contributed by Scott Fenton, 4-Mar-2025.)
⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))    &   ⊢ (𝜑 → 𝑋 ∈ ( O ‘( bday ‘𝐴)))    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → (𝑋 ·s 𝐵) ∈ No )
Theorem	mulsproplem3 28021*	Lemma for surreal multiplication. Under the inductive hypothesis, the product of 𝐴 itself and a member of the old set of 𝐵 is a surreal number. (Contributed by Scott Fenton, 4-Mar-2025.)
⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝑌 ∈ ( O ‘( bday ‘𝐵)))    ⇒   ⊢ (𝜑 → (𝐴 ·s 𝑌) ∈ No )
Theorem	mulsproplem4 28022*	Lemma for surreal multiplication. Under the inductive hypothesis, the product of a member of the old set of 𝐴 and a member of the old set of 𝐵 is a surreal number. (Contributed by Scott Fenton, 4-Mar-2025.)
⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))    &   ⊢ (𝜑 → 𝑋 ∈ ( O ‘( bday ‘𝐴)))    &   ⊢ (𝜑 → 𝑌 ∈ ( O ‘( bday ‘𝐵)))    ⇒   ⊢ (𝜑 → (𝑋 ·s 𝑌) ∈ No )
Theorem	mulsproplem5 28023*	Lemma for surreal multiplication. Show one of the inequalities involved in surreal multiplication's cuts. (Contributed by Scott Fenton, 4-Mar-2025.)
⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝑃 ∈ ( L ‘𝐴))    &   ⊢ (𝜑 → 𝑄 ∈ ( L ‘𝐵))    &   ⊢ (𝜑 → 𝑇 ∈ ( L ‘𝐴))    &   ⊢ (𝜑 → 𝑈 ∈ ( R ‘𝐵))    ⇒   ⊢ (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)))
Theorem	mulsproplem6 28024*	Lemma for surreal multiplication. Show one of the inequalities involved in surreal multiplication's cuts. (Contributed by Scott Fenton, 5-Mar-2025.)
⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝑃 ∈ ( L ‘𝐴))    &   ⊢ (𝜑 → 𝑄 ∈ ( L ‘𝐵))    &   ⊢ (𝜑 → 𝑉 ∈ ( R ‘𝐴))    &   ⊢ (𝜑 → 𝑊 ∈ ( L ‘𝐵))    ⇒   ⊢ (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊)))
Theorem	mulsproplem7 28025*	Lemma for surreal multiplication. Show one of the inequalities involved in surreal multiplication's cuts. (Contributed by Scott Fenton, 5-Mar-2025.)
⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝑅 ∈ ( R ‘𝐴))    &   ⊢ (𝜑 → 𝑆 ∈ ( R ‘𝐵))    &   ⊢ (𝜑 → 𝑇 ∈ ( L ‘𝐴))    &   ⊢ (𝜑 → 𝑈 ∈ ( R ‘𝐵))    ⇒   ⊢ (𝜑 → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)))
Theorem	mulsproplem8 28026*	Lemma for surreal multiplication. Show one of the inequalities involved in surreal multiplication's cuts. (Contributed by Scott Fenton, 5-Mar-2025.)
⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝑅 ∈ ( R ‘𝐴))    &   ⊢ (𝜑 → 𝑆 ∈ ( R ‘𝐵))    &   ⊢ (𝜑 → 𝑉 ∈ ( R ‘𝐴))    &   ⊢ (𝜑 → 𝑊 ∈ ( L ‘𝐵))    ⇒   ⊢ (𝜑 → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊)))
Theorem	mulsproplem9 28027*	Lemma for surreal multiplication. Show that the cut involved in surreal multiplication makes sense. (Contributed by Scott Fenton, 5-Mar-2025.)
⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → ({𝑔 ∣ ∃𝑝 ∈ ( L ‘𝐴)∃𝑞 ∈ ( L ‘𝐵)𝑔 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {ℎ ∣ ∃𝑟 ∈ ( R ‘𝐴)∃𝑠 ∈ ( R ‘𝐵)ℎ = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) <<s ({𝑖 ∣ ∃𝑡 ∈ ( L ‘𝐴)∃𝑢 ∈ ( R ‘𝐵)𝑖 = (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ ( R ‘𝐴)∃𝑤 ∈ ( L ‘𝐵)𝑗 = (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤))}))
Theorem	mulsproplem10 28028*	Lemma for surreal multiplication. State the cut properties of surreal multiplication. (Contributed by Scott Fenton, 5-Mar-2025.)
⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 ·s 𝐵) ∈ No ∧ ({𝑔 ∣ ∃𝑝 ∈ ( L ‘𝐴)∃𝑞 ∈ ( L ‘𝐵)𝑔 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {ℎ ∣ ∃𝑟 ∈ ( R ‘𝐴)∃𝑠 ∈ ( R ‘𝐵)ℎ = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) <<s {(𝐴 ·s 𝐵)} ∧ {(𝐴 ·s 𝐵)} <<s ({𝑖 ∣ ∃𝑡 ∈ ( L ‘𝐴)∃𝑢 ∈ ( R ‘𝐵)𝑖 = (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ ( R ‘𝐴)∃𝑤 ∈ ( L ‘𝐵)𝑗 = (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤))})))
Theorem	mulsproplem11 28029*	Lemma for surreal multiplication. Under the inductive hypothesis, demonstrate closure of surreal multiplication. (Contributed by Scott Fenton, 5-Mar-2025.)
⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 ·s 𝐵) ∈ No )
Theorem	mulsproplem12 28030*	Lemma for surreal multiplication. Demonstrate the second half of the inductive statement assuming 𝐶 and 𝐷 are not the same age and 𝐸 and 𝐹 are not the same age. (Contributed by Scott Fenton, 5-Mar-2025.)
⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐷 ∈ No )    &   ⊢ (𝜑 → 𝐸 ∈ No )    &   ⊢ (𝜑 → 𝐹 ∈ No )    &   ⊢ (𝜑 → 𝐶 <s 𝐷)    &   ⊢ (𝜑 → 𝐸 <s 𝐹)    &   ⊢ (𝜑 → (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∨ ( bday ‘𝐷) ∈ ( bday ‘𝐶)))    &   ⊢ (𝜑 → (( bday ‘𝐸) ∈ ( bday ‘𝐹) ∨ ( bday ‘𝐹) ∈ ( bday ‘𝐸)))    ⇒   ⊢ (𝜑 → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
Theorem	mulsproplem13 28031*	Lemma for surreal multiplication. Remove the restriction on 𝐶 and 𝐷 from mulsproplem12 28030. (Contributed by Scott Fenton, 5-Mar-2025.)
⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐷 ∈ No )    &   ⊢ (𝜑 → 𝐸 ∈ No )    &   ⊢ (𝜑 → 𝐹 ∈ No )    &   ⊢ (𝜑 → 𝐶 <s 𝐷)    &   ⊢ (𝜑 → 𝐸 <s 𝐹)    &   ⊢ (𝜑 → (( bday ‘𝐸) ∈ ( bday ‘𝐹) ∨ ( bday ‘𝐹) ∈ ( bday ‘𝐸)))    ⇒   ⊢ (𝜑 → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
Theorem	mulsproplem14 28032*	Lemma for surreal multiplication. Finally, we remove the restriction on 𝐸 and 𝐹 from mulsproplem12 28030 and mulsproplem13 28031. This completes the induction on surreal multiplication. mulsprop 28033 brings all this together technically. (Contributed by Scott Fenton, 5-Mar-2025.)
⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐷 ∈ No )    &   ⊢ (𝜑 → 𝐸 ∈ No )    &   ⊢ (𝜑 → 𝐹 ∈ No )    &   ⊢ (𝜑 → 𝐶 <s 𝐷)    &   ⊢ (𝜑 → 𝐸 <s 𝐹)    ⇒   ⊢ (𝜑 → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
Theorem	mulsprop 28033	Surreals are closed under multiplication and obey a particular ordering law. Theorem 3.4 of [Gonshor] p. 17. (Contributed by Scott Fenton, 5-Mar-2025.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ (𝐶 ∈ No ∧ 𝐷 ∈ No ) ∧ (𝐸 ∈ No ∧ 𝐹 ∈ No )) → ((𝐴 ·s 𝐵) ∈ No ∧ ((𝐶 <s 𝐷 ∧ 𝐸 <s 𝐹) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))))
Theorem	mulscutlem 28034*	Lemma for mulscut 28035. State the theorem with extra DV conditions. (Contributed by Scott Fenton, 7-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 ·s 𝐵) ∈ No ∧ ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)∃𝑞 ∈ ( L ‘𝐵)𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ ( R ‘𝐴)∃𝑠 ∈ ( R ‘𝐵)𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) <<s {(𝐴 ·s 𝐵)} ∧ {(𝐴 ·s 𝐵)} <<s ({𝑐 ∣ ∃𝑡 ∈ ( L ‘𝐴)∃𝑢 ∈ ( R ‘𝐵)𝑐 = (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑑 ∣ ∃𝑣 ∈ ( R ‘𝐴)∃𝑤 ∈ ( L ‘𝐵)𝑑 = (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤))})))
Theorem	mulscut 28035*	Show the cut properties of surreal multiplication. (Contributed by Scott Fenton, 8-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 ·s 𝐵) ∈ No ∧ ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)∃𝑞 ∈ ( L ‘𝐵)𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ ( R ‘𝐴)∃𝑠 ∈ ( R ‘𝐵)𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) <<s {(𝐴 ·s 𝐵)} ∧ {(𝐴 ·s 𝐵)} <<s ({𝑐 ∣ ∃𝑡 ∈ ( L ‘𝐴)∃𝑢 ∈ ( R ‘𝐵)𝑐 = (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑑 ∣ ∃𝑣 ∈ ( R ‘𝐴)∃𝑤 ∈ ( L ‘𝐵)𝑑 = (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤))})))
Theorem	mulscut2 28036*	Show that the cut involved in surreal multiplication is actually a cut. (Contributed by Scott Fenton, 7-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)∃𝑞 ∈ ( L ‘𝐵)𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ ( R ‘𝐴)∃𝑠 ∈ ( R ‘𝐵)𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) <<s ({𝑐 ∣ ∃𝑡 ∈ ( L ‘𝐴)∃𝑢 ∈ ( R ‘𝐵)𝑐 = (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑑 ∣ ∃𝑣 ∈ ( R ‘𝐴)∃𝑤 ∈ ( L ‘𝐵)𝑑 = (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤))}))
Theorem	mulscl 28037	The surreals are closed under multiplication. Theorem 8(i) of [Conway] p. 19. (Contributed by Scott Fenton, 5-Mar-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 ·s 𝐵) ∈ No )
Theorem	mulscld 28038	The surreals are closed under multiplication. Theorem 8(i) of [Conway] p. 19. (Contributed by Scott Fenton, 6-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 ·s 𝐵) ∈ No )
Theorem	sltmul 28039	An ordering relationship for surreal multiplication. Compare theorem 8(iii) of [Conway] p. 19. (Contributed by Scott Fenton, 5-Mar-2025.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ (𝐶 ∈ No ∧ 𝐷 ∈ No )) → ((𝐴 <s 𝐵 ∧ 𝐶 <s 𝐷) → ((𝐴 ·s 𝐷) -s (𝐴 ·s 𝐶)) <s ((𝐵 ·s 𝐷) -s (𝐵 ·s 𝐶))))
Theorem	sltmuld 28040	An ordering relationship for surreal multiplication. Compare theorem 8(iii) of [Conway] p. 19. (Contributed by Scott Fenton, 6-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐷 ∈ No )    &   ⊢ (𝜑 → 𝐴 <s 𝐵)    &   ⊢ (𝜑 → 𝐶 <s 𝐷)    ⇒   ⊢ (𝜑 → ((𝐴 ·s 𝐷) -s (𝐴 ·s 𝐶)) <s ((𝐵 ·s 𝐷) -s (𝐵 ·s 𝐶)))
Theorem	slemuld 28041	An ordering relationship for surreal multiplication. Compare theorem 8(iii) of [Conway] p. 19. (Contributed by Scott Fenton, 7-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐷 ∈ No )    &   ⊢ (𝜑 → 𝐴 ≤s 𝐵)    &   ⊢ (𝜑 → 𝐶 ≤s 𝐷)    ⇒   ⊢ (𝜑 → ((𝐴 ·s 𝐷) -s (𝐴 ·s 𝐶)) ≤s ((𝐵 ·s 𝐷) -s (𝐵 ·s 𝐶)))
Theorem	mulscom 28042	Surreal multiplication commutes. Part of theorem 7 of [Conway] p. 19. (Contributed by Scott Fenton, 6-Mar-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 ·s 𝐵) = (𝐵 ·s 𝐴))
Theorem	mulscomd 28043	Surreal multiplication commutes. Part of theorem 7 of [Conway] p. 19. (Contributed by Scott Fenton, 6-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 ·s 𝐵) = (𝐵 ·s 𝐴))
Theorem	muls02 28044	Surreal multiplication by zero. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ (𝐴 ∈ No → ( 0s ·s 𝐴) = 0s )
Theorem	mulslid 28045	Surreal one is a left identity element for multiplication. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ (𝐴 ∈ No → ( 1s ·s 𝐴) = 𝐴)
Theorem	mulslidd 28046	Surreal one is a left identity element for multiplication. (Contributed by Scott Fenton, 14-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    ⇒   ⊢ (𝜑 → ( 1s ·s 𝐴) = 𝐴)
Theorem	mulsgt0 28047	The product of two positive surreals is positive. Theorem 9 of [Conway] p. 20. (Contributed by Scott Fenton, 6-Mar-2025.)
⊢ (((𝐴 ∈ No ∧ 0s <s 𝐴) ∧ (𝐵 ∈ No ∧ 0s <s 𝐵)) → 0s <s (𝐴 ·s 𝐵))
Theorem	mulsgt0d 28048	The product of two positive surreals is positive. Theorem 9 of [Conway] p. 20. (Contributed by Scott Fenton, 6-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 0s <s 𝐴)    &   ⊢ (𝜑 → 0s <s 𝐵)    ⇒   ⊢ (𝜑 → 0s <s (𝐴 ·s 𝐵))
Theorem	mulsge0d 28049	The product of two non-negative surreals is non-negative. (Contributed by Scott Fenton, 6-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 0s ≤s 𝐴)    &   ⊢ (𝜑 → 0s ≤s 𝐵)    ⇒   ⊢ (𝜑 → 0s ≤s (𝐴 ·s 𝐵))
Theorem	ssltmul1 28050*	One surreal set less-than relationship for cuts of 𝐴 and 𝐵. (Contributed by Scott Fenton, 7-Mar-2025.)
⊢ (𝜑 → 𝐿 <<s 𝑅)    &   ⊢ (𝜑 → 𝑀 <<s 𝑆)    &   ⊢ (𝜑 → 𝐴 = (𝐿 |s 𝑅))    &   ⊢ (𝜑 → 𝐵 = (𝑀 |s 𝑆))    ⇒   ⊢ (𝜑 → ({𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) <<s {(𝐴 ·s 𝐵)})
Theorem	ssltmul2 28051*	One surreal set less-than relationship for cuts of 𝐴 and 𝐵. (Contributed by Scott Fenton, 7-Mar-2025.)
⊢ (𝜑 → 𝐿 <<s 𝑅)    &   ⊢ (𝜑 → 𝑀 <<s 𝑆)    &   ⊢ (𝜑 → 𝐴 = (𝐿 |s 𝑅))    &   ⊢ (𝜑 → 𝐵 = (𝑀 |s 𝑆))    ⇒   ⊢ (𝜑 → {(𝐴 ·s 𝐵)} <<s ({𝑐 ∣ ∃𝑡 ∈ 𝐿 ∃𝑢 ∈ 𝑆 𝑐 = (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑑 ∣ ∃𝑣 ∈ 𝑅 ∃𝑤 ∈ 𝑀 𝑑 = (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤))}))
Theorem	mulsuniflem 28052*	Lemma for mulsunif 28053. State the theorem with some extra distinct variable conditions. (Contributed by Scott Fenton, 8-Mar-2025.)
⊢ (𝜑 → 𝐿 <<s 𝑅)    &   ⊢ (𝜑 → 𝑀 <<s 𝑆)    &   ⊢ (𝜑 → 𝐴 = (𝐿 |s 𝑅))    &   ⊢ (𝜑 → 𝐵 = (𝑀 |s 𝑆))    ⇒   ⊢ (𝜑 → (𝐴 ·s 𝐵) = (({𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) |s ({𝑐 ∣ ∃𝑡 ∈ 𝐿 ∃𝑢 ∈ 𝑆 𝑐 = (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑑 ∣ ∃𝑣 ∈ 𝑅 ∃𝑤 ∈ 𝑀 𝑑 = (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤))})))
Theorem	mulsunif 28053*	Surreal multiplication has the uniformity property. That is, any cuts that define 𝐴 and 𝐵 can be used in the definition of (𝐴 ·s 𝐵). Theorem 3.5 of [Gonshor] p. 18. (Contributed by Scott Fenton, 7-Mar-2025.)
⊢ (𝜑 → 𝐿 <<s 𝑅)    &   ⊢ (𝜑 → 𝑀 <<s 𝑆)    &   ⊢ (𝜑 → 𝐴 = (𝐿 |s 𝑅))    &   ⊢ (𝜑 → 𝐵 = (𝑀 |s 𝑆))    ⇒   ⊢ (𝜑 → (𝐴 ·s 𝐵) = (({𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) |s ({𝑐 ∣ ∃𝑡 ∈ 𝐿 ∃𝑢 ∈ 𝑆 𝑐 = (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑑 ∣ ∃𝑣 ∈ 𝑅 ∃𝑤 ∈ 𝑀 𝑑 = (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤))})))
Theorem	addsdilem1 28054*	Lemma for surreal distribution. Expand the left hand side of the main expression. (Contributed by Scott Fenton, 8-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 ·s (𝐵 +s 𝐶)) = ((({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑎 = (((𝑥𝐿 ·s (𝐵 +s 𝐶)) +s (𝐴 ·s (𝑦𝐿 +s 𝐶))) -s (𝑥𝐿 ·s (𝑦𝐿 +s 𝐶)))} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑥𝐿 ·s (𝐵 +s 𝐶)) +s (𝐴 ·s (𝐵 +s 𝑧𝐿))) -s (𝑥𝐿 ·s (𝐵 +s 𝑧𝐿)))}) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑎 = (((𝑥𝑅 ·s (𝐵 +s 𝐶)) +s (𝐴 ·s (𝑦𝑅 +s 𝐶))) -s (𝑥𝑅 ·s (𝑦𝑅 +s 𝐶)))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑥𝑅 ·s (𝐵 +s 𝐶)) +s (𝐴 ·s (𝐵 +s 𝑧𝑅))) -s (𝑥𝑅 ·s (𝐵 +s 𝑧𝑅)))})) |s (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑎 = (((𝑥𝐿 ·s (𝐵 +s 𝐶)) +s (𝐴 ·s (𝑦𝑅 +s 𝐶))) -s (𝑥𝐿 ·s (𝑦𝑅 +s 𝐶)))} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑥𝐿 ·s (𝐵 +s 𝐶)) +s (𝐴 ·s (𝐵 +s 𝑧𝑅))) -s (𝑥𝐿 ·s (𝐵 +s 𝑧𝑅)))}) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑎 = (((𝑥𝑅 ·s (𝐵 +s 𝐶)) +s (𝐴 ·s (𝑦𝐿 +s 𝐶))) -s (𝑥𝑅 ·s (𝑦𝐿 +s 𝐶)))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑥𝑅 ·s (𝐵 +s 𝐶)) +s (𝐴 ·s (𝐵 +s 𝑧𝐿))) -s (𝑥𝑅 ·s (𝐵 +s 𝑧𝐿)))}))))
Theorem	addsdilem2 28055*	Lemma for surreal distribution. Expand the right hand side of the main expression. (Contributed by Scott Fenton, 8-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝐶)) = ((({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑎 = ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝐿 ·s 𝑦𝐿)) +s (𝐴 ·s 𝐶))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑎 = ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝑅 ·s 𝑦𝑅)) +s (𝐴 ·s 𝐶))}) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((𝐴 ·s 𝐵) +s (((𝑥𝐿 ·s 𝐶) +s (𝐴 ·s 𝑧𝐿)) -s (𝑥𝐿 ·s 𝑧𝐿)))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((𝐴 ·s 𝐵) +s (((𝑥𝑅 ·s 𝐶) +s (𝐴 ·s 𝑧𝑅)) -s (𝑥𝑅 ·s 𝑧𝑅)))})) |s (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑎 = ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝐿 ·s 𝑦𝑅)) +s (𝐴 ·s 𝐶))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑎 = ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝑅 ·s 𝑦𝐿)) +s (𝐴 ·s 𝐶))}) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((𝐴 ·s 𝐵) +s (((𝑥𝐿 ·s 𝐶) +s (𝐴 ·s 𝑧𝑅)) -s (𝑥𝐿 ·s 𝑧𝑅)))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((𝐴 ·s 𝐵) +s (((𝑥𝑅 ·s 𝐶) +s (𝐴 ·s 𝑧𝐿)) -s (𝑥𝑅 ·s 𝑧𝐿)))}))))
Theorem	addsdilem3 28056*	Lemma for addsdi 28058. Show one of the equalities involved in the final expression. (Contributed by Scott Fenton, 9-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))(𝑥𝑂 ·s (𝐵 +s 𝐶)) = ((𝑥𝑂 ·s 𝐵) +s (𝑥𝑂 ·s 𝐶)))    &   ⊢ (𝜑 → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))(𝐴 ·s (𝑦𝑂 +s 𝐶)) = ((𝐴 ·s 𝑦𝑂) +s (𝐴 ·s 𝐶)))    &   ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))(𝑥𝑂 ·s (𝑦𝑂 +s 𝐶)) = ((𝑥𝑂 ·s 𝑦𝑂) +s (𝑥𝑂 ·s 𝐶)))    &   ⊢ (𝜓 → 𝑋 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))    &   ⊢ (𝜓 → 𝑌 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵)))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (((𝑋 ·s (𝐵 +s 𝐶)) +s (𝐴 ·s (𝑌 +s 𝐶))) -s (𝑋 ·s (𝑌 +s 𝐶))) = ((((𝑋 ·s 𝐵) +s (𝐴 ·s 𝑌)) -s (𝑋 ·s 𝑌)) +s (𝐴 ·s 𝐶)))
Theorem	addsdilem4 28057*	Lemma for addsdi 28058. Show one of the equalities involved in the final expression. (Contributed by Scott Fenton, 9-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))(𝑥𝑂 ·s (𝐵 +s 𝐶)) = ((𝑥𝑂 ·s 𝐵) +s (𝑥𝑂 ·s 𝐶)))    &   ⊢ (𝜑 → ∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))(𝐴 ·s (𝐵 +s 𝑧𝑂)) = ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝑧𝑂)))    &   ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))(𝑥𝑂 ·s (𝐵 +s 𝑧𝑂)) = ((𝑥𝑂 ·s 𝐵) +s (𝑥𝑂 ·s 𝑧𝑂)))    &   ⊢ (𝜓 → 𝑋 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))    &   ⊢ (𝜓 → 𝑍 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶)))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (((𝑋 ·s (𝐵 +s 𝐶)) +s (𝐴 ·s (𝐵 +s 𝑍))) -s (𝑋 ·s (𝐵 +s 𝑍))) = ((𝐴 ·s 𝐵) +s (((𝑋 ·s 𝐶) +s (𝐴 ·s 𝑍)) -s (𝑋 ·s 𝑍))))
Theorem	addsdi 28058	Distributive law for surreal numbers. Commuted form of part of theorem 7 of [Conway] p. 19. (Contributed by Scott Fenton, 9-Mar-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 ·s (𝐵 +s 𝐶)) = ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝐶)))
Theorem	addsdid 28059	Distributive law for surreal numbers. Commuted form of part of theorem 7 of [Conway] p. 19. (Contributed by Scott Fenton, 9-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 ·s (𝐵 +s 𝐶)) = ((𝐴 ·s 𝐵) +s (𝐴 ·s 𝐶)))
Theorem	addsdird 28060	Distributive law for surreal numbers. Part of theorem 7 of [Conway] p. 19. (Contributed by Scott Fenton, 9-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 +s 𝐵) ·s 𝐶) = ((𝐴 ·s 𝐶) +s (𝐵 ·s 𝐶)))
Theorem	subsdid 28061	Distribution of surreal multiplication over subtraction. (Contributed by Scott Fenton, 9-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 ·s (𝐵 -s 𝐶)) = ((𝐴 ·s 𝐵) -s (𝐴 ·s 𝐶)))
Theorem	subsdird 28062	Distribution of surreal multiplication over subtraction. (Contributed by Scott Fenton, 9-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 -s 𝐵) ·s 𝐶) = ((𝐴 ·s 𝐶) -s (𝐵 ·s 𝐶)))
Theorem	mulnegs1d 28063	Product with negative is negative of product. Part of theorem 7 of [Conway] p. 19. (Contributed by Scott Fenton, 10-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → (( -us ‘𝐴) ·s 𝐵) = ( -us ‘(𝐴 ·s 𝐵)))
Theorem	mulnegs2d 28064	Product with negative is negative of product. Part of theorem 7 of [Conway] p. 19. (Contributed by Scott Fenton, 10-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 ·s ( -us ‘𝐵)) = ( -us ‘(𝐴 ·s 𝐵)))
Theorem	mul2negsd 28065	Surreal product of two negatives. (Contributed by Scott Fenton, 15-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → (( -us ‘𝐴) ·s ( -us ‘𝐵)) = (𝐴 ·s 𝐵))
Theorem	mulsasslem1 28066*	Lemma for mulsass 28069. Expand the left hand side of the formula. (Contributed by Scott Fenton, 9-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 ·s 𝐵) ·s 𝐶) = ((({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝐿))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝐿))}) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝑅))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝑅))})) |s (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝐿 ·s 𝑦𝐿)) ·s 𝑧𝑅))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝑅 ·s 𝑦𝑅)) ·s 𝑧𝑅))}) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s ((((𝑥𝐿 ·s 𝐵) +s (𝐴 ·s 𝑦𝑅)) -s (𝑥𝐿 ·s 𝑦𝑅)) ·s 𝑧𝐿))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s ((((𝑥𝑅 ·s 𝐵) +s (𝐴 ·s 𝑦𝐿)) -s (𝑥𝑅 ·s 𝑦𝐿)) ·s 𝑧𝐿))}))))
Theorem	mulsasslem2 28067*	Lemma for mulsass 28069. Expand the right hand side of the formula. (Contributed by Scott Fenton, 9-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 ·s (𝐵 ·s 𝐶)) = ((({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑥𝐿 ·s (𝐵 ·s 𝐶)) +s (𝐴 ·s (((𝑦𝐿 ·s 𝐶) +s (𝐵 ·s 𝑧𝐿)) -s (𝑦𝐿 ·s 𝑧𝐿)))) -s (𝑥𝐿 ·s (((𝑦𝐿 ·s 𝐶) +s (𝐵 ·s 𝑧𝐿)) -s (𝑦𝐿 ·s 𝑧𝐿))))} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑥𝐿 ·s (𝐵 ·s 𝐶)) +s (𝐴 ·s (((𝑦𝑅 ·s 𝐶) +s (𝐵 ·s 𝑧𝑅)) -s (𝑦𝑅 ·s 𝑧𝑅)))) -s (𝑥𝐿 ·s (((𝑦𝑅 ·s 𝐶) +s (𝐵 ·s 𝑧𝑅)) -s (𝑦𝑅 ·s 𝑧𝑅))))}) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑥𝑅 ·s (𝐵 ·s 𝐶)) +s (𝐴 ·s (((𝑦𝐿 ·s 𝐶) +s (𝐵 ·s 𝑧𝑅)) -s (𝑦𝐿 ·s 𝑧𝑅)))) -s (𝑥𝑅 ·s (((𝑦𝐿 ·s 𝐶) +s (𝐵 ·s 𝑧𝑅)) -s (𝑦𝐿 ·s 𝑧𝑅))))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑥𝑅 ·s (𝐵 ·s 𝐶)) +s (𝐴 ·s (((𝑦𝑅 ·s 𝐶) +s (𝐵 ·s 𝑧𝐿)) -s (𝑦𝑅 ·s 𝑧𝐿)))) -s (𝑥𝑅 ·s (((𝑦𝑅 ·s 𝐶) +s (𝐵 ·s 𝑧𝐿)) -s (𝑦𝑅 ·s 𝑧𝐿))))})) |s (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑥𝐿 ·s (𝐵 ·s 𝐶)) +s (𝐴 ·s (((𝑦𝐿 ·s 𝐶) +s (𝐵 ·s 𝑧𝑅)) -s (𝑦𝐿 ·s 𝑧𝑅)))) -s (𝑥𝐿 ·s (((𝑦𝐿 ·s 𝐶) +s (𝐵 ·s 𝑧𝑅)) -s (𝑦𝐿 ·s 𝑧𝑅))))} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑥𝐿 ·s (𝐵 ·s 𝐶)) +s (𝐴 ·s (((𝑦𝑅 ·s 𝐶) +s (𝐵 ·s 𝑧𝐿)) -s (𝑦𝑅 ·s 𝑧𝐿)))) -s (𝑥𝐿 ·s (((𝑦𝑅 ·s 𝐶) +s (𝐵 ·s 𝑧𝐿)) -s (𝑦𝑅 ·s 𝑧𝐿))))}) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑥𝑅 ·s (𝐵 ·s 𝐶)) +s (𝐴 ·s (((𝑦𝐿 ·s 𝐶) +s (𝐵 ·s 𝑧𝐿)) -s (𝑦𝐿 ·s 𝑧𝐿)))) -s (𝑥𝑅 ·s (((𝑦𝐿 ·s 𝐶) +s (𝐵 ·s 𝑧𝐿)) -s (𝑦𝐿 ·s 𝑧𝐿))))} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑥𝑅 ·s (𝐵 ·s 𝐶)) +s (𝐴 ·s (((𝑦𝑅 ·s 𝐶) +s (𝐵 ·s 𝑧𝑅)) -s (𝑦𝑅 ·s 𝑧𝑅)))) -s (𝑥𝑅 ·s (((𝑦𝑅 ·s 𝐶) +s (𝐵 ·s 𝑧𝑅)) -s (𝑦𝑅 ·s 𝑧𝑅))))}))))
Theorem	mulsasslem3 28068*	Lemma for mulsass 28069. Demonstrate the central equality. (Contributed by Scott Fenton, 10-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ 𝑃 ⊆ (( L ‘𝐴) ∪ ( R ‘𝐴))    &   ⊢ 𝑄 ⊆ (( L ‘𝐵) ∪ ( R ‘𝐵))    &   ⊢ 𝑅 ⊆ (( L ‘𝐶) ∪ ( R ‘𝐶))    &   ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝑥𝑂 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝑧𝑂)))    &   ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))((𝑥𝑂 ·s 𝑦𝑂) ·s 𝐶) = (𝑥𝑂 ·s (𝑦𝑂 ·s 𝐶)))    &   ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝑥𝑂 ·s 𝐵) ·s 𝑧𝑂) = (𝑥𝑂 ·s (𝐵 ·s 𝑧𝑂)))    &   ⊢ (𝜑 → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝐴 ·s 𝑦𝑂) ·s 𝑧𝑂) = (𝐴 ·s (𝑦𝑂 ·s 𝑧𝑂)))    &   ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))((𝑥𝑂 ·s 𝐵) ·s 𝐶) = (𝑥𝑂 ·s (𝐵 ·s 𝐶)))    &   ⊢ (𝜑 → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))((𝐴 ·s 𝑦𝑂) ·s 𝐶) = (𝐴 ·s (𝑦𝑂 ·s 𝐶)))    &   ⊢ (𝜑 → ∀𝑧𝑂 ∈ (( L ‘𝐶) ∪ ( R ‘𝐶))((𝐴 ·s 𝐵) ·s 𝑧𝑂) = (𝐴 ·s (𝐵 ·s 𝑧𝑂)))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑄 ∃𝑧 ∈ 𝑅 𝑎 = ((((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧)) -s ((((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦)) ·s 𝑧)) ↔ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑄 ∃𝑧 ∈ 𝑅 𝑎 = (((𝑥 ·s (𝐵 ·s 𝐶)) +s (𝐴 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧)))) -s (𝑥 ·s (((𝑦 ·s 𝐶) +s (𝐵 ·s 𝑧)) -s (𝑦 ·s 𝑧))))))
Theorem	mulsass 28069	Associative law for surreal multiplication. Part of theorem 7 of [Conway] p. 19. Much like the case for additive groups, this theorem together with mulscom 28042, addsdi 28058, mulsgt0 28047, and the addition theorems would make the surreals into an ordered ring except that they are a proper class. (Contributed by Scott Fenton, 10-Mar-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐴 ·s 𝐵) ·s 𝐶) = (𝐴 ·s (𝐵 ·s 𝐶)))
Theorem	mulsassd 28070	Associative law for surreal multiplication. Part of theorem 7 of [Conway] p. 19. (Contributed by Scott Fenton, 10-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 ·s 𝐵) ·s 𝐶) = (𝐴 ·s (𝐵 ·s 𝐶)))
Theorem	muls4d 28071	Rearrangement of four surreal factors. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐷 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 ·s 𝐵) ·s (𝐶 ·s 𝐷)) = ((𝐴 ·s 𝐶) ·s (𝐵 ·s 𝐷)))
Theorem	mulsunif2lem 28072*	Lemma for mulsunif2 28073. State the theorem with extra disjoint variable conditions. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ (𝜑 → 𝐿 <<s 𝑅)    &   ⊢ (𝜑 → 𝑀 <<s 𝑆)    &   ⊢ (𝜑 → 𝐴 = (𝐿 |s 𝑅))    &   ⊢ (𝜑 → 𝐵 = (𝑀 |s 𝑆))    ⇒   ⊢ (𝜑 → (𝐴 ·s 𝐵) = (({𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑝) ·s (𝐵 -s 𝑞)))} ∪ {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = ((𝐴 ·s 𝐵) -s ((𝑟 -s 𝐴) ·s (𝑠 -s 𝐵)))}) |s ({𝑐 ∣ ∃𝑡 ∈ 𝐿 ∃𝑢 ∈ 𝑆 𝑐 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵)))} ∪ {𝑑 ∣ ∃𝑣 ∈ 𝑅 ∃𝑤 ∈ 𝑀 𝑑 = ((𝐴 ·s 𝐵) +s ((𝑣 -s 𝐴) ·s (𝐵 -s 𝑤)))})))
Theorem	mulsunif2 28073*	Alternate expression for surreal multiplication. Note from [Conway] p. 19. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ (𝜑 → 𝐿 <<s 𝑅)    &   ⊢ (𝜑 → 𝑀 <<s 𝑆)    &   ⊢ (𝜑 → 𝐴 = (𝐿 |s 𝑅))    &   ⊢ (𝜑 → 𝐵 = (𝑀 |s 𝑆))    ⇒   ⊢ (𝜑 → (𝐴 ·s 𝐵) = (({𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑝) ·s (𝐵 -s 𝑞)))} ∪ {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = ((𝐴 ·s 𝐵) -s ((𝑟 -s 𝐴) ·s (𝑠 -s 𝐵)))}) |s ({𝑐 ∣ ∃𝑡 ∈ 𝐿 ∃𝑢 ∈ 𝑆 𝑐 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵)))} ∪ {𝑑 ∣ ∃𝑣 ∈ 𝑅 ∃𝑤 ∈ 𝑀 𝑑 = ((𝐴 ·s 𝐵) +s ((𝑣 -s 𝐴) ·s (𝐵 -s 𝑤)))})))
Theorem	sltmul2 28074	Multiplication of both sides of surreal less-than by a positive number. (Contributed by Scott Fenton, 10-Mar-2025.)
⊢ (((𝐴 ∈ No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐵 <s 𝐶 ↔ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)))
Theorem	sltmul2d 28075	Multiplication of both sides of surreal less-than by a positive number. (Contributed by Scott Fenton, 10-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 0s <s 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ (𝐶 ·s 𝐴) <s (𝐶 ·s 𝐵)))
Theorem	sltmul1d 28076	Multiplication of both sides of surreal less-than by a positive number. (Contributed by Scott Fenton, 10-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 0s <s 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ (𝐴 ·s 𝐶) <s (𝐵 ·s 𝐶)))
Theorem	slemul2d 28077	Multiplication of both sides of surreal less-than or equal by a positive number. (Contributed by Scott Fenton, 10-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 0s <s 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 ≤s 𝐵 ↔ (𝐶 ·s 𝐴) ≤s (𝐶 ·s 𝐵)))
Theorem	slemul1d 28078	Multiplication of both sides of surreal less-than or equal by a positive number. (Contributed by Scott Fenton, 10-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 0s <s 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 ≤s 𝐵 ↔ (𝐴 ·s 𝐶) ≤s (𝐵 ·s 𝐶)))
Theorem	sltmulneg1d 28079	Multiplication of both sides of surreal less-than by a negative number. (Contributed by Scott Fenton, 14-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐶 <s 0s )    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ (𝐵 ·s 𝐶) <s (𝐴 ·s 𝐶)))
Theorem	sltmulneg2d 28080	Multiplication of both sides of surreal less-than by a negative number. (Contributed by Scott Fenton, 14-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐶 <s 0s )    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ (𝐶 ·s 𝐵) <s (𝐶 ·s 𝐴)))
Theorem	mulscan2dlem 28081	Lemma for mulscan2d 28082. Cancellation of multiplication when the right term is positive. (Contributed by Scott Fenton, 10-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 0s <s 𝐶)    ⇒   ⊢ (𝜑 → ((𝐴 ·s 𝐶) = (𝐵 ·s 𝐶) ↔ 𝐴 = 𝐵))
Theorem	mulscan2d 28082	Cancellation of surreal multiplication when the right term is non-zero. (Contributed by Scott Fenton, 10-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐶 ≠ 0s )    ⇒   ⊢ (𝜑 → ((𝐴 ·s 𝐶) = (𝐵 ·s 𝐶) ↔ 𝐴 = 𝐵))
Theorem	mulscan1d 28083	Cancellation of surreal multiplication when the left term is non-zero. (Contributed by Scott Fenton, 10-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐶 ≠ 0s )    ⇒   ⊢ (𝜑 → ((𝐶 ·s 𝐴) = (𝐶 ·s 𝐵) ↔ 𝐴 = 𝐵))
Theorem	muls12d 28084	Commutative/associative law for surreal multiplication. (Contributed by Scott Fenton, 14-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 ·s (𝐵 ·s 𝐶)) = (𝐵 ·s (𝐴 ·s 𝐶)))
Theorem	slemul1ad 28085	Multiplication of both sides of surreal less-than or equal by a non-negative number. (Contributed by Scott Fenton, 17-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 0s ≤s 𝐶)    &   ⊢ (𝜑 → 𝐴 ≤s 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ·s 𝐶) ≤s (𝐵 ·s 𝐶))
Theorem	sltmul12ad 28086	Comparison of the product of two positive surreals. (Contributed by Scott Fenton, 17-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐷 ∈ No )    &   ⊢ (𝜑 → 0s ≤s 𝐴)    &   ⊢ (𝜑 → 𝐴 <s 𝐵)    &   ⊢ (𝜑 → 0s ≤s 𝐶)    &   ⊢ (𝜑 → 𝐶 <s 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ·s 𝐶) <s (𝐵 ·s 𝐷))
Theorem	divsmo 28087*	Uniqueness of surreal inversion. Given a non-zero surreal 𝐴, there is at most one surreal giving a particular product. (Contributed by Scott Fenton, 10-Mar-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐴 ≠ 0s ) → ∃*𝑥 ∈ No (𝐴 ·s 𝑥) = 𝐵)
Theorem	muls0ord 28088	If a surreal product is zero, one of its factors must be zero. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 ·s 𝐵) = 0s ↔ (𝐴 = 0s ∨ 𝐵 = 0s )))
Theorem	mulsne0bd 28089	The product of two non-zero surreals is non-zero. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 ·s 𝐵) ≠ 0s ↔ (𝐴 ≠ 0s ∧ 𝐵 ≠ 0s )))
15.5.4  Division
Syntax	cdivs 28090	Declare the syntax for surreal division.
class /su
Definition	df-divs 28091*	Define surreal division. This is not the definition used in the literature, but we use it here because it is technically easier to work with. (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ /su = (𝑥 ∈ No , 𝑦 ∈ ( No ∖ { 0s }) ↦ (℩𝑧 ∈ No (𝑦 ·s 𝑧) = 𝑥))
Theorem	divsval 28092*	The value of surreal division. (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐵 ≠ 0s ) → (𝐴 /su 𝐵) = (℩𝑥 ∈ No (𝐵 ·s 𝑥) = 𝐴))
Theorem	norecdiv 28093*	If a surreal has a reciprocal, then it has any division. (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ (((𝐴 ∈ No ∧ 𝐴 ≠ 0s ∧ 𝐵 ∈ No ) ∧ ∃𝑥 ∈ No (𝐴 ·s 𝑥) = 1s ) → ∃𝑦 ∈ No (𝐴 ·s 𝑦) = 𝐵)
Theorem	noreceuw 28094*	If a surreal has a reciprocal, then it has unique division. (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ (((𝐴 ∈ No ∧ 𝐴 ≠ 0s ∧ 𝐵 ∈ No ) ∧ ∃𝑥 ∈ No (𝐴 ·s 𝑥) = 1s ) → ∃!𝑦 ∈ No (𝐴 ·s 𝑦) = 𝐵)
Theorem	recsne0 28095*	If a surreal has a reciprocal, then it is non-zero. (Contributed by Scott Fenton, 5-Sep-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → ∃𝑥 ∈ No (𝐴 ·s 𝑥) = 1s )    ⇒   ⊢ (𝜑 → 𝐴 ≠ 0s )
Theorem	divsmulw 28096*	Relationship between surreal division and multiplication. Weak version that does not assume reciprocals. Later, when we prove precsex 28120, we can eliminate the existence hypothesis (see divsmul 28123). (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ (𝐶 ∈ No ∧ 𝐶 ≠ 0s )) ∧ ∃𝑥 ∈ No (𝐶 ·s 𝑥) = 1s ) → ((𝐴 /su 𝐶) = 𝐵 ↔ (𝐶 ·s 𝐵) = 𝐴))
Theorem	divsmulwd 28097*	Relationship between surreal division and multiplication. Weak version that does not assume reciprocals. (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐶 ≠ 0s )    &   ⊢ (𝜑 → ∃𝑥 ∈ No (𝐶 ·s 𝑥) = 1s )    ⇒   ⊢ (𝜑 → ((𝐴 /su 𝐶) = 𝐵 ↔ (𝐶 ·s 𝐵) = 𝐴))
Theorem	divsclw 28098*	Weak division closure law. (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐵 ≠ 0s ) ∧ ∃𝑥 ∈ No (𝐵 ·s 𝑥) = 1s ) → (𝐴 /su 𝐵) ∈ No )
Theorem	divsclwd 28099*	Weak division closure law. (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐵 ≠ 0s )    &   ⊢ (𝜑 → ∃𝑥 ∈ No (𝐵 ·s 𝑥) = 1s )    ⇒   ⊢ (𝜑 → (𝐴 /su 𝐵) ∈ No )
Theorem	divscan2wd 28100*	A weak cancellation law for surreal division. (Contributed by Scott Fenton, 13-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐵 ≠ 0s )    &   ⊢ (𝜑 → ∃𝑥 ∈ No (𝐵 ·s 𝑥) = 1s )    ⇒   ⊢ (𝜑 → (𝐵 ·s (𝐴 /su 𝐵)) = 𝐴)