P. 278 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 27701-27800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	addscut2 27701*	Show that the cut involved in surreal addition is legitimate. (Contributed by Scott Fenton, 8-Mar-2025.)
⊢ (𝜑 → 𝑋 ∈ No )    &   ⊢ (𝜑 → 𝑌 ∈ No )    ⇒   ⊢ (𝜑 → ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) <<s ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)}))
Theorem	addscld 27702	Surreal numbers are closed under addition. Theorem 6(iii) of [Conway] p. 18. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ (𝜑 → 𝑋 ∈ No )    &   ⊢ (𝜑 → 𝑌 ∈ No )    ⇒   ⊢ (𝜑 → (𝑋 +s 𝑌) ∈ No )
Theorem	addscl 27703	Surreal numbers are closed under addition. Theorem 6(iii) of [Conway[ p. 18. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 +s 𝐵) ∈ No )
Theorem	addsf 27704	Function statement for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ +s :( No × No )⟶ No
Theorem	addsfo 27705	Surreal addition is onto. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ +s :( No × No )–onto→ No
Theorem	peano2no 27706	A theorem for surreals that is analagous to the second Peano postulate peano2 7883. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ (𝐴 ∈ No → (𝐴 +s 1s ) ∈ No )
Theorem	sltadd1im 27707	Surreal less-than is preserved under addition. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 <s 𝐵 → (𝐴 +s 𝐶) <s (𝐵 +s 𝐶)))
Theorem	sltadd2im 27708	Surreal less-than is preserved under addition. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 <s 𝐵 → (𝐶 +s 𝐴) <s (𝐶 +s 𝐵)))
Theorem	sleadd1im 27709	Surreal less-than or equal cancels under addition. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶) → 𝐴 ≤s 𝐵))
Theorem	sleadd2im 27710	Surreal less-than or equal cancels under addition. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐶 +s 𝐴) ≤s (𝐶 +s 𝐵) → 𝐴 ≤s 𝐵))
Theorem	sleadd1 27711	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	sleadd2 27712	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	sltadd2 27713	Addition to both sides of surreal less-than. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 <s 𝐵 ↔ (𝐶 +s 𝐴) <s (𝐶 +s 𝐵)))
Theorem	sltadd1 27714	Addition to both sides of surreal less-than. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 <s 𝐵 ↔ (𝐴 +s 𝐶) <s (𝐵 +s 𝐶)))
Theorem	addscan2 27715	Cancellation law for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐴 +s 𝐶) = (𝐵 +s 𝐶) ↔ 𝐴 = 𝐵))
Theorem	addscan1 27716	Cancellation law for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐶 +s 𝐴) = (𝐶 +s 𝐵) ↔ 𝐴 = 𝐵))
Theorem	sleadd1d 27717	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	sleadd2d 27718	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	sltadd2d 27719	Addition to both sides of surreal less-than. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ (𝐶 +s 𝐴) <s (𝐶 +s 𝐵)))
Theorem	sltadd1d 27720	Addition to both sides of surreal less-than. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ (𝐴 +s 𝐶) <s (𝐵 +s 𝐶)))
Theorem	addscan2d 27721	Cancellation law for surreal addition. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 +s 𝐶) = (𝐵 +s 𝐶) ↔ 𝐴 = 𝐵))
Theorem	addscan1d 27722	Cancellation law for surreal addition. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐶 +s 𝐴) = (𝐶 +s 𝐵) ↔ 𝐴 = 𝐵))
Theorem	addsuniflem 27723*	Lemma for addsunif 27724. 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 27724*	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 27725*	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 27726*	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 27727	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 27728	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 27729	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 27730	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 27731	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 27732	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 𝐵)))
15.5.2  Negation and Subtraction
Syntax	cnegs 27733	Declare the syntax for surreal negation.
class -us
Syntax	csubs 27734	Declare the syntax for surreal subtraction.
class -s
Definition	df-negs 27735*	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 27736*	Define surreal subtraction. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ -s = (𝑥 ∈ No , 𝑦 ∈ No ↦ (𝑥 +s ( -us ‘𝑦)))
Theorem	negsfn 27737	Surreal negation is a function over surreals. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ -us Fn No
Theorem	subsfn 27738	Surreal subtraction is a function over pairs of surreals. (Contributed by Scott Fenton, 22-Jan-2025.)
⊢ -s Fn ( No × No )
Theorem	negsval 27739	The value of the surreal negation function. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ (𝐴 ∈ No → ( -us ‘𝐴) = (( -us “ ( R ‘𝐴)) |s ( -us “ ( L ‘𝐴))))
Theorem	negs0s 27740	Negative surreal zero is surreal zero. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ ( -us ‘ 0s ) = 0s
Theorem	negsproplem1 27741*	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 27742*	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 27743*	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 27744*	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 27745*	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 27746*	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 27747*	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 27748	Show closure and ordering properties of negation. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (( -us ‘𝐴) ∈ No ∧ (𝐴 <s 𝐵 → ( -us ‘𝐵) <s ( -us ‘𝐴))))
Theorem	negscl 27749	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 27750	The surreals are closed under negation. Theorem 6(ii) of [Conway] p. 18. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    ⇒   ⊢ (𝜑 → ( -us ‘𝐴) ∈ No )
Theorem	sltnegim 27751	The forward direction of the ordering properties of negation. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 → ( -us ‘𝐵) <s ( -us ‘𝐴)))
Theorem	negscut 27752	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	negscut2 27753	The cut that defines surreal negation is legitimate. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝐴 ∈ No → ( -us “ ( R ‘𝐴)) <<s ( -us “ ( L ‘𝐴)))
Theorem	negsid 27754	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 27755	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 27756*	Every surreal has a negative. Note that this theorem, addscl 27703, addscom 27688, addsass 27727, addsrid 27686, and sltadd1im 27707 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 27757	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	sltneg 27758	Negative of both sides of surreal less-than. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 ↔ ( -us ‘𝐵) <s ( -us ‘𝐴)))
Theorem	sleneg 27759	Negative of both sides of surreal less-than or equal. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 ≤s 𝐵 ↔ ( -us ‘𝐵) ≤s ( -us ‘𝐴)))
Theorem	sltnegd 27760	Negative of both sides of surreal less-than. (Contributed by Scott Fenton, 14-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ ( -us ‘𝐵) <s ( -us ‘𝐴)))
Theorem	slenegd 27761	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 27762	Surreal negation is one-to-one. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (( -us ‘𝐴) = ( -us ‘𝐵) ↔ 𝐴 = 𝐵))
Theorem	negsdi 27763	Distribution of surreal negative over addition. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( -us ‘(𝐴 +s 𝐵)) = (( -us ‘𝐴) +s ( -us ‘𝐵)))
Theorem	slt0neg2d 27764	Comparison of a surreal and its negative to zero. (Contributed by Scott Fenton, 10-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    ⇒   ⊢ (𝜑 → ( 0s <s 𝐴 ↔ ( -us ‘𝐴) <s 0s ))
Theorem	negsf 27765	Function statement for surreal negation. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ -us : No ⟶ No
Theorem	negsfo 27766	Function statement for surreal negation. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ -us : No –onto→ No
Theorem	negsf1o 27767	Surreal negation is a bijection. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ -us : No –1-1-onto→ No
Theorem	negsunif 27768	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	negsbdaylem 27769	Lemma for negsbday 27770. Bound the birthday of the negative of a surreal number above. (Contributed by Scott Fenton, 8-Mar-2025.)
⊢ (𝐴 ∈ No → ( bday ‘( -us ‘𝐴)) ⊆ ( bday ‘𝐴))
Theorem	negsbday 27770	Negation of a surreal number preserves birthday. (Contributed by Scott Fenton, 8-Mar-2025.)
⊢ (𝐴 ∈ No → ( bday ‘( -us ‘𝐴)) = ( bday ‘𝐴))
Theorem	subsval 27771	The value of surreal subtraction. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 -s 𝐵) = (𝐴 +s ( -us ‘𝐵)))
Theorem	subsvald 27772	The value of surreal subtraction. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 -s 𝐵) = (𝐴 +s ( -us ‘𝐵)))
Theorem	subscl 27773	Closure law for surreal subtraction. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 -s 𝐵) ∈ No )
Theorem	subscld 27774	Closure law for surreal subtraction. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 -s 𝐵) ∈ No )
Theorem	subsid1 27775	Identity law for subtraction. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝐴 ∈ No → (𝐴 -s 0s ) = 𝐴)
Theorem	subsid 27776	Subtraction of a surreal from itself. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝐴 ∈ No → (𝐴 -s 𝐴) = 0s )
Theorem	subadds 27777	Relationship between addition and subtraction for surreals. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐴 -s 𝐵) = 𝐶 ↔ (𝐵 +s 𝐶) = 𝐴))
Theorem	subaddsd 27778	Relationship between addition and subtraction for surreals. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 -s 𝐵) = 𝐶 ↔ (𝐵 +s 𝐶) = 𝐴))
Theorem	pncans 27779	Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → ((𝐴 +s 𝐵) -s 𝐵) = 𝐴)
Theorem	pncan3s 27780	Subtraction and addition of equals. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 +s (𝐵 -s 𝐴)) = 𝐵)
Theorem	npcans 27781	Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → ((𝐴 -s 𝐵) +s 𝐵) = 𝐴)
Theorem	sltsub1 27782	Subtraction from both sides of surreal less-than. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 <s 𝐵 ↔ (𝐴 -s 𝐶) <s (𝐵 -s 𝐶)))
Theorem	sltsub2 27783	Subtraction from both sides of surreal less-than. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 <s 𝐵 ↔ (𝐶 -s 𝐵) <s (𝐶 -s 𝐴)))
Theorem	sltsub1d 27784	Subtraction from both sides of surreal less-than. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ (𝐴 -s 𝐶) <s (𝐵 -s 𝐶)))
Theorem	sltsub2d 27785	Subtraction from both sides of surreal less-than. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ (𝐶 -s 𝐵) <s (𝐶 -s 𝐴)))
Theorem	negsubsdi2d 27786	Distribution of negative over subtraction. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → ( -us ‘(𝐴 -s 𝐵)) = (𝐵 -s 𝐴))
Theorem	addsubsassd 27787	Associative-type law for surreal addition and subtraction. (Contributed by Scott Fenton, 6-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 +s 𝐵) -s 𝐶) = (𝐴 +s (𝐵 -s 𝐶)))
Theorem	addsubsd 27788	Law for surreal addition and subtraction. (Contributed by Scott Fenton, 4-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 +s 𝐵) -s 𝐶) = ((𝐴 -s 𝐶) +s 𝐵))
Theorem	sltsubsubbd 27789	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	sltsubsub2bd 27790	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	sltsubsub3bd 27791	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	slesubsubbd 27792	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	slesubsub2bd 27793	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	slesubsub3bd 27794	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	sltsubaddd 27795	Surreal less-than relationship between subtraction and addition. (Contributed by Scott Fenton, 27-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 -s 𝐵) <s 𝐶 ↔ 𝐴 <s (𝐶 +s 𝐵)))
Theorem	sltsubadd2d 27796	Surreal less-than relationship between subtraction and addition. (Contributed by Scott Fenton, 27-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 -s 𝐵) <s 𝐶 ↔ 𝐴 <s (𝐵 +s 𝐶)))
Theorem	sltaddsubd 27797	Surreal less-than relationship between subtraction and addition. (Contributed by Scott Fenton, 28-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 +s 𝐵) <s 𝐶 ↔ 𝐴 <s (𝐶 -s 𝐵)))
Theorem	sltaddsub2d 27798	Surreal less-than relationship between subtraction and addition. (Contributed by Scott Fenton, 28-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 +s 𝐵) <s 𝐶 ↔ 𝐵 <s (𝐶 -s 𝐴)))
Theorem	subsubs4d 27799	Law for double surreal subtraction. (Contributed by Scott Fenton, 9-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 -s 𝐵) -s 𝐶) = (𝐴 -s (𝐵 +s 𝐶)))
Theorem	posdifsd 27800	Comparison of two surreals whose difference is positive. (Contributed by Scott Fenton, 10-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ 0s <s (𝐵 -s 𝐴)))