P. 286 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28501-28600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ltsubsubs3bd 28501	Equivalence for the surreal less-than relationship between differences. (Contributed by Scott Fenton, 21-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 𝐷 ∈ No)    ⇒   ⊢ (𝜑 → ((𝐴 −s 𝐶) <s (𝐵 −s 𝐷) ↔ (𝐷 −s 𝐶) <s (𝐵 −s 𝐴)))
Theorem	lesubsubsbd 28502	Equivalence for the surreal less-than or equal relationship between differences. (Contributed by Scott Fenton, 7-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 𝐷 ∈ No)    ⇒   ⊢ (𝜑 → ((𝐴 −s 𝐶) ≤s (𝐵 −s 𝐷) ↔ (𝐴 −s 𝐵) ≤s (𝐶 −s 𝐷)))
Theorem	lesubsubs2bd 28503	Equivalence for the surreal less-than or equal relationship between differences. (Contributed by Scott Fenton, 7-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 𝐷 ∈ No)    ⇒   ⊢ (𝜑 → ((𝐴 −s 𝐵) ≤s (𝐶 −s 𝐷) ↔ (𝐷 −s 𝐶) ≤s (𝐵 −s 𝐴)))
Theorem	lesubsubs3bd 28504	Equivalence for the surreal less-than or equal relationship between differences. (Contributed by Scott Fenton, 7-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 𝐷 ∈ No)    ⇒   ⊢ (𝜑 → ((𝐴 −s 𝐶) ≤s (𝐵 −s 𝐷) ↔ (𝐷 −s 𝐶) ≤s (𝐵 −s 𝐴)))
Theorem	ltsubaddsd 28505	Surreal less-than relationship between subtraction and addition. (Contributed by Scott Fenton, 27-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    ⇒   ⊢ (𝜑 → ((𝐴 −s 𝐵) <s 𝐶 ↔ 𝐴 <s (𝐶 +s 𝐵)))
Theorem	ltsubadds2d 28506	Surreal less-than relationship between subtraction and addition. (Contributed by Scott Fenton, 27-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    ⇒   ⊢ (𝜑 → ((𝐴 −s 𝐵) <s 𝐶 ↔ 𝐴 <s (𝐵 +s 𝐶)))
Theorem	ltaddsubsd 28507	Surreal less-than relationship between subtraction and addition. (Contributed by Scott Fenton, 28-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    ⇒   ⊢ (𝜑 → ((𝐴 +s 𝐵) <s 𝐶 ↔ 𝐴 <s (𝐶 −s 𝐵)))
Theorem	ltaddsubs2d 28508	Surreal less-than relationship between subtraction and addition. (Contributed by Scott Fenton, 28-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    ⇒   ⊢ (𝜑 → ((𝐴 +s 𝐵) <s 𝐶 ↔ 𝐵 <s (𝐶 −s 𝐴)))
Theorem	lesubaddsd 28509	Surreal less-than or equal relationship between subtraction and addition. (Contributed by Scott Fenton, 26-May-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    ⇒   ⊢ (𝜑 → ((𝐴 −s 𝐵) ≤s 𝐶 ↔ 𝐴 ≤s (𝐶 +s 𝐵)))
Theorem	subsubs4d 28510	Law for double surreal subtraction. (Contributed by Scott Fenton, 9-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    ⇒   ⊢ (𝜑 → ((𝐴 −s 𝐵) −s 𝐶) = (𝐴 −s (𝐵 +s 𝐶)))
Theorem	subsubs2d 28511	Law for double surreal subtraction. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    ⇒   ⊢ (𝜑 → (𝐴 −s (𝐵 −s 𝐶)) = (𝐴 +s (𝐶 −s 𝐵)))
Theorem	lesubsd 28512	Swap subtrahends in a surreal inequality. (Contributed by Scott Fenton, 29-Jan-2026.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    ⇒   ⊢ (𝜑 → (𝐴 ≤s (𝐵 −s 𝐶) ↔ 𝐶 ≤s (𝐵 −s 𝐴)))
Theorem	nncansd 28513	Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    ⇒   ⊢ (𝜑 → (𝐴 −s (𝐴 −s 𝐵)) = 𝐵)
Theorem	posdifsd 28514	Comparison of two surreals whose difference is positive. (Contributed by Scott Fenton, 10-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ 0s <s (𝐵 −s 𝐴)))
Theorem	ltsubsposd 28515	Subtraction of a positive number decreases the sum. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    ⇒   ⊢ (𝜑 → ( 0s <s 𝐴 ↔ (𝐵 −s 𝐴) <s 𝐵))
Theorem	subsge0d 28516	Non-negative subtraction. (Contributed by Scott Fenton, 26-May-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    ⇒   ⊢ (𝜑 → ( 0s ≤s (𝐴 −s 𝐵) ↔ 𝐵 ≤s 𝐴))
Theorem	addsubs4d 28517	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	ltsm1d 28518	A surreal is greater than itself minus one. (Contributed by Scott Fenton, 20-Aug-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    ⇒   ⊢ (𝜑 → (𝐴 −s 1s ) <s 𝐴)
Theorem	subscan1d 28519	Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    ⇒   ⊢ (𝜑 → ((𝐶 −s 𝐴) = (𝐶 −s 𝐵) ↔ 𝐴 = 𝐵))
Theorem	subscan2d 28520	Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    ⇒   ⊢ (𝜑 → ((𝐴 −s 𝐶) = (𝐵 −s 𝐶) ↔ 𝐴 = 𝐵))
Theorem	subseq0d 28521	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 28522	Set up the syntax for surreal multiplication.
class ·s
Definition	df-muls 28523*	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 28524	Surreal multiplication is a function over surreals. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ·s Fn (No × No)
Theorem	mulsval 28525*	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 28526*	Lemma for mulsval2 28527. 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 28527*	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 28528	Surreal multiplication by zero. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ (𝐴 ∈ No → (𝐴 ·s 0s ) = 0s )
Theorem	mulsrid 28529	Surreal one is a right identity element for multiplication. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ (𝐴 ∈ No → (𝐴 ·s 1s ) = 𝐴)
Theorem	mulsridd 28530	Surreal one is a right identity element for multiplication. (Contributed by Scott Fenton, 14-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    ⇒   ⊢ (𝜑 → (𝐴 ·s 1s ) = 𝐴)
Theorem	mulsproplemcbv 28531*	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 28532*	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 28533*	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 28534*	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 28535*	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 28536*	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 28537*	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 28538*	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 28539*	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 28540*	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 28541*	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 28542*	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 28543*	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 28544*	Lemma for surreal multiplication. Remove the restriction on 𝐶 and 𝐷 from mulsproplem12 28543. (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 28545*	Lemma for surreal multiplication. Finally, we remove the restriction on 𝐸 and 𝐹 from mulsproplem12 28543 and mulsproplem13 28544. This completes the induction on surreal multiplication. mulsprop 28546 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 28546	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	mulcutlem 28547*	Lemma for mulcut 28548. 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	mulcut 28548*	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	mulcut2 28549*	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 28550	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 28551	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	ltmuls 28552	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	ltmulsd 28553	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	lemulsd 28554	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 28555	Surreal multiplication is commutative. Part of theorem 7 of [Conway] p. 19. (Contributed by Scott Fenton, 6-Mar-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No) → (𝐴 ·s 𝐵) = (𝐵 ·s 𝐴))
Theorem	mulscomd 28556	Surreal multiplication is commutative. Part of theorem 7 of [Conway] p. 19. (Contributed by Scott Fenton, 6-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    ⇒   ⊢ (𝜑 → (𝐴 ·s 𝐵) = (𝐵 ·s 𝐴))
Theorem	muls02 28557	Surreal multiplication by zero. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ (𝐴 ∈ No → ( 0s ·s 𝐴) = 0s )
Theorem	mulslid 28558	Surreal one is a left identity element for multiplication. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ (𝐴 ∈ No → ( 1s ·s 𝐴) = 𝐴)
Theorem	mulslidd 28559	Surreal one is a left identity element for multiplication. (Contributed by Scott Fenton, 14-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    ⇒   ⊢ (𝜑 → ( 1s ·s 𝐴) = 𝐴)
Theorem	mulsgt0 28560	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 28561	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 28562	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	sltmuls1 28563*	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	sltmuls2 28564*	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 28565*	Lemma for mulsunif 28566. 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 28566*	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 28567*	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 28568*	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 28569*	Lemma for addsdi 28571. 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 28570*	Lemma for addsdi 28571. 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 28571	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 28572	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 28573	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 28574	Distribution of surreal multiplication over subtraction. (Contributed by Scott Fenton, 9-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    ⇒   ⊢ (𝜑 → (𝐴 ·s (𝐵 −s 𝐶)) = ((𝐴 ·s 𝐵) −s (𝐴 ·s 𝐶)))
Theorem	subsdird 28575	Distribution of surreal multiplication over subtraction. (Contributed by Scott Fenton, 9-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    ⇒   ⊢ (𝜑 → ((𝐴 −s 𝐵) ·s 𝐶) = ((𝐴 ·s 𝐶) −s (𝐵 ·s 𝐶)))
Theorem	mulnegs1d 28576	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‘𝐴) ·s 𝐵) = ( -s‘(𝐴 ·s 𝐵)))
Theorem	mulnegs2d 28577	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 ( -s‘𝐵)) = ( -s‘(𝐴 ·s 𝐵)))
Theorem	mul2negsd 28578	Surreal product of two negatives. (Contributed by Scott Fenton, 15-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    ⇒   ⊢ (𝜑 → (( -s‘𝐴) ·s ( -s‘𝐵)) = (𝐴 ·s 𝐵))
Theorem	mulsasslem1 28579*	Lemma for mulsass 28582. 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 28580*	Lemma for mulsass 28582. 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 28581*	Lemma for mulsass 28582. 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 28582	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 28555, addsdi 28571, mulsgt0 28560, 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 28583	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 28584	Rearrangement of four surreal factors. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 𝐷 ∈ No)    ⇒   ⊢ (𝜑 → ((𝐴 ·s 𝐵) ·s (𝐶 ·s 𝐷)) = ((𝐴 ·s 𝐶) ·s (𝐵 ·s 𝐷)))
Theorem	mulsunif2lem 28585*	Lemma for mulsunif2 28586. 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 28586*	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	ltmuls2 28587	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	ltmuls2d 28588	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	ltmuls1d 28589	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	lemuls2d 28590	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	lemuls1d 28591	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	ltmulnegs1d 28592	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	ltmulnegs2d 28593	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 28594	Lemma for mulscan2d 28595. 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 28595	Cancellation of surreal multiplication when the right term is nonzero. (Contributed by Scott Fenton, 10-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 𝐶 ≠ 0s )    ⇒   ⊢ (𝜑 → ((𝐴 ·s 𝐶) = (𝐵 ·s 𝐶) ↔ 𝐴 = 𝐵))
Theorem	mulscan1d 28596	Cancellation of surreal multiplication when the left term is nonzero. (Contributed by Scott Fenton, 10-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 𝐶 ≠ 0s )    ⇒   ⊢ (𝜑 → ((𝐶 ·s 𝐴) = (𝐶 ·s 𝐵) ↔ 𝐴 = 𝐵))
Theorem	muls12d 28597	Commutative/associative law for surreal multiplication. (Contributed by Scott Fenton, 14-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    ⇒   ⊢ (𝜑 → (𝐴 ·s (𝐵 ·s 𝐶)) = (𝐵 ·s (𝐴 ·s 𝐶)))
Theorem	lemuls1ad 28598	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	ltmuls12ad 28599	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 28600*	Uniqueness of surreal inversion. Given a nonzero surreal 𝐴, there is at most one surreal giving a particular product. (Contributed by Scott Fenton, 10-Mar-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐴 ≠ 0s ) → ∃*𝑥 ∈ No (𝐴 ·s 𝑥) = 𝐵)