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	leadds1im 28001	Surreal less-than or equal cancels under addition. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶) → 𝐴 ≤s 𝐵))
Theorem	leadds2im 28002	Surreal less-than or equal cancels under addition. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐶 +s 𝐴) ≤s (𝐶 +s 𝐵) → 𝐴 ≤s 𝐵))
Theorem	leadds1 28003	Addition to both sides of surreal less-than or equal. Theorem 5 of [Conway] p. 18. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 ≤s 𝐵 ↔ (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶)))
Theorem	leadds2 28004	Addition to both sides of surreal less-than or equal. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 ≤s 𝐵 ↔ (𝐶 +s 𝐴) ≤s (𝐶 +s 𝐵)))
Theorem	ltadds2 28005	Addition to both sides of surreal less-than. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 <s 𝐵 ↔ (𝐶 +s 𝐴) <s (𝐶 +s 𝐵)))
Theorem	ltadds1 28006	Addition to both sides of surreal less-than. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 <s 𝐵 ↔ (𝐴 +s 𝐶) <s (𝐵 +s 𝐶)))
Theorem	addscan2 28007	Cancellation law for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐴 +s 𝐶) = (𝐵 +s 𝐶) ↔ 𝐴 = 𝐵))
Theorem	addscan1 28008	Cancellation law for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐶 +s 𝐴) = (𝐶 +s 𝐵) ↔ 𝐴 = 𝐵))
Theorem	leadds1d 28009	Addition to both sides of surreal less-than or equal. Theorem 5 of [Conway] p. 18. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 ≤s 𝐵 ↔ (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶)))
Theorem	leadds2d 28010	Addition to both sides of surreal less-than or equal. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 ≤s 𝐵 ↔ (𝐶 +s 𝐴) ≤s (𝐶 +s 𝐵)))
Theorem	ltadds2d 28011	Addition to both sides of surreal less-than. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ (𝐶 +s 𝐴) <s (𝐶 +s 𝐵)))
Theorem	ltadds1d 28012	Addition to both sides of surreal less-than. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ (𝐴 +s 𝐶) <s (𝐵 +s 𝐶)))
Theorem	addscan2d 28013	Cancellation law for surreal addition. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 +s 𝐶) = (𝐵 +s 𝐶) ↔ 𝐴 = 𝐵))
Theorem	addscan1d 28014	Cancellation law for surreal addition. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐶 +s 𝐴) = (𝐶 +s 𝐵) ↔ 𝐴 = 𝐵))
Theorem	addsuniflem 28015*	Lemma for addsunif 28016. State the whole theorem with extra distinct variable conditions. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ (𝜑 → 𝐿 <<s 𝑅)    &   ⊢ (𝜑 → 𝑀 <<s 𝑆)    &   ⊢ (𝜑 → 𝐴 = (𝐿 |s 𝑅))    &   ⊢ (𝜑 → 𝐵 = (𝑀 |s 𝑆))    ⇒   ⊢ (𝜑 → (𝐴 +s 𝐵) = (({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) |s ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})))
Theorem	addsunif 28016*	Uniformity theorem for surreal addition. This theorem states that we can use any cuts that define 𝐴 and 𝐵 in the definition of surreal addition. Theorem 3.2 of [Gonshor] p. 15. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ (𝜑 → 𝐿 <<s 𝑅)    &   ⊢ (𝜑 → 𝑀 <<s 𝑆)    &   ⊢ (𝜑 → 𝐴 = (𝐿 |s 𝑅))    &   ⊢ (𝜑 → 𝐵 = (𝑀 |s 𝑆))    ⇒   ⊢ (𝜑 → (𝐴 +s 𝐵) = (({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) |s ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)})))
Theorem	addsasslem1 28017*	Lemma for addition associativity. Expand one form of the triple sum. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 +s 𝐵) +s 𝐶) = ((({𝑦 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑦 = ((𝑙 +s 𝐵) +s 𝐶)} ∪ {𝑧 ∣ ∃𝑚 ∈ ( L ‘𝐵)𝑧 = ((𝐴 +s 𝑚) +s 𝐶)}) ∪ {𝑤 ∣ ∃𝑛 ∈ ( L ‘𝐶)𝑤 = ((𝐴 +s 𝐵) +s 𝑛)}) |s (({𝑎 ∣ ∃𝑝 ∈ ( R ‘𝐴)𝑎 = ((𝑝 +s 𝐵) +s 𝐶)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( R ‘𝐵)𝑏 = ((𝐴 +s 𝑞) +s 𝐶)}) ∪ {𝑐 ∣ ∃𝑟 ∈ ( R ‘𝐶)𝑐 = ((𝐴 +s 𝐵) +s 𝑟)})))
Theorem	addsasslem2 28018*	Lemma for addition associativity. Expand the other form of the triple sum. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 +s (𝐵 +s 𝐶)) = ((({𝑦 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑦 = (𝑙 +s (𝐵 +s 𝐶))} ∪ {𝑧 ∣ ∃𝑚 ∈ ( L ‘𝐵)𝑧 = (𝐴 +s (𝑚 +s 𝐶))}) ∪ {𝑤 ∣ ∃𝑛 ∈ ( L ‘𝐶)𝑤 = (𝐴 +s (𝐵 +s 𝑛))}) |s (({𝑎 ∣ ∃𝑝 ∈ ( R ‘𝐴)𝑎 = (𝑝 +s (𝐵 +s 𝐶))} ∪ {𝑏 ∣ ∃𝑞 ∈ ( R ‘𝐵)𝑏 = (𝐴 +s (𝑞 +s 𝐶))}) ∪ {𝑐 ∣ ∃𝑟 ∈ ( R ‘𝐶)𝑐 = (𝐴 +s (𝐵 +s 𝑟))})))
Theorem	addsass 28019	Surreal addition is associative. Part of theorem 3 of [Conway] p. 17. (Contributed by Scott Fenton, 22-Jan-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐴 +s 𝐵) +s 𝐶) = (𝐴 +s (𝐵 +s 𝐶)))
Theorem	addsassd 28020	Surreal addition is associative. Part of theorem 3 of [Conway] p. 17. (Contributed by Scott Fenton, 22-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 +s 𝐵) +s 𝐶) = (𝐴 +s (𝐵 +s 𝐶)))
Theorem	adds32d 28021	Commutative/associative law that swaps the last two terms in a triple sum. (Contributed by Scott Fenton, 22-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 +s 𝐵) +s 𝐶) = ((𝐴 +s 𝐶) +s 𝐵))
Theorem	adds12d 28022	Commutative/associative law that swaps the first two terms in a triple sum. (Contributed by Scott Fenton, 9-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 +s (𝐵 +s 𝐶)) = (𝐵 +s (𝐴 +s 𝐶)))
Theorem	adds4d 28023	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 28024	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 28025	Addition of a positive number increases the sum. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → ( 0s <s 𝐴 ↔ 𝐵 <s (𝐵 +s 𝐴)))
Theorem	ltaddspos2d 28026	Addition of a positive number increases the sum. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → ( 0s <s 𝐴 ↔ 𝐵 <s (𝐴 +s 𝐵)))
Theorem	lt2addsd 28027	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 28028	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 28029	A surreal is less than itself plus one. (Contributed by Scott Fenton, 13-Aug-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    ⇒   ⊢ (𝜑 → 𝐴 <s (𝐴 +s 1s ))
Theorem	addsge01d 28030	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 28031*	Lemma for addbday 28032. (Contributed by Scott Fenton, 13-Aug-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))( bday ‘(𝐴 +s 𝑦𝑂)) ⊆ (( bday ‘𝐴) +no ( bday ‘𝑦𝑂)))    &   ⊢ 𝑆 ⊆ (( L ‘𝐵) ∪ ( R ‘𝐵))    ⇒   ⊢ (𝜑 → ( bday “ {𝑧 ∣ ∃𝑦𝐿 ∈ 𝑆 𝑧 = (𝐴 +s 𝑦𝐿)}) ⊆ (( bday ‘𝐴) +no ( bday ‘𝐵)))
Theorem	addbday 28032	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 28033	Declare the syntax for surreal negation.
class -us
Syntax	csubs 28034	Declare the syntax for surreal subtraction.
class -s
Definition	df-negs 28035*	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 28036*	Define surreal subtraction. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ -s = (𝑥 ∈ No , 𝑦 ∈ No ↦ (𝑥 +s ( -us ‘𝑦)))
Theorem	negsfn 28037	Surreal negation is a function over surreals. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ -us Fn No
Theorem	subsfn 28038	Surreal subtraction is a function over pairs of surreals. (Contributed by Scott Fenton, 22-Jan-2025.)
⊢ -s Fn ( No × No )
Theorem	negsval 28039	The value of the surreal negation function. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ (𝐴 ∈ No → ( -us ‘𝐴) = (( -us “ ( R ‘𝐴)) |s ( -us “ ( L ‘𝐴))))
Theorem	neg0s 28040	Negative surreal zero is surreal zero. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ ( -us ‘ 0s ) = 0s
Theorem	neg1s 28041	An expression for negative surreal one. (Contributed by Scott Fenton, 24-Jul-2025.)
⊢ ( -us ‘ 1s ) = (∅ |s { 0s })
Theorem	negsproplem1 28042*	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 28043*	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 28044*	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 28045*	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 28046*	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 28047*	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 28048*	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 28049	Show closure and ordering properties of negation. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (( -us ‘𝐴) ∈ No ∧ (𝐴 <s 𝐵 → ( -us ‘𝐵) <s ( -us ‘𝐴))))
Theorem	negscl 28050	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 28051	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 28052	The forward direction of the ordering properties of negation. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 → ( -us ‘𝐵) <s ( -us ‘𝐴)))
Theorem	negcut 28053	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 28054	The cut that defines surreal negation is legitimate. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝐴 ∈ No → ( -us “ ( R ‘𝐴)) <<s ( -us “ ( L ‘𝐴)))
Theorem	negsid 28055	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 28056	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 28057*	Every surreal has a negative. Note that this theorem, addscl 27995, addscom 27980, addsass 28019, addsrid 27978, and ltadds1im 27999 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 28058	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 28059	Negative of both sides of surreal less-than. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 ↔ ( -us ‘𝐵) <s ( -us ‘𝐴)))
Theorem	lenegs 28060	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 28061	Negative of both sides of surreal less-than. (Contributed by Scott Fenton, 14-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ ( -us ‘𝐵) <s ( -us ‘𝐴)))
Theorem	lenegsd 28062	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 28063	Surreal negation is one-to-one. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (( -us ‘𝐴) = ( -us ‘𝐵) ↔ 𝐴 = 𝐵))
Theorem	negsdi 28064	Distribution of surreal negative over addition. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( -us ‘(𝐴 +s 𝐵)) = (( -us ‘𝐴) +s ( -us ‘𝐵)))
Theorem	lt0negs2d 28065	Comparison of a surreal and its negative to zero. (Contributed by Scott Fenton, 10-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    ⇒   ⊢ (𝜑 → ( 0s <s 𝐴 ↔ ( -us ‘𝐴) <s 0s ))
Theorem	negsf 28066	Function statement for surreal negation. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ -us : No ⟶ No
Theorem	negsfo 28067	Function statement for surreal negation. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ -us : No –onto→ No
Theorem	negsf1o 28068	Surreal negation is a bijection. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ -us : No –1-1-onto→ No
Theorem	negsunif 28069	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 28070	Lemma for negbday 28071. Bound the birthday of the negative of a surreal number above. (Contributed by Scott Fenton, 8-Mar-2025.)
⊢ (𝐴 ∈ No → ( bday ‘( -us ‘𝐴)) ⊆ ( bday ‘𝐴))
Theorem	negbday 28071	Negation of a surreal number preserves birthday. (Contributed by Scott Fenton, 8-Mar-2025.)
⊢ (𝐴 ∈ No → ( bday ‘( -us ‘𝐴)) = ( bday ‘𝐴))
Theorem	negleft 28072	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 28073	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 28074	The value of surreal subtraction. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 -s 𝐵) = (𝐴 +s ( -us ‘𝐵)))
Theorem	subsvald 28075	The value of surreal subtraction. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 -s 𝐵) = (𝐴 +s ( -us ‘𝐵)))
Theorem	subscl 28076	Closure law for surreal subtraction. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 -s 𝐵) ∈ No )
Theorem	subscld 28077	Closure law for surreal subtraction. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 -s 𝐵) ∈ No )
Theorem	subsf 28078	Function statement for surreal subtraction. (Contributed by Scott Fenton, 17-May-2025.)
⊢ -s :( No × No )⟶ No
Theorem	subsfo 28079	Surreal subtraction is an onto function. (Contributed by Scott Fenton, 17-May-2025.)
⊢ -s :( No × No )–onto→ No
Theorem	negsval2 28080	Surreal negation in terms of subtraction. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ No → ( -us ‘𝐴) = ( 0s -s 𝐴))
Theorem	negsval2d 28081	Surreal negation in terms of subtraction. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    ⇒   ⊢ (𝜑 → ( -us ‘𝐴) = ( 0s -s 𝐴))
Theorem	subsid1 28082	Identity law for subtraction. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝐴 ∈ No → (𝐴 -s 0s ) = 𝐴)
Theorem	subsid 28083	Subtraction of a surreal from itself. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝐴 ∈ No → (𝐴 -s 𝐴) = 0s )
Theorem	subadds 28084	Relationship between addition and subtraction for surreals. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐴 -s 𝐵) = 𝐶 ↔ (𝐵 +s 𝐶) = 𝐴))
Theorem	subaddsd 28085	Relationship between addition and subtraction for surreals. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 -s 𝐵) = 𝐶 ↔ (𝐵 +s 𝐶) = 𝐴))
Theorem	pncans 28086	Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → ((𝐴 +s 𝐵) -s 𝐵) = 𝐴)
Theorem	pncan3s 28087	Subtraction and addition of equals. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 +s (𝐵 -s 𝐴)) = 𝐵)
Theorem	pncan2s 28088	Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → ((𝐴 +s 𝐵) -s 𝐴) = 𝐵)
Theorem	npcans 28089	Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → ((𝐴 -s 𝐵) +s 𝐵) = 𝐴)
Theorem	ltsubs1 28090	Subtraction from both sides of surreal less-than. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 <s 𝐵 ↔ (𝐴 -s 𝐶) <s (𝐵 -s 𝐶)))
Theorem	ltsubs2 28091	Subtraction from both sides of surreal less-than. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 <s 𝐵 ↔ (𝐶 -s 𝐵) <s (𝐶 -s 𝐴)))
Theorem	ltsubs1d 28092	Subtraction from both sides of surreal less-than. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ (𝐴 -s 𝐶) <s (𝐵 -s 𝐶)))
Theorem	ltsubs2d 28093	Subtraction from both sides of surreal less-than. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ (𝐶 -s 𝐵) <s (𝐶 -s 𝐴)))
Theorem	negsubsdi2d 28094	Distribution of negative over subtraction. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → ( -us ‘(𝐴 -s 𝐵)) = (𝐵 -s 𝐴))
Theorem	addsubsassd 28095	Associative-type law for surreal addition and subtraction. (Contributed by Scott Fenton, 6-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 +s 𝐵) -s 𝐶) = (𝐴 +s (𝐵 -s 𝐶)))
Theorem	addsubsd 28096	Law for surreal addition and subtraction. (Contributed by Scott Fenton, 4-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 +s 𝐵) -s 𝐶) = ((𝐴 -s 𝐶) +s 𝐵))
Theorem	ltsubsubsbd 28097	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 28098	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 28099	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 28100	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 𝐷)))