Metamath Proof Explorer

Table of Contents - 15.5. Surreal arithmetic

1. Addition
   1. cadds
   2. df-adds
   3. addsfn
   4. addsval
   5. addsval2
   6. addsrid
   7. addsridd
   8. addscom
   9. addscomd
   10. addslid
   11. addsproplem1
   12. addsproplem2
   13. addsproplem3
   14. addsproplem4
   15. addsproplem5
   16. addsproplem6
   17. addsproplem7
   18. addsprop
   19. addscutlem
   20. addscut
   21. addscut2
   22. addscld
   23. addscl
   24. addsf
   25. addsfo
   26. peano2no
   27. sltadd1im
   28. sltadd2im
   29. sleadd1im
   30. sleadd2im
   31. sleadd1
   32. sleadd2
   33. sltadd2
   34. sltadd1
   35. addscan2
   36. addscan1
   37. sleadd1d
   38. sleadd2d
   39. sltadd2d
   40. sltadd1d
   41. addscan2d
   42. addscan1d
   43. addsuniflem
   44. addsunif
   45. addsasslem1
   46. addsasslem2
   47. addsass
   48. addsassd
   49. adds32d
   50. adds12d
   51. adds4d
   52. adds42d
   53. sltaddpos1d
   54. sltaddpos2d
   55. slt2addd
   56. addsgt0d
   57. sltp1d
   58. addsbdaylem
   59. addsbday
2. Negation and Subtraction
   1. cnegs
   2. csubs
   3. df-negs
   4. df-subs
   5. negsfn
   6. subsfn
   7. negsval
   8. negs0s
   9. negs1s
   10. negsproplem1
   11. negsproplem2
   12. negsproplem3
   13. negsproplem4
   14. negsproplem5
   15. negsproplem6
   16. negsproplem7
   17. negsprop
   18. negscl
   19. negscld
   20. sltnegim
   21. negscut
   22. negscut2
   23. negsid
   24. negsidd
   25. negsex
   26. negnegs
   27. sltneg
   28. sleneg
   29. sltnegd
   30. slenegd
   31. negs11
   32. negsdi
   33. slt0neg2d
   34. negsf
   35. negsfo
   36. negsf1o
   37. negsunif
   38. negsbdaylem
   39. negsbday
   40. subsval
   41. subsvald
   42. subscl
   43. subscld
   44. subsf
   45. subsfo
   46. negsval2
   47. negsval2d
   48. subsid1
   49. subsid
   50. subadds
   51. subaddsd
   52. pncans
   53. pncan3s
   54. pncan2s
   55. npcans
   56. sltsub1
   57. sltsub2
   58. sltsub1d
   59. sltsub2d
   60. negsubsdi2d
   61. addsubsassd
   62. addsubsd
   63. sltsubsubbd
   64. sltsubsub2bd
   65. sltsubsub3bd
   66. slesubsubbd
   67. slesubsub2bd
   68. slesubsub3bd
   69. sltsubaddd
   70. sltsubadd2d
   71. sltaddsubd
   72. sltaddsub2d
   73. slesubaddd
   74. subsubs4d
   75. subsubs2d
   76. nncansd
   77. posdifsd
   78. sltsubposd
   79. subsge0d
   80. addsubs4d
   81. sltm1d
   82. subscan1d
   83. subscan2d
   84. subseq0d
3. Multiplication
   1. cmuls
   2. df-muls
   3. mulsfn
   4. mulsval
   5. mulsval2lem
   6. mulsval2
   7. muls01
   8. mulsrid
   9. mulsridd
   10. mulsproplemcbv
   11. mulsproplem1
   12. mulsproplem2
   13. mulsproplem3
   14. mulsproplem4
   15. mulsproplem5
   16. mulsproplem6
   17. mulsproplem7
   18. mulsproplem8
   19. mulsproplem9
   20. mulsproplem10
   21. mulsproplem11
   22. mulsproplem12
   23. mulsproplem13
   24. mulsproplem14
   25. mulsprop
   26. mulscutlem
   27. mulscut
   28. mulscut2
   29. mulscl
   30. mulscld
   31. sltmul
   32. sltmuld
   33. slemuld
   34. mulscom
   35. mulscomd
   36. muls02
   37. mulslid
   38. mulslidd
   39. mulsgt0
   40. mulsgt0d
   41. mulsge0d
   42. ssltmul1
   43. ssltmul2
   44. mulsuniflem
   45. mulsunif
   46. addsdilem1
   47. addsdilem2
   48. addsdilem3
   49. addsdilem4
   50. addsdi
   51. addsdid
   52. addsdird
   53. subsdid
   54. subsdird
   55. mulnegs1d
   56. mulnegs2d
   57. mul2negsd
   58. mulsasslem1
   59. mulsasslem2
   60. mulsasslem3
   61. mulsass
   62. mulsassd
   63. muls4d
   64. mulsunif2lem
   65. mulsunif2
   66. sltmul2
   67. sltmul2d
   68. sltmul1d
   69. slemul2d
   70. slemul1d
   71. sltmulneg1d
   72. sltmulneg2d
   73. mulscan2dlem
   74. mulscan2d
   75. mulscan1d
   76. muls12d
   77. slemul1ad
   78. sltmul12ad
   79. divsmo
   80. muls0ord
   81. mulsne0bd
4. Division
   1. cdivs
   2. df-divs
   3. divsval
   4. norecdiv
   5. noreceuw
   6. recsne0
   7. divsmulw
   8. divsmulwd
   9. divsclw
   10. divsclwd
   11. divscan2wd
   12. divscan1wd
   13. sltdivmulwd
   14. sltdivmul2wd
   15. sltmuldivwd
   16. sltmuldiv2wd
   17. divsasswd
   18. divs1
   19. precsexlemcbv
   20. precsexlem1
   21. precsexlem2
   22. precsexlem3
   23. precsexlem4
   24. precsexlem5
   25. precsexlem6
   26. precsexlem7
   27. precsexlem8
   28. precsexlem9
   29. precsexlem10
   30. precsexlem11
   31. precsex
   32. recsex
   33. recsexd
   34. divsmul
   35. divsmuld
   36. divscl
   37. divscld
   38. divscan2d
   39. divscan1d
   40. sltdivmuld
   41. sltdivmul2d
   42. sltmuldivd
   43. sltmuldiv2d
   44. divsassd
   45. divmuldivsd
   46. divdivs1d
   47. divsrecd
   48. divsdird
   49. divscan3d
5. Absolute value
   1. cabss
   2. df-abss
   3. abssval
   4. absscl
   5. abssid
   6. abs0s
   7. abssnid
   8. absmuls
   9. abssge0
   10. abssor
   11. abssneg
   12. sleabs
   13. absslt