P. 283 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28201-28300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mulnegs2d 28201	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 28202	Surreal product of two negatives. (Contributed by Scott Fenton, 15-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → (( -us ‘𝐴) ·s ( -us ‘𝐵)) = (𝐴 ·s 𝐵))
Theorem	mulsasslem1 28203*	Lemma for mulsass 28206. 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 28204*	Lemma for mulsass 28206. 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 28205*	Lemma for mulsass 28206. 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 28206	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 28179, addsdi 28195, mulsgt0 28184, 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 28207	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 28208	Rearrangement of four surreal factors. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐷 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 ·s 𝐵) ·s (𝐶 ·s 𝐷)) = ((𝐴 ·s 𝐶) ·s (𝐵 ·s 𝐷)))
Theorem	mulsunif2lem 28209*	Lemma for mulsunif2 28210. 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 28210*	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 28211	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 28212	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 28213	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 28214	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 28215	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 28216	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 28217	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 28218	Lemma for mulscan2d 28219. 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 28219	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 28220	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 28221	Commutative/associative law for surreal multiplication. (Contributed by Scott Fenton, 14-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 ·s (𝐵 ·s 𝐶)) = (𝐵 ·s (𝐴 ·s 𝐶)))
Theorem	slemul1ad 28222	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 28223	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 28224*	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 28225	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 28226	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 28227	Declare the syntax for surreal division.
class /su
Definition	df-divs 28228*	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 28229*	The value of surreal division. (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐵 ≠ 0s ) → (𝐴 /su 𝐵) = (℩𝑥 ∈ No (𝐵 ·s 𝑥) = 𝐴))
Theorem	norecdiv 28230*	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 28231*	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	divsmulw 28232*	Relationship between surreal division and multiplication. Weak version that does not assume reciprocals. Later, when we prove precsex 28256, we can eliminate the existence hypothesis (see divsmul 28259). (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ (𝐶 ∈ No ∧ 𝐶 ≠ 0s )) ∧ ∃𝑥 ∈ No (𝐶 ·s 𝑥) = 1s ) → ((𝐴 /su 𝐶) = 𝐵 ↔ (𝐶 ·s 𝐵) = 𝐴))
Theorem	divsmulwd 28233*	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 28234*	Weak division closure law. (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐵 ≠ 0s ) ∧ ∃𝑥 ∈ No (𝐵 ·s 𝑥) = 1s ) → (𝐴 /su 𝐵) ∈ No )
Theorem	divsclwd 28235*	Weak division closure law. (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐵 ≠ 0s )    &   ⊢ (𝜑 → ∃𝑥 ∈ No (𝐵 ·s 𝑥) = 1s )    ⇒   ⊢ (𝜑 → (𝐴 /su 𝐵) ∈ No )
Theorem	divscan2wd 28236*	A weak cancellation law for surreal division. (Contributed by Scott Fenton, 13-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐵 ≠ 0s )    &   ⊢ (𝜑 → ∃𝑥 ∈ No (𝐵 ·s 𝑥) = 1s )    ⇒   ⊢ (𝜑 → (𝐵 ·s (𝐴 /su 𝐵)) = 𝐴)
Theorem	divscan1wd 28237*	A weak cancellation law for surreal division. (Contributed by Scott Fenton, 13-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐵 ≠ 0s )    &   ⊢ (𝜑 → ∃𝑥 ∈ No (𝐵 ·s 𝑥) = 1s )    ⇒   ⊢ (𝜑 → ((𝐴 /su 𝐵) ·s 𝐵) = 𝐴)
Theorem	sltdivmulwd 28238*	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	sltdivmul2wd 28239*	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	sltmuldivwd 28240*	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	sltmuldiv2wd 28241*	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 28242*	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 28243	A surreal divided by one is itself. (Contributed by Scott Fenton, 13-Mar-2025.)
⊢ (𝐴 ∈ No → (𝐴 /su 1s ) = 𝐴)
Theorem	precsexlemcbv 28244*	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 28245	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 28246	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 28247*	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 28248*	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 28249*	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 28250*	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 28251*	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	precsexlem8 28252*	Lemma for surreal reciprocal. Show that the left and right functions give sets of surreals. (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 ∘ 𝐹)    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 0s <s 𝐴)    &   ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))    ⇒   ⊢ ((𝜑 ∧ 𝐼 ∈ ω) → ((𝐿‘𝐼) ⊆ No ∧ (𝑅‘𝐼) ⊆ No ))
Theorem	precsexlem9 28253*	Lemma for surreal reciprocal. Show that the product of 𝐴 and a left element is less than one and the product of 𝐴 and a right element is greater than one. (Contributed by Scott Fenton, 14-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 ∘ 𝐹)    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 0s <s 𝐴)    &   ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))    ⇒   ⊢ ((𝜑 ∧ 𝐼 ∈ ω) → (∀𝑏 ∈ (𝐿‘𝐼)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝐼) 1s <s (𝐴 ·s 𝑐)))
Theorem	precsexlem10 28254*	Lemma for surreal reciprocal. Show that the union of the left sets is less than the union of the right sets. Note that this is the first theorem in the surreal numbers to require the axiom of infinity. (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 ∘ 𝐹)    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 0s <s 𝐴)    &   ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))    ⇒   ⊢ (𝜑 → ∪ (𝐿 “ ω) <<s ∪ (𝑅 “ ω))
Theorem	precsexlem11 28255*	Lemma for surreal reciprocal. Show that the cut of the left and right sets is a multiplicative inverse for 𝐴. (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 ∘ 𝐹)    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 0s <s 𝐴)    &   ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))    &   ⊢ 𝑌 = (∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))    ⇒   ⊢ (𝜑 → (𝐴 ·s 𝑌) = 1s )
Theorem	precsex 28256*	Every positive surreal has a reciprocal. Theorem 10(iv) of [Conway] p. 21. (Contributed by Scott Fenton, 15-Mar-2025.)
⊢ ((𝐴 ∈ No ∧ 0s <s 𝐴) → ∃𝑦 ∈ No (𝐴 ·s 𝑦) = 1s )
Theorem	recsex 28257*	A non-zero surreal has a reciprocal. (Contributed by Scott Fenton, 15-Mar-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐴 ≠ 0s ) → ∃𝑥 ∈ No (𝐴 ·s 𝑥) = 1s )
Theorem	recsexd 28258*	A non-zero surreal has a reciprocal. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐴 ≠ 0s )    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ No (𝐴 ·s 𝑥) = 1s )
Theorem	divsmul 28259	Relationship between surreal division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ (𝐶 ∈ No ∧ 𝐶 ≠ 0s )) → ((𝐴 /su 𝐶) = 𝐵 ↔ (𝐶 ·s 𝐵) = 𝐴))
Theorem	divsmuld 28260	Relationship between surreal division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐶 ≠ 0s )    ⇒   ⊢ (𝜑 → ((𝐴 /su 𝐶) = 𝐵 ↔ (𝐶 ·s 𝐵) = 𝐴))
Theorem	divscl 28261	Surreal division closure law. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐵 ≠ 0s ) → (𝐴 /su 𝐵) ∈ No )
Theorem	divscld 28262	Surreal division closure law. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐵 ≠ 0s )    ⇒   ⊢ (𝜑 → (𝐴 /su 𝐵) ∈ No )
Theorem	divscan2d 28263	A cancellation law for surreal division. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐵 ≠ 0s )    ⇒   ⊢ (𝜑 → (𝐵 ·s (𝐴 /su 𝐵)) = 𝐴)
Theorem	divscan1d 28264	A cancellation law for surreal division. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐵 ≠ 0s )    ⇒   ⊢ (𝜑 → ((𝐴 /su 𝐵) ·s 𝐵) = 𝐴)
Theorem	sltdivmuld 28265	Surreal less-than relationship between division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 0s <s 𝐶)    ⇒   ⊢ (𝜑 → ((𝐴 /su 𝐶) <s 𝐵 ↔ 𝐴 <s (𝐶 ·s 𝐵)))
Theorem	sltdivmul2d 28266	Surreal less-than relationship between division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 0s <s 𝐶)    ⇒   ⊢ (𝜑 → ((𝐴 /su 𝐶) <s 𝐵 ↔ 𝐴 <s (𝐵 ·s 𝐶)))
Theorem	sltmuldivd 28267	Surreal less-than relationship between division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 0s <s 𝐶)    ⇒   ⊢ (𝜑 → ((𝐴 ·s 𝐶) <s 𝐵 ↔ 𝐴 <s (𝐵 /su 𝐶)))
Theorem	sltmuldiv2d 28268	Surreal less-than relationship between division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 0s <s 𝐶)    ⇒   ⊢ (𝜑 → ((𝐶 ·s 𝐴) <s 𝐵 ↔ 𝐴 <s (𝐵 /su 𝐶)))
Theorem	divsassd 28269	An associative law for surreal division. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐶 ≠ 0s )    ⇒   ⊢ (𝜑 → ((𝐴 ·s 𝐵) /su 𝐶) = (𝐴 ·s (𝐵 /su 𝐶)))
Theorem	divmuldivsd 28270	Multiplication of two surreal ratios. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐷 ∈ No )    &   ⊢ (𝜑 → 𝐵 ≠ 0s )    &   ⊢ (𝜑 → 𝐷 ≠ 0s )    ⇒   ⊢ (𝜑 → ((𝐴 /su 𝐵) ·s (𝐶 /su 𝐷)) = ((𝐴 ·s 𝐶) /su (𝐵 ·s 𝐷)))
Theorem	divdivs1d 28271	Surreal division into a fraction. (Contributed by Scott Fenton, 7-Aug-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐵 ≠ 0s )    &   ⊢ (𝜑 → 𝐶 ≠ 0s )    ⇒   ⊢ (𝜑 → ((𝐴 /su 𝐵) /su 𝐶) = (𝐴 /su (𝐵 ·s 𝐶)))
Theorem	divsrecd 28272	Relationship between surreal division and reciprocal. (Contributed by Scott Fenton, 13-Aug-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐵 ≠ 0s )    ⇒   ⊢ (𝜑 → (𝐴 /su 𝐵) = (𝐴 ·s ( 1s /su 𝐵)))
Theorem	divsdird 28273	Distribution of surreal division over addition. (Contributed by Scott Fenton, 13-Aug-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐶 ≠ 0s )    ⇒   ⊢ (𝜑 → ((𝐴 +s 𝐵) /su 𝐶) = ((𝐴 /su 𝐶) +s (𝐵 /su 𝐶)))
Theorem	divscan3d 28274	A cancellation law for surreal division. (Contributed by Scott Fenton, 13-Aug-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐵 ≠ 0s )    ⇒   ⊢ (𝜑 → ((𝐵 ·s 𝐴) /su 𝐵) = 𝐴)
15.5.5  Absolute value
Syntax	cabss 28275	Declare the syntax for surreal absolute value.
class abss
Definition	df-abss 28276	Define the surreal absolute value function. See abssval 28277 for its value and absscl 28278 for its closure. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ abss = (𝑥 ∈ No ↦ if( 0s ≤s 𝑥, 𝑥, ( -us ‘𝑥)))
Theorem	abssval 28277	The value of surreal absolute value. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝐴 ∈ No → (abss‘𝐴) = if( 0s ≤s 𝐴, 𝐴, ( -us ‘𝐴)))
Theorem	absscl 28278	Closure law for surreal absolute value. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝐴 ∈ No → (abss‘𝐴) ∈ No )
Theorem	abssid 28279	The absolute value of a non-negative surreal is itself. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ ((𝐴 ∈ No ∧ 0s ≤s 𝐴) → (abss‘𝐴) = 𝐴)
Theorem	abs0s 28280	The absolute value of surreal zero. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (abss‘ 0s ) = 0s
Theorem	abssnid 28281	For a negative surreal, its absolute value is its negation. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐴 ≤s 0s ) → (abss‘𝐴) = ( -us ‘𝐴))
Theorem	absmuls 28282	Surreal absolute value distributes over multiplication. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (abss‘(𝐴 ·s 𝐵)) = ((abss‘𝐴) ·s (abss‘𝐵)))
Theorem	abssge0 28283	The absolute value of a surreal number is non-negative. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝐴 ∈ No → 0s ≤s (abss‘𝐴))
Theorem	abssor 28284	The absolute value of a surreal is either that surreal or its negative. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝐴 ∈ No → ((abss‘𝐴) = 𝐴 ∨ (abss‘𝐴) = ( -us ‘𝐴)))
Theorem	abssneg 28285	Surreal absolute value of the negative. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝐴 ∈ No → (abss‘( -us ‘𝐴)) = (abss‘𝐴))
Theorem	sleabs 28286	A surreal is less than or equal to its absolute value. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝐴 ∈ No → 𝐴 ≤s (abss‘𝐴))
Theorem	absslt 28287	Surreal absolute value and less-than relation. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → ((abss‘𝐴) <s 𝐵 ↔ (( -us ‘𝐵) <s 𝐴 ∧ 𝐴 <s 𝐵)))
15.6  Subsystems of surreals
15.6.1  Ordinal numbers
Syntax	cons 28288	Declare the syntax for surreal ordinals.
class Ons
Definition	df-ons 28289	Define the surreal ordinals. These are the maximum members of each generation of surreals. Variant of definition from [Conway] p. 27. (Contributed by Scott Fenton, 18-Mar-2025.)
⊢ Ons = {𝑥 ∈ No ∣ ( R ‘𝑥) = ∅}
Theorem	elons 28290	Membership in the class of surreal ordinals. (Contributed by Scott Fenton, 18-Mar-2025.)
⊢ (𝐴 ∈ Ons ↔ (𝐴 ∈ No ∧ ( R ‘𝐴) = ∅))
Theorem	onssno 28291	The surreal ordinals are a subclass of the surreals. (Contributed by Scott Fenton, 18-Mar-2025.)
⊢ Ons ⊆ No
Theorem	onsno 28292	A surreal ordinal is a surreal. (Contributed by Scott Fenton, 18-Mar-2025.)
⊢ (𝐴 ∈ Ons → 𝐴 ∈ No )
Theorem	0ons 28293	Surreal zero is a surreal ordinal. (Contributed by Scott Fenton, 18-Mar-2025.)
⊢ 0s ∈ Ons
Theorem	1ons 28294	Surreal one is a surreal ordinal. (Contributed by Scott Fenton, 18-Mar-2025.)
⊢ 1s ∈ Ons
Theorem	elons2 28295*	A surreal is ordinal iff it is the cut of some set of surreals and the empty set. Definition from [Conway] p. 27. (Contributed by Scott Fenton, 19-Mar-2025.)
⊢ (𝐴 ∈ Ons ↔ ∃𝑎 ∈ 𝒫 No 𝐴 = (𝑎 |s ∅))
Theorem	elons2d 28296	The cut of any set of surreals and the empty set is a surreal ordinal. (Contributed by Scott Fenton, 19-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ⊆ No )    &   ⊢ (𝜑 → 𝑋 = (𝐴 |s ∅))    ⇒   ⊢ (𝜑 → 𝑋 ∈ Ons)
Theorem	sltonold 28297*	The class of ordinals less than any surreal is a subset of that surreal's old set. (Contributed by Scott Fenton, 22-Mar-2025.)
⊢ (𝐴 ∈ No → {𝑥 ∈ Ons ∣ 𝑥 <s 𝐴} ⊆ ( O ‘( bday ‘𝐴)))
Theorem	sltonex 28298*	The class of ordinals less than any particular surreal is a set. Theorem 14 of [Conway] p. 27. (Contributed by Scott Fenton, 22-Mar-2025.)
⊢ (𝐴 ∈ No → {𝑥 ∈ Ons ∣ 𝑥 <s 𝐴} ∈ V)
Theorem	onscutleft 28299	A surreal ordinal is equal to the cut of its left set and the empty set. (Contributed by Scott Fenton, 29-Mar-2025.)
⊢ (𝐴 ∈ Ons → 𝐴 = (( L ‘𝐴) |s ∅))
Theorem	onaddscl 28300	The surreal ordinals are closed under addition. (Contributed by Scott Fenton, 22-Aug-2025.)
⊢ ((𝐴 ∈ Ons ∧ 𝐵 ∈ Ons) → (𝐴 +s 𝐵) ∈ Ons)