P. 281 of Theorem List - Metamath Proof Explorer

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

Type	Label	Description
Statement
Theorem	adds4d 28001	Rearrangement of four terms in a surreal sum. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐷 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 +s 𝐵) +s (𝐶 +s 𝐷)) = ((𝐴 +s 𝐶) +s (𝐵 +s 𝐷)))
Theorem	adds42d 28002	Rearrangement of four terms in a surreal sum. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐷 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 +s 𝐵) +s (𝐶 +s 𝐷)) = ((𝐴 +s 𝐶) +s (𝐷 +s 𝐵)))
Theorem	ltaddspos1d 28003	Addition of a positive number increases the sum. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → ( 0s <s 𝐴 ↔ 𝐵 <s (𝐵 +s 𝐴)))
Theorem	ltaddspos2d 28004	Addition of a positive number increases the sum. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → ( 0s <s 𝐴 ↔ 𝐵 <s (𝐴 +s 𝐵)))
Theorem	lt2addsd 28005	Adding both sides of two surreal less-than relations. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐷 ∈ No )    &   ⊢ (𝜑 → 𝐴 <s 𝐶)    &   ⊢ (𝜑 → 𝐵 <s 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 +s 𝐵) <s (𝐶 +s 𝐷))
Theorem	addsgt0d 28006	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 28007	A surreal is less than itself plus one. (Contributed by Scott Fenton, 13-Aug-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    ⇒   ⊢ (𝜑 → 𝐴 <s (𝐴 +s 1s ))
Theorem	addsge01d 28008	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 28009*	Lemma for addbday 28010. (Contributed by Scott Fenton, 13-Aug-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))( bday ‘(𝐴 +s 𝑦𝑂)) ⊆ (( bday ‘𝐴) +no ( bday ‘𝑦𝑂)))    &   ⊢ 𝑆 ⊆ (( L ‘𝐵) ∪ ( R ‘𝐵))    ⇒   ⊢ (𝜑 → ( bday “ {𝑧 ∣ ∃𝑦𝐿 ∈ 𝑆 𝑧 = (𝐴 +s 𝑦𝐿)}) ⊆ (( bday ‘𝐴) +no ( bday ‘𝐵)))
Theorem	addbday 28010	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 28011	Declare the syntax for surreal negation.
class -us
Syntax	csubs 28012	Declare the syntax for surreal subtraction.
class -s
Definition	df-negs 28013*	Define surreal negation. Definition from [Conway] p. 5. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ -us = norec ((𝑥 ∈ V, 𝑛 ∈ V ↦ ((𝑛 “ ( R ‘𝑥)) |s (𝑛 “ ( L ‘𝑥)))))
Definition	df-subs 28014*	Define surreal subtraction. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ -s = (𝑥 ∈ No , 𝑦 ∈ No ↦ (𝑥 +s ( -us ‘𝑦)))
Theorem	negsfn 28015	Surreal negation is a function over surreals. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ -us Fn No
Theorem	subsfn 28016	Surreal subtraction is a function over pairs of surreals. (Contributed by Scott Fenton, 22-Jan-2025.)
⊢ -s Fn ( No × No )
Theorem	negsval 28017	The value of the surreal negation function. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ (𝐴 ∈ No → ( -us ‘𝐴) = (( -us “ ( R ‘𝐴)) |s ( -us “ ( L ‘𝐴))))
Theorem	neg0s 28018	Negative surreal zero is surreal zero. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ ( -us ‘ 0s ) = 0s
Theorem	neg1s 28019	An expression for negative surreal one. (Contributed by Scott Fenton, 24-Jul-2025.)
⊢ ( -us ‘ 1s ) = (∅ |s { 0s })
Theorem	negsproplem1 28020*	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 ‘𝐵)) → (( -us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥)))))    &   ⊢ (𝜑 → 𝑋 ∈ No )    &   ⊢ (𝜑 → 𝑌 ∈ No )    &   ⊢ (𝜑 → (( bday ‘𝑋) ∪ ( bday ‘𝑌)) ∈ (( bday ‘𝐴) ∪ ( bday ‘𝐵)))    ⇒   ⊢ (𝜑 → (( -us ‘𝑋) ∈ No ∧ (𝑋 <s 𝑌 → ( -us ‘𝑌) <s ( -us ‘𝑋))))
Theorem	negsproplem2 28021*	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 ‘𝐵)) → (( -us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥)))))    &   ⊢ (𝜑 → 𝐴 ∈ No )    ⇒   ⊢ (𝜑 → ( -us “ ( R ‘𝐴)) <<s ( -us “ ( L ‘𝐴)))
Theorem	negsproplem3 28022*	Lemma for surreal negation. Give the cut properties of surreal negation. (Contributed by Scott Fenton, 2-Feb-2025.)
⊢ (𝜑 → ∀𝑥 ∈ No ∀𝑦 ∈ No ((( bday ‘𝑥) ∪ ( bday ‘𝑦)) ∈ (( bday ‘𝐴) ∪ ( bday ‘𝐵)) → (( -us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥)))))    &   ⊢ (𝜑 → 𝐴 ∈ No )    ⇒   ⊢ (𝜑 → (( -us ‘𝐴) ∈ No ∧ ( -us “ ( R ‘𝐴)) <<s {( -us ‘𝐴)} ∧ {( -us ‘𝐴)} <<s ( -us “ ( L ‘𝐴))))
Theorem	negsproplem4 28023*	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 ‘𝐵)) → (( -us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥)))))    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐴 <s 𝐵)    &   ⊢ (𝜑 → ( bday ‘𝐴) ∈ ( bday ‘𝐵))    ⇒   ⊢ (𝜑 → ( -us ‘𝐵) <s ( -us ‘𝐴))
Theorem	negsproplem5 28024*	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 ‘𝐵)) → (( -us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥)))))    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐴 <s 𝐵)    &   ⊢ (𝜑 → ( bday ‘𝐵) ∈ ( bday ‘𝐴))    ⇒   ⊢ (𝜑 → ( -us ‘𝐵) <s ( -us ‘𝐴))
Theorem	negsproplem6 28025*	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 ‘𝐵)) → (( -us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥)))))    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐴 <s 𝐵)    &   ⊢ (𝜑 → ( bday ‘𝐴) = ( bday ‘𝐵))    ⇒   ⊢ (𝜑 → ( -us ‘𝐵) <s ( -us ‘𝐴))
Theorem	negsproplem7 28026*	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 ‘𝐵)) → (( -us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥)))))    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐴 <s 𝐵)    ⇒   ⊢ (𝜑 → ( -us ‘𝐵) <s ( -us ‘𝐴))
Theorem	negsprop 28027	Show closure and ordering properties of negation. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (( -us ‘𝐴) ∈ No ∧ (𝐴 <s 𝐵 → ( -us ‘𝐵) <s ( -us ‘𝐴))))
Theorem	negscl 28028	The surreals are closed under negation. Theorem 6(ii) of [Conway] p. 18. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝐴 ∈ No → ( -us ‘𝐴) ∈ No )
Theorem	negscld 28029	The surreals are closed under negation. Theorem 6(ii) of [Conway] p. 18. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    ⇒   ⊢ (𝜑 → ( -us ‘𝐴) ∈ No )
Theorem	ltnegsim 28030	The forward direction of the ordering properties of negation. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 → ( -us ‘𝐵) <s ( -us ‘𝐴)))
Theorem	negcut 28031	The cut properties of surreal negation. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝐴 ∈ No → (( -us ‘𝐴) ∈ No ∧ ( -us “ ( R ‘𝐴)) <<s {( -us ‘𝐴)} ∧ {( -us ‘𝐴)} <<s ( -us “ ( L ‘𝐴))))
Theorem	negcut2 28032	The cut that defines surreal negation is legitimate. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝐴 ∈ No → ( -us “ ( R ‘𝐴)) <<s ( -us “ ( L ‘𝐴)))
Theorem	negsid 28033	Surreal addition of a number and its negative. Theorem 4(iii) of [Conway] p. 17. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝐴 ∈ No → (𝐴 +s ( -us ‘𝐴)) = 0s )
Theorem	negsidd 28034	Surreal addition of a number and its negative. Theorem 4(iii) of [Conway] p. 17. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 +s ( -us ‘𝐴)) = 0s )
Theorem	negsex 28035*	Every surreal has a negative. Note that this theorem, addscl 27973, addscom 27958, addsass 27997, addsrid 27956, and ltadds1im 27977 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 28036	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 → ( -us ‘( -us ‘𝐴)) = 𝐴)
Theorem	ltnegs 28037	Negative of both sides of surreal less-than. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 ↔ ( -us ‘𝐵) <s ( -us ‘𝐴)))
Theorem	lenegs 28038	Negative of both sides of surreal less-than or equal. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 ≤s 𝐵 ↔ ( -us ‘𝐵) ≤s ( -us ‘𝐴)))
Theorem	ltnegsd 28039	Negative of both sides of surreal less-than. (Contributed by Scott Fenton, 14-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ ( -us ‘𝐵) <s ( -us ‘𝐴)))
Theorem	lenegsd 28040	Negative of both sides of surreal less-than or equal. (Contributed by Scott Fenton, 14-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 ≤s 𝐵 ↔ ( -us ‘𝐵) ≤s ( -us ‘𝐴)))
Theorem	negs11 28041	Surreal negation is one-to-one. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (( -us ‘𝐴) = ( -us ‘𝐵) ↔ 𝐴 = 𝐵))
Theorem	negsdi 28042	Distribution of surreal negative over addition. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( -us ‘(𝐴 +s 𝐵)) = (( -us ‘𝐴) +s ( -us ‘𝐵)))
Theorem	lt0negs2d 28043	Comparison of a surreal and its negative to zero. (Contributed by Scott Fenton, 10-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    ⇒   ⊢ (𝜑 → ( 0s <s 𝐴 ↔ ( -us ‘𝐴) <s 0s ))
Theorem	negsf 28044	Function statement for surreal negation. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ -us : No ⟶ No
Theorem	negsfo 28045	Function statement for surreal negation. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ -us : No –onto→ No
Theorem	negsf1o 28046	Surreal negation is a bijection. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ -us : No –1-1-onto→ No
Theorem	negsunif 28047	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 𝑅))    ⇒   ⊢ (𝜑 → ( -us ‘𝐴) = (( -us “ 𝑅) |s ( -us “ 𝐿)))
Theorem	negbdaylem 28048	Lemma for negbday 28049. Bound the birthday of the negative of a surreal number above. (Contributed by Scott Fenton, 8-Mar-2025.)
⊢ (𝐴 ∈ No → ( bday ‘( -us ‘𝐴)) ⊆ ( bday ‘𝐴))
Theorem	negbday 28049	Negation of a surreal number preserves birthday. (Contributed by Scott Fenton, 8-Mar-2025.)
⊢ (𝐴 ∈ No → ( bday ‘( -us ‘𝐴)) = ( bday ‘𝐴))
Theorem	negleft 28050	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 ‘( -us ‘𝐴)) = ( -us “ ( R ‘𝐴)))
Theorem	negright 28051	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 ‘( -us ‘𝐴)) = ( -us “ ( L ‘𝐴)))
Theorem	subsval 28052	The value of surreal subtraction. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 -s 𝐵) = (𝐴 +s ( -us ‘𝐵)))
Theorem	subsvald 28053	The value of surreal subtraction. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 -s 𝐵) = (𝐴 +s ( -us ‘𝐵)))
Theorem	subscl 28054	Closure law for surreal subtraction. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 -s 𝐵) ∈ No )
Theorem	subscld 28055	Closure law for surreal subtraction. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 -s 𝐵) ∈ No )
Theorem	subsf 28056	Function statement for surreal subtraction. (Contributed by Scott Fenton, 17-May-2025.)
⊢ -s :( No × No )⟶ No
Theorem	subsfo 28057	Surreal subtraction is an onto function. (Contributed by Scott Fenton, 17-May-2025.)
⊢ -s :( No × No )–onto→ No
Theorem	negsval2 28058	Surreal negation in terms of subtraction. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ No → ( -us ‘𝐴) = ( 0s -s 𝐴))
Theorem	negsval2d 28059	Surreal negation in terms of subtraction. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    ⇒   ⊢ (𝜑 → ( -us ‘𝐴) = ( 0s -s 𝐴))
Theorem	subsid1 28060	Identity law for subtraction. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝐴 ∈ No → (𝐴 -s 0s ) = 𝐴)
Theorem	subsid 28061	Subtraction of a surreal from itself. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝐴 ∈ No → (𝐴 -s 𝐴) = 0s )
Theorem	subadds 28062	Relationship between addition and subtraction for surreals. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐴 -s 𝐵) = 𝐶 ↔ (𝐵 +s 𝐶) = 𝐴))
Theorem	subaddsd 28063	Relationship between addition and subtraction for surreals. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 -s 𝐵) = 𝐶 ↔ (𝐵 +s 𝐶) = 𝐴))
Theorem	pncans 28064	Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → ((𝐴 +s 𝐵) -s 𝐵) = 𝐴)
Theorem	pncan3s 28065	Subtraction and addition of equals. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 +s (𝐵 -s 𝐴)) = 𝐵)
Theorem	pncan2s 28066	Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → ((𝐴 +s 𝐵) -s 𝐴) = 𝐵)
Theorem	npcans 28067	Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → ((𝐴 -s 𝐵) +s 𝐵) = 𝐴)
Theorem	ltsubs1 28068	Subtraction from both sides of surreal less-than. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 <s 𝐵 ↔ (𝐴 -s 𝐶) <s (𝐵 -s 𝐶)))
Theorem	ltsubs2 28069	Subtraction from both sides of surreal less-than. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 <s 𝐵 ↔ (𝐶 -s 𝐵) <s (𝐶 -s 𝐴)))
Theorem	ltsubs1d 28070	Subtraction from both sides of surreal less-than. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ (𝐴 -s 𝐶) <s (𝐵 -s 𝐶)))
Theorem	ltsubs2d 28071	Subtraction from both sides of surreal less-than. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ (𝐶 -s 𝐵) <s (𝐶 -s 𝐴)))
Theorem	negsubsdi2d 28072	Distribution of negative over subtraction. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → ( -us ‘(𝐴 -s 𝐵)) = (𝐵 -s 𝐴))
Theorem	addsubsassd 28073	Associative-type law for surreal addition and subtraction. (Contributed by Scott Fenton, 6-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 +s 𝐵) -s 𝐶) = (𝐴 +s (𝐵 -s 𝐶)))
Theorem	addsubsd 28074	Law for surreal addition and subtraction. (Contributed by Scott Fenton, 4-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 +s 𝐵) -s 𝐶) = ((𝐴 -s 𝐶) +s 𝐵))
Theorem	ltsubsubsbd 28075	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 28076	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 28077	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 28078	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 28079	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 28080	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 28081	Surreal less-than relationship between subtraction and addition. (Contributed by Scott Fenton, 27-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 -s 𝐵) <s 𝐶 ↔ 𝐴 <s (𝐶 +s 𝐵)))
Theorem	ltsubadds2d 28082	Surreal less-than relationship between subtraction and addition. (Contributed by Scott Fenton, 27-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 -s 𝐵) <s 𝐶 ↔ 𝐴 <s (𝐵 +s 𝐶)))
Theorem	ltaddsubsd 28083	Surreal less-than relationship between subtraction and addition. (Contributed by Scott Fenton, 28-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 +s 𝐵) <s 𝐶 ↔ 𝐴 <s (𝐶 -s 𝐵)))
Theorem	ltaddsubs2d 28084	Surreal less-than relationship between subtraction and addition. (Contributed by Scott Fenton, 28-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 +s 𝐵) <s 𝐶 ↔ 𝐵 <s (𝐶 -s 𝐴)))
Theorem	lesubaddsd 28085	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 28086	Law for double surreal subtraction. (Contributed by Scott Fenton, 9-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 -s 𝐵) -s 𝐶) = (𝐴 -s (𝐵 +s 𝐶)))
Theorem	subsubs2d 28087	Law for double surreal subtraction. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 -s (𝐵 -s 𝐶)) = (𝐴 +s (𝐶 -s 𝐵)))
Theorem	lesubsd 28088	Swap subtrahends in a surreal inequality. (Contributed by Scott Fenton, 29-Jan-2026.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 ≤s (𝐵 -s 𝐶) ↔ 𝐶 ≤s (𝐵 -s 𝐴)))
Theorem	nncansd 28089	Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 -s (𝐴 -s 𝐵)) = 𝐵)
Theorem	posdifsd 28090	Comparison of two surreals whose difference is positive. (Contributed by Scott Fenton, 10-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ 0s <s (𝐵 -s 𝐴)))
Theorem	ltsubsposd 28091	Subtraction of a positive number decreases the sum. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → ( 0s <s 𝐴 ↔ (𝐵 -s 𝐴) <s 𝐵))
Theorem	subsge0d 28092	Non-negative subtraction. (Contributed by Scott Fenton, 26-May-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → ( 0s ≤s (𝐴 -s 𝐵) ↔ 𝐵 ≤s 𝐴))
Theorem	addsubs4d 28093	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 28094	A surreal is greater than itself minus one. (Contributed by Scott Fenton, 20-Aug-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 -s 1s ) <s 𝐴)
Theorem	subscan1d 28095	Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐶 -s 𝐴) = (𝐶 -s 𝐵) ↔ 𝐴 = 𝐵))
Theorem	subscan2d 28096	Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 -s 𝐶) = (𝐵 -s 𝐶) ↔ 𝐴 = 𝐵))
Theorem	subseq0d 28097	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 28098	Set up the syntax for surreal multiplication.
class ·s
Definition	df-muls 28099*	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 28100	Surreal multiplication is a function over surreals. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ·s Fn ( No × No )