Metamath Proof Explorer

Table of Contents - 15.6. Subsystems of surreals

1. Ordinal numbers
   1. cons
   2. df-ons
   3. elons
   4. onssno
   5. onno
   6. 0ons
   7. 1ons
   8. elons2
   9. elons2d
   10. onleft
   11. ltonold
   12. ltonsex
   13. oncutleft
   14. oncutlt
   15. bday11on
   16. onnolt
   17. onlts
   18. onles
   19. onltsd
   20. onlesd
   21. oniso
   22. onswe
   23. onsse
   24. onsis
   25. ons2ind
   26. bdayons
   27. onaddscl
   28. onmulscl
   29. addonbday
   30. peano2ons
   31. onsbnd
   32. onsbnd2
2. Surreal recursive sequences
   1. cseqs
   2. df-seqs
   3. seqsex
   4. seqseq123d
   5. nfseqs
   6. seqsval
   7. noseqex
   8. noseq0
   9. noseqp1
   10. noseqind
   11. noseqinds
   12. noseqssno
   13. noseqno
   14. om2noseq0
   15. om2noseqsuc
   16. om2noseqfo
   17. om2noseqlt
   18. om2noseqlt2
   19. om2noseqf1o
   20. om2noseqiso
   21. om2noseqoi
   22. om2noseqrdg
   23. noseqrdglem
   24. noseqrdgfn
   25. noseqrdg0
   26. noseqrdgsuc
   27. seqsfn
   28. seqs1
   29. seqsp1
3. Natural numbers
   1. cn0s
   2. cnns
   3. df-n0s
   4. df-nns
   5. n0sexg
   6. n0sex
   7. nnsex
   8. peano5n0s
   9. n0ssno
   10. nnssn0s
   11. nnssno
   12. n0no
   13. nnno
   14. n0nod
   15. nnnod
   16. nnn0s
   17. nnn0sd
   18. 0n0s
   19. peano2n0s
   20. peano2n0sd
   21. dfn0s2
   22. n0sind
   23. n0cut
   24. n0cut2
   25. n0on
   26. nnne0s
   27. n0sge0
   28. nnsgt0
   29. elnns
   30. elnns2
   31. n0s0suc
   32. nnsge1
   33. n0addscl
   34. n0mulscl
   35. nnaddscl
   36. nnmulscl
   37. 1n0s
   38. 1nns
   39. peano2nns
   40. nnsrecgt0d
   41. n0bday
   42. n0ssoldg
   43. n0ssold
   44. n0fincut
   45. onsfi
   46. eln0s2
   47. onltn0s
   48. n0cutlt
   49. seqn0sfn
   50. eln0s
   51. n0s0m1
   52. n0subs
   53. n0subs2
   54. n0ltsp1le
   55. n0lesltp1
   56. n0lesm1lt
   57. n0lts1e0
   58. bdayn0p1
   59. bdayn0sf1o
   60. n0p1nns
   61. dfnns2
   62. nnsind
   63. nn1m1nns
   64. nnm1n0s
   65. eucliddivs
   66. oldfib
4. Integers
   1. czs
   2. df-zs
   3. zsex
   4. zssno
   5. zno
   6. znod
   7. elzs
   8. nnzsubs
   9. nnzs
   10. nnzsd
   11. 0zs
   12. n0zs
   13. n0zsd
   14. 1zs
   15. znegscl
   16. znegscld
   17. zaddscl
   18. zaddscld
   19. zsubscld
   20. zmulscld
   21. elzn0s
   22. elzs2
   23. eln0zs
   24. elnnzs
   25. elznns
   26. zn0subs
   27. peano5uzs
   28. uzsind
   29. zsbday
   30. zcuts
   31. zcuts0
   32. zsoring
5. Dyadic fractions
   1. c2s
   2. df-2s
   3. cexps
   4. df-exps
   5. cz12s
   6. df-z12s
   7. 1p1e2s
   8. no2times
   9. 2nns
   10. 2no
   11. 2ne0s
   12. n0seo
   13. zseo
   14. twocut
   15. nohalf
   16. expsval
   17. expnnsval
   18. exps0
   19. exps1
   20. expsp1
   21. expscllem
   22. expscl
   23. n0expscl
   24. nnexpscl
   25. zexpscl
   26. expadds
   27. expsne0
   28. expsgt0
   29. pw2recs
   30. pw2divscld
   31. pw2divmulsd
   32. pw2divscan3d
   33. pw2divscan2d
   34. pw2divsassd
   35. pw2divscan4d
   36. pw2gt0divsd
   37. pw2ge0divsd
   38. pw2divsrecd
   39. pw2divsdird
   40. pw2divsnegd
   41. pw2ltdivmulsd
   42. pw2ltmuldivs2d
   43. pw2ltsdiv1d
   44. avglts1d
   45. avglts2d
   46. pw2divs0d
   47. pw2divsidd
   48. pw2ltdivmuls2d
   49. halfcut
   50. addhalfcut
   51. pw2cut
   52. pw2cutp1
   53. pw2cut2
   54. bdaypw2n0bndlem
   55. bdaypw2n0bnd
   56. bdaypw2bnd
   57. bdayfinbndcbv
   58. bdayfinbndlem1
   59. bdayfinbndlem2
   60. bdayfinbnd
   61. z12bdaylem1
   62. z12bdaylem2
   63. elz12s
   64. elz12si
   65. z12sex
   66. zz12s
   67. z12no
   68. z12addscl
   69. z12negscl
   70. z12subscl
   71. z12shalf
   72. z12negsclb
   73. z12zsodd
   74. z12sge0
   75. z12bdaylem
   76. z12bday
   77. bdayfinlem
   78. bdayfin
   79. dfz12s2
6. Real numbers
   1. creno
   2. df-reno
   3. elreno
   4. reno
   5. renod
   6. recut
   7. elreno2
   8. 0reno
   9. 1reno
   10. renegscl
   11. readdscl
   12. remulscllem1
   13. remulscllem2
   14. remulscl