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	neg1s 28201	An expression for negative surreal one. (Contributed by Scott Fenton, 24-Jul-2025.)
⊢ ( -us ‘ 1s ) = (∅ |s { 0s })
Theorem	negsproplem1 28202*	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 28203*	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 28204*	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 28205*	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 28206*	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 28207*	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 28208*	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 28209	Show closure and ordering properties of negation. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (( -us ‘𝐴) ∈ No ∧ (𝐴 <s 𝐵 → ( -us ‘𝐵) <s ( -us ‘𝐴))))
Theorem	negscl 28210	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 28211	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 28212	The forward direction of the ordering properties of negation. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 → ( -us ‘𝐵) <s ( -us ‘𝐴)))
Theorem	negcut 28213	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 28214	The cut that defines surreal negation is legitimate. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝐴 ∈ No → ( -us “ ( R ‘𝐴)) <<s ( -us “ ( L ‘𝐴)))
Theorem	negsid 28215	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 28216	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 28217*	Every surreal has a negative. Note that this theorem, addscl 28155, addscom 28140, addsass 28179, addsrid 28138, and ltadds1im 28159 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 28218	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 28219	Negative of both sides of surreal less-than. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 ↔ ( -us ‘𝐵) <s ( -us ‘𝐴)))
Theorem	lenegs 28220	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 28221	Negative of both sides of surreal less-than. (Contributed by Scott Fenton, 14-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ ( -us ‘𝐵) <s ( -us ‘𝐴)))
Theorem	lenegsd 28222	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 28223	Surreal negation is one-to-one. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (( -us ‘𝐴) = ( -us ‘𝐵) ↔ 𝐴 = 𝐵))
Theorem	negsdi 28224	Distribution of surreal negative over addition. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( -us ‘(𝐴 +s 𝐵)) = (( -us ‘𝐴) +s ( -us ‘𝐵)))
Theorem	lt0negs2d 28225	Comparison of a surreal and its negative to zero. (Contributed by Scott Fenton, 10-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    ⇒   ⊢ (𝜑 → ( 0s <s 𝐴 ↔ ( -us ‘𝐴) <s 0s ))
Theorem	negsf 28226	Function statement for surreal negation. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ -us : No ⟶ No
Theorem	negsfo 28227	Function statement for surreal negation. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ -us : No –onto→ No
Theorem	negsf1o 28228	Surreal negation is a bijection. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ -us : No –1-1-onto→ No
Theorem	negsunif 28229	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 28230	Lemma for negbday 28231. Bound the birthday of the negative of a surreal number above. (Contributed by Scott Fenton, 8-Mar-2025.)
⊢ (𝐴 ∈ No → ( bday ‘( -us ‘𝐴)) ⊆ ( bday ‘𝐴))
Theorem	negbday 28231	Negation of a surreal number preserves birthday. (Contributed by Scott Fenton, 8-Mar-2025.)
⊢ (𝐴 ∈ No → ( bday ‘( -us ‘𝐴)) = ( bday ‘𝐴))
Theorem	negleft 28232	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 28233	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 28234	The value of surreal subtraction. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 -s 𝐵) = (𝐴 +s ( -us ‘𝐵)))
Theorem	subsvald 28235	The value of surreal subtraction. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 -s 𝐵) = (𝐴 +s ( -us ‘𝐵)))
Theorem	subscl 28236	Closure law for surreal subtraction. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 -s 𝐵) ∈ No )
Theorem	subscld 28237	Closure law for surreal subtraction. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 -s 𝐵) ∈ No )
Theorem	subsf 28238	Function statement for surreal subtraction. (Contributed by Scott Fenton, 17-May-2025.)
⊢ -s :( No × No )⟶ No
Theorem	subsfo 28239	Surreal subtraction is an onto function. (Contributed by Scott Fenton, 17-May-2025.)
⊢ -s :( No × No )–onto→ No
Theorem	negsval2 28240	Surreal negation in terms of subtraction. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ No → ( -us ‘𝐴) = ( 0s -s 𝐴))
Theorem	negsval2d 28241	Surreal negation in terms of subtraction. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    ⇒   ⊢ (𝜑 → ( -us ‘𝐴) = ( 0s -s 𝐴))
Theorem	subsid1 28242	Identity law for subtraction. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝐴 ∈ No → (𝐴 -s 0s ) = 𝐴)
Theorem	subsid 28243	Subtraction of a surreal from itself. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝐴 ∈ No → (𝐴 -s 𝐴) = 0s )
Theorem	subadds 28244	Relationship between addition and subtraction for surreals. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐴 -s 𝐵) = 𝐶 ↔ (𝐵 +s 𝐶) = 𝐴))
Theorem	subaddsd 28245	Relationship between addition and subtraction for surreals. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 -s 𝐵) = 𝐶 ↔ (𝐵 +s 𝐶) = 𝐴))
Theorem	pncans 28246	Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → ((𝐴 +s 𝐵) -s 𝐵) = 𝐴)
Theorem	pncan3s 28247	Subtraction and addition of equals. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 +s (𝐵 -s 𝐴)) = 𝐵)
Theorem	pncan2s 28248	Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → ((𝐴 +s 𝐵) -s 𝐴) = 𝐵)
Theorem	npcans 28249	Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → ((𝐴 -s 𝐵) +s 𝐵) = 𝐴)
Theorem	ltsubs1 28250	Subtraction from both sides of surreal less-than. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 <s 𝐵 ↔ (𝐴 -s 𝐶) <s (𝐵 -s 𝐶)))
Theorem	ltsubs2 28251	Subtraction from both sides of surreal less-than. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 <s 𝐵 ↔ (𝐶 -s 𝐵) <s (𝐶 -s 𝐴)))
Theorem	ltsubs1d 28252	Subtraction from both sides of surreal less-than. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ (𝐴 -s 𝐶) <s (𝐵 -s 𝐶)))
Theorem	ltsubs2d 28253	Subtraction from both sides of surreal less-than. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ (𝐶 -s 𝐵) <s (𝐶 -s 𝐴)))
Theorem	negsubsdi2d 28254	Distribution of negative over subtraction. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → ( -us ‘(𝐴 -s 𝐵)) = (𝐵 -s 𝐴))
Theorem	addsubsassd 28255	Associative-type law for surreal addition and subtraction. (Contributed by Scott Fenton, 6-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 +s 𝐵) -s 𝐶) = (𝐴 +s (𝐵 -s 𝐶)))
Theorem	addsubsd 28256	Law for surreal addition and subtraction. (Contributed by Scott Fenton, 4-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 +s 𝐵) -s 𝐶) = ((𝐴 -s 𝐶) +s 𝐵))
Theorem	ltsubsubsbd 28257	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 28258	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 28259	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 28260	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 28261	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 28262	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 28263	Surreal less-than relationship between subtraction and addition. (Contributed by Scott Fenton, 27-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 -s 𝐵) <s 𝐶 ↔ 𝐴 <s (𝐶 +s 𝐵)))
Theorem	ltsubadds2d 28264	Surreal less-than relationship between subtraction and addition. (Contributed by Scott Fenton, 27-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 -s 𝐵) <s 𝐶 ↔ 𝐴 <s (𝐵 +s 𝐶)))
Theorem	ltaddsubsd 28265	Surreal less-than relationship between subtraction and addition. (Contributed by Scott Fenton, 28-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 +s 𝐵) <s 𝐶 ↔ 𝐴 <s (𝐶 -s 𝐵)))
Theorem	ltaddsubs2d 28266	Surreal less-than relationship between subtraction and addition. (Contributed by Scott Fenton, 28-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 +s 𝐵) <s 𝐶 ↔ 𝐵 <s (𝐶 -s 𝐴)))
Theorem	lesubaddsd 28267	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 28268	Law for double surreal subtraction. (Contributed by Scott Fenton, 9-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 -s 𝐵) -s 𝐶) = (𝐴 -s (𝐵 +s 𝐶)))
Theorem	subsubs2d 28269	Law for double surreal subtraction. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 -s (𝐵 -s 𝐶)) = (𝐴 +s (𝐶 -s 𝐵)))
Theorem	lesubsd 28270	Swap subtrahends in a surreal inequality. (Contributed by Scott Fenton, 29-Jan-2026.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 ≤s (𝐵 -s 𝐶) ↔ 𝐶 ≤s (𝐵 -s 𝐴)))
Theorem	nncansd 28271	Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 -s (𝐴 -s 𝐵)) = 𝐵)
Theorem	posdifsd 28272	Comparison of two surreals whose difference is positive. (Contributed by Scott Fenton, 10-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ 0s <s (𝐵 -s 𝐴)))
Theorem	ltsubsposd 28273	Subtraction of a positive number decreases the sum. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → ( 0s <s 𝐴 ↔ (𝐵 -s 𝐴) <s 𝐵))
Theorem	subsge0d 28274	Non-negative subtraction. (Contributed by Scott Fenton, 26-May-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → ( 0s ≤s (𝐴 -s 𝐵) ↔ 𝐵 ≤s 𝐴))
Theorem	addsubs4d 28275	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 28276	A surreal is greater than itself minus one. (Contributed by Scott Fenton, 20-Aug-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 -s 1s ) <s 𝐴)
Theorem	subscan1d 28277	Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐶 -s 𝐴) = (𝐶 -s 𝐵) ↔ 𝐴 = 𝐵))
Theorem	subscan2d 28278	Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 -s 𝐶) = (𝐵 -s 𝐶) ↔ 𝐴 = 𝐵))
Theorem	subseq0d 28279	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 28280	Set up the syntax for surreal multiplication.
class ·s
Definition	df-muls 28281*	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 28282	Surreal multiplication is a function over surreals. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ·s Fn ( No × No )
Theorem	mulsval 28283*	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 28284*	Lemma for mulsval2 28285. 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 28285*	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 28286	Surreal multiplication by zero. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ (𝐴 ∈ No → (𝐴 ·s 0s ) = 0s )
Theorem	mulsrid 28287	Surreal one is a right identity element for multiplication. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ (𝐴 ∈ No → (𝐴 ·s 1s ) = 𝐴)
Theorem	mulsridd 28288	Surreal one is a right identity element for multiplication. (Contributed by Scott Fenton, 14-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 ·s 1s ) = 𝐴)
Theorem	mulsproplemcbv 28289*	Lemma for surreal multiplication. Change some bound variables for later use. (Contributed by Scott Fenton, 5-Mar-2025.)
⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))    ⇒   ⊢ (𝜑 → ∀𝑔 ∈ No ∀ℎ ∈ No ∀𝑖 ∈ No ∀𝑗 ∈ No ∀𝑘 ∈ No ∀𝑙 ∈ No (((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))))
Theorem	mulsproplem1 28290*	Lemma for surreal multiplication. Instantiate some variables. (Contributed by Scott Fenton, 4-Mar-2025.)
⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))    &   ⊢ (𝜑 → 𝑋 ∈ No )    &   ⊢ (𝜑 → 𝑌 ∈ No )    &   ⊢ (𝜑 → 𝑍 ∈ No )    &   ⊢ (𝜑 → 𝑊 ∈ No )    &   ⊢ (𝜑 → 𝑇 ∈ No )    &   ⊢ (𝜑 → 𝑈 ∈ No )    &   ⊢ (𝜑 → ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (((( bday ‘𝑍) +no ( bday ‘𝑇)) ∪ (( bday ‘𝑊) +no ( bday ‘𝑈))) ∪ ((( bday ‘𝑍) +no ( bday ‘𝑈)) ∪ (( bday ‘𝑊) +no ( bday ‘𝑇))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))))    ⇒   ⊢ (𝜑 → ((𝑋 ·s 𝑌) ∈ No ∧ ((𝑍 <s 𝑊 ∧ 𝑇 <s 𝑈) → ((𝑍 ·s 𝑈) -s (𝑍 ·s 𝑇)) <s ((𝑊 ·s 𝑈) -s (𝑊 ·s 𝑇)))))
Theorem	mulsproplem2 28291*	Lemma for surreal multiplication. Under the inductive hypothesis, the product of a member of the old set of 𝐴 and 𝐵 itself is a surreal number. (Contributed by Scott Fenton, 4-Mar-2025.)
⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))    &   ⊢ (𝜑 → 𝑋 ∈ ( O ‘( bday ‘𝐴)))    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → (𝑋 ·s 𝐵) ∈ No )
Theorem	mulsproplem3 28292*	Lemma for surreal multiplication. Under the inductive hypothesis, the product of 𝐴 itself and a member of the old set of 𝐵 is a surreal number. (Contributed by Scott Fenton, 4-Mar-2025.)
⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝑌 ∈ ( O ‘( bday ‘𝐵)))    ⇒   ⊢ (𝜑 → (𝐴 ·s 𝑌) ∈ No )
Theorem	mulsproplem4 28293*	Lemma for surreal multiplication. Under the inductive hypothesis, the product of a member of the old set of 𝐴 and a member of the old set of 𝐵 is a surreal number. (Contributed by Scott Fenton, 4-Mar-2025.)
⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))    &   ⊢ (𝜑 → 𝑋 ∈ ( O ‘( bday ‘𝐴)))    &   ⊢ (𝜑 → 𝑌 ∈ ( O ‘( bday ‘𝐵)))    ⇒   ⊢ (𝜑 → (𝑋 ·s 𝑌) ∈ No )
Theorem	mulsproplem5 28294*	Lemma for surreal multiplication. Show one of the inequalities involved in surreal multiplication's cuts. (Contributed by Scott Fenton, 4-Mar-2025.)
⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝑃 ∈ ( L ‘𝐴))    &   ⊢ (𝜑 → 𝑄 ∈ ( L ‘𝐵))    &   ⊢ (𝜑 → 𝑇 ∈ ( L ‘𝐴))    &   ⊢ (𝜑 → 𝑈 ∈ ( R ‘𝐵))    ⇒   ⊢ (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)))
Theorem	mulsproplem6 28295*	Lemma for surreal multiplication. Show one of the inequalities involved in surreal multiplication's cuts. (Contributed by Scott Fenton, 5-Mar-2025.)
⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝑃 ∈ ( L ‘𝐴))    &   ⊢ (𝜑 → 𝑄 ∈ ( L ‘𝐵))    &   ⊢ (𝜑 → 𝑉 ∈ ( R ‘𝐴))    &   ⊢ (𝜑 → 𝑊 ∈ ( L ‘𝐵))    ⇒   ⊢ (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊)))
Theorem	mulsproplem7 28296*	Lemma for surreal multiplication. Show one of the inequalities involved in surreal multiplication's cuts. (Contributed by Scott Fenton, 5-Mar-2025.)
⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝑅 ∈ ( R ‘𝐴))    &   ⊢ (𝜑 → 𝑆 ∈ ( R ‘𝐵))    &   ⊢ (𝜑 → 𝑇 ∈ ( L ‘𝐴))    &   ⊢ (𝜑 → 𝑈 ∈ ( R ‘𝐵))    ⇒   ⊢ (𝜑 → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)))
Theorem	mulsproplem8 28297*	Lemma for surreal multiplication. Show one of the inequalities involved in surreal multiplication's cuts. (Contributed by Scott Fenton, 5-Mar-2025.)
⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝑅 ∈ ( R ‘𝐴))    &   ⊢ (𝜑 → 𝑆 ∈ ( R ‘𝐵))    &   ⊢ (𝜑 → 𝑉 ∈ ( R ‘𝐴))    &   ⊢ (𝜑 → 𝑊 ∈ ( L ‘𝐵))    ⇒   ⊢ (𝜑 → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊)))
Theorem	mulsproplem9 28298*	Lemma for surreal multiplication. Show that the cut involved in surreal multiplication makes sense. (Contributed by Scott Fenton, 5-Mar-2025.)
⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → ({𝑔 ∣ ∃𝑝 ∈ ( 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	mulsproplem10 28299*	Lemma for surreal multiplication. State the cut properties of surreal multiplication. (Contributed by Scott Fenton, 5-Mar-2025.)
⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → ((𝐴 ·s 𝐵) ∈ No ∧ ({𝑔 ∣ ∃𝑝 ∈ ( L ‘𝐴)∃𝑞 ∈ ( L ‘𝐵)𝑔 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {ℎ ∣ ∃𝑟 ∈ ( R ‘𝐴)∃𝑠 ∈ ( R ‘𝐵)ℎ = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) <<s {(𝐴 ·s 𝐵)} ∧ {(𝐴 ·s 𝐵)} <<s ({𝑖 ∣ ∃𝑡 ∈ ( L ‘𝐴)∃𝑢 ∈ ( R ‘𝐵)𝑖 = (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ ( R ‘𝐴)∃𝑤 ∈ ( L ‘𝐵)𝑗 = (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤))})))
Theorem	mulsproplem11 28300*	Lemma for surreal multiplication. Under the inductive hypothesis, demonstrate closure of surreal multiplication. (Contributed by Scott Fenton, 5-Mar-2025.)
⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 ·s 𝐵) ∈ No )