![]() |
Metamath
Proof Explorer Theorem List (p. 277 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 | mulsgt0d 27601 | The product of two positive surreals is positive. Theorem 9 of [Conway] p. 20. (Contributed by Scott Fenton, 6-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ 0s <s ๐ด) & โข (๐ โ 0s <s ๐ต) โ โข (๐ โ 0s <s (๐ด ยทs ๐ต)) | ||
Theorem | ssltmul1 27602* | One surreal set less-than relationship for cuts of ๐ด and ๐ต. (Contributed by Scott Fenton, 7-Mar-2025.) |
โข (๐ โ ๐ฟ <<s ๐ ) & โข (๐ โ ๐ <<s ๐) & โข (๐ โ ๐ด = (๐ฟ |s ๐ )) & โข (๐ โ ๐ต = (๐ |s ๐)) โ โข (๐ โ ({๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ๐ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) <<s {(๐ด ยทs ๐ต)}) | ||
Theorem | ssltmul2 27603* | One surreal set less-than relationship for cuts of ๐ด and ๐ต. (Contributed by Scott Fenton, 7-Mar-2025.) |
โข (๐ โ ๐ฟ <<s ๐ ) & โข (๐ โ ๐ <<s ๐) & โข (๐ โ ๐ด = (๐ฟ |s ๐ )) & โข (๐ โ ๐ต = (๐ |s ๐)) โ โข (๐ โ {(๐ด ยทs ๐ต)} <<s ({๐ โฃ โ๐ก โ ๐ฟ โ๐ข โ ๐ ๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))} โช {๐ โฃ โ๐ฃ โ ๐ โ๐ค โ ๐ ๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))})) | ||
Theorem | mulsuniflem 27604* | Lemma for mulsunif 27605. State the theorem with some extra distinct variable conditions. (Contributed by Scott Fenton, 8-Mar-2025.) |
โข (๐ โ ๐ฟ <<s ๐ ) & โข (๐ โ ๐ <<s ๐) & โข (๐ โ ๐ด = (๐ฟ |s ๐ )) & โข (๐ โ ๐ต = (๐ |s ๐)) โ โข (๐ โ (๐ด ยทs ๐ต) = (({๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ๐ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) |s ({๐ โฃ โ๐ก โ ๐ฟ โ๐ข โ ๐ ๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))} โช {๐ โฃ โ๐ฃ โ ๐ โ๐ค โ ๐ ๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))}))) | ||
Theorem | mulsunif 27605* | Surreal multiplication has the uniformity property. That is, any cuts that define ๐ด and ๐ต can be used in the definition of (๐ด ยทs ๐ต). Theorem 3.5 of [Gonshor] p. 18. (Contributed by Scott Fenton, 7-Mar-2025.) |
โข (๐ โ ๐ฟ <<s ๐ ) & โข (๐ โ ๐ <<s ๐) & โข (๐ โ ๐ด = (๐ฟ |s ๐ )) & โข (๐ โ ๐ต = (๐ |s ๐)) โ โข (๐ โ (๐ด ยทs ๐ต) = (({๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ๐ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) |s ({๐ โฃ โ๐ก โ ๐ฟ โ๐ข โ ๐ ๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))} โช {๐ โฃ โ๐ฃ โ ๐ โ๐ค โ ๐ ๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))}))) | ||
Theorem | addsdilem1 27606* | Lemma for surreal distribution. Expand the left hand side of the main expression. (Contributed by Scott Fenton, 8-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ถ โ No ) โ โข (๐ โ (๐ด ยทs (๐ต +s ๐ถ)) = ((({๐ โฃ โ๐ฅ๐ฟ โ ( L โ๐ด)โ๐ฆ๐ฟ โ ( L โ๐ต)๐ = (((๐ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ฆ๐ฟ +s ๐ถ))) -s (๐ฅ๐ฟ ยทs (๐ฆ๐ฟ +s ๐ถ)))} โช {๐ โฃ โ๐ฅ๐ฟ โ ( L โ๐ด)โ๐ง๐ฟ โ ( L โ๐ถ)๐ = (((๐ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐ง๐ฟ))) -s (๐ฅ๐ฟ ยทs (๐ต +s ๐ง๐ฟ)))}) โช ({๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ โ ( R โ๐ต)๐ = (((๐ฅ๐ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ฆ๐ +s ๐ถ))) -s (๐ฅ๐ ยทs (๐ฆ๐ +s ๐ถ)))} โช {๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ง๐ โ ( R โ๐ถ)๐ = (((๐ฅ๐ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐ง๐ ))) -s (๐ฅ๐ ยทs (๐ต +s ๐ง๐ )))})) |s (({๐ โฃ โ๐ฅ๐ฟ โ ( L โ๐ด)โ๐ฆ๐ โ ( R โ๐ต)๐ = (((๐ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ฆ๐ +s ๐ถ))) -s (๐ฅ๐ฟ ยทs (๐ฆ๐ +s ๐ถ)))} โช {๐ โฃ โ๐ฅ๐ฟ โ ( L โ๐ด)โ๐ง๐ โ ( R โ๐ถ)๐ = (((๐ฅ๐ฟ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐ง๐ ))) -s (๐ฅ๐ฟ ยทs (๐ต +s ๐ง๐ )))}) โช ({๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ฟ โ ( L โ๐ต)๐ = (((๐ฅ๐ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ฆ๐ฟ +s ๐ถ))) -s (๐ฅ๐ ยทs (๐ฆ๐ฟ +s ๐ถ)))} โช {๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ง๐ฟ โ ( L โ๐ถ)๐ = (((๐ฅ๐ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐ง๐ฟ))) -s (๐ฅ๐ ยทs (๐ต +s ๐ง๐ฟ)))})))) | ||
Theorem | addsdilem2 27607* | Lemma for surreal distribution. Expand the right hand side of the main expression. (Contributed by Scott Fenton, 8-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ถ โ No ) โ โข (๐ โ ((๐ด ยทs ๐ต) +s (๐ด ยทs ๐ถ)) = ((({๐ โฃ โ๐ฅ๐ฟ โ ( L โ๐ด)โ๐ฆ๐ฟ โ ( L โ๐ต)๐ = ((((๐ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐ฆ๐ฟ)) -s (๐ฅ๐ฟ ยทs ๐ฆ๐ฟ)) +s (๐ด ยทs ๐ถ))} โช {๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ โ ( R โ๐ต)๐ = ((((๐ฅ๐ ยทs ๐ต) +s (๐ด ยทs ๐ฆ๐ )) -s (๐ฅ๐ ยทs ๐ฆ๐ )) +s (๐ด ยทs ๐ถ))}) โช ({๐ โฃ โ๐ฅ๐ฟ โ ( L โ๐ด)โ๐ง๐ฟ โ ( L โ๐ถ)๐ = ((๐ด ยทs ๐ต) +s (((๐ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐ง๐ฟ)) -s (๐ฅ๐ฟ ยทs ๐ง๐ฟ)))} โช {๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ง๐ โ ( R โ๐ถ)๐ = ((๐ด ยทs ๐ต) +s (((๐ฅ๐ ยทs ๐ถ) +s (๐ด ยทs ๐ง๐ )) -s (๐ฅ๐ ยทs ๐ง๐ )))})) |s (({๐ โฃ โ๐ฅ๐ฟ โ ( L โ๐ด)โ๐ฆ๐ โ ( R โ๐ต)๐ = ((((๐ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐ฆ๐ )) -s (๐ฅ๐ฟ ยทs ๐ฆ๐ )) +s (๐ด ยทs ๐ถ))} โช {๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ฟ โ ( L โ๐ต)๐ = ((((๐ฅ๐ ยทs ๐ต) +s (๐ด ยทs ๐ฆ๐ฟ)) -s (๐ฅ๐ ยทs ๐ฆ๐ฟ)) +s (๐ด ยทs ๐ถ))}) โช ({๐ โฃ โ๐ฅ๐ฟ โ ( L โ๐ด)โ๐ง๐ โ ( R โ๐ถ)๐ = ((๐ด ยทs ๐ต) +s (((๐ฅ๐ฟ ยทs ๐ถ) +s (๐ด ยทs ๐ง๐ )) -s (๐ฅ๐ฟ ยทs ๐ง๐ )))} โช {๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ง๐ฟ โ ( L โ๐ถ)๐ = ((๐ด ยทs ๐ต) +s (((๐ฅ๐ ยทs ๐ถ) +s (๐ด ยทs ๐ง๐ฟ)) -s (๐ฅ๐ ยทs ๐ง๐ฟ)))})))) | ||
Theorem | addsdilem3 27608* | Lemma for addsdi 27610. Show one of the equalities involved in the final expression. (Contributed by Scott Fenton, 9-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ถ โ No ) & โข (๐ โ โ๐ฅ๐ โ (( L โ๐ด) โช ( R โ๐ด))(๐ฅ๐ ยทs (๐ต +s ๐ถ)) = ((๐ฅ๐ ยทs ๐ต) +s (๐ฅ๐ ยทs ๐ถ))) & โข (๐ โ โ๐ฆ๐ โ (( L โ๐ต) โช ( R โ๐ต))(๐ด ยทs (๐ฆ๐ +s ๐ถ)) = ((๐ด ยทs ๐ฆ๐) +s (๐ด ยทs ๐ถ))) & โข (๐ โ โ๐ฅ๐ โ (( L โ๐ด) โช ( R โ๐ด))โ๐ฆ๐ โ (( L โ๐ต) โช ( R โ๐ต))(๐ฅ๐ ยทs (๐ฆ๐ +s ๐ถ)) = ((๐ฅ๐ ยทs ๐ฆ๐) +s (๐ฅ๐ ยทs ๐ถ))) & โข (๐ โ ๐ โ (( L โ๐ด) โช ( R โ๐ด))) & โข (๐ โ ๐ โ (( L โ๐ต) โช ( R โ๐ต))) โ โข ((๐ โง ๐) โ (((๐ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ +s ๐ถ))) -s (๐ ยทs (๐ +s ๐ถ))) = ((((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) +s (๐ด ยทs ๐ถ))) | ||
Theorem | addsdilem4 27609* | Lemma for addsdi 27610. Show one of the equalities involved in the final expression. (Contributed by Scott Fenton, 9-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ถ โ No ) & โข (๐ โ โ๐ฅ๐ โ (( L โ๐ด) โช ( R โ๐ด))(๐ฅ๐ ยทs (๐ต +s ๐ถ)) = ((๐ฅ๐ ยทs ๐ต) +s (๐ฅ๐ ยทs ๐ถ))) & โข (๐ โ โ๐ง๐ โ (( L โ๐ถ) โช ( R โ๐ถ))(๐ด ยทs (๐ต +s ๐ง๐)) = ((๐ด ยทs ๐ต) +s (๐ด ยทs ๐ง๐))) & โข (๐ โ โ๐ฅ๐ โ (( L โ๐ด) โช ( R โ๐ด))โ๐ง๐ โ (( L โ๐ถ) โช ( R โ๐ถ))(๐ฅ๐ ยทs (๐ต +s ๐ง๐)) = ((๐ฅ๐ ยทs ๐ต) +s (๐ฅ๐ ยทs ๐ง๐))) & โข (๐ โ ๐ โ (( L โ๐ด) โช ( R โ๐ด))) & โข (๐ โ ๐ โ (( L โ๐ถ) โช ( R โ๐ถ))) โ โข ((๐ โง ๐) โ (((๐ ยทs (๐ต +s ๐ถ)) +s (๐ด ยทs (๐ต +s ๐))) -s (๐ ยทs (๐ต +s ๐))) = ((๐ด ยทs ๐ต) +s (((๐ ยทs ๐ถ) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)))) | ||
Theorem | addsdi 27610 | Distributive law for surreal numbers. Commuted form of part of theorem 7 of [Conway] p. 19. (Contributed by Scott Fenton, 9-Mar-2025.) |
โข ((๐ด โ No โง ๐ต โ No โง ๐ถ โ No ) โ (๐ด ยทs (๐ต +s ๐ถ)) = ((๐ด ยทs ๐ต) +s (๐ด ยทs ๐ถ))) | ||
Theorem | addsdid 27611 | Distributive law for surreal numbers. Commuted form of part of theorem 7 of [Conway] p. 19. (Contributed by Scott Fenton, 9-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ถ โ No ) โ โข (๐ โ (๐ด ยทs (๐ต +s ๐ถ)) = ((๐ด ยทs ๐ต) +s (๐ด ยทs ๐ถ))) | ||
Theorem | addsdird 27612 | Distributive law for surreal numbers. Part of theorem 7 of [Conway] p. 19. (Contributed by Scott Fenton, 9-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ถ โ No ) โ โข (๐ โ ((๐ด +s ๐ต) ยทs ๐ถ) = ((๐ด ยทs ๐ถ) +s (๐ต ยทs ๐ถ))) | ||
Theorem | subsdid 27613 | Distribution of surreal multiplication over subtraction. (Contributed by Scott Fenton, 9-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ถ โ No ) โ โข (๐ โ (๐ด ยทs (๐ต -s ๐ถ)) = ((๐ด ยทs ๐ต) -s (๐ด ยทs ๐ถ))) | ||
Theorem | subsdird 27614 | Distribution of surreal multiplication over subtraction. (Contributed by Scott Fenton, 9-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ถ โ No ) โ โข (๐ โ ((๐ด -s ๐ต) ยทs ๐ถ) = ((๐ด ยทs ๐ถ) -s (๐ต ยทs ๐ถ))) | ||
Theorem | mulnegs1d 27615 | Product with negative is negative of product. Part of theorem 7 of [Conway] p. 19. (Contributed by Scott Fenton, 10-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) โ โข (๐ โ (( -us โ๐ด) ยทs ๐ต) = ( -us โ(๐ด ยทs ๐ต))) | ||
Theorem | mulnegs2d 27616 | Product with negative is negative of product. Part of theorem 7 of [Conway] p. 19. (Contributed by Scott Fenton, 10-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) โ โข (๐ โ (๐ด ยทs ( -us โ๐ต)) = ( -us โ(๐ด ยทs ๐ต))) | ||
Theorem | mul2negsd 27617 | Surreal product of two negatives. (Contributed by Scott Fenton, 15-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) โ โข (๐ โ (( -us โ๐ด) ยทs ( -us โ๐ต)) = (๐ด ยทs ๐ต)) | ||
Theorem | mulsasslem1 27618* | Lemma for mulsass 27621. Expand the left hand side of the formula. (Contributed by Scott Fenton, 9-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ถ โ No ) โ โข (๐ โ ((๐ด ยทs ๐ต) ยทs ๐ถ) = ((({๐ โฃ โ๐ฅ๐ฟ โ ( L โ๐ด)โ๐ฆ๐ฟ โ ( L โ๐ต)โ๐ง๐ฟ โ ( L โ๐ถ)๐ = ((((((๐ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐ฆ๐ฟ)) -s (๐ฅ๐ฟ ยทs ๐ฆ๐ฟ)) ยทs ๐ถ) +s ((๐ด ยทs ๐ต) ยทs ๐ง๐ฟ)) -s ((((๐ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐ฆ๐ฟ)) -s (๐ฅ๐ฟ ยทs ๐ฆ๐ฟ)) ยทs ๐ง๐ฟ))} โช {๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ โ ( R โ๐ต)โ๐ง๐ฟ โ ( L โ๐ถ)๐ = ((((((๐ฅ๐ ยทs ๐ต) +s (๐ด ยทs ๐ฆ๐ )) -s (๐ฅ๐ ยทs ๐ฆ๐ )) ยทs ๐ถ) +s ((๐ด ยทs ๐ต) ยทs ๐ง๐ฟ)) -s ((((๐ฅ๐ ยทs ๐ต) +s (๐ด ยทs ๐ฆ๐ )) -s (๐ฅ๐ ยทs ๐ฆ๐ )) ยทs ๐ง๐ฟ))}) โช ({๐ โฃ โ๐ฅ๐ฟ โ ( L โ๐ด)โ๐ฆ๐ โ ( R โ๐ต)โ๐ง๐ โ ( R โ๐ถ)๐ = ((((((๐ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐ฆ๐ )) -s (๐ฅ๐ฟ ยทs ๐ฆ๐ )) ยทs ๐ถ) +s ((๐ด ยทs ๐ต) ยทs ๐ง๐ )) -s ((((๐ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐ฆ๐ )) -s (๐ฅ๐ฟ ยทs ๐ฆ๐ )) ยทs ๐ง๐ ))} โช {๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ฟ โ ( L โ๐ต)โ๐ง๐ โ ( R โ๐ถ)๐ = ((((((๐ฅ๐ ยทs ๐ต) +s (๐ด ยทs ๐ฆ๐ฟ)) -s (๐ฅ๐ ยทs ๐ฆ๐ฟ)) ยทs ๐ถ) +s ((๐ด ยทs ๐ต) ยทs ๐ง๐ )) -s ((((๐ฅ๐ ยทs ๐ต) +s (๐ด ยทs ๐ฆ๐ฟ)) -s (๐ฅ๐ ยทs ๐ฆ๐ฟ)) ยทs ๐ง๐ ))})) |s (({๐ โฃ โ๐ฅ๐ฟ โ ( L โ๐ด)โ๐ฆ๐ฟ โ ( L โ๐ต)โ๐ง๐ โ ( R โ๐ถ)๐ = ((((((๐ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐ฆ๐ฟ)) -s (๐ฅ๐ฟ ยทs ๐ฆ๐ฟ)) ยทs ๐ถ) +s ((๐ด ยทs ๐ต) ยทs ๐ง๐ )) -s ((((๐ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐ฆ๐ฟ)) -s (๐ฅ๐ฟ ยทs ๐ฆ๐ฟ)) ยทs ๐ง๐ ))} โช {๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ โ ( R โ๐ต)โ๐ง๐ โ ( R โ๐ถ)๐ = ((((((๐ฅ๐ ยทs ๐ต) +s (๐ด ยทs ๐ฆ๐ )) -s (๐ฅ๐ ยทs ๐ฆ๐ )) ยทs ๐ถ) +s ((๐ด ยทs ๐ต) ยทs ๐ง๐ )) -s ((((๐ฅ๐ ยทs ๐ต) +s (๐ด ยทs ๐ฆ๐ )) -s (๐ฅ๐ ยทs ๐ฆ๐ )) ยทs ๐ง๐ ))}) โช ({๐ โฃ โ๐ฅ๐ฟ โ ( L โ๐ด)โ๐ฆ๐ โ ( R โ๐ต)โ๐ง๐ฟ โ ( L โ๐ถ)๐ = ((((((๐ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐ฆ๐ )) -s (๐ฅ๐ฟ ยทs ๐ฆ๐ )) ยทs ๐ถ) +s ((๐ด ยทs ๐ต) ยทs ๐ง๐ฟ)) -s ((((๐ฅ๐ฟ ยทs ๐ต) +s (๐ด ยทs ๐ฆ๐ )) -s (๐ฅ๐ฟ ยทs ๐ฆ๐ )) ยทs ๐ง๐ฟ))} โช {๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ฟ โ ( L โ๐ต)โ๐ง๐ฟ โ ( L โ๐ถ)๐ = ((((((๐ฅ๐ ยทs ๐ต) +s (๐ด ยทs ๐ฆ๐ฟ)) -s (๐ฅ๐ ยทs ๐ฆ๐ฟ)) ยทs ๐ถ) +s ((๐ด ยทs ๐ต) ยทs ๐ง๐ฟ)) -s ((((๐ฅ๐ ยทs ๐ต) +s (๐ด ยทs ๐ฆ๐ฟ)) -s (๐ฅ๐ ยทs ๐ฆ๐ฟ)) ยทs ๐ง๐ฟ))})))) | ||
Theorem | mulsasslem2 27619* | Lemma for mulsass 27621. Expand the right hand side of the formula. (Contributed by Scott Fenton, 9-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ถ โ No ) โ โข (๐ โ (๐ด ยทs (๐ต ยทs ๐ถ)) = ((({๐ โฃ โ๐ฅ๐ฟ โ ( L โ๐ด)โ๐ฆ๐ฟ โ ( L โ๐ต)โ๐ง๐ฟ โ ( L โ๐ถ)๐ = (((๐ฅ๐ฟ ยทs (๐ต ยทs ๐ถ)) +s (๐ด ยทs (((๐ฆ๐ฟ ยทs ๐ถ) +s (๐ต ยทs ๐ง๐ฟ)) -s (๐ฆ๐ฟ ยทs ๐ง๐ฟ)))) -s (๐ฅ๐ฟ ยทs (((๐ฆ๐ฟ ยทs ๐ถ) +s (๐ต ยทs ๐ง๐ฟ)) -s (๐ฆ๐ฟ ยทs ๐ง๐ฟ))))} โช {๐ โฃ โ๐ฅ๐ฟ โ ( L โ๐ด)โ๐ฆ๐ โ ( R โ๐ต)โ๐ง๐ โ ( R โ๐ถ)๐ = (((๐ฅ๐ฟ ยทs (๐ต ยทs ๐ถ)) +s (๐ด ยทs (((๐ฆ๐ ยทs ๐ถ) +s (๐ต ยทs ๐ง๐ )) -s (๐ฆ๐ ยทs ๐ง๐ )))) -s (๐ฅ๐ฟ ยทs (((๐ฆ๐ ยทs ๐ถ) +s (๐ต ยทs ๐ง๐ )) -s (๐ฆ๐ ยทs ๐ง๐ ))))}) โช ({๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ฟ โ ( L โ๐ต)โ๐ง๐ โ ( R โ๐ถ)๐ = (((๐ฅ๐ ยทs (๐ต ยทs ๐ถ)) +s (๐ด ยทs (((๐ฆ๐ฟ ยทs ๐ถ) +s (๐ต ยทs ๐ง๐ )) -s (๐ฆ๐ฟ ยทs ๐ง๐ )))) -s (๐ฅ๐ ยทs (((๐ฆ๐ฟ ยทs ๐ถ) +s (๐ต ยทs ๐ง๐ )) -s (๐ฆ๐ฟ ยทs ๐ง๐ ))))} โช {๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ โ ( R โ๐ต)โ๐ง๐ฟ โ ( L โ๐ถ)๐ = (((๐ฅ๐ ยทs (๐ต ยทs ๐ถ)) +s (๐ด ยทs (((๐ฆ๐ ยทs ๐ถ) +s (๐ต ยทs ๐ง๐ฟ)) -s (๐ฆ๐ ยทs ๐ง๐ฟ)))) -s (๐ฅ๐ ยทs (((๐ฆ๐ ยทs ๐ถ) +s (๐ต ยทs ๐ง๐ฟ)) -s (๐ฆ๐ ยทs ๐ง๐ฟ))))})) |s (({๐ โฃ โ๐ฅ๐ฟ โ ( L โ๐ด)โ๐ฆ๐ฟ โ ( L โ๐ต)โ๐ง๐ โ ( R โ๐ถ)๐ = (((๐ฅ๐ฟ ยทs (๐ต ยทs ๐ถ)) +s (๐ด ยทs (((๐ฆ๐ฟ ยทs ๐ถ) +s (๐ต ยทs ๐ง๐ )) -s (๐ฆ๐ฟ ยทs ๐ง๐ )))) -s (๐ฅ๐ฟ ยทs (((๐ฆ๐ฟ ยทs ๐ถ) +s (๐ต ยทs ๐ง๐ )) -s (๐ฆ๐ฟ ยทs ๐ง๐ ))))} โช {๐ โฃ โ๐ฅ๐ฟ โ ( L โ๐ด)โ๐ฆ๐ โ ( R โ๐ต)โ๐ง๐ฟ โ ( L โ๐ถ)๐ = (((๐ฅ๐ฟ ยทs (๐ต ยทs ๐ถ)) +s (๐ด ยทs (((๐ฆ๐ ยทs ๐ถ) +s (๐ต ยทs ๐ง๐ฟ)) -s (๐ฆ๐ ยทs ๐ง๐ฟ)))) -s (๐ฅ๐ฟ ยทs (((๐ฆ๐ ยทs ๐ถ) +s (๐ต ยทs ๐ง๐ฟ)) -s (๐ฆ๐ ยทs ๐ง๐ฟ))))}) โช ({๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ฟ โ ( L โ๐ต)โ๐ง๐ฟ โ ( L โ๐ถ)๐ = (((๐ฅ๐ ยทs (๐ต ยทs ๐ถ)) +s (๐ด ยทs (((๐ฆ๐ฟ ยทs ๐ถ) +s (๐ต ยทs ๐ง๐ฟ)) -s (๐ฆ๐ฟ ยทs ๐ง๐ฟ)))) -s (๐ฅ๐ ยทs (((๐ฆ๐ฟ ยทs ๐ถ) +s (๐ต ยทs ๐ง๐ฟ)) -s (๐ฆ๐ฟ ยทs ๐ง๐ฟ))))} โช {๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ โ ( R โ๐ต)โ๐ง๐ โ ( R โ๐ถ)๐ = (((๐ฅ๐ ยทs (๐ต ยทs ๐ถ)) +s (๐ด ยทs (((๐ฆ๐ ยทs ๐ถ) +s (๐ต ยทs ๐ง๐ )) -s (๐ฆ๐ ยทs ๐ง๐ )))) -s (๐ฅ๐ ยทs (((๐ฆ๐ ยทs ๐ถ) +s (๐ต ยทs ๐ง๐ )) -s (๐ฆ๐ ยทs ๐ง๐ ))))})))) | ||
Theorem | mulsasslem3 27620* | Lemma for mulsass 27621. Demonstrate the central equality. (Contributed by Scott Fenton, 10-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ถ โ No ) & โข ๐ โ (( L โ๐ด) โช ( R โ๐ด)) & โข ๐ โ (( L โ๐ต) โช ( R โ๐ต)) & โข ๐ โ (( L โ๐ถ) โช ( R โ๐ถ)) & โข (๐ โ โ๐ฅ๐ โ (( L โ๐ด) โช ( R โ๐ด))โ๐ฆ๐ โ (( L โ๐ต) โช ( R โ๐ต))โ๐ง๐ โ (( L โ๐ถ) โช ( R โ๐ถ))((๐ฅ๐ ยทs ๐ฆ๐) ยทs ๐ง๐) = (๐ฅ๐ ยทs (๐ฆ๐ ยทs ๐ง๐))) & โข (๐ โ โ๐ฅ๐ โ (( L โ๐ด) โช ( R โ๐ด))โ๐ฆ๐ โ (( L โ๐ต) โช ( R โ๐ต))((๐ฅ๐ ยทs ๐ฆ๐) ยทs ๐ถ) = (๐ฅ๐ ยทs (๐ฆ๐ ยทs ๐ถ))) & โข (๐ โ โ๐ฅ๐ โ (( L โ๐ด) โช ( R โ๐ด))โ๐ง๐ โ (( L โ๐ถ) โช ( R โ๐ถ))((๐ฅ๐ ยทs ๐ต) ยทs ๐ง๐) = (๐ฅ๐ ยทs (๐ต ยทs ๐ง๐))) & โข (๐ โ โ๐ฆ๐ โ (( L โ๐ต) โช ( R โ๐ต))โ๐ง๐ โ (( L โ๐ถ) โช ( R โ๐ถ))((๐ด ยทs ๐ฆ๐) ยทs ๐ง๐) = (๐ด ยทs (๐ฆ๐ ยทs ๐ง๐))) & โข (๐ โ โ๐ฅ๐ โ (( L โ๐ด) โช ( R โ๐ด))((๐ฅ๐ ยทs ๐ต) ยทs ๐ถ) = (๐ฅ๐ ยทs (๐ต ยทs ๐ถ))) & โข (๐ โ โ๐ฆ๐ โ (( L โ๐ต) โช ( R โ๐ต))((๐ด ยทs ๐ฆ๐) ยทs ๐ถ) = (๐ด ยทs (๐ฆ๐ ยทs ๐ถ))) & โข (๐ โ โ๐ง๐ โ (( L โ๐ถ) โช ( R โ๐ถ))((๐ด ยทs ๐ต) ยทs ๐ง๐) = (๐ด ยทs (๐ต ยทs ๐ง๐))) โ โข (๐ โ (โ๐ฅ โ ๐ โ๐ฆ โ ๐ โ๐ง โ ๐ ๐ = ((((((๐ฅ ยทs ๐ต) +s (๐ด ยทs ๐ฆ)) -s (๐ฅ ยทs ๐ฆ)) ยทs ๐ถ) +s ((๐ด ยทs ๐ต) ยทs ๐ง)) -s ((((๐ฅ ยทs ๐ต) +s (๐ด ยทs ๐ฆ)) -s (๐ฅ ยทs ๐ฆ)) ยทs ๐ง)) โ โ๐ฅ โ ๐ โ๐ฆ โ ๐ โ๐ง โ ๐ ๐ = (((๐ฅ ยทs (๐ต ยทs ๐ถ)) +s (๐ด ยทs (((๐ฆ ยทs ๐ถ) +s (๐ต ยทs ๐ง)) -s (๐ฆ ยทs ๐ง)))) -s (๐ฅ ยทs (((๐ฆ ยทs ๐ถ) +s (๐ต ยทs ๐ง)) -s (๐ฆ ยทs ๐ง)))))) | ||
Theorem | mulsass 27621 | Associative law for surreal multiplication. Part of theorem 7 of [Conway] p. 19. Much like the case for additive groups, this theorem together with mulscom 27595, addsdi 27610, mulsgt0 27600, and the addition theorems would make the surreals into an ordered ring except that they are a proper class. (Contributed by Scott Fenton, 10-Mar-2025.) |
โข ((๐ด โ No โง ๐ต โ No โง ๐ถ โ No ) โ ((๐ด ยทs ๐ต) ยทs ๐ถ) = (๐ด ยทs (๐ต ยทs ๐ถ))) | ||
Theorem | mulsassd 27622 | Associative law for surreal multiplication. Part of theorem 7 of [Conway] p. 19. (Contributed by Scott Fenton, 10-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ถ โ No ) โ โข (๐ โ ((๐ด ยทs ๐ต) ยทs ๐ถ) = (๐ด ยทs (๐ต ยทs ๐ถ))) | ||
Theorem | sltmul2 27623 | Multiplication of both sides of surreal less-than by a positive number. (Contributed by Scott Fenton, 10-Mar-2025.) |
โข (((๐ด โ No โง 0s <s ๐ด) โง ๐ต โ No โง ๐ถ โ No ) โ (๐ต <s ๐ถ โ (๐ด ยทs ๐ต) <s (๐ด ยทs ๐ถ))) | ||
Theorem | sltmul2d 27624 | Multiplication of both sides of surreal less-than by a positive number. (Contributed by Scott Fenton, 10-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ถ โ No ) & โข (๐ โ 0s <s ๐ถ) โ โข (๐ โ (๐ด <s ๐ต โ (๐ถ ยทs ๐ด) <s (๐ถ ยทs ๐ต))) | ||
Theorem | sltmul1d 27625 | Multiplication of both sides of surreal less-than by a positive number. (Contributed by Scott Fenton, 10-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ถ โ No ) & โข (๐ โ 0s <s ๐ถ) โ โข (๐ โ (๐ด <s ๐ต โ (๐ด ยทs ๐ถ) <s (๐ต ยทs ๐ถ))) | ||
Theorem | slemul2d 27626 | Multiplication of both sides of surreal less-than or equal by a positive number. (Contributed by Scott Fenton, 10-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ถ โ No ) & โข (๐ โ 0s <s ๐ถ) โ โข (๐ โ (๐ด โคs ๐ต โ (๐ถ ยทs ๐ด) โคs (๐ถ ยทs ๐ต))) | ||
Theorem | slemul1d 27627 | Multiplication of both sides of surreal less-than or equal by a positive number. (Contributed by Scott Fenton, 10-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ถ โ No ) & โข (๐ โ 0s <s ๐ถ) โ โข (๐ โ (๐ด โคs ๐ต โ (๐ด ยทs ๐ถ) โคs (๐ต ยทs ๐ถ))) | ||
Theorem | sltmulneg1d 27628 | Multiplication of both sides of surreal less-than by a negative number. (Contributed by Scott Fenton, 14-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ถ โ No ) & โข (๐ โ ๐ถ <s 0s ) โ โข (๐ โ (๐ด <s ๐ต โ (๐ต ยทs ๐ถ) <s (๐ด ยทs ๐ถ))) | ||
Theorem | sltmulneg2d 27629 | Multiplication of both sides of surreal less-than by a negative number. (Contributed by Scott Fenton, 14-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ถ โ No ) & โข (๐ โ ๐ถ <s 0s ) โ โข (๐ โ (๐ด <s ๐ต โ (๐ถ ยทs ๐ต) <s (๐ถ ยทs ๐ด))) | ||
Theorem | mulscan2dlem 27630 | Lemma for mulscan2d 27631. Cancellation of multiplication when the right term is positive. (Contributed by Scott Fenton, 10-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ถ โ No ) & โข (๐ โ 0s <s ๐ถ) โ โข (๐ โ ((๐ด ยทs ๐ถ) = (๐ต ยทs ๐ถ) โ ๐ด = ๐ต)) | ||
Theorem | mulscan2d 27631 | Cancellation of surreal multiplication when the right term is non-zero. (Contributed by Scott Fenton, 10-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ถ โ No ) & โข (๐ โ ๐ถ โ 0s ) โ โข (๐ โ ((๐ด ยทs ๐ถ) = (๐ต ยทs ๐ถ) โ ๐ด = ๐ต)) | ||
Theorem | mulscan1d 27632 | Cancellation of surreal multiplication when the left term is non-zero. (Contributed by Scott Fenton, 10-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ถ โ No ) & โข (๐ โ ๐ถ โ 0s ) โ โข (๐ โ ((๐ถ ยทs ๐ด) = (๐ถ ยทs ๐ต) โ ๐ด = ๐ต)) | ||
Theorem | muls12d 27633 | Commutative/associative law for surreal multiplication. (Contributed by Scott Fenton, 14-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ถ โ No ) โ โข (๐ โ (๐ด ยทs (๐ต ยทs ๐ถ)) = (๐ต ยทs (๐ด ยทs ๐ถ))) | ||
Theorem | divsmo 27634* | Uniqueness of surreal inversion. Given a non-zero surreal ๐ด, there is at most one surreal giving a particular product. (Contributed by Scott Fenton, 10-Mar-2025.) |
โข ((๐ด โ No โง ๐ด โ 0s ) โ โ*๐ฅ โ No (๐ด ยทs ๐ฅ) = ๐ต) | ||
Syntax | cdivs 27635 | Declare the syntax for surreal division. |
class /su | ||
Definition | df-divs 27636* | Define surreal division. This is not the definition used in the literature, but we use it here because it is technically easier to work with. (Contributed by Scott Fenton, 12-Mar-2025.) |
โข /su = (๐ฅ โ No , ๐ฆ โ ( No โ { 0s }) โฆ (โฉ๐ง โ No (๐ฆ ยทs ๐ง) = ๐ฅ)) | ||
Theorem | divsval 27637* | The value of surreal division. (Contributed by Scott Fenton, 12-Mar-2025.) |
โข ((๐ด โ No โง ๐ต โ No โง ๐ต โ 0s ) โ (๐ด /su ๐ต) = (โฉ๐ฅ โ No (๐ต ยทs ๐ฅ) = ๐ด)) | ||
Theorem | norecdiv 27638* | If a surreal has a reciprocal, then it has any division. (Contributed by Scott Fenton, 12-Mar-2025.) |
โข (((๐ด โ No โง ๐ด โ 0s โง ๐ต โ No ) โง โ๐ฅ โ No (๐ด ยทs ๐ฅ) = 1s ) โ โ๐ฆ โ No (๐ด ยทs ๐ฆ) = ๐ต) | ||
Theorem | noreceuw 27639* | If a surreal has a reciprocal, then it has unique division. (Contributed by Scott Fenton, 12-Mar-2025.) |
โข (((๐ด โ No โง ๐ด โ 0s โง ๐ต โ No ) โง โ๐ฅ โ No (๐ด ยทs ๐ฅ) = 1s ) โ โ!๐ฆ โ No (๐ด ยทs ๐ฆ) = ๐ต) | ||
Theorem | divsmulw 27640* | Relationship between surreal division and multiplication. Weak version that does not assume reciprocals. Later, when we prove precsex 27664, we can eliminate the existence hypothesis (see divsmul 27667). (Contributed by Scott Fenton, 12-Mar-2025.) |
โข (((๐ด โ No โง ๐ต โ No โง (๐ถ โ No โง ๐ถ โ 0s )) โง โ๐ฅ โ No (๐ถ ยทs ๐ฅ) = 1s ) โ ((๐ด /su ๐ถ) = ๐ต โ (๐ถ ยทs ๐ต) = ๐ด)) | ||
Theorem | divsmulwd 27641* | Relationship between surreal division and multiplication. Weak version that does not assume reciprocals. (Contributed by Scott Fenton, 12-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ถ โ No ) & โข (๐ โ ๐ถ โ 0s ) & โข (๐ โ โ๐ฅ โ No (๐ถ ยทs ๐ฅ) = 1s ) โ โข (๐ โ ((๐ด /su ๐ถ) = ๐ต โ (๐ถ ยทs ๐ต) = ๐ด)) | ||
Theorem | divsclw 27642* | Weak division closure law. (Contributed by Scott Fenton, 12-Mar-2025.) |
โข (((๐ด โ No โง ๐ต โ No โง ๐ต โ 0s ) โง โ๐ฅ โ No (๐ต ยทs ๐ฅ) = 1s ) โ (๐ด /su ๐ต) โ No ) | ||
Theorem | divsclwd 27643* | Weak division closure law. (Contributed by Scott Fenton, 12-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ต โ 0s ) & โข (๐ โ โ๐ฅ โ No (๐ต ยทs ๐ฅ) = 1s ) โ โข (๐ โ (๐ด /su ๐ต) โ No ) | ||
Theorem | divscan2wd 27644* | A weak cancellation law for surreal division. (Contributed by Scott Fenton, 13-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ต โ 0s ) & โข (๐ โ โ๐ฅ โ No (๐ต ยทs ๐ฅ) = 1s ) โ โข (๐ โ (๐ต ยทs (๐ด /su ๐ต)) = ๐ด) | ||
Theorem | divscan1wd 27645* | A weak cancellation law for surreal division. (Contributed by Scott Fenton, 13-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ต โ 0s ) & โข (๐ โ โ๐ฅ โ No (๐ต ยทs ๐ฅ) = 1s ) โ โข (๐ โ ((๐ด /su ๐ต) ยทs ๐ต) = ๐ด) | ||
Theorem | sltdivmulwd 27646* | Surreal less-than relationship between division and multiplication. Weak version. (Contributed by Scott Fenton, 14-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ถ โ No ) & โข (๐ โ 0s <s ๐ถ) & โข (๐ โ โ๐ฅ โ No (๐ถ ยทs ๐ฅ) = 1s ) โ โข (๐ โ ((๐ด /su ๐ถ) <s ๐ต โ ๐ด <s (๐ถ ยทs ๐ต))) | ||
Theorem | sltdivmul2wd 27647* | Surreal less-than relationship between division and multiplication. Weak version. (Contributed by Scott Fenton, 14-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ถ โ No ) & โข (๐ โ 0s <s ๐ถ) & โข (๐ โ โ๐ฅ โ No (๐ถ ยทs ๐ฅ) = 1s ) โ โข (๐ โ ((๐ด /su ๐ถ) <s ๐ต โ ๐ด <s (๐ต ยทs ๐ถ))) | ||
Theorem | sltmuldivwd 27648* | Surreal less-than relationship between division and multiplication. Weak version. (Contributed by Scott Fenton, 14-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ถ โ No ) & โข (๐ โ 0s <s ๐ถ) & โข (๐ โ โ๐ฅ โ No (๐ถ ยทs ๐ฅ) = 1s ) โ โข (๐ โ ((๐ด ยทs ๐ถ) <s ๐ต โ ๐ด <s (๐ต /su ๐ถ))) | ||
Theorem | sltmuldiv2wd 27649* | Surreal less-than relationship between division and multiplication. Weak version. (Contributed by Scott Fenton, 14-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ถ โ No ) & โข (๐ โ 0s <s ๐ถ) & โข (๐ โ โ๐ฅ โ No (๐ถ ยทs ๐ฅ) = 1s ) โ โข (๐ โ ((๐ถ ยทs ๐ด) <s ๐ต โ ๐ด <s (๐ต /su ๐ถ))) | ||
Theorem | divsasswd 27650* | An associative law for surreal division. Weak version. (Contributed by Scott Fenton, 14-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ถ โ No ) & โข (๐ โ ๐ถ โ 0s ) & โข (๐ โ โ๐ฅ โ No (๐ถ ยทs ๐ฅ) = 1s ) โ โข (๐ โ ((๐ด ยทs ๐ต) /su ๐ถ) = (๐ด ยทs (๐ต /su ๐ถ))) | ||
Theorem | divs1 27651 | A surreal divided by one is itself. (Contributed by Scott Fenton, 13-Mar-2025.) |
โข (๐ด โ No โ (๐ด /su 1s ) = ๐ด) | ||
Theorem | precsexlemcbv 27652* | Lemma for surreal reciprocals. Change some bound variables. (Contributed by Scott Fenton, 15-Mar-2025.) |
โข ๐น = rec((๐ โ V โฆ โฆ(1st โ๐) / ๐โฆโฆ(2nd โ๐) / ๐โฆโจ(๐ โช ({๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ฟ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ -s ๐ด) ยทs ๐ฆ๐ฟ)) /su ๐ฅ๐ )} โช {๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}โ๐ฆ๐ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐ )) /su ๐ฅ๐ฟ)})), (๐ โช ({๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}โ๐ฆ๐ฟ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐ฟ)) /su ๐ฅ๐ฟ)} โช {๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ -s ๐ด) ยทs ๐ฆ๐ )) /su ๐ฅ๐ )}))โฉ), โจ{ 0s }, โ โฉ) โ โข ๐น = rec((๐ โ V โฆ โฆ(1st โ๐) / ๐โฆโฆ(2nd โ๐) / ๐ โฆโจ(๐ โช ({๐ โฃ โ๐ง๐ โ ( R โ๐ด)โ๐ค โ ๐ ๐ = (( 1s +s ((๐ง๐ -s ๐ด) ยทs ๐ค)) /su ๐ง๐ )} โช {๐ โฃ โ๐ง๐ฟ โ {๐ง โ ( L โ๐ด) โฃ 0s <s ๐ง}โ๐ก โ ๐ ๐ = (( 1s +s ((๐ง๐ฟ -s ๐ด) ยทs ๐ก)) /su ๐ง๐ฟ)})), (๐ โช ({๐ โฃ โ๐ง๐ฟ โ {๐ง โ ( L โ๐ด) โฃ 0s <s ๐ง}โ๐ค โ ๐ ๐ = (( 1s +s ((๐ง๐ฟ -s ๐ด) ยทs ๐ค)) /su ๐ง๐ฟ)} โช {๐ โฃ โ๐ง๐ โ ( R โ๐ด)โ๐ก โ ๐ ๐ = (( 1s +s ((๐ง๐ -s ๐ด) ยทs ๐ก)) /su ๐ง๐ )}))โฉ), โจ{ 0s }, โ โฉ) | ||
Theorem | precsexlem1 27653 | Lemma for surreal reciprocals. Calculate the value of the recursive left function at zero. (Contributed by Scott Fenton, 13-Mar-2025.) |
โข ๐น = rec((๐ โ V โฆ โฆ(1st โ๐) / ๐โฆโฆ(2nd โ๐) / ๐โฆโจ(๐ โช ({๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ฟ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ -s ๐ด) ยทs ๐ฆ๐ฟ)) /su ๐ฅ๐ )} โช {๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}โ๐ฆ๐ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐ )) /su ๐ฅ๐ฟ)})), (๐ โช ({๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}โ๐ฆ๐ฟ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐ฟ)) /su ๐ฅ๐ฟ)} โช {๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ -s ๐ด) ยทs ๐ฆ๐ )) /su ๐ฅ๐ )}))โฉ), โจ{ 0s }, โ โฉ) & โข ๐ฟ = (1st โ ๐น) & โข ๐ = (2nd โ ๐น) โ โข (๐ฟโโ ) = { 0s } | ||
Theorem | precsexlem2 27654 | Lemma for surreal reciprocals. Calculate the value of the recursive right function at zero. (Contributed by Scott Fenton, 13-Mar-2025.) |
โข ๐น = rec((๐ โ V โฆ โฆ(1st โ๐) / ๐โฆโฆ(2nd โ๐) / ๐โฆโจ(๐ โช ({๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ฟ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ -s ๐ด) ยทs ๐ฆ๐ฟ)) /su ๐ฅ๐ )} โช {๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}โ๐ฆ๐ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐ )) /su ๐ฅ๐ฟ)})), (๐ โช ({๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}โ๐ฆ๐ฟ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐ฟ)) /su ๐ฅ๐ฟ)} โช {๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ -s ๐ด) ยทs ๐ฆ๐ )) /su ๐ฅ๐ )}))โฉ), โจ{ 0s }, โ โฉ) & โข ๐ฟ = (1st โ ๐น) & โข ๐ = (2nd โ ๐น) โ โข (๐ โโ ) = โ | ||
Theorem | precsexlem3 27655* | Lemma for surreal reciprocals. Calculate the value of the recursive function at a successor. (Contributed by Scott Fenton, 12-Mar-2025.) |
โข ๐น = rec((๐ โ V โฆ โฆ(1st โ๐) / ๐โฆโฆ(2nd โ๐) / ๐โฆโจ(๐ โช ({๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ฟ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ -s ๐ด) ยทs ๐ฆ๐ฟ)) /su ๐ฅ๐ )} โช {๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}โ๐ฆ๐ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐ )) /su ๐ฅ๐ฟ)})), (๐ โช ({๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}โ๐ฆ๐ฟ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐ฟ)) /su ๐ฅ๐ฟ)} โช {๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ -s ๐ด) ยทs ๐ฆ๐ )) /su ๐ฅ๐ )}))โฉ), โจ{ 0s }, โ โฉ) & โข ๐ฟ = (1st โ ๐น) & โข ๐ = (2nd โ ๐น) โ โข (๐ผ โ ฯ โ (๐นโsuc ๐ผ) = โจ((๐ฟโ๐ผ) โช ({๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ฟ โ (๐ฟโ๐ผ)๐ = (( 1s +s ((๐ฅ๐ -s ๐ด) ยทs ๐ฆ๐ฟ)) /su ๐ฅ๐ )} โช {๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}โ๐ฆ๐ โ (๐ โ๐ผ)๐ = (( 1s +s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐ )) /su ๐ฅ๐ฟ)})), ((๐ โ๐ผ) โช ({๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}โ๐ฆ๐ฟ โ (๐ฟโ๐ผ)๐ = (( 1s +s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐ฟ)) /su ๐ฅ๐ฟ)} โช {๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ โ (๐ โ๐ผ)๐ = (( 1s +s ((๐ฅ๐ -s ๐ด) ยทs ๐ฆ๐ )) /su ๐ฅ๐ )}))โฉ) | ||
Theorem | precsexlem4 27656* | Lemma for surreal reciprocals. Calculate the value of the recursive left function at a successor. (Contributed by Scott Fenton, 13-Mar-2025.) |
โข ๐น = rec((๐ โ V โฆ โฆ(1st โ๐) / ๐โฆโฆ(2nd โ๐) / ๐โฆโจ(๐ โช ({๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ฟ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ -s ๐ด) ยทs ๐ฆ๐ฟ)) /su ๐ฅ๐ )} โช {๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}โ๐ฆ๐ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐ )) /su ๐ฅ๐ฟ)})), (๐ โช ({๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}โ๐ฆ๐ฟ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐ฟ)) /su ๐ฅ๐ฟ)} โช {๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ -s ๐ด) ยทs ๐ฆ๐ )) /su ๐ฅ๐ )}))โฉ), โจ{ 0s }, โ โฉ) & โข ๐ฟ = (1st โ ๐น) & โข ๐ = (2nd โ ๐น) โ โข (๐ผ โ ฯ โ (๐ฟโsuc ๐ผ) = ((๐ฟโ๐ผ) โช ({๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ฟ โ (๐ฟโ๐ผ)๐ = (( 1s +s ((๐ฅ๐ -s ๐ด) ยทs ๐ฆ๐ฟ)) /su ๐ฅ๐ )} โช {๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}โ๐ฆ๐ โ (๐ โ๐ผ)๐ = (( 1s +s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐ )) /su ๐ฅ๐ฟ)}))) | ||
Theorem | precsexlem5 27657* | Lemma for surreal reciprocals. Calculate the value of the recursive right function at a successor. (Contributed by Scott Fenton, 13-Mar-2025.) |
โข ๐น = rec((๐ โ V โฆ โฆ(1st โ๐) / ๐โฆโฆ(2nd โ๐) / ๐โฆโจ(๐ โช ({๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ฟ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ -s ๐ด) ยทs ๐ฆ๐ฟ)) /su ๐ฅ๐ )} โช {๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}โ๐ฆ๐ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐ )) /su ๐ฅ๐ฟ)})), (๐ โช ({๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}โ๐ฆ๐ฟ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐ฟ)) /su ๐ฅ๐ฟ)} โช {๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ -s ๐ด) ยทs ๐ฆ๐ )) /su ๐ฅ๐ )}))โฉ), โจ{ 0s }, โ โฉ) & โข ๐ฟ = (1st โ ๐น) & โข ๐ = (2nd โ ๐น) โ โข (๐ผ โ ฯ โ (๐ โsuc ๐ผ) = ((๐ โ๐ผ) โช ({๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}โ๐ฆ๐ฟ โ (๐ฟโ๐ผ)๐ = (( 1s +s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐ฟ)) /su ๐ฅ๐ฟ)} โช {๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ โ (๐ โ๐ผ)๐ = (( 1s +s ((๐ฅ๐ -s ๐ด) ยทs ๐ฆ๐ )) /su ๐ฅ๐ )}))) | ||
Theorem | precsexlem6 27658* | Lemma for surreal reciprocal. Show that ๐ฟ is non-strictly increasing in its argument. (Contributed by Scott Fenton, 15-Mar-2025.) |
โข ๐น = rec((๐ โ V โฆ โฆ(1st โ๐) / ๐โฆโฆ(2nd โ๐) / ๐โฆโจ(๐ โช ({๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ฟ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ -s ๐ด) ยทs ๐ฆ๐ฟ)) /su ๐ฅ๐ )} โช {๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}โ๐ฆ๐ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐ )) /su ๐ฅ๐ฟ)})), (๐ โช ({๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}โ๐ฆ๐ฟ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐ฟ)) /su ๐ฅ๐ฟ)} โช {๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ -s ๐ด) ยทs ๐ฆ๐ )) /su ๐ฅ๐ )}))โฉ), โจ{ 0s }, โ โฉ) & โข ๐ฟ = (1st โ ๐น) & โข ๐ = (2nd โ ๐น) โ โข ((๐ผ โ ฯ โง ๐ฝ โ ฯ โง ๐ผ โ ๐ฝ) โ (๐ฟโ๐ผ) โ (๐ฟโ๐ฝ)) | ||
Theorem | precsexlem7 27659* | Lemma for surreal reciprocal. Show that ๐ is non-strictly increasing in its argument. (Contributed by Scott Fenton, 15-Mar-2025.) |
โข ๐น = rec((๐ โ V โฆ โฆ(1st โ๐) / ๐โฆโฆ(2nd โ๐) / ๐โฆโจ(๐ โช ({๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ฟ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ -s ๐ด) ยทs ๐ฆ๐ฟ)) /su ๐ฅ๐ )} โช {๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}โ๐ฆ๐ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐ )) /su ๐ฅ๐ฟ)})), (๐ โช ({๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}โ๐ฆ๐ฟ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐ฟ)) /su ๐ฅ๐ฟ)} โช {๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ -s ๐ด) ยทs ๐ฆ๐ )) /su ๐ฅ๐ )}))โฉ), โจ{ 0s }, โ โฉ) & โข ๐ฟ = (1st โ ๐น) & โข ๐ = (2nd โ ๐น) โ โข ((๐ผ โ ฯ โง ๐ฝ โ ฯ โง ๐ผ โ ๐ฝ) โ (๐ โ๐ผ) โ (๐ โ๐ฝ)) | ||
Theorem | precsexlem8 27660* | Lemma for surreal reciprocal. Show that the left and right functions give sets of surreals. (Contributed by Scott Fenton, 13-Mar-2025.) |
โข ๐น = rec((๐ โ V โฆ โฆ(1st โ๐) / ๐โฆโฆ(2nd โ๐) / ๐โฆโจ(๐ โช ({๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ฟ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ -s ๐ด) ยทs ๐ฆ๐ฟ)) /su ๐ฅ๐ )} โช {๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}โ๐ฆ๐ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐ )) /su ๐ฅ๐ฟ)})), (๐ โช ({๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}โ๐ฆ๐ฟ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐ฟ)) /su ๐ฅ๐ฟ)} โช {๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ -s ๐ด) ยทs ๐ฆ๐ )) /su ๐ฅ๐ )}))โฉ), โจ{ 0s }, โ โฉ) & โข ๐ฟ = (1st โ ๐น) & โข ๐ = (2nd โ ๐น) & โข (๐ โ ๐ด โ No ) & โข (๐ โ 0s <s ๐ด) & โข (๐ โ โ๐ฅ๐ โ (( L โ๐ด) โช ( R โ๐ด))( 0s <s ๐ฅ๐ โ โ๐ฆ โ No (๐ฅ๐ ยทs ๐ฆ) = 1s )) โ โข ((๐ โง ๐ผ โ ฯ) โ ((๐ฟโ๐ผ) โ No โง (๐ โ๐ผ) โ No )) | ||
Theorem | precsexlem9 27661* | Lemma for surreal reciprocal. Show that the product of ๐ด and a left element is less than one and the product of ๐ด and a right element is greater than one. (Contributed by Scott Fenton, 14-Mar-2025.) |
โข ๐น = rec((๐ โ V โฆ โฆ(1st โ๐) / ๐โฆโฆ(2nd โ๐) / ๐โฆโจ(๐ โช ({๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ฟ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ -s ๐ด) ยทs ๐ฆ๐ฟ)) /su ๐ฅ๐ )} โช {๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}โ๐ฆ๐ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐ )) /su ๐ฅ๐ฟ)})), (๐ โช ({๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}โ๐ฆ๐ฟ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐ฟ)) /su ๐ฅ๐ฟ)} โช {๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ -s ๐ด) ยทs ๐ฆ๐ )) /su ๐ฅ๐ )}))โฉ), โจ{ 0s }, โ โฉ) & โข ๐ฟ = (1st โ ๐น) & โข ๐ = (2nd โ ๐น) & โข (๐ โ ๐ด โ No ) & โข (๐ โ 0s <s ๐ด) & โข (๐ โ โ๐ฅ๐ โ (( L โ๐ด) โช ( R โ๐ด))( 0s <s ๐ฅ๐ โ โ๐ฆ โ No (๐ฅ๐ ยทs ๐ฆ) = 1s )) โ โข ((๐ โง ๐ผ โ ฯ) โ (โ๐ โ (๐ฟโ๐ผ)(๐ด ยทs ๐) <s 1s โง โ๐ โ (๐ โ๐ผ) 1s <s (๐ด ยทs ๐))) | ||
Theorem | precsexlem10 27662* | Lemma for surreal reciprocal. Show that the union of the left sets is less than the union of the right sets. Note that this is the first theorem in the surreal numbers to require the axiom of infinity. (Contributed by Scott Fenton, 15-Mar-2025.) |
โข ๐น = rec((๐ โ V โฆ โฆ(1st โ๐) / ๐โฆโฆ(2nd โ๐) / ๐โฆโจ(๐ โช ({๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ฟ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ -s ๐ด) ยทs ๐ฆ๐ฟ)) /su ๐ฅ๐ )} โช {๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}โ๐ฆ๐ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐ )) /su ๐ฅ๐ฟ)})), (๐ โช ({๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}โ๐ฆ๐ฟ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐ฟ)) /su ๐ฅ๐ฟ)} โช {๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ -s ๐ด) ยทs ๐ฆ๐ )) /su ๐ฅ๐ )}))โฉ), โจ{ 0s }, โ โฉ) & โข ๐ฟ = (1st โ ๐น) & โข ๐ = (2nd โ ๐น) & โข (๐ โ ๐ด โ No ) & โข (๐ โ 0s <s ๐ด) & โข (๐ โ โ๐ฅ๐ โ (( L โ๐ด) โช ( R โ๐ด))( 0s <s ๐ฅ๐ โ โ๐ฆ โ No (๐ฅ๐ ยทs ๐ฆ) = 1s )) โ โข (๐ โ โช (๐ฟ โ ฯ) <<s โช (๐ โ ฯ)) | ||
Theorem | precsexlem11 27663* | Lemma for surreal reciprocal. Show that the cut of the left and right sets is a multiplicative inverse for ๐ด. (Contributed by Scott Fenton, 15-Mar-2025.) |
โข ๐น = rec((๐ โ V โฆ โฆ(1st โ๐) / ๐โฆโฆ(2nd โ๐) / ๐โฆโจ(๐ โช ({๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ฟ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ -s ๐ด) ยทs ๐ฆ๐ฟ)) /su ๐ฅ๐ )} โช {๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}โ๐ฆ๐ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐ )) /su ๐ฅ๐ฟ)})), (๐ โช ({๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}โ๐ฆ๐ฟ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐ฟ)) /su ๐ฅ๐ฟ)} โช {๐ โฃ โ๐ฅ๐ โ ( R โ๐ด)โ๐ฆ๐ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ -s ๐ด) ยทs ๐ฆ๐ )) /su ๐ฅ๐ )}))โฉ), โจ{ 0s }, โ โฉ) & โข ๐ฟ = (1st โ ๐น) & โข ๐ = (2nd โ ๐น) & โข (๐ โ ๐ด โ No ) & โข (๐ โ 0s <s ๐ด) & โข (๐ โ โ๐ฅ๐ โ (( L โ๐ด) โช ( R โ๐ด))( 0s <s ๐ฅ๐ โ โ๐ฆ โ No (๐ฅ๐ ยทs ๐ฆ) = 1s )) & โข ๐ = (โช (๐ฟ โ ฯ) |s โช (๐ โ ฯ)) โ โข (๐ โ (๐ด ยทs ๐) = 1s ) | ||
Theorem | precsex 27664* | Every positive surreal has a reciprocal. Theorem 10(iv) of [Conway] p. 21. (Contributed by Scott Fenton, 15-Mar-2025.) |
โข ((๐ด โ No โง 0s <s ๐ด) โ โ๐ฆ โ No (๐ด ยทs ๐ฆ) = 1s ) | ||
Theorem | recsex 27665* | A non-zero surreal has a reciprocal. (Contributed by Scott Fenton, 15-Mar-2025.) |
โข ((๐ด โ No โง ๐ด โ 0s ) โ โ๐ฅ โ No (๐ด ยทs ๐ฅ) = 1s ) | ||
Theorem | recsexd 27666* | A non-zero surreal has a reciprocal. (Contributed by Scott Fenton, 16-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ด โ 0s ) โ โข (๐ โ โ๐ฅ โ No (๐ด ยทs ๐ฅ) = 1s ) | ||
Theorem | divsmul 27667 | Relationship between surreal division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.) |
โข ((๐ด โ No โง ๐ต โ No โง (๐ถ โ No โง ๐ถ โ 0s )) โ ((๐ด /su ๐ถ) = ๐ต โ (๐ถ ยทs ๐ต) = ๐ด)) | ||
Theorem | divsmuld 27668 | Relationship between surreal division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ถ โ No ) & โข (๐ โ ๐ถ โ 0s ) โ โข (๐ โ ((๐ด /su ๐ถ) = ๐ต โ (๐ถ ยทs ๐ต) = ๐ด)) | ||
Theorem | divscl 27669 | Surreal division closure law. (Contributed by Scott Fenton, 16-Mar-2025.) |
โข ((๐ด โ No โง ๐ต โ No โง ๐ต โ 0s ) โ (๐ด /su ๐ต) โ No ) | ||
Theorem | divscld 27670 | Surreal division closure law. (Contributed by Scott Fenton, 16-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ต โ 0s ) โ โข (๐ โ (๐ด /su ๐ต) โ No ) | ||
Theorem | divscan2d 27671 | A cancellation law for surreal division. (Contributed by Scott Fenton, 16-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ต โ 0s ) โ โข (๐ โ (๐ต ยทs (๐ด /su ๐ต)) = ๐ด) | ||
Theorem | divscan1d 27672 | A cancellation law for surreal division. (Contributed by Scott Fenton, 16-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ต โ 0s ) โ โข (๐ โ ((๐ด /su ๐ต) ยทs ๐ต) = ๐ด) | ||
Theorem | sltdivmuld 27673 | Surreal less-than relationship between division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ถ โ No ) & โข (๐ โ 0s <s ๐ถ) โ โข (๐ โ ((๐ด /su ๐ถ) <s ๐ต โ ๐ด <s (๐ถ ยทs ๐ต))) | ||
Theorem | sltdivmul2d 27674 | Surreal less-than relationship between division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ถ โ No ) & โข (๐ โ 0s <s ๐ถ) โ โข (๐ โ ((๐ด /su ๐ถ) <s ๐ต โ ๐ด <s (๐ต ยทs ๐ถ))) | ||
Theorem | sltmuldivd 27675 | Surreal less-than relationship between division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ถ โ No ) & โข (๐ โ 0s <s ๐ถ) โ โข (๐ โ ((๐ด ยทs ๐ถ) <s ๐ต โ ๐ด <s (๐ต /su ๐ถ))) | ||
Theorem | sltmuldiv2d 27676 | Surreal less-than relationship between division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ถ โ No ) & โข (๐ โ 0s <s ๐ถ) โ โข (๐ โ ((๐ถ ยทs ๐ด) <s ๐ต โ ๐ด <s (๐ต /su ๐ถ))) | ||
Theorem | divsassd 27677 | An associative law for surreal division. (Contributed by Scott Fenton, 16-Mar-2025.) |
โข (๐ โ ๐ด โ No ) & โข (๐ โ ๐ต โ No ) & โข (๐ โ ๐ถ โ No ) & โข (๐ โ ๐ถ โ 0s ) โ โข (๐ โ ((๐ด ยทs ๐ต) /su ๐ถ) = (๐ด ยทs (๐ต /su ๐ถ))) | ||
This part develops elementary geometry based on Tarski's axioms, following [Schwabhauser]. Tarski's geometry is a first-order theory with one sort, the "points". It has two primitive notions, the ternary predicate of "betweenness" and the quaternary predicate of "congruence". To adapt this theory to the framework of set.mm, and to be able to talk of *a* Tarski structure as a space satisfying the given axioms, we use the following definition, stated informally: A Tarski structure ๐ is a set (of points) (Baseโ๐) together with functions (Itvโ๐) and (distโ๐) on ((Baseโ๐) ร (Baseโ๐)) satisfying certain axioms (given in Definitions df-trkg 27704 et sequentes). This allows to treat a Tarski structure as a special kind of extensible structure (see df-struct 17080). The translation to and from Tarski's treatment is as follows (given, again, informally). Suppose that one is given an extensible structure ๐. One defines a betweenness ternary predicate Btw by positing that, for any ๐ฅ, ๐ฆ, ๐ง โ (Baseโ๐), one has "Btw ๐ฅ๐ฆ๐ง " if and only if ๐ฆ โ ๐ฅ(Itvโ๐)๐ง, and a congruence quaternary predicate Congr by positing that, for any ๐ฅ, ๐ฆ, ๐ง, ๐ก โ (Baseโ๐), one has "Congr ๐ฅ๐ฆ๐ง๐ก " if and only if ๐ฅ(distโ๐)๐ฆ = ๐ง(distโ๐)๐ก. It is easy to check that if ๐ satisfies our Tarski axioms, then Btw and Congr satisfy Tarski's Tarski axioms when (Baseโ๐) is interpreted as the universe of discourse. Conversely, suppose that one is given a set ๐, a ternary predicate Btw, and a quaternary predicate Congr. One defines the extensible structure ๐ such that (Baseโ๐) is ๐, and (Itvโ๐) is the function which associates with each โจ๐ฅ, ๐ฆโฉ โ (๐ ร ๐) the set of points ๐ง โ ๐ such that "Btw ๐ฅ๐ง๐ฆ", and (distโ๐) is the function which associates with each โจ๐ฅ, ๐ฆโฉ โ (๐ ร ๐) the set of ordered pairs โจ๐ง, ๐กโฉ โ (๐ ร ๐) such that "Congr ๐ฅ๐ฆ๐ง๐ก". It is easy to check that if Btw and Congr satisfy Tarski's Tarski axioms when ๐ is interpreted as the universe of discourse, then ๐ satisfies our Tarski axioms. We intentionally choose to represent congruence (without loss of generality) as ๐ฅ(distโ๐)๐ฆ = ๐ง(distโ๐)๐ก instead of "Congr ๐ฅ๐ฆ๐ง๐ก", as it is more convenient. It is always possible to define dist for any particular geometry to produce equal results when conguence is desired, and in many cases there is an obvious interpretation of "distance" between two points that can be useful in other situations. Encoding congruence as an equality of distances makes it easier to use these theorems in cases where there is a preferred distance function. We prove that representing a congruence relationship using a distance in the form ๐ฅ(distโ๐)๐ฆ = ๐ง(distโ๐)๐ก causes no loss of generality in tgjustc1 27726 and tgjustc2 27727, which in turn are supported by tgjustf 27724 and tgjustr 27725. A similar representation of congruence (using a "distance" function) is used in Axiom A1 of [Beeson2016] p. 5, which discusses how a large number of formalized proofs were found in Tarskian Geometry using OTTER. Their detailed proofs in Tarski Geometry, along with other information, are available at https://www.michaelbeeson.com/research/FormalTarski/ 27725. Most theorems are in deduction form, as this is a very general, simple, and convenient format to use in Metamath. An assertion in deduction form can be easily converted into an assertion in inference form (removing the antecedents ๐ โ) by insert a โค โ in each hypothesis, using a1i 11, then using mptru 1549 to remove the final โค โ prefix. In some cases we represent, without loss of generality, an implication antecedent in [Schwabhauser] as a hypothesis. The implication can be retrieved from the by using simpr 486, the theorem as stated, and ex 414. For descriptions of individual axioms, we refer to the specific definitions below. A particular feature of Tarski's axioms is modularity, so by using various subsets of the set of axioms, we can define the classes of "absolute dimensionless Tarski structures" (df-trkg 27704), of "Euclidean dimensionless Tarski structures" (df-trkge 27702) and of "Tarski structures of dimension no less than N" (df-trkgld 27703). In this system, angles are not a primitive notion, but instead a derived notion (see df-cgra 28059 and iscgra 28060). To maintain its simplicity, in this system congruence between shapes (a finite sequence of points) is the case where corresponding segments between all corresponding points are congruent. This includes triangles (a shape of 3 distinct points). Note that this definition has no direct regard for angles. For more details and rationale, see df-cgrg 27762. The first section is devoted to the definitions of these various structures. The second section ("Tarskian geometry") develops the synthetic treatment of geometry. The remaining sections prove that real Euclidean spaces and complex Hilbert spaces, with intended interpretations, are Euclidean Tarski structures. Most of the work in this part is due to Thierry Arnoux, with earlier work by Mario Carneiro and Scott Fenton. See also the credits in the comment of each statement. | ||
Syntax | cstrkg 27678 | Extends class notation with the class of Tarski geometries. |
class TarskiG | ||
Syntax | cstrkgc 27679 | Extends class notation with the class of geometries fulfilling the congruence axioms. |
class TarskiGC | ||
Syntax | cstrkgb 27680 | Extends class notation with the class of geometries fulfilling the betweenness axioms. |
class TarskiGB | ||
Syntax | cstrkgcb 27681 | Extends class notation with the class of geometries fulfilling the congruence and betweenness axioms. |
class TarskiGCB | ||
Syntax | cstrkgld 27682 | Extends class notation with the relation for geometries fulfilling the lower dimension axioms. |
class DimTarskiGโฅ | ||
Syntax | cstrkge 27683 | Extends class notation with the class of geometries fulfilling Euclid's axiom. |
class TarskiGE | ||
Syntax | citv 27684 | Declare the syntax for the Interval (segment) index extractor. |
class Itv | ||
Syntax | clng 27685 | Declare the syntax for the Line function. |
class LineG | ||
Definition | df-itv 27686 | Define the Interval (segment) index extractor for Tarski geometries. (Contributed by Thierry Arnoux, 24-Aug-2017.) Use its index-independent form itvid 27690 instead. (New usage is discouraged.) |
โข Itv = Slot ;16 | ||
Definition | df-lng 27687 | Define the line index extractor for geometries. (Contributed by Thierry Arnoux, 27-Mar-2019.) Use its index-independent form lngid 27691 instead. (New usage is discouraged.) |
โข LineG = Slot ;17 | ||
Theorem | itvndx 27688 | Index value of the Interval (segment) slot. Use ndxarg 17129. (Contributed by Thierry Arnoux, 24-Aug-2017.) (New usage is discouraged.) |
โข (Itvโndx) = ;16 | ||
Theorem | lngndx 27689 | Index value of the "line" slot. Use ndxarg 17129. (Contributed by Thierry Arnoux, 27-Mar-2019.) (New usage is discouraged.) |
โข (LineGโndx) = ;17 | ||
Theorem | itvid 27690 | Utility theorem: index-independent form of df-itv 27686. (Contributed by Thierry Arnoux, 24-Aug-2017.) |
โข Itv = Slot (Itvโndx) | ||
Theorem | lngid 27691 | Utility theorem: index-independent form of df-lng 27687. (Contributed by Thierry Arnoux, 27-Mar-2019.) |
โข LineG = Slot (LineGโndx) | ||
Theorem | slotsinbpsd 27692 | The slots Base, +g, ยท๐ and dist are different from the slot Itv. Formerly part of ttglem 28128 and proofs using it. (Contributed by AV, 29-Oct-2024.) |
โข (((Itvโndx) โ (Baseโndx) โง (Itvโndx) โ (+gโndx)) โง ((Itvโndx) โ ( ยท๐ โndx) โง (Itvโndx) โ (distโndx))) | ||
Theorem | slotslnbpsd 27693 | The slots Base, +g, ยท๐ and dist are different from the slot LineG. Formerly part of ttglem 28128 and proofs using it. (Contributed by AV, 29-Oct-2024.) |
โข (((LineGโndx) โ (Baseโndx) โง (LineGโndx) โ (+gโndx)) โง ((LineGโndx) โ ( ยท๐ โndx) โง (LineGโndx) โ (distโndx))) | ||
Theorem | lngndxnitvndx 27694 | The slot for the line is not the slot for the Interval (segment) in an extensible structure. Formerly part of proof for ttgval 28126. (Contributed by AV, 9-Nov-2024.) |
โข (LineGโndx) โ (Itvโndx) | ||
Theorem | trkgstr 27695 | Functionality of a Tarski geometry. (Contributed by Thierry Arnoux, 24-Aug-2017.) |
โข ๐ = {โจ(Baseโndx), ๐โฉ, โจ(distโndx), ๐ทโฉ, โจ(Itvโndx), ๐ผโฉ} โ โข ๐ Struct โจ1, ;16โฉ | ||
Theorem | trkgbas 27696 | The base set of a Tarski geometry. (Contributed by Thierry Arnoux, 24-Aug-2017.) |
โข ๐ = {โจ(Baseโndx), ๐โฉ, โจ(distโndx), ๐ทโฉ, โจ(Itvโndx), ๐ผโฉ} โ โข (๐ โ ๐ โ ๐ = (Baseโ๐)) | ||
Theorem | trkgdist 27697 | The measure of a distance in a Tarski geometry. (Contributed by Thierry Arnoux, 24-Aug-2017.) |
โข ๐ = {โจ(Baseโndx), ๐โฉ, โจ(distโndx), ๐ทโฉ, โจ(Itvโndx), ๐ผโฉ} โ โข (๐ท โ ๐ โ ๐ท = (distโ๐)) | ||
Theorem | trkgitv 27698 | The congruence relation in a Tarski geometry. (Contributed by Thierry Arnoux, 24-Aug-2017.) |
โข ๐ = {โจ(Baseโndx), ๐โฉ, โจ(distโndx), ๐ทโฉ, โจ(Itvโndx), ๐ผโฉ} โ โข (๐ผ โ ๐ โ ๐ผ = (Itvโ๐)) | ||
Definition | df-trkgc 27699* | Define the class of geometries fulfilling the congruence axioms of reflexivity, identity and transitivity. These are axioms A1 to A3 of [Schwabhauser] p. 10. With our distance based notation for congruence, transitivity of congruence boils down to transitivity of equality and is already given by eqtr 2756, so it is not listed in this definition. (Contributed by Thierry Arnoux, 24-Aug-2017.) |
โข TarskiGC = {๐ โฃ [(Baseโ๐) / ๐][(distโ๐) / ๐](โ๐ฅ โ ๐ โ๐ฆ โ ๐ (๐ฅ๐๐ฆ) = (๐ฆ๐๐ฅ) โง โ๐ฅ โ ๐ โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐๐ฆ) = (๐ง๐๐ง) โ ๐ฅ = ๐ฆ))} | ||
Definition | df-trkgb 27700* | Define the class of geometries fulfilling the 3 betweenness axioms in Tarski's Axiomatization of Geometry: identity, Axiom A6 of [Schwabhauser] p. 11, axiom of Pasch, Axiom A7 of [Schwabhauser] p. 12, and continuity, Axiom A11 of [Schwabhauser] p. 13. (Contributed by Thierry Arnoux, 24-Aug-2017.) |
โข TarskiGB = {๐ โฃ [(Baseโ๐) / ๐][(Itvโ๐) / ๐](โ๐ฅ โ ๐ โ๐ฆ โ ๐ (๐ฆ โ (๐ฅ๐๐ฅ) โ ๐ฅ = ๐ฆ) โง โ๐ฅ โ ๐ โ๐ฆ โ ๐ โ๐ง โ ๐ โ๐ข โ ๐ โ๐ฃ โ ๐ ((๐ข โ (๐ฅ๐๐ง) โง ๐ฃ โ (๐ฆ๐๐ง)) โ โ๐ โ ๐ (๐ โ (๐ข๐๐ฆ) โง ๐ โ (๐ฃ๐๐ฅ))) โง โ๐ โ ๐ซ ๐โ๐ก โ ๐ซ ๐(โ๐ โ ๐ โ๐ฅ โ ๐ โ๐ฆ โ ๐ก ๐ฅ โ (๐๐๐ฆ) โ โ๐ โ ๐ โ๐ฅ โ ๐ โ๐ฆ โ ๐ก ๐ โ (๐ฅ๐๐ฆ)))} |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |