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	mulsridd 28501	Surreal one is a right identity element for multiplication. (Contributed by Scott Fenton, 14-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    ⇒   ⊢ (𝜑 → (𝐴 ·s 1s ) = 𝐴)
Theorem	mulsproplemcbv 28502*	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 28503*	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 28504*	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 28505*	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 28506*	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 28507*	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 28508*	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 28509*	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 28510*	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 28511*	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 28512*	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 28513*	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 28514*	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 28515*	Lemma for surreal multiplication. Remove the restriction on 𝐶 and 𝐷 from mulsproplem12 28514. (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 28516*	Lemma for surreal multiplication. Finally, we remove the restriction on 𝐸 and 𝐹 from mulsproplem12 28514 and mulsproplem13 28515. This completes the induction on surreal multiplication. mulsprop 28517 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 28517	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 28518*	Lemma for mulcut 28519. 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 28519*	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 28520*	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 28521	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 28522	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 28523	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 28524	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 28525	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 28526	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 28527	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 28528	Surreal multiplication by zero. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ (𝐴 ∈ No → ( 0s ·s 𝐴) = 0s )
Theorem	mulslid 28529	Surreal one is a left identity element for multiplication. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ (𝐴 ∈ No → ( 1s ·s 𝐴) = 𝐴)
Theorem	mulslidd 28530	Surreal one is a left identity element for multiplication. (Contributed by Scott Fenton, 14-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    ⇒   ⊢ (𝜑 → ( 1s ·s 𝐴) = 𝐴)
Theorem	mulsgt0 28531	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 28532	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 28533	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 28534*	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 28535*	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 28536*	Lemma for mulsunif 28537. 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 28537*	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 28538*	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 28539*	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 28540*	Lemma for addsdi 28542. 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 28541*	Lemma for addsdi 28542. 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 28542	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 28543	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 28544	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 28545	Distribution of surreal multiplication over subtraction. (Contributed by Scott Fenton, 9-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    ⇒   ⊢ (𝜑 → (𝐴 ·s (𝐵 −s 𝐶)) = ((𝐴 ·s 𝐵) −s (𝐴 ·s 𝐶)))
Theorem	subsdird 28546	Distribution of surreal multiplication over subtraction. (Contributed by Scott Fenton, 9-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    ⇒   ⊢ (𝜑 → ((𝐴 −s 𝐵) ·s 𝐶) = ((𝐴 ·s 𝐶) −s (𝐵 ·s 𝐶)))
Theorem	mulnegs1d 28547	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 28548	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 28549	Surreal product of two negatives. (Contributed by Scott Fenton, 15-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    ⇒   ⊢ (𝜑 → (( -s‘𝐴) ·s ( -s‘𝐵)) = (𝐴 ·s 𝐵))
Theorem	mulsasslem1 28550*	Lemma for mulsass 28553. 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 28551*	Lemma for mulsass 28553. 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 28552*	Lemma for mulsass 28553. 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 28553	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 28526, addsdi 28542, mulsgt0 28531, 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 28554	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 28555	Rearrangement of four surreal factors. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 𝐷 ∈ No)    ⇒   ⊢ (𝜑 → ((𝐴 ·s 𝐵) ·s (𝐶 ·s 𝐷)) = ((𝐴 ·s 𝐶) ·s (𝐵 ·s 𝐷)))
Theorem	mulsunif2lem 28556*	Lemma for mulsunif2 28557. 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 28557*	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 28558	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 28559	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 28560	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 28561	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 28562	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 28563	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 28564	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 28565	Lemma for mulscan2d 28566. 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 28566	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 28567	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 28568	Commutative/associative law for surreal multiplication. (Contributed by Scott Fenton, 14-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    ⇒   ⊢ (𝜑 → (𝐴 ·s (𝐵 ·s 𝐶)) = (𝐵 ·s (𝐴 ·s 𝐶)))
Theorem	lemuls1ad 28569	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 28570	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 28571*	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 𝑥) = 𝐵)
Theorem	muls0ord 28572	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 28573	The product of two nonzero surreals is nonzero. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    ⇒   ⊢ (𝜑 → ((𝐴 ·s 𝐵) ≠ 0s ↔ (𝐴 ≠ 0s ∧ 𝐵 ≠ 0s )))
15.5.4  Division
Syntax	cdivs 28574	Declare the syntax for surreal division.
class /su
Definition	df-divs 28575*	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 28576*	The value of surreal division. (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐵 ≠ 0s ) → (𝐴 /su 𝐵) = (℩𝑥 ∈ No (𝐵 ·s 𝑥) = 𝐴))
Theorem	norecdiv 28577*	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 28578*	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 28579*	If a surreal has a reciprocal, then it is nonzero. (Contributed by Scott Fenton, 5-Sep-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → ∃𝑥 ∈ No (𝐴 ·s 𝑥) = 1s )    ⇒   ⊢ (𝜑 → 𝐴 ≠ 0s )
Theorem	divmulsw 28580*	Relationship between surreal division and multiplication. Weak version that does not assume reciprocals. Later, when we prove precsex 28605, we can eliminate the existence hypothesis (see divmuls 28608). (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ (𝐶 ∈ No ∧ 𝐶 ≠ 0s )) ∧ ∃𝑥 ∈ No (𝐶 ·s 𝑥) = 1s ) → ((𝐴 /su 𝐶) = 𝐵 ↔ (𝐶 ·s 𝐵) = 𝐴))
Theorem	divmulswd 28581*	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 28582*	Weak division closure law. (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐵 ≠ 0s ) ∧ ∃𝑥 ∈ No (𝐵 ·s 𝑥) = 1s ) → (𝐴 /su 𝐵) ∈ No)
Theorem	divsclwd 28583*	Weak division closure law. (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐵 ≠ 0s )    &   ⊢ (𝜑 → ∃𝑥 ∈ No (𝐵 ·s 𝑥) = 1s )    ⇒   ⊢ (𝜑 → (𝐴 /su 𝐵) ∈ No)
Theorem	divscan2wd 28584*	A weak cancellation law for surreal division. (Contributed by Scott Fenton, 13-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐵 ≠ 0s )    &   ⊢ (𝜑 → ∃𝑥 ∈ No (𝐵 ·s 𝑥) = 1s )    ⇒   ⊢ (𝜑 → (𝐵 ·s (𝐴 /su 𝐵)) = 𝐴)
Theorem	divscan1wd 28585*	A weak cancellation law for surreal division. (Contributed by Scott Fenton, 13-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐵 ≠ 0s )    &   ⊢ (𝜑 → ∃𝑥 ∈ No (𝐵 ·s 𝑥) = 1s )    ⇒   ⊢ (𝜑 → ((𝐴 /su 𝐵) ·s 𝐵) = 𝐴)
Theorem	ltdivmulswd 28586*	Surreal less-than relationship between division and multiplication. Weak version. (Contributed by Scott Fenton, 14-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 0s <s 𝐶)    &   ⊢ (𝜑 → ∃𝑥 ∈ No (𝐶 ·s 𝑥) = 1s )    ⇒   ⊢ (𝜑 → ((𝐴 /su 𝐶) <s 𝐵 ↔ 𝐴 <s (𝐶 ·s 𝐵)))
Theorem	ltdivmuls2wd 28587*	Surreal less-than relationship between division and multiplication. Weak version. (Contributed by Scott Fenton, 14-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 0s <s 𝐶)    &   ⊢ (𝜑 → ∃𝑥 ∈ No (𝐶 ·s 𝑥) = 1s )    ⇒   ⊢ (𝜑 → ((𝐴 /su 𝐶) <s 𝐵 ↔ 𝐴 <s (𝐵 ·s 𝐶)))
Theorem	ltmuldivswd 28588*	Surreal less-than relationship between division and multiplication. Weak version. (Contributed by Scott Fenton, 14-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 0s <s 𝐶)    &   ⊢ (𝜑 → ∃𝑥 ∈ No (𝐶 ·s 𝑥) = 1s )    ⇒   ⊢ (𝜑 → ((𝐴 ·s 𝐶) <s 𝐵 ↔ 𝐴 <s (𝐵 /su 𝐶)))
Theorem	ltmuldivs2wd 28589*	Surreal less-than relationship between division and multiplication. Weak version. (Contributed by Scott Fenton, 14-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 0s <s 𝐶)    &   ⊢ (𝜑 → ∃𝑥 ∈ No (𝐶 ·s 𝑥) = 1s )    ⇒   ⊢ (𝜑 → ((𝐶 ·s 𝐴) <s 𝐵 ↔ 𝐴 <s (𝐵 /su 𝐶)))
Theorem	divsasswd 28590*	An associative law for surreal division. Weak version. (Contributed by Scott Fenton, 14-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 𝐶 ≠ 0s )    &   ⊢ (𝜑 → ∃𝑥 ∈ No (𝐶 ·s 𝑥) = 1s )    ⇒   ⊢ (𝜑 → ((𝐴 ·s 𝐵) /su 𝐶) = (𝐴 ·s (𝐵 /su 𝐶)))
Theorem	divs1 28591	A surreal divided by one is itself. (Contributed by Scott Fenton, 13-Mar-2025.)
⊢ (𝐴 ∈ No → (𝐴 /su 1s ) = 𝐴)
Theorem	divs1d 28592	A surreal divided by one is itself. Deduction version. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝜑 → 𝐴 ∈ No)    ⇒   ⊢ (𝜑 → (𝐴 /su 1s ) = 𝐴)
Theorem	precsexlemcbv 28593*	Lemma for surreal reciprocals. Change some bound variables. (Contributed by Scott Fenton, 15-Mar-2025.)
⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))⟩), ⟨{ 0s }, ∅⟩)    ⇒   ⊢ 𝐹 = rec((𝑞 ∈ V ↦ ⦋(1st ‘𝑞) / 𝑚⦌⦋(2nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧𝑅 ∈ (R‘𝐴)∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝑅 −s 𝐴) ·s 𝑤)) /su 𝑧𝑅)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0s <s 𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿 −s 𝐴) ·s 𝑡)) /su 𝑧𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0s <s 𝑧}∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝐿 −s 𝐴) ·s 𝑤)) /su 𝑧𝐿)} ∪ {𝑏 ∣ ∃𝑧𝑅 ∈ (R‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝑅 −s 𝐴) ·s 𝑡)) /su 𝑧𝑅)}))⟩), ⟨{ 0s }, ∅⟩)
Theorem	precsexlem1 28594	Lemma for surreal reciprocals. Calculate the value of the recursive left function at zero. (Contributed by Scott Fenton, 13-Mar-2025.)
⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))⟩), ⟨{ 0s }, ∅⟩)    &   ⊢ 𝐿 = (1st ∘ 𝐹)    &   ⊢ 𝑅 = (2nd ∘ 𝐹)    ⇒   ⊢ (𝐿‘∅) = { 0s }
Theorem	precsexlem2 28595	Lemma for surreal reciprocals. Calculate the value of the recursive right function at zero. (Contributed by Scott Fenton, 13-Mar-2025.)
⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))⟩), ⟨{ 0s }, ∅⟩)    &   ⊢ 𝐿 = (1st ∘ 𝐹)    &   ⊢ 𝑅 = (2nd ∘ 𝐹)    ⇒   ⊢ (𝑅‘∅) = ∅
Theorem	precsexlem3 28596*	Lemma for surreal reciprocals. Calculate the value of the recursive function at a successor. (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))⟩), ⟨{ 0s }, ∅⟩)    &   ⊢ 𝐿 = (1st ∘ 𝐹)    &   ⊢ 𝑅 = (2nd ∘ 𝐹)    ⇒   ⊢ (𝐼 ∈ ω → (𝐹‘suc 𝐼) = ⟨((𝐿‘𝐼) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝐼)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), ((𝑅‘𝐼) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝐼)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))⟩)
Theorem	precsexlem4 28597*	Lemma for surreal reciprocals. Calculate the value of the recursive left function at a successor. (Contributed by Scott Fenton, 13-Mar-2025.)
⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))⟩), ⟨{ 0s }, ∅⟩)    &   ⊢ 𝐿 = (1st ∘ 𝐹)    &   ⊢ 𝑅 = (2nd ∘ 𝐹)    ⇒   ⊢ (𝐼 ∈ ω → (𝐿‘suc 𝐼) = ((𝐿‘𝐼) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝐼)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})))
Theorem	precsexlem5 28598*	Lemma for surreal reciprocals. Calculate the value of the recursive right function at a successor. (Contributed by Scott Fenton, 13-Mar-2025.)
⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))⟩), ⟨{ 0s }, ∅⟩)    &   ⊢ 𝐿 = (1st ∘ 𝐹)    &   ⊢ 𝑅 = (2nd ∘ 𝐹)    ⇒   ⊢ (𝐼 ∈ ω → (𝑅‘suc 𝐼) = ((𝑅‘𝐼) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝐼)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})))
Theorem	precsexlem6 28599*	Lemma for surreal reciprocal. Show that 𝐿 is non-strictly increasing in its argument. (Contributed by Scott Fenton, 15-Mar-2025.)
⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))⟩), ⟨{ 0s }, ∅⟩)    &   ⊢ 𝐿 = (1st ∘ 𝐹)    &   ⊢ 𝑅 = (2nd ∘ 𝐹)    ⇒   ⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝐼 ⊆ 𝐽) → (𝐿‘𝐼) ⊆ (𝐿‘𝐽))
Theorem	precsexlem7 28600*	Lemma for surreal reciprocal. Show that 𝑅 is non-strictly increasing in its argument. (Contributed by Scott Fenton, 15-Mar-2025.)
⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))⟩), ⟨{ 0s }, ∅⟩)    &   ⊢ 𝐿 = (1st ∘ 𝐹)    &   ⊢ 𝑅 = (2nd ∘ 𝐹)    ⇒   ⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝐼 ⊆ 𝐽) → (𝑅‘𝐼) ⊆ (𝑅‘𝐽))