![]() |
Metamath
Proof Explorer Theorem List (p. 279 of 481) | < 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-30640) |
![]() (30641-32163) |
![]() (32164-48040) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | addslid 27801 | Surreal addition to zero is identity. (Contributed by Scott Fenton, 3-Feb-2025.) |
âĒ (ðī â No â ( 0s +s ðī) = ðī) | ||
Theorem | addsproplem1 27802* | Lemma for surreal addition properties. To prove closure on surreal addition we need to prove that addition is compatible with order at the same time. We do this by inducting over the maximum of two natural sums of the birthdays of surreals numbers. In the final step we will loop around and use tfr3 8394 to prove this of all surreals. This first lemma just instantiates the inductive hypothesis so we do not need to do it continuously throughout the proof. (Contributed by Scott Fenton, 21-Jan-2025.) |
âĒ (ð â âðĨ â No âðĶ â No âð§ â No (((( bday âðĨ) +no ( bday âðĶ)) ⊠(( bday âðĨ) +no ( bday âð§))) â ((( bday âð) +no ( bday âð)) ⊠(( bday âð) +no ( bday âð))) â ((ðĨ +s ðĶ) â No â§ (ðĶ <s ð§ â (ðĶ +s ðĨ) <s (ð§ +s ðĨ))))) & âĒ (ð â ðī â No ) & âĒ (ð â ðĩ â No ) & âĒ (ð â ðķ â No ) & âĒ (ð â ((( bday âðī) +no ( bday âðĩ)) ⊠(( bday âðī) +no ( bday âðķ))) â ((( bday âð) +no ( bday âð)) ⊠(( bday âð) +no ( bday âð)))) â âĒ (ð â ((ðī +s ðĩ) â No â§ (ðĩ <s ðķ â (ðĩ +s ðī) <s (ðķ +s ðī)))) | ||
Theorem | addsproplem2 27803* | Lemma for surreal addition properties. When proving closure for operations defined using norec and norec2, it is a strictly stronger statement to say that the cut defined is actually a cut than it is to say that the operation is closed. We will often prove this stronger statement. Here, we do so for the cut involved in surreal addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
âĒ (ð â âðĨ â No âðĶ â No âð§ â No (((( bday âðĨ) +no ( bday âðĶ)) ⊠(( bday âðĨ) +no ( bday âð§))) â ((( bday âð) +no ( bday âð)) ⊠(( bday âð) +no ( bday âð))) â ((ðĨ +s ðĶ) â No â§ (ðĶ <s ð§ â (ðĶ +s ðĨ) <s (ð§ +s ðĨ))))) & âĒ (ð â ð â No ) & âĒ (ð â ð â No ) â âĒ (ð â ({ð âĢ âð â ( L âð)ð = (ð +s ð)} ⊠{ð âĢ âð â ( L âð)ð = (ð +s ð)}) <<s ({ðĪ âĢ âð â ( R âð)ðĪ = (ð +s ð)} ⊠{ðĄ âĢ âð â ( R âð)ðĄ = (ð +s ð )})) | ||
Theorem | addsproplem3 27804* | Lemma for surreal addition properties. Show the cut properties of surreal addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
âĒ (ð â âðĨ â No âðĶ â No âð§ â No (((( bday âðĨ) +no ( bday âðĶ)) ⊠(( bday âðĨ) +no ( bday âð§))) â ((( bday âð) +no ( bday âð)) ⊠(( bday âð) +no ( bday âð))) â ((ðĨ +s ðĶ) â No â§ (ðĶ <s ð§ â (ðĶ +s ðĨ) <s (ð§ +s ðĨ))))) & âĒ (ð â ð â No ) & âĒ (ð â ð â No ) â âĒ (ð â ((ð +s ð) â No â§ ({ð âĢ âð â ( L âð)ð = (ð +s ð)} ⊠{ð âĢ âð â ( L âð)ð = (ð +s ð)}) <<s {(ð +s ð)} â§ {(ð +s ð)} <<s ({ðĪ âĢ âð â ( R âð)ðĪ = (ð +s ð)} ⊠{ðĄ âĢ âð â ( R âð)ðĄ = (ð +s ð )}))) | ||
Theorem | addsproplem4 27805* | Lemma for surreal addition properties. Show the second half of the inductive hypothesis when ð is older than ð. (Contributed by Scott Fenton, 21-Jan-2025.) |
âĒ (ð â âðĨ â No âðĶ â No âð§ â No (((( bday âðĨ) +no ( bday âðĶ)) ⊠(( bday âðĨ) +no ( bday âð§))) â ((( bday âð) +no ( bday âð)) ⊠(( bday âð) +no ( bday âð))) â ((ðĨ +s ðĶ) â No â§ (ðĶ <s ð§ â (ðĶ +s ðĨ) <s (ð§ +s ðĨ))))) & âĒ (ð â ð â No ) & âĒ (ð â ð â No ) & âĒ (ð â ð â No ) & âĒ (ð â ð <s ð) & âĒ (ð â ( bday âð) â ( bday âð)) â âĒ (ð â (ð +s ð) <s (ð +s ð)) | ||
Theorem | addsproplem5 27806* | Lemma for surreal addition properties. Show the second half of the inductive hypothesis when ð is older than ð. (Contributed by Scott Fenton, 21-Jan-2025.) |
âĒ (ð â âðĨ â No âðĶ â No âð§ â No (((( bday âðĨ) +no ( bday âðĶ)) ⊠(( bday âðĨ) +no ( bday âð§))) â ((( bday âð) +no ( bday âð)) ⊠(( bday âð) +no ( bday âð))) â ((ðĨ +s ðĶ) â No â§ (ðĶ <s ð§ â (ðĶ +s ðĨ) <s (ð§ +s ðĨ))))) & âĒ (ð â ð â No ) & âĒ (ð â ð â No ) & âĒ (ð â ð â No ) & âĒ (ð â ð <s ð) & âĒ (ð â ( bday âð) â ( bday âð)) â âĒ (ð â (ð +s ð) <s (ð +s ð)) | ||
Theorem | addsproplem6 27807* | Lemma for surreal addition properties. Finally, we show the second half of the induction hypothesis when ð and ð are the same age. (Contributed by Scott Fenton, 21-Jan-2025.) |
âĒ (ð â âðĨ â No âðĶ â No âð§ â No (((( bday âðĨ) +no ( bday âðĶ)) ⊠(( bday âðĨ) +no ( bday âð§))) â ((( bday âð) +no ( bday âð)) ⊠(( bday âð) +no ( bday âð))) â ((ðĨ +s ðĶ) â No â§ (ðĶ <s ð§ â (ðĶ +s ðĨ) <s (ð§ +s ðĨ))))) & âĒ (ð â ð â No ) & âĒ (ð â ð â No ) & âĒ (ð â ð â No ) & âĒ (ð â ð <s ð) & âĒ (ð â ( bday âð) = ( bday âð)) â âĒ (ð â (ð +s ð) <s (ð +s ð)) | ||
Theorem | addsproplem7 27808* | Lemma for surreal addition properties. Putting together the three previous lemmas, we now show the second half of the inductive hypothesis unconditionally. (Contributed by Scott Fenton, 21-Jan-2025.) |
âĒ (ð â âðĨ â No âðĶ â No âð§ â No (((( bday âðĨ) +no ( bday âðĶ)) ⊠(( bday âðĨ) +no ( bday âð§))) â ((( bday âð) +no ( bday âð)) ⊠(( bday âð) +no ( bday âð))) â ((ðĨ +s ðĶ) â No â§ (ðĶ <s ð§ â (ðĶ +s ðĨ) <s (ð§ +s ðĨ))))) & âĒ (ð â ð â No ) & âĒ (ð â ð â No ) & âĒ (ð â ð â No ) & âĒ (ð â ð <s ð) â âĒ (ð â (ð +s ð) <s (ð +s ð)) | ||
Theorem | addsprop 27809 | Inductively show that surreal addition is closed and compatible with less-than. This proof follows from induction on the birthdays of the surreal numbers involved. This pattern occurs throughout surreal development. Theorem 3.1 of [Gonshor] p. 14. (Contributed by Scott Fenton, 21-Jan-2025.) |
âĒ ((ð â No â§ ð â No â§ ð â No ) â ((ð +s ð) â No â§ (ð <s ð â (ð +s ð) <s (ð +s ð)))) | ||
Theorem | addscutlem 27810* | Lemma for addscut 27811. Show the statement with some additional distinct variable conditions. (Contributed by Scott Fenton, 8-Mar-2025.) |
âĒ (ð â ð â No ) & âĒ (ð â ð â No ) â âĒ (ð â ((ð +s ð) â No â§ ({ð âĢ âð â ( L âð)ð = (ð +s ð)} ⊠{ð âĢ âð â ( L âð)ð = (ð +s ð)}) <<s {(ð +s ð)} â§ {(ð +s ð)} <<s ({ðĪ âĢ âð â ( R âð)ðĪ = (ð +s ð)} ⊠{ðĄ âĢ âð â ( R âð)ðĄ = (ð +s ð )}))) | ||
Theorem | addscut 27811* | Demonstrate the cut properties of surreal addition. This gives us closure together with a pair of set-less-than relationships for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
âĒ (ð â ð â No ) & âĒ (ð â ð â No ) â âĒ (ð â ((ð +s ð) â No â§ ({ð âĢ âð â ( L âð)ð = (ð +s ð)} ⊠{ð âĢ âð â ( L âð)ð = (ð +s ð)}) <<s {(ð +s ð)} â§ {(ð +s ð)} <<s ({ðĪ âĢ âð â ( R âð)ðĪ = (ð +s ð)} ⊠{ðĄ âĢ âð â ( R âð)ðĄ = (ð +s ð )}))) | ||
Theorem | addscut2 27812* | 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 27813 | 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 27814 | 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 27815 | Function statement for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
âĒ +s :( No à No )âķ No | ||
Theorem | addsfo 27816 | Surreal addition is onto. (Contributed by Scott Fenton, 21-Jan-2025.) |
âĒ +s :( No à No )âontoâ No | ||
Theorem | peano2no 27817 | A theorem for surreals that is analagous to the second Peano postulate peano2 7874. (Contributed by Scott Fenton, 17-Mar-2025.) |
âĒ (ðī â No â (ðī +s 1s ) â No ) | ||
Theorem | sltadd1im 27818 | Surreal less-than is preserved under addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
âĒ ((ðī â No â§ ðĩ â No â§ ðķ â No ) â (ðī <s ðĩ â (ðī +s ðķ) <s (ðĩ +s ðķ))) | ||
Theorem | sltadd2im 27819 | Surreal less-than is preserved under addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
âĒ ((ðī â No â§ ðĩ â No â§ ðķ â No ) â (ðī <s ðĩ â (ðķ +s ðī) <s (ðķ +s ðĩ))) | ||
Theorem | sleadd1im 27820 | Surreal less-than or equal cancels under addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
âĒ ((ðī â No â§ ðĩ â No â§ ðķ â No ) â ((ðī +s ðķ) âĪs (ðĩ +s ðķ) â ðī âĪs ðĩ)) | ||
Theorem | sleadd2im 27821 | Surreal less-than or equal cancels under addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
âĒ ((ðī â No â§ ðĩ â No â§ ðķ â No ) â ((ðķ +s ðī) âĪs (ðķ +s ðĩ) â ðī âĪs ðĩ)) | ||
Theorem | sleadd1 27822 | 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 27823 | 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 27824 | Addition to both sides of surreal less-than. (Contributed by Scott Fenton, 21-Jan-2025.) |
âĒ ((ðī â No â§ ðĩ â No â§ ðķ â No ) â (ðī <s ðĩ â (ðķ +s ðī) <s (ðķ +s ðĩ))) | ||
Theorem | sltadd1 27825 | Addition to both sides of surreal less-than. (Contributed by Scott Fenton, 21-Jan-2025.) |
âĒ ((ðī â No â§ ðĩ â No â§ ðķ â No ) â (ðī <s ðĩ â (ðī +s ðķ) <s (ðĩ +s ðķ))) | ||
Theorem | addscan2 27826 | Cancellation law for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
âĒ ((ðī â No â§ ðĩ â No â§ ðķ â No ) â ((ðī +s ðķ) = (ðĩ +s ðķ) â ðī = ðĩ)) | ||
Theorem | addscan1 27827 | Cancellation law for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
âĒ ((ðī â No â§ ðĩ â No â§ ðķ â No ) â ((ðķ +s ðī) = (ðķ +s ðĩ) â ðī = ðĩ)) | ||
Theorem | sleadd1d 27828 | 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 27829 | 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 27830 | Addition to both sides of surreal less-than. (Contributed by Scott Fenton, 21-Jan-2025.) |
âĒ (ð â ðī â No ) & âĒ (ð â ðĩ â No ) & âĒ (ð â ðķ â No ) â âĒ (ð â (ðī <s ðĩ â (ðķ +s ðī) <s (ðķ +s ðĩ))) | ||
Theorem | sltadd1d 27831 | Addition to both sides of surreal less-than. (Contributed by Scott Fenton, 5-Feb-2025.) |
âĒ (ð â ðī â No ) & âĒ (ð â ðĩ â No ) & âĒ (ð â ðķ â No ) â âĒ (ð â (ðī <s ðĩ â (ðī +s ðķ) <s (ðĩ +s ðķ))) | ||
Theorem | addscan2d 27832 | Cancellation law for surreal addition. (Contributed by Scott Fenton, 5-Feb-2025.) |
âĒ (ð â ðī â No ) & âĒ (ð â ðĩ â No ) & âĒ (ð â ðķ â No ) â âĒ (ð â ((ðī +s ðķ) = (ðĩ +s ðķ) â ðī = ðĩ)) | ||
Theorem | addscan1d 27833 | Cancellation law for surreal addition. (Contributed by Scott Fenton, 5-Feb-2025.) |
âĒ (ð â ðī â No ) & âĒ (ð â ðĩ â No ) & âĒ (ð â ðķ â No ) â âĒ (ð â ((ðķ +s ðī) = (ðķ +s ðĩ) â ðī = ðĩ)) | ||
Theorem | addsuniflem 27834* | Lemma for addsunif 27835. 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 27835* | 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 27836* | 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 27837* | 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 27838 | 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 27839 | 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 27840 | 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 27841 | 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 27842 | 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 27843 | 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 | sltaddpos1d 27844 | Addition of a positive number increases the sum. (Contributed by Scott Fenton, 15-Apr-2025.) |
âĒ (ð â ðī â No ) & âĒ (ð â ðĩ â No ) â âĒ (ð â ( 0s <s ðī â ðĩ <s (ðĩ +s ðī))) | ||
Theorem | sltaddpos2d 27845 | Addition of a positive number increases the sum. (Contributed by Scott Fenton, 15-Apr-2025.) |
âĒ (ð â ðī â No ) & âĒ (ð â ðĩ â No ) â âĒ (ð â ( 0s <s ðī â ðĩ <s (ðī +s ðĩ))) | ||
Theorem | slt2addd 27846 | 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 27847 | The sum of two positive surreals is positive. (Contributed by Scott Fenton, 15-Apr-2025.) |
âĒ (ð â ðī â No ) & âĒ (ð â ðĩ â No ) & âĒ (ð â 0s <s ðī) & âĒ (ð â 0s <s ðĩ) â âĒ (ð â 0s <s (ðī +s ðĩ)) | ||
Syntax | cnegs 27848 | Declare the syntax for surreal negation. |
class -us | ||
Syntax | csubs 27849 | Declare the syntax for surreal subtraction. |
class -s | ||
Definition | df-negs 27850* | 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 27851* | Define surreal subtraction. (Contributed by Scott Fenton, 20-Aug-2024.) |
âĒ -s = (ðĨ â No , ðĶ â No âĶ (ðĨ +s ( -us âðĶ))) | ||
Theorem | negsfn 27852 | Surreal negation is a function over surreals. (Contributed by Scott Fenton, 20-Aug-2024.) |
âĒ -us Fn No | ||
Theorem | subsfn 27853 | Surreal subtraction is a function over pairs of surreals. (Contributed by Scott Fenton, 22-Jan-2025.) |
âĒ -s Fn ( No à No ) | ||
Theorem | negsval 27854 | The value of the surreal negation function. (Contributed by Scott Fenton, 20-Aug-2024.) |
âĒ (ðī â No â ( -us âðī) = (( -us â ( R âðī)) |s ( -us â ( L âðī)))) | ||
Theorem | negs0s 27855 | Negative surreal zero is surreal zero. (Contributed by Scott Fenton, 20-Aug-2024.) |
âĒ ( -us â 0s ) = 0s | ||
Theorem | negsproplem1 27856* | 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 27857* | 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 27858* | 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 27859* | 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 27860* | 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 27861* | 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 27862* | 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 27863 | Show closure and ordering properties of negation. (Contributed by Scott Fenton, 3-Feb-2025.) |
âĒ ((ðī â No â§ ðĩ â No ) â (( -us âðī) â No â§ (ðī <s ðĩ â ( -us âðĩ) <s ( -us âðī)))) | ||
Theorem | negscl 27864 | 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 27865 | 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 27866 | The forward direction of the ordering properties of negation. (Contributed by Scott Fenton, 3-Feb-2025.) |
âĒ ((ðī â No â§ ðĩ â No ) â (ðī <s ðĩ â ( -us âðĩ) <s ( -us âðī))) | ||
Theorem | negscut 27867 | 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 27868 | The cut that defines surreal negation is legitimate. (Contributed by Scott Fenton, 3-Feb-2025.) |
âĒ (ðī â No â ( -us â ( R âðī)) <<s ( -us â ( L âðī))) | ||
Theorem | negsid 27869 | 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 27870 | 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 27871* | Every surreal has a negative. Note that this theorem, addscl 27814, addscom 27799, addsass 27838, addsrid 27797, and sltadd1im 27818 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 27872 | 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 27873 | Negative of both sides of surreal less-than. (Contributed by Scott Fenton, 3-Feb-2025.) |
âĒ ((ðī â No â§ ðĩ â No ) â (ðī <s ðĩ â ( -us âðĩ) <s ( -us âðī))) | ||
Theorem | sleneg 27874 | 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 27875 | Negative of both sides of surreal less-than. (Contributed by Scott Fenton, 14-Mar-2025.) |
âĒ (ð â ðī â No ) & âĒ (ð â ðĩ â No ) â âĒ (ð â (ðī <s ðĩ â ( -us âðĩ) <s ( -us âðī))) | ||
Theorem | slenegd 27876 | 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 27877 | Surreal negation is one-to-one. (Contributed by Scott Fenton, 3-Feb-2025.) |
âĒ ((ðī â No â§ ðĩ â No ) â (( -us âðī) = ( -us âðĩ) â ðī = ðĩ)) | ||
Theorem | negsdi 27878 | Distribution of surreal negative over addition. (Contributed by Scott Fenton, 5-Feb-2025.) |
âĒ ((ðī â No â§ ðĩ â No ) â ( -us â(ðī +s ðĩ)) = (( -us âðī) +s ( -us âðĩ))) | ||
Theorem | slt0neg2d 27879 | Comparison of a surreal and its negative to zero. (Contributed by Scott Fenton, 10-Mar-2025.) |
âĒ (ð â ðī â No ) â âĒ (ð â ( 0s <s ðī â ( -us âðī) <s 0s )) | ||
Theorem | negsf 27880 | Function statement for surreal negation. (Contributed by Scott Fenton, 3-Feb-2025.) |
âĒ -us : No âķ No | ||
Theorem | negsfo 27881 | Function statement for surreal negation. (Contributed by Scott Fenton, 3-Feb-2025.) |
âĒ -us : No âontoâ No | ||
Theorem | negsf1o 27882 | Surreal negation is a bijection. (Contributed by Scott Fenton, 3-Feb-2025.) |
âĒ -us : No â1-1-ontoâ No | ||
Theorem | negsunif 27883 | 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 27884 | Lemma for negsbday 27885. Bound the birthday of the negative of a surreal number above. (Contributed by Scott Fenton, 8-Mar-2025.) |
âĒ (ðī â No â ( bday â( -us âðī)) â ( bday âðī)) | ||
Theorem | negsbday 27885 | Negation of a surreal number preserves birthday. (Contributed by Scott Fenton, 8-Mar-2025.) |
âĒ (ðī â No â ( bday â( -us âðī)) = ( bday âðī)) | ||
Theorem | subsval 27886 | The value of surreal subtraction. (Contributed by Scott Fenton, 3-Feb-2025.) |
âĒ ((ðī â No â§ ðĩ â No ) â (ðī -s ðĩ) = (ðī +s ( -us âðĩ))) | ||
Theorem | subsvald 27887 | The value of surreal subtraction. (Contributed by Scott Fenton, 5-Feb-2025.) |
âĒ (ð â ðī â No ) & âĒ (ð â ðĩ â No ) â âĒ (ð â (ðī -s ðĩ) = (ðī +s ( -us âðĩ))) | ||
Theorem | subscl 27888 | Closure law for surreal subtraction. (Contributed by Scott Fenton, 3-Feb-2025.) |
âĒ ((ðī â No â§ ðĩ â No ) â (ðī -s ðĩ) â No ) | ||
Theorem | subscld 27889 | Closure law for surreal subtraction. (Contributed by Scott Fenton, 5-Feb-2025.) |
âĒ (ð â ðī â No ) & âĒ (ð â ðĩ â No ) â âĒ (ð â (ðī -s ðĩ) â No ) | ||
Theorem | negsval2 27890 | Surreal negation in terms of subtraction. (Contributed by Scott Fenton, 15-Apr-2025.) |
âĒ (ðī â No â ( -us âðī) = ( 0s -s ðī)) | ||
Theorem | negsval2d 27891 | Surreal negation in terms of subtraction. (Contributed by Scott Fenton, 15-Apr-2025.) |
âĒ (ð â ðī â No ) â âĒ (ð â ( -us âðī) = ( 0s -s ðī)) | ||
Theorem | subsid1 27892 | Identity law for subtraction. (Contributed by Scott Fenton, 3-Feb-2025.) |
âĒ (ðī â No â (ðī -s 0s ) = ðī) | ||
Theorem | subsid 27893 | Subtraction of a surreal from itself. (Contributed by Scott Fenton, 3-Feb-2025.) |
âĒ (ðī â No â (ðī -s ðī) = 0s ) | ||
Theorem | subadds 27894 | Relationship between addition and subtraction for surreals. (Contributed by Scott Fenton, 3-Feb-2025.) |
âĒ ((ðī â No â§ ðĩ â No â§ ðķ â No ) â ((ðī -s ðĩ) = ðķ â (ðĩ +s ðķ) = ðī)) | ||
Theorem | subaddsd 27895 | Relationship between addition and subtraction for surreals. (Contributed by Scott Fenton, 5-Feb-2025.) |
âĒ (ð â ðī â No ) & âĒ (ð â ðĩ â No ) & âĒ (ð â ðķ â No ) â âĒ (ð â ((ðī -s ðĩ) = ðķ â (ðĩ +s ðķ) = ðī)) | ||
Theorem | pncans 27896 | Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 4-Feb-2025.) |
âĒ ((ðī â No â§ ðĩ â No ) â ((ðī +s ðĩ) -s ðĩ) = ðī) | ||
Theorem | pncan3s 27897 | Subtraction and addition of equals. (Contributed by Scott Fenton, 4-Feb-2025.) |
âĒ ((ðī â No â§ ðĩ â No ) â (ðī +s (ðĩ -s ðī)) = ðĩ) | ||
Theorem | pncan2s 27898 | Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 16-Apr-2025.) |
âĒ ((ðī â No â§ ðĩ â No ) â ((ðī +s ðĩ) -s ðī) = ðĩ) | ||
Theorem | npcans 27899 | Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 4-Feb-2025.) |
âĒ ((ðī â No â§ ðĩ â No ) â ((ðī -s ðĩ) +s ðĩ) = ðī) | ||
Theorem | sltsub1 27900 | Subtraction from both sides of surreal less-than. (Contributed by Scott Fenton, 4-Feb-2025.) |
âĒ ((ðī â No â§ ðĩ â No â§ ðķ â No ) â (ðī <s ðĩ â (ðī -s ðķ) <s (ðĩ -s ðķ))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |