Metamath Proof Explorer

Table of Contents - 20.27. Mathbox for Steven Nguyen

1. Miscellaneous theorems
   1. bicomdALT
   2. elabgw
   3. elab2gw
   4. elrab2w
   5. ruvALT
   6. sn-wcdeq
   7. acos1half
   8. isdomn5
   9. isdomn4
2. Utility theorems
   1. ioin9i8
   2. jaodd
   3. syl3an12
   4. sbtd
   5. sbor2
   6. 19.9dev
   7. rspcedvdw
   8. 2rspcedvdw
   9. 3rspcedvdw
   10. 3rspcedvd
   11. eqimssd
   12. rabdif
   13. sn-axrep5v
   14. sn-axprlem3
   15. sn-el
   16. sn-dtru
   17. sn-iotalem
   18. sn-iotalemcor
   19. abbi1sn
   20. iotavallem
   21. sn-iotauni
   22. sn-iotanul
   23. sn-iotaval
   24. sn-iotassuni
   25. sn-iotaex
   26. brif1
   27. brif2
   28. brif12
   29. pssexg
   30. pssn0
   31. psspwb
   32. xppss12
   33. elpwbi
   34. opelxpii
   35. imaopab
   36. fnsnbt
   37. fnimasnd
   38. fvmptd4
   39. ofun
   40. dfqs2
   41. dfqs3
   42. qseq12d
   43. qsalrel
   44. elmapdd
   45. isfsuppd
   46. fzosumm1
   47. ccatcan2d
3. Structures
   1. nelsubginvcld
   2. nelsubgcld
   3. nelsubgsubcld
   4. rnasclg
   5. selvval2lem1
   6. selvval2lem2
   7. selvval2lem3
   8. selvval2lemn
   9. selvval2lem4
   10. selvval2lem5
   11. selvcl
   12. frlmfielbas
   13. frlmfzwrd
   14. frlmfzowrd
   15. frlmfzolen
   16. frlmfzowrdb
   17. frlmfzoccat
   18. frlmvscadiccat
   19. ismhmd
   20. ablcmnd
   21. ringcld
   22. ringassd
   23. ringlidmd
   24. ringridmd
   25. ringabld
   26. ringcmnd
   27. drngringd
   28. drnggrpd
   29. drnginvrcld
   30. drnginvrn0d
   31. drnginvrld
   32. drnginvrrd
   33. drngmulcanad
   34. drngmulcan2ad
   35. drnginvmuld
   36. fldcrngd
   37. lmodgrpd
   38. lvecgrp
   39. lveclmodd
   40. lvecgrpd
   41. lvecring
   42. lmhmlvec
   43. frlm0vald
   44. frlmsnic
   45. uvccl
   46. uvcn0
   47. pwselbasr
   48. pwspjmhmmgpd
   49. pwsexpg
   50. pwsgprod
   51. mplascl0
   52. evl0
   53. evlsval3
   54. evlsscaval
   55. evlsvarval
   56. evlsbagval
   57. evlsexpval
   58. evlsaddval
   59. evlsmulval
   60. fsuppind
   61. fsuppssindlem1
   62. fsuppssindlem2
   63. fsuppssind
   64. mhpind
   65. mhphflem
   66. mhphf
   67. mhphf2
   68. mhphf3
   69. mhphf4
4. Arithmetic theorems
   1. c0exALT
   2. 0cnALT3
   3. elre0re
   4. 1t1e1ALT
   5. remulcan2d
   6. readdid1addid2d
   7. sn-1ne2
   8. nnn1suc
   9. nnadd1com
   10. nnaddcom
   11. nnaddcomli
   12. nnadddir
   13. nnmul1com
   14. nnmulcom
   15. mvrrsubd
   16. laddrotrd
   17. raddcom12d
   18. lsubrotld
   19. lsubcom23d
   20. addsubeq4com
   21. sqsumi
   22. negn0nposznnd
   23. sqmid3api
   24. decaddcom
   25. sqn5i
   26. sqn5ii
   27. decpmulnc
   28. decpmul
   29. sqdeccom12
   30. sq3deccom12
   31. 235t711
   32. ex-decpmul
5. Exponents and divisibility
   1. oexpreposd
   2. ltexp1d
   3. ltexp1dd
   4. exp11nnd
   5. exp11d
   6. 0dvds0
   7. absdvdsabsb
   8. dvdsexpim
   9. gcdnn0id
   10. gcdle1d
   11. gcdle2d
   12. dvdsexpad
   13. nn0rppwr
   14. expgcd
   15. nn0expgcd
   16. zexpgcd
   17. numdenexp
   18. numexp
   19. denexp
   20. dvdsexpnn
   21. dvdsexpnn0
   22. dvdsexpb
   23. posqsqznn
   24. cxpgt0d
   25. zrtelqelz
   26. zrtdvds
   27. rtprmirr
6. Real subtraction
   1. cresub
   2. df-resub
   3. resubval
   4. renegeulemv
   5. renegeulem
   6. renegeu
   7. rernegcl
   8. renegadd
   9. renegid
   10. reneg0addid2
   11. resubeulem1
   12. resubeulem2
   13. resubeu
   14. rersubcl
   15. resubadd
   16. resubaddd
   17. resubf
   18. repncan2
   19. repncan3
   20. readdsub
   21. reladdrsub
   22. reltsub1
   23. reltsubadd2
   24. resubcan2
   25. resubsub4
   26. rennncan2
   27. renpncan3
   28. repnpcan
   29. reppncan
   30. resubidaddid1lem
   31. resubidaddid1
   32. resubdi
   33. re1m1e0m0
   34. sn-00idlem1
   35. sn-00idlem2
   36. sn-00idlem3
   37. sn-00id
   38. re0m0e0
   39. readdid2
   40. sn-addid2
   41. remul02
   42. sn-0ne2
   43. remul01
   44. resubid
   45. readdid1
   46. resubid1
   47. renegneg
   48. readdcan2
   49. renegid2
   50. sn-it0e0
   51. sn-negex12
   52. sn-negex
   53. sn-negex2
   54. sn-addcand
   55. sn-addid1
   56. sn-addcan2d
   57. reixi
   58. rei4
   59. sn-addid0
   60. sn-mul01
   61. sn-subeu
   62. sn-subcl
   63. sn-subf
   64. resubeqsub
   65. subresre
   66. addinvcom
   67. remulinvcom
   68. remulid2
   69. sn-1ticom
   70. sn-mulid2
   71. it1ei
   72. ipiiie0
   73. remulcand
   74. sn-0tie0
   75. sn-mul02
   76. sn-ltaddpos
   77. reposdif
   78. relt0neg1
   79. relt0neg2
   80. mulgt0con1dlem
   81. mulgt0con1d
   82. mulgt0con2d
   83. mulgt0b2d
   84. sn-ltmul2d
   85. sn-0lt1
   86. sn-ltp1
   87. reneg1lt0
   88. sn-inelr
   89. itrere
   90. retire
   91. cnreeu
   92. sn-sup2
7. Projective spaces
   1. cprjsp
   2. df-prjsp
   3. prjspval
   4. prjsprel
   5. prjspertr
   6. prjsperref
   7. prjspersym
   8. prjsper
   9. prjspreln0
   10. prjspvs
   11. prjsprellsp
   12. prjspeclsp
   13. prjspval2
   14. cprjspn
   15. df-prjspn
   16. prjspnval
   17. prjspnerlem
   18. prjspnval2
   19. prjspner
   20. prjspnvs
   21. 0prjspnlem
   22. prjspnfv01
   23. prjspner01
   24. prjspner1
   25. 0prjspnrel
   26. 0prjspn
   27. cprjcrv
   28. df-prjcrv
   29. prjcrvfval
   30. prjcrvval
   31. prjcrv0
8. Basic reductions for Fermat's Last Theorem
   1. dffltz
   2. fltmul
   3. fltdiv
   4. flt0
   5. fltdvdsabdvdsc
   6. fltabcoprmex
   7. fltaccoprm
   8. fltbccoprm
   9. fltabcoprm
   10. infdesc
   11. fltne
   12. flt4lem
   13. flt4lem1
   14. flt4lem2
   15. flt4lem3
   16. flt4lem4
   17. flt4lem5
   18. flt4lem5elem
   19. flt4lem5a
   20. flt4lem5b
   21. flt4lem5c
   22. flt4lem5d
   23. flt4lem5e
   24. flt4lem5f
   25. flt4lem6
   26. flt4lem7
   27. nna4b4nsq
   28. fltltc
   29. fltnltalem
   30. fltnlta