P. 285 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28401-28500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	addsgt0d 28401	The sum of two positive surreals is positive. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 0s <s 𝐴)    &   ⊢ (𝜑 → 0s <s 𝐵)    ⇒   ⊢ (𝜑 → 0s <s (𝐴 +s 𝐵))
Theorem	ltsp1d 28402	A surreal is less than itself plus one. (Contributed by Scott Fenton, 13-Aug-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    ⇒   ⊢ (𝜑 → 𝐴 <s (𝐴 +s 1s ))
Theorem	addsge01d 28403	A surreal is less-than or equal to itself plus a non-negative surreal. (Contributed by Scott Fenton, 24-Feb-2026.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    ⇒   ⊢ (𝜑 → ( 0s ≤s 𝐵 ↔ 𝐴 ≤s (𝐴 +s 𝐵)))
Theorem	addbdaylem 28404*	Lemma for addbday 28405. (Contributed by Scott Fenton, 13-Aug-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → ∀𝑦𝑂 ∈ ((L‘𝐵) ∪ (R‘𝐵))(bday‘(𝐴 +s 𝑦𝑂)) ⊆ ((bday‘𝐴) +no (bday‘𝑦𝑂)))    &   ⊢ 𝑆 ⊆ ((L‘𝐵) ∪ (R‘𝐵))    ⇒   ⊢ (𝜑 → (bday “ {𝑧 ∣ ∃𝑦𝐿 ∈ 𝑆 𝑧 = (𝐴 +s 𝑦𝐿)}) ⊆ ((bday‘𝐴) +no (bday‘𝐵)))
Theorem	addbday 28405	The birthday of the sum of two surreals is less than or equal to the natural ordinal sum of their individual birthdays. Theorem 6.1 of [Gonshor] p. 95. (Contributed by Scott Fenton, 12-Aug-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No) → (bday‘(𝐴 +s 𝐵)) ⊆ ((bday‘𝐴) +no (bday‘𝐵)))
15.5.2  Negation and Subtraction
Syntax	cnegs 28406	Declare the syntax for surreal negation.
class -s
Syntax	csubs 28407	Declare the syntax for surreal subtraction.
class −s
Definition	df-negs 28408*	Define surreal negation. Definition from [Conway] p. 5. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ -s = norec ((𝑥 ∈ V, 𝑛 ∈ V ↦ ((𝑛 “ (R‘𝑥)) |s (𝑛 “ (L‘𝑥)))))
Definition	df-subs 28409*	Define surreal subtraction. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ −s = (𝑥 ∈ No, 𝑦 ∈ No ↦ (𝑥 +s ( -s‘𝑦)))
Theorem	negsfn 28410	Surreal negation is a function over surreals. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ -s Fn No
Theorem	subsfn 28411	Surreal subtraction is a function over pairs of surreals. (Contributed by Scott Fenton, 22-Jan-2025.)
⊢ −s Fn (No × No)
Theorem	negsval 28412	The value of the surreal negation function. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ (𝐴 ∈ No → ( -s‘𝐴) = (( -s “ (R‘𝐴)) |s ( -s “ (L‘𝐴))))
Theorem	neg0s 28413	Negative surreal zero is surreal zero. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ ( -s‘ 0s ) = 0s
Theorem	neg1s 28414	An expression for negative surreal one. (Contributed by Scott Fenton, 24-Jul-2025.)
⊢ ( -s‘ 1s ) = (∅ |s { 0s })
Theorem	negsproplem1 28415*	Lemma for surreal negation. We prove a pair of properties of surreal negation simultaneously. First, we instantiate some quantifiers. (Contributed by Scott Fenton, 2-Feb-2025.)
⊢ (𝜑 → ∀𝑥 ∈ No ∀𝑦 ∈ No (((bday‘𝑥) ∪ (bday‘𝑦)) ∈ ((bday‘𝐴) ∪ (bday‘𝐵)) → (( -s‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -s‘𝑦) <s ( -s‘𝑥)))))    &   ⊢ (𝜑 → 𝑋 ∈ No)    &   ⊢ (𝜑 → 𝑌 ∈ No)    &   ⊢ (𝜑 → ((bday‘𝑋) ∪ (bday‘𝑌)) ∈ ((bday‘𝐴) ∪ (bday‘𝐵)))    ⇒   ⊢ (𝜑 → (( -s‘𝑋) ∈ No ∧ (𝑋 <s 𝑌 → ( -s‘𝑌) <s ( -s‘𝑋))))
Theorem	negsproplem2 28416*	Lemma for surreal negation. Show that the cut that defines negation is legitimate. (Contributed by Scott Fenton, 2-Feb-2025.)
⊢ (𝜑 → ∀𝑥 ∈ No ∀𝑦 ∈ No (((bday‘𝑥) ∪ (bday‘𝑦)) ∈ ((bday‘𝐴) ∪ (bday‘𝐵)) → (( -s‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -s‘𝑦) <s ( -s‘𝑥)))))    &   ⊢ (𝜑 → 𝐴 ∈ No)    ⇒   ⊢ (𝜑 → ( -s “ (R‘𝐴)) <<s ( -s “ (L‘𝐴)))
Theorem	negsproplem3 28417*	Lemma for surreal negation. Give the cut properties of surreal negation. (Contributed by Scott Fenton, 2-Feb-2025.)
⊢ (𝜑 → ∀𝑥 ∈ No ∀𝑦 ∈ No (((bday‘𝑥) ∪ (bday‘𝑦)) ∈ ((bday‘𝐴) ∪ (bday‘𝐵)) → (( -s‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -s‘𝑦) <s ( -s‘𝑥)))))    &   ⊢ (𝜑 → 𝐴 ∈ No)    ⇒   ⊢ (𝜑 → (( -s‘𝐴) ∈ No ∧ ( -s “ (R‘𝐴)) <<s {( -s‘𝐴)} ∧ {( -s‘𝐴)} <<s ( -s “ (L‘𝐴))))
Theorem	negsproplem4 28418*	Lemma for surreal negation. Show the second half of the inductive hypothesis when 𝐴 is simpler than 𝐵. (Contributed by Scott Fenton, 2-Feb-2025.)
⊢ (𝜑 → ∀𝑥 ∈ No ∀𝑦 ∈ No (((bday‘𝑥) ∪ (bday‘𝑦)) ∈ ((bday‘𝐴) ∪ (bday‘𝐵)) → (( -s‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -s‘𝑦) <s ( -s‘𝑥)))))    &   ⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐴 <s 𝐵)    &   ⊢ (𝜑 → (bday‘𝐴) ∈ (bday‘𝐵))    ⇒   ⊢ (𝜑 → ( -s‘𝐵) <s ( -s‘𝐴))
Theorem	negsproplem5 28419*	Lemma for surreal negation. Show the second half of the inductive hypothesis when 𝐵 is simpler than 𝐴. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝜑 → ∀𝑥 ∈ No ∀𝑦 ∈ No (((bday‘𝑥) ∪ (bday‘𝑦)) ∈ ((bday‘𝐴) ∪ (bday‘𝐵)) → (( -s‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -s‘𝑦) <s ( -s‘𝑥)))))    &   ⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐴 <s 𝐵)    &   ⊢ (𝜑 → (bday‘𝐵) ∈ (bday‘𝐴))    ⇒   ⊢ (𝜑 → ( -s‘𝐵) <s ( -s‘𝐴))
Theorem	negsproplem6 28420*	Lemma for surreal negation. Show the second half of the inductive hypothesis when 𝐴 is the same age as 𝐵. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝜑 → ∀𝑥 ∈ No ∀𝑦 ∈ No (((bday‘𝑥) ∪ (bday‘𝑦)) ∈ ((bday‘𝐴) ∪ (bday‘𝐵)) → (( -s‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -s‘𝑦) <s ( -s‘𝑥)))))    &   ⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐴 <s 𝐵)    &   ⊢ (𝜑 → (bday‘𝐴) = (bday‘𝐵))    ⇒   ⊢ (𝜑 → ( -s‘𝐵) <s ( -s‘𝐴))
Theorem	negsproplem7 28421*	Lemma for surreal negation. Show the second half of the inductive hypothesis unconditionally. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝜑 → ∀𝑥 ∈ No ∀𝑦 ∈ No (((bday‘𝑥) ∪ (bday‘𝑦)) ∈ ((bday‘𝐴) ∪ (bday‘𝐵)) → (( -s‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -s‘𝑦) <s ( -s‘𝑥)))))    &   ⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐴 <s 𝐵)    ⇒   ⊢ (𝜑 → ( -s‘𝐵) <s ( -s‘𝐴))
Theorem	negsprop 28422	Show closure and ordering properties of negation. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No) → (( -s‘𝐴) ∈ No ∧ (𝐴 <s 𝐵 → ( -s‘𝐵) <s ( -s‘𝐴))))
Theorem	negscl 28423	The surreals are closed under negation. Theorem 6(ii) of [Conway] p. 18. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝐴 ∈ No → ( -s‘𝐴) ∈ No)
Theorem	negscld 28424	The surreals are closed under negation. Theorem 6(ii) of [Conway] p. 18. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    ⇒   ⊢ (𝜑 → ( -s‘𝐴) ∈ No)
Theorem	ltnegsim 28425	The forward direction of the ordering properties of negation. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No) → (𝐴 <s 𝐵 → ( -s‘𝐵) <s ( -s‘𝐴)))
Theorem	negcut 28426	The cut properties of surreal negation. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝐴 ∈ No → (( -s‘𝐴) ∈ No ∧ ( -s “ (R‘𝐴)) <<s {( -s‘𝐴)} ∧ {( -s‘𝐴)} <<s ( -s “ (L‘𝐴))))
Theorem	negcut2 28427	The cut that defines surreal negation is legitimate. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝐴 ∈ No → ( -s “ (R‘𝐴)) <<s ( -s “ (L‘𝐴)))
Theorem	negsid 28428	Surreal addition of a number and its negative. Theorem 4(iii) of [Conway] p. 17. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝐴 ∈ No → (𝐴 +s ( -s‘𝐴)) = 0s )
Theorem	negsidd 28429	Surreal addition of a number and its negative. Theorem 4(iii) of [Conway] p. 17. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    ⇒   ⊢ (𝜑 → (𝐴 +s ( -s‘𝐴)) = 0s )
Theorem	negsex 28430*	Every surreal has a negative. Note that this theorem, addscl 28368, addscom 28353, addsass 28392, addsrid 28351, and ltadds1im 28372 are the ordered Abelian group axioms. However, the surreals cannot be said to be an ordered Abelian group because No is a proper class. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝐴 ∈ No → ∃𝑥 ∈ No (𝐴 +s 𝑥) = 0s )
Theorem	negnegs 28431	A surreal is equal to the negative of its negative. Theorem 4(ii) of [Conway] p. 17. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝐴 ∈ No → ( -s‘( -s‘𝐴)) = 𝐴)
Theorem	ltnegs 28432	Negative of both sides of surreal less-than. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No) → (𝐴 <s 𝐵 ↔ ( -s‘𝐵) <s ( -s‘𝐴)))
Theorem	lenegs 28433	Negative of both sides of surreal less-than or equal. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No) → (𝐴 ≤s 𝐵 ↔ ( -s‘𝐵) ≤s ( -s‘𝐴)))
Theorem	ltnegsd 28434	Negative of both sides of surreal less-than. (Contributed by Scott Fenton, 14-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ ( -s‘𝐵) <s ( -s‘𝐴)))
Theorem	lenegsd 28435	Negative of both sides of surreal less-than or equal. (Contributed by Scott Fenton, 14-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    ⇒   ⊢ (𝜑 → (𝐴 ≤s 𝐵 ↔ ( -s‘𝐵) ≤s ( -s‘𝐴)))
Theorem	negs11 28436	Surreal negation is one-to-one. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No) → (( -s‘𝐴) = ( -s‘𝐵) ↔ 𝐴 = 𝐵))
Theorem	negsdi 28437	Distribution of surreal negative over addition. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No) → ( -s‘(𝐴 +s 𝐵)) = (( -s‘𝐴) +s ( -s‘𝐵)))
Theorem	lt0negs2d 28438	Comparison of a surreal and its negative to zero. (Contributed by Scott Fenton, 10-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    ⇒   ⊢ (𝜑 → ( 0s <s 𝐴 ↔ ( -s‘𝐴) <s 0s ))
Theorem	negsf 28439	Function statement for surreal negation. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ -s:No⟶No
Theorem	negsfo 28440	Function statement for surreal negation. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ -s:No–onto→No
Theorem	negsf1o 28441	Surreal negation is a bijection. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ -s:No–1-1-onto→No
Theorem	negsunif 28442	Uniformity property for surreal negation. If 𝐿 and 𝑅 are any cut that represents 𝐴, then they may be used instead of (L‘𝐴) and (R‘𝐴) in the definition of negation. (Contributed by Scott Fenton, 14-Feb-2025.)
⊢ (𝜑 → 𝐿 <<s 𝑅)    &   ⊢ (𝜑 → 𝐴 = (𝐿 |s 𝑅))    ⇒   ⊢ (𝜑 → ( -s‘𝐴) = (( -s “ 𝑅) |s ( -s “ 𝐿)))
Theorem	negbdaylem 28443	Lemma for negbday 28444. Bound the birthday of the negative of a surreal number above. (Contributed by Scott Fenton, 8-Mar-2025.)
⊢ (𝐴 ∈ No → (bday‘( -s‘𝐴)) ⊆ (bday‘𝐴))
Theorem	negbday 28444	Negation of a surreal number preserves birthday. (Contributed by Scott Fenton, 8-Mar-2025.)
⊢ (𝐴 ∈ No → (bday‘( -s‘𝐴)) = (bday‘𝐴))
Theorem	negleft 28445	The left set of the negative of a surreal is the set of negatives of its right set. (Contributed by Scott Fenton, 21-Feb-2026.)
⊢ (𝐴 ∈ No → (L‘( -s‘𝐴)) = ( -s “ (R‘𝐴)))
Theorem	negright 28446	The right set of the negative of a surreal is the set of negatives of its left set. (Contributed by Scott Fenton, 21-Feb-2026.)
⊢ (𝐴 ∈ No → (R‘( -s‘𝐴)) = ( -s “ (L‘𝐴)))
Theorem	subsval 28447	The value of surreal subtraction. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No) → (𝐴 −s 𝐵) = (𝐴 +s ( -s‘𝐵)))
Theorem	subsvald 28448	The value of surreal subtraction. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    ⇒   ⊢ (𝜑 → (𝐴 −s 𝐵) = (𝐴 +s ( -s‘𝐵)))
Theorem	subscl 28449	Closure law for surreal subtraction. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No) → (𝐴 −s 𝐵) ∈ No)
Theorem	subscld 28450	Closure law for surreal subtraction. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    ⇒   ⊢ (𝜑 → (𝐴 −s 𝐵) ∈ No)
Theorem	subsf 28451	Function statement for surreal subtraction. (Contributed by Scott Fenton, 17-May-2025.)
⊢ −s :(No × No)⟶No
Theorem	subsfo 28452	Surreal subtraction is an onto function. (Contributed by Scott Fenton, 17-May-2025.)
⊢ −s :(No × No)–onto→No
Theorem	negsval2 28453	Surreal negation in terms of subtraction. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ No → ( -s‘𝐴) = ( 0s −s 𝐴))
Theorem	negsval2d 28454	Surreal negation in terms of subtraction. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    ⇒   ⊢ (𝜑 → ( -s‘𝐴) = ( 0s −s 𝐴))
Theorem	subsid1 28455	Identity law for subtraction. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝐴 ∈ No → (𝐴 −s 0s ) = 𝐴)
Theorem	subsid 28456	Subtraction of a surreal from itself. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝐴 ∈ No → (𝐴 −s 𝐴) = 0s )
Theorem	subadds 28457	Relationship between addition and subtraction for surreals. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No) → ((𝐴 −s 𝐵) = 𝐶 ↔ (𝐵 +s 𝐶) = 𝐴))
Theorem	subaddsd 28458	Relationship between addition and subtraction for surreals. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    ⇒   ⊢ (𝜑 → ((𝐴 −s 𝐵) = 𝐶 ↔ (𝐵 +s 𝐶) = 𝐴))
Theorem	pncans 28459	Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No) → ((𝐴 +s 𝐵) −s 𝐵) = 𝐴)
Theorem	pncan3s 28460	Subtraction and addition of equals. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No) → (𝐴 +s (𝐵 −s 𝐴)) = 𝐵)
Theorem	pncan2s 28461	Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No) → ((𝐴 +s 𝐵) −s 𝐴) = 𝐵)
Theorem	npcans 28462	Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No) → ((𝐴 −s 𝐵) +s 𝐵) = 𝐴)
Theorem	ltsubs1 28463	Subtraction from both sides of surreal less-than. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No) → (𝐴 <s 𝐵 ↔ (𝐴 −s 𝐶) <s (𝐵 −s 𝐶)))
Theorem	ltsubs2 28464	Subtraction from both sides of surreal less-than. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No) → (𝐴 <s 𝐵 ↔ (𝐶 −s 𝐵) <s (𝐶 −s 𝐴)))
Theorem	ltsubs1d 28465	Subtraction from both sides of surreal less-than. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ (𝐴 −s 𝐶) <s (𝐵 −s 𝐶)))
Theorem	ltsubs2d 28466	Subtraction from both sides of surreal less-than. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ (𝐶 −s 𝐵) <s (𝐶 −s 𝐴)))
Theorem	negsubsdi2d 28467	Distribution of negative over subtraction. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    ⇒   ⊢ (𝜑 → ( -s‘(𝐴 −s 𝐵)) = (𝐵 −s 𝐴))
Theorem	addsubsassd 28468	Associative-type law for surreal addition and subtraction. (Contributed by Scott Fenton, 6-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    ⇒   ⊢ (𝜑 → ((𝐴 +s 𝐵) −s 𝐶) = (𝐴 +s (𝐵 −s 𝐶)))
Theorem	addsubsd 28469	Law for surreal addition and subtraction. (Contributed by Scott Fenton, 4-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    ⇒   ⊢ (𝜑 → ((𝐴 +s 𝐵) −s 𝐶) = ((𝐴 −s 𝐶) +s 𝐵))
Theorem	ltsubsubsbd 28470	Equivalence for the surreal less-than relationship between differences. (Contributed by Scott Fenton, 6-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    &   ⊢ (𝜑 → 𝐷 ∈ No)    ⇒   ⊢ (𝜑 → ((𝐴 −s 𝐶) <s (𝐵 −s 𝐷) ↔ (𝐴 −s 𝐵) <s (𝐶 −s 𝐷)))
Theorem	ltsubsubs2bd 28471	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	ltsubsubs3bd 28472	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 28473	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 28474	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 28475	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 28476	Surreal less-than relationship between subtraction and addition. (Contributed by Scott Fenton, 27-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    ⇒   ⊢ (𝜑 → ((𝐴 −s 𝐵) <s 𝐶 ↔ 𝐴 <s (𝐶 +s 𝐵)))
Theorem	ltsubadds2d 28477	Surreal less-than relationship between subtraction and addition. (Contributed by Scott Fenton, 27-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    ⇒   ⊢ (𝜑 → ((𝐴 −s 𝐵) <s 𝐶 ↔ 𝐴 <s (𝐵 +s 𝐶)))
Theorem	ltaddsubsd 28478	Surreal less-than relationship between subtraction and addition. (Contributed by Scott Fenton, 28-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    ⇒   ⊢ (𝜑 → ((𝐴 +s 𝐵) <s 𝐶 ↔ 𝐴 <s (𝐶 −s 𝐵)))
Theorem	ltaddsubs2d 28479	Surreal less-than relationship between subtraction and addition. (Contributed by Scott Fenton, 28-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    ⇒   ⊢ (𝜑 → ((𝐴 +s 𝐵) <s 𝐶 ↔ 𝐵 <s (𝐶 −s 𝐴)))
Theorem	lesubaddsd 28480	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 28481	Law for double surreal subtraction. (Contributed by Scott Fenton, 9-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    ⇒   ⊢ (𝜑 → ((𝐴 −s 𝐵) −s 𝐶) = (𝐴 −s (𝐵 +s 𝐶)))
Theorem	subsubs2d 28482	Law for double surreal subtraction. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    ⇒   ⊢ (𝜑 → (𝐴 −s (𝐵 −s 𝐶)) = (𝐴 +s (𝐶 −s 𝐵)))
Theorem	lesubsd 28483	Swap subtrahends in a surreal inequality. (Contributed by Scott Fenton, 29-Jan-2026.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    ⇒   ⊢ (𝜑 → (𝐴 ≤s (𝐵 −s 𝐶) ↔ 𝐶 ≤s (𝐵 −s 𝐴)))
Theorem	nncansd 28484	Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    ⇒   ⊢ (𝜑 → (𝐴 −s (𝐴 −s 𝐵)) = 𝐵)
Theorem	posdifsd 28485	Comparison of two surreals whose difference is positive. (Contributed by Scott Fenton, 10-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ 0s <s (𝐵 −s 𝐴)))
Theorem	ltsubsposd 28486	Subtraction of a positive number decreases the sum. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    ⇒   ⊢ (𝜑 → ( 0s <s 𝐴 ↔ (𝐵 −s 𝐴) <s 𝐵))
Theorem	subsge0d 28487	Non-negative subtraction. (Contributed by Scott Fenton, 26-May-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    ⇒   ⊢ (𝜑 → ( 0s ≤s (𝐴 −s 𝐵) ↔ 𝐵 ≤s 𝐴))
Theorem	addsubs4d 28488	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 28489	A surreal is greater than itself minus one. (Contributed by Scott Fenton, 20-Aug-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    ⇒   ⊢ (𝜑 → (𝐴 −s 1s ) <s 𝐴)
Theorem	subscan1d 28490	Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    ⇒   ⊢ (𝜑 → ((𝐶 −s 𝐴) = (𝐶 −s 𝐵) ↔ 𝐴 = 𝐵))
Theorem	subscan2d 28491	Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ No)    &   ⊢ (𝜑 → 𝐵 ∈ No)    &   ⊢ (𝜑 → 𝐶 ∈ No)    ⇒   ⊢ (𝜑 → ((𝐴 −s 𝐶) = (𝐵 −s 𝐶) ↔ 𝐴 = 𝐵))
Theorem	subseq0d 28492	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 28493	Set up the syntax for surreal multiplication.
class ·s
Definition	df-muls 28494*	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 28495	Surreal multiplication is a function over surreals. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ·s Fn (No × No)
Theorem	mulsval 28496*	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 28497*	Lemma for mulsval2 28498. 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 28498*	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 28499	Surreal multiplication by zero. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ (𝐴 ∈ No → (𝐴 ·s 0s ) = 0s )
Theorem	mulsrid 28500	Surreal one is a right identity element for multiplication. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ (𝐴 ∈ No → (𝐴 ·s 1s ) = 𝐴)