![]() |
Metamath
Proof Explorer Theorem List (p. 276 of 479) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | negs0s 27501 | Negative surreal zero is surreal zero. (Contributed by Scott Fenton, 20-Aug-2024.) |
âĒ ( -us â 0s ) = 0s | ||
Theorem | negsproplem1 27502* | 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 27503* | 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 27504* | 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 27505* | 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 27506* | 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 27507* | 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 27508* | 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 27509 | Show closure and ordering properties of negation. (Contributed by Scott Fenton, 3-Feb-2025.) |
âĒ ((ðī â No ⧠ðĩ â No ) â (( -us âðī) â No ⧠(ðī <s ðĩ â ( -us âðĩ) <s ( -us âðī)))) | ||
Theorem | negscl 27510 | 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 27511 | 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 27512 | The forward direction of the ordering properties of negation. (Contributed by Scott Fenton, 3-Feb-2025.) |
âĒ ((ðī â No ⧠ðĩ â No ) â (ðī <s ðĩ â ( -us âðĩ) <s ( -us âðī))) | ||
Theorem | negscut 27513 | 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 27514 | The cut that defines surreal negation is legitimate. (Contributed by Scott Fenton, 3-Feb-2025.) |
âĒ (ðī â No â ( -us â ( R âðī)) <<s ( -us â ( L âðī))) | ||
Theorem | negsid 27515 | 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 27516 | 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 27517* | Every surreal has a negative. Note that this theorem, addscl 27465, addscom 27450, addsass 27488, addsrid 27448, and sltadd1im 27468 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 27518 | 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 27519 | Negative of both sides of surreal less-than. (Contributed by Scott Fenton, 3-Feb-2025.) |
âĒ ((ðī â No ⧠ðĩ â No ) â (ðī <s ðĩ â ( -us âðĩ) <s ( -us âðī))) | ||
Theorem | sleneg 27520 | 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 27521 | Negative of both sides of surreal less-than. (Contributed by Scott Fenton, 14-Mar-2025.) |
âĒ (ð â ðī â No ) & âĒ (ð â ðĩ â No ) â âĒ (ð â (ðī <s ðĩ â ( -us âðĩ) <s ( -us âðī))) | ||
Theorem | slenegd 27522 | 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 27523 | Surreal negation is one-to-one. (Contributed by Scott Fenton, 3-Feb-2025.) |
âĒ ((ðī â No ⧠ðĩ â No ) â (( -us âðī) = ( -us âðĩ) â ðī = ðĩ)) | ||
Theorem | negsdi 27524 | Distribution of surreal negative over addition. (Contributed by Scott Fenton, 5-Feb-2025.) |
âĒ ((ðī â No ⧠ðĩ â No ) â ( -us â(ðī +s ðĩ)) = (( -us âðī) +s ( -us âðĩ))) | ||
Theorem | slt0neg2d 27525 | Comparison of a surreal and its negative to zero. (Contributed by Scott Fenton, 10-Mar-2025.) |
âĒ (ð â ðī â No ) â âĒ (ð â ( 0s <s ðī â ( -us âðī) <s 0s )) | ||
Theorem | negsf 27526 | Function statement for surreal negation. (Contributed by Scott Fenton, 3-Feb-2025.) |
âĒ -us : No âķ No | ||
Theorem | negsfo 27527 | Function statement for surreal negation. (Contributed by Scott Fenton, 3-Feb-2025.) |
âĒ -us : No âontoâ No | ||
Theorem | negsf1o 27528 | Surreal negation is a bijection. (Contributed by Scott Fenton, 3-Feb-2025.) |
âĒ -us : No â1-1-ontoâ No | ||
Theorem | negsunif 27529 | 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 27530 | Lemma for negsbday 27531. Bound the birthday of the negative of a surreal number above. (Contributed by Scott Fenton, 8-Mar-2025.) |
âĒ (ðī â No â ( bday â( -us âðī)) â ( bday âðī)) | ||
Theorem | negsbday 27531 | Negation of a surreal number preserves birthday. (Contributed by Scott Fenton, 8-Mar-2025.) |
âĒ (ðī â No â ( bday â( -us âðī)) = ( bday âðī)) | ||
Theorem | subsval 27532 | The value of surreal subtraction. (Contributed by Scott Fenton, 3-Feb-2025.) |
âĒ ((ðī â No ⧠ðĩ â No ) â (ðī -s ðĩ) = (ðī +s ( -us âðĩ))) | ||
Theorem | subsvald 27533 | The value of surreal subtraction. (Contributed by Scott Fenton, 5-Feb-2025.) |
âĒ (ð â ðī â No ) & âĒ (ð â ðĩ â No ) â âĒ (ð â (ðī -s ðĩ) = (ðī +s ( -us âðĩ))) | ||
Theorem | subscl 27534 | Closure law for surreal subtraction. (Contributed by Scott Fenton, 3-Feb-2025.) |
âĒ ((ðī â No ⧠ðĩ â No ) â (ðī -s ðĩ) â No ) | ||
Theorem | subscld 27535 | Closure law for surreal subtraction. (Contributed by Scott Fenton, 5-Feb-2025.) |
âĒ (ð â ðī â No ) & âĒ (ð â ðĩ â No ) â âĒ (ð â (ðī -s ðĩ) â No ) | ||
Theorem | subsid1 27536 | Identity law for subtraction. (Contributed by Scott Fenton, 3-Feb-2025.) |
âĒ (ðī â No â (ðī -s 0s ) = ðī) | ||
Theorem | subsid 27537 | Subtraction of a surreal from itself. (Contributed by Scott Fenton, 3-Feb-2025.) |
âĒ (ðī â No â (ðī -s ðī) = 0s ) | ||
Theorem | subadds 27538 | Relationship between addition and subtraction for surreals. (Contributed by Scott Fenton, 3-Feb-2025.) |
âĒ ((ðī â No ⧠ðĩ â No ⧠ðķ â No ) â ((ðī -s ðĩ) = ðķ â (ðĩ +s ðķ) = ðī)) | ||
Theorem | subaddsd 27539 | Relationship between addition and subtraction for surreals. (Contributed by Scott Fenton, 5-Feb-2025.) |
âĒ (ð â ðī â No ) & âĒ (ð â ðĩ â No ) & âĒ (ð â ðķ â No ) â âĒ (ð â ((ðī -s ðĩ) = ðķ â (ðĩ +s ðķ) = ðī)) | ||
Theorem | pncans 27540 | Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 4-Feb-2025.) |
âĒ ((ðī â No ⧠ðĩ â No ) â ((ðī +s ðĩ) -s ðĩ) = ðī) | ||
Theorem | pncan3s 27541 | Subtraction and addition of equals. (Contributed by Scott Fenton, 4-Feb-2025.) |
âĒ ((ðī â No ⧠ðĩ â No ) â (ðī +s (ðĩ -s ðī)) = ðĩ) | ||
Theorem | npcans 27542 | Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 4-Feb-2025.) |
âĒ ((ðī â No ⧠ðĩ â No ) â ((ðī -s ðĩ) +s ðĩ) = ðī) | ||
Theorem | sltsub1 27543 | Subtraction from both sides of surreal less-than. (Contributed by Scott Fenton, 4-Feb-2025.) |
âĒ ((ðī â No ⧠ðĩ â No ⧠ðķ â No ) â (ðī <s ðĩ â (ðī -s ðķ) <s (ðĩ -s ðķ))) | ||
Theorem | sltsub2 27544 | Subtraction from both sides of surreal less-than. (Contributed by Scott Fenton, 4-Feb-2025.) |
âĒ ((ðī â No ⧠ðĩ â No ⧠ðķ â No ) â (ðī <s ðĩ â (ðķ -s ðĩ) <s (ðķ -s ðī))) | ||
Theorem | sltsub1d 27545 | Subtraction from both sides of surreal less-than. (Contributed by Scott Fenton, 5-Feb-2025.) |
âĒ (ð â ðī â No ) & âĒ (ð â ðĩ â No ) & âĒ (ð â ðķ â No ) â âĒ (ð â (ðī <s ðĩ â (ðī -s ðķ) <s (ðĩ -s ðķ))) | ||
Theorem | sltsub2d 27546 | Subtraction from both sides of surreal less-than. (Contributed by Scott Fenton, 5-Feb-2025.) |
âĒ (ð â ðī â No ) & âĒ (ð â ðĩ â No ) & âĒ (ð â ðķ â No ) â âĒ (ð â (ðī <s ðĩ â (ðķ -s ðĩ) <s (ðķ -s ðī))) | ||
Theorem | negsubsdi2d 27547 | Distribution of negative over subtraction. (Contributed by Scott Fenton, 5-Feb-2025.) |
âĒ (ð â ðī â No ) & âĒ (ð â ðĩ â No ) â âĒ (ð â ( -us â(ðī -s ðĩ)) = (ðĩ -s ðī)) | ||
Theorem | addsubsassd 27548 | Associative-type law for surreal addition and subtraction. (Contributed by Scott Fenton, 6-Feb-2025.) |
âĒ (ð â ðī â No ) & âĒ (ð â ðĩ â No ) & âĒ (ð â ðķ â No ) â âĒ (ð â ((ðī +s ðĩ) -s ðķ) = (ðī +s (ðĩ -s ðķ))) | ||
Theorem | addsubsd 27549 | Law for surreal addition and subtraction. (Contributed by Scott Fenton, 4-Mar-2025.) |
âĒ (ð â ðī â No ) & âĒ (ð â ðĩ â No ) & âĒ (ð â ðķ â No ) â âĒ (ð â ((ðī +s ðĩ) -s ðķ) = ((ðī -s ðķ) +s ðĩ)) | ||
Theorem | sltsubsubbd 27550 | 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 27551 | 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 27552 | 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 27553 | 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 27554 | 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 27555 | 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 27556 | Surreal less-than relationship between subtraction and addition. (Contributed by Scott Fenton, 27-Feb-2025.) |
âĒ (ð â ðī â No ) & âĒ (ð â ðĩ â No ) & âĒ (ð â ðķ â No ) â âĒ (ð â ((ðī -s ðĩ) <s ðķ â ðī <s (ðķ +s ðĩ))) | ||
Theorem | sltsubadd2d 27557 | Surreal less-than relationship between subtraction and addition. (Contributed by Scott Fenton, 27-Feb-2025.) |
âĒ (ð â ðī â No ) & âĒ (ð â ðĩ â No ) & âĒ (ð â ðķ â No ) â âĒ (ð â ((ðī -s ðĩ) <s ðķ â ðī <s (ðĩ +s ðķ))) | ||
Theorem | sltaddsubd 27558 | Surreal less-than relationship between subtraction and addition. (Contributed by Scott Fenton, 28-Feb-2025.) |
âĒ (ð â ðī â No ) & âĒ (ð â ðĩ â No ) & âĒ (ð â ðķ â No ) â âĒ (ð â ((ðī +s ðĩ) <s ðķ â ðī <s (ðķ -s ðĩ))) | ||
Theorem | sltaddsub2d 27559 | Surreal less-than relationship between subtraction and addition. (Contributed by Scott Fenton, 28-Feb-2025.) |
âĒ (ð â ðī â No ) & âĒ (ð â ðĩ â No ) & âĒ (ð â ðķ â No ) â âĒ (ð â ((ðī +s ðĩ) <s ðķ â ðĩ <s (ðķ -s ðī))) | ||
Theorem | subsubs4d 27560 | Law for double surreal subtraction. (Contributed by Scott Fenton, 9-Mar-2025.) |
âĒ (ð â ðī â No ) & âĒ (ð â ðĩ â No ) & âĒ (ð â ðķ â No ) â âĒ (ð â ((ðī -s ðĩ) -s ðķ) = (ðī -s (ðĩ +s ðķ))) | ||
Theorem | posdifsd 27561 | Comparison of two surreals whose difference is positive. (Contributed by Scott Fenton, 10-Mar-2025.) |
âĒ (ð â ðī â No ) & âĒ (ð â ðĩ â No ) â âĒ (ð â (ðī <s ðĩ â 0s <s (ðĩ -s ðī))) | ||
Syntax | cmuls 27562 | Set up the syntax for surreal multiplication. |
class ·s | ||
Definition | df-muls 27563* | 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 27564 | Surreal multiplication is a function over surreals. (Contributed by Scott Fenton, 4-Feb-2025.) |
âĒ ·s Fn ( No à No ) | ||
Theorem | mulsval 27565* | 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 27566* | Lemma for mulsval2 27567. 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 27567* | 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 27568 | Surreal multiplication by zero. (Contributed by Scott Fenton, 4-Feb-2025.) |
âĒ (ðī â No â (ðī ·s 0s ) = 0s ) | ||
Theorem | mulsrid 27569 | Surreal one is a right identity element for multiplication. (Contributed by Scott Fenton, 4-Feb-2025.) |
âĒ (ðī â No â (ðī ·s 1s ) = ðī) | ||
Theorem | mulsridd 27570 | Surreal one is a right identity element for multiplication. (Contributed by Scott Fenton, 14-Mar-2025.) |
âĒ (ð â ðī â No ) â âĒ (ð â (ðī ·s 1s ) = ðī) | ||
Theorem | mulsproplemcbv 27571* | 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 27572* | 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 27573* | 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 27574* | 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 27575* | 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 27576* | 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 27577* | 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 27578* | 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 27579* | 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 27580* | 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 27581* | 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 27582* | 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 ) | ||
Theorem | mulsproplem12 27583* | Lemma for surreal multiplication. Demonstrate the second half of the inductive statement assuming ðķ and ð· are not the same age and ðļ and ðđ are not the same age. (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 ) & âĒ (ð â ðķ <s ð·) & âĒ (ð â ðļ <s ðđ) & âĒ (ð â (( bday âðķ) â ( bday âð·) âĻ ( bday âð·) â ( bday âðķ))) & âĒ (ð â (( bday âðļ) â ( bday âðđ) âĻ ( bday âðđ) â ( bday âðļ))) â âĒ (ð â ((ðķ ·s ðđ) -s (ðķ ·s ðļ)) <s ((ð· ·s ðđ) -s (ð· ·s ðļ))) | ||
Theorem | mulsproplem13 27584* | Lemma for surreal multiplication. Remove the restriction on ðķ and ð· from mulsproplem12 27583. (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 ) & âĒ (ð â ðķ <s ð·) & âĒ (ð â ðļ <s ðđ) & âĒ (ð â (( bday âðļ) â ( bday âðđ) âĻ ( bday âðđ) â ( bday âðļ))) â âĒ (ð â ((ðķ ·s ðđ) -s (ðķ ·s ðļ)) <s ((ð· ·s ðđ) -s (ð· ·s ðļ))) | ||
Theorem | mulsproplem14 27585* | Lemma for surreal multiplication. Finally, we remove the restriction on ðļ and ðđ from mulsproplem12 27583 and mulsproplem13 27584. This completes the induction on surreal multiplication. mulsprop 27586 brings all this together technically. (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 ) & âĒ (ð â ðķ <s ð·) & âĒ (ð â ðļ <s ðđ) â âĒ (ð â ((ðķ ·s ðđ) -s (ðķ ·s ðļ)) <s ((ð· ·s ðđ) -s (ð· ·s ðļ))) | ||
Theorem | mulsprop 27586 | Surreals are closed under multiplication and obey a particular ordering law. Theorem 3.4 of [Gonshor] p. 17. (Contributed by Scott Fenton, 5-Mar-2025.) |
âĒ (((ðī â No ⧠ðĩ â No ) ⧠(ðķ â No ⧠ð· â No ) ⧠(ðļ â No ⧠ðđ â No )) â ((ðī ·s ðĩ) â No ⧠((ðķ <s ð· ⧠ðļ <s ðđ) â ((ðķ ·s ðđ) -s (ðķ ·s ðļ)) <s ((ð· ·s ðđ) -s (ð· ·s ðļ))))) | ||
Theorem | mulscutlem 27587* | Lemma for mulscut 27588. State the theorem with extra DV conditions. (Contributed by Scott Fenton, 7-Mar-2025.) |
âĒ (ð â ðī â 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 | mulscut 27588* | Show the cut properties of surreal multiplication. (Contributed by Scott Fenton, 8-Mar-2025.) |
âĒ (ð â ðī â 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 | mulscut2 27589* | Show that the cut involved in surreal multiplication is actually a cut. (Contributed by Scott Fenton, 7-Mar-2025.) |
âĒ (ð â ðī â 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 | mulscl 27590 | The surreals are closed under multiplication. Theorem 8(i) of [Conway] p. 19. (Contributed by Scott Fenton, 5-Mar-2025.) |
âĒ ((ðī â No ⧠ðĩ â No ) â (ðī ·s ðĩ) â No ) | ||
Theorem | mulscld 27591 | The surreals are closed under multiplication. Theorem 8(i) of [Conway] p. 19. (Contributed by Scott Fenton, 6-Mar-2025.) |
âĒ (ð â ðī â No ) & âĒ (ð â ðĩ â No ) â âĒ (ð â (ðī ·s ðĩ) â No ) | ||
Theorem | sltmul 27592 | An ordering relationship for surreal multiplication. Compare theorem 8(iii) of [Conway] p. 19. (Contributed by Scott Fenton, 5-Mar-2025.) |
âĒ (((ðī â No ⧠ðĩ â No ) ⧠(ðķ â No ⧠ð· â No )) â ((ðī <s ðĩ ⧠ðķ <s ð·) â ((ðī ·s ð·) -s (ðī ·s ðķ)) <s ((ðĩ ·s ð·) -s (ðĩ ·s ðķ)))) | ||
Theorem | sltmuld 27593 | An ordering relationship for surreal multiplication. Compare theorem 8(iii) of [Conway] p. 19. (Contributed by Scott Fenton, 6-Mar-2025.) |
âĒ (ð â ðī â No ) & âĒ (ð â ðĩ â No ) & âĒ (ð â ðķ â No ) & âĒ (ð â ð· â No ) & âĒ (ð â ðī <s ðĩ) & âĒ (ð â ðķ <s ð·) â âĒ (ð â ((ðī ·s ð·) -s (ðī ·s ðķ)) <s ((ðĩ ·s ð·) -s (ðĩ ·s ðķ))) | ||
Theorem | slemuld 27594 | An ordering relationship for surreal multiplication. Compare theorem 8(iii) of [Conway] p. 19. (Contributed by Scott Fenton, 7-Mar-2025.) |
âĒ (ð â ðī â No ) & âĒ (ð â ðĩ â No ) & âĒ (ð â ðķ â No ) & âĒ (ð â ð· â No ) & âĒ (ð â ðī âĪs ðĩ) & âĒ (ð â ðķ âĪs ð·) â âĒ (ð â ((ðī ·s ð·) -s (ðī ·s ðķ)) âĪs ((ðĩ ·s ð·) -s (ðĩ ·s ðķ))) | ||
Theorem | mulscom 27595 | Surreal multiplication commutes. Part of theorem 7 of [Conway] p. 19. (Contributed by Scott Fenton, 6-Mar-2025.) |
âĒ ((ðī â No ⧠ðĩ â No ) â (ðī ·s ðĩ) = (ðĩ ·s ðī)) | ||
Theorem | mulscomd 27596 | Surreal multiplication commutes. Part of theorem 7 of [Conway] p. 19. (Contributed by Scott Fenton, 6-Mar-2025.) |
âĒ (ð â ðī â No ) & âĒ (ð â ðĩ â No ) â âĒ (ð â (ðī ·s ðĩ) = (ðĩ ·s ðī)) | ||
Theorem | muls02 27597 | Surreal multiplication by zero. (Contributed by Scott Fenton, 4-Feb-2025.) |
âĒ (ðī â No â ( 0s ·s ðī) = 0s ) | ||
Theorem | mulslid 27598 | Surreal one is a left identity element for multiplication. (Contributed by Scott Fenton, 4-Feb-2025.) |
âĒ (ðī â No â ( 1s ·s ðī) = ðī) | ||
Theorem | mulslidd 27599 | Surreal one is a left identity element for multiplication. (Contributed by Scott Fenton, 14-Mar-2025.) |
âĒ (ð â ðī â No ) â âĒ (ð â ( 1s ·s ðī) = ðī) | ||
Theorem | mulsgt0 27600 | The product of two positive surreals is positive. Theorem 9 of [Conway] p. 20. (Contributed by Scott Fenton, 6-Mar-2025.) |
âĒ (((ðī â No ⧠0s <s ðī) ⧠(ðĩ â No ⧠0s <s ðĩ)) â 0s <s (ðī ·s ðĩ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |