Metamath Proof Explorer

Table of Contents - 21.31. Mathbox for Steven Nguyen

1. Utility theorems
   1. jarrii
   2. intnanrt
   3. ioin9i8
   4. jaodd
   5. syl3an12
   6. exbiii
   7. sbtd
   8. sbor2
   9. sbalexi
   10. 19.9dev
   11. 3rspcedvd
   12. sn-axrep5v
   13. sn-axprlem3
   14. sn-exelALT
   15. ss2ab1
   16. ssabdv
   17. sn-iotalem
   18. sn-iotalemcor
   19. abbi1sn
   20. brif2
   21. brif12
   22. pssexg
   23. pssn0
   24. psspwb
   25. xppss12
   26. elpwbi
   27. imaopab
   28. eqresfnbd
   29. f1o2d2
   30. fmpocos
   31. ovmpogad
   32. ofun
   33. dfqs2
   34. dfqs3
   35. qseq12d
   36. qsalrel
   37. elmapssresd
   38. supinf
   39. mapcod
   40. fisdomnn
   41. ltex
   42. leex
   43. subex
   44. absex
   45. cjex
   46. fzosumm1
   47. ccatcan2d
2. Arithmetic theorems
   1. c0exALT
   2. 0cnALT3
   3. elre0re
   4. 1t1e1ALT
   5. lttrii
   6. remulcan2d
   7. readdridaddlidd
   8. 1p3e4
   9. 5ne0
   10. 6ne0
   11. 7ne0
   12. 8ne0
   13. 9ne0
   14. sn-1ne2
   15. nnn1suc
   16. nnadd1com
   17. nnaddcom
   18. nnaddcomli
   19. nnadddir
   20. nnmul1com
   21. nnmulcom
   22. readdrcl2d
   23. mvrrsubd
   24. laddrotrd
   25. raddswap12d
   26. lsubrotld
   27. rsubrotld
   28. lsubswap23d
   29. addsubeq4com
   30. sqsumi
   31. negn0nposznnd
   32. sqmid3api
   33. decaddcom
   34. sqn5i
   35. sqn5ii
   36. decpmulnc
   37. decpmul
   38. sqdeccom12
   39. sq3deccom12
   40. 4t5e20
   41. 3rdpwhole
   42. sq4
   43. sq5
   44. sq6
   45. sq7
   46. sq8
   47. sq9
   48. rpsscn
   49. 4rp
   50. 6rp
   51. 7rp
   52. 8rp
   53. 9rp
   54. 235t711
   55. ex-decpmul
   56. eluzp1
   57. sn-eluzp1l
   58. fz1sumconst
   59. fz1sump1
   60. oddnumth
   61. nicomachus
   62. sumcubes
   63. ine1
   64. 0tie0
   65. it1ei
   66. 1tiei
   67. itrere
   68. retire
   69. iocioodisjd
   70. rpabsid
3. Exponents and divisibility
   1. oexpreposd
   2. explt1d
   3. expeq1d
   4. expeqidd
   5. exp11d
   6. 0dvds0
   7. absdvdsabsb
   8. gcdnn0id
   9. gcdle1d
   10. gcdle2d
   11. dvdsexpad
   12. dvdsexpnn
   13. dvdsexpnn0
   14. dvdsexpb
   15. posqsqznn
   16. zdivgd
   17. efsubd
   18. ef11d
   19. logccne0d
   20. cxp112d
   21. cxp111d
   22. cxpi11d
   23. logne0d
   24. rxp112d
   25. log11d
   26. rplog11d
   27. rxp11d
4. Trigonometry and Calculus
   1. tanhalfpim
   2. sinpim
   3. cospim
   4. tan3rdpi
   5. sin2t3rdpi
   6. cos2t3rdpi
   7. sin4t3rdpi
   8. cos4t3rdpi
   9. asin1half
   10. acos1half
   11. dvun
   12. redvmptabs
   13. readvrec2
   14. readvrec
   15. resuppsinopn
   16. readvcot
5. Independence of ax-mulcom
   1. cresub
   2. df-resub
   3. resubval
   4. renegeulemv
   5. renegeulem
   6. renegeu
   7. rernegcl
   8. renegadd
   9. renegid
   10. reneg0addlid
   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. resubidaddlidlem
   31. resubidaddlid
   32. resubdi
   33. re1m1e0m0
   34. sn-00idlem1
   35. sn-00idlem2
   36. sn-00idlem3
   37. sn-00id
   38. re0m0e0
   39. readdlid
   40. sn-addlid
   41. remul02
   42. sn-0ne2
   43. remul01
   44. sn-remul0ord
   45. resubid
   46. readdrid
   47. resubid1
   48. renegneg
   49. readdcan2
   50. renegid2
   51. remulneg2d
   52. sn-it0e0
   53. sn-negex12
   54. sn-negex
   55. sn-negex2
   56. sn-addcand
   57. sn-addrid
   58. sn-addcan2d
   59. reixi
   60. rei4
   61. sn-addid0
   62. sn-mul01
   63. sn-subeu
   64. sn-subcl
   65. sn-subf
   66. resubeqsub
   67. subresre
   68. addinvcom
   69. remulinvcom
   70. remullid
   71. sn-1ticom
   72. sn-mullid
   73. sn-it1ei
   74. ipiiie0
   75. remulcand
   76. crediv
   77. df-rediv
   78. redivvald
   79. rediveud
   80. sn-redivcld
   81. redivmuld
   82. redivcan2d
   83. redivcan3d
   84. sn-rereccld
   85. rerecid
   86. rerecid2
   87. sn-0tie0
   88. sn-mul02
   89. sn-ltaddpos
   90. sn-ltaddneg
   91. reposdif
   92. relt0neg1
   93. relt0neg2
   94. sn-addlt0d
   95. sn-addgt0d
   96. sn-nnne0
   97. reelznn0nn
   98. nn0addcom
   99. zaddcomlem
   100. zaddcom
   101. renegmulnnass
   102. nn0mulcom
   103. zmulcomlem
   104. zmulcom
   105. mulgt0con1dlem
   106. mulgt0con1d
   107. mulgt0con2d
   108. mulgt0b1d
   109. sn-ltmul2d
   110. sn-ltmulgt11d
   111. sn-0lt1
   112. sn-ltp1
   113. sn-recgt0d
   114. mulgt0b2d
   115. sn-mulgt1d
   116. reneg1lt0
   117. sn-reclt0d
   118. mulltgt0d
   119. mullt0b1d
   120. mullt0b2d
   121. sn-mullt0d
   122. sn-msqgt0d
   123. sn-inelr
   124. sn-itrere
   125. sn-retire
   126. cnreeu
   127. sn-sup2
   128. sn-sup3d
   129. sn-suprcld
   130. sn-suprubd
6. Structures
   1. sn-base0
   2. nelsubginvcld
   3. nelsubgcld
   4. nelsubgsubcld
   5. rnasclg
   6. frlmfielbas
   7. frlmfzwrd
   8. frlmfzowrd
   9. frlmfzolen
   10. frlmfzowrdb
   11. frlmfzoccat
   12. frlmvscadiccat
   13. grpasscan2d
   14. grpcominv1
   15. grpcominv2
   16. finsubmsubg
   17. opprmndb
   18. opprgrpb
   19. opprablb
   20. imacrhmcl
   21. rimrcl1
   22. rimrcl2
   23. rimcnv
   24. rimco
   25. ricsym
   26. rictr
   27. riccrng1
   28. riccrng
   29. domnexpgn0cl
   30. drnginvrn0d
   31. drngmullcan
   32. drngmulrcan
   33. drnginvmuld
   34. ricdrng1
   35. ricdrng
   36. ricfld
   37. asclf1
   38. abvexp
   39. fimgmcyclem
   40. fimgmcyc
   41. fidomncyc
   42. fiabv
   43. lvecgrp
   44. lvecring
   45. frlm0vald
   46. frlmsnic
   47. uvccl
   48. uvcn0
   49. pwselbasr
   50. pwsgprod
   51. psrmnd
   52. psrbagres
   53. mplcrngd
   54. mplsubrgcl
   55. mhmcopsr
   56. mhmcoaddpsr
   57. rhmcomulpsr
   58. rhmpsr
   59. rhmpsr1
   60. mplascl0
   61. mplascl1
   62. mplmapghm
   63. evl0
   64. evlscl
   65. evlsval3
   66. evlsvval
   67. evlsvvvallem
   68. evlsvvvallem2
   69. evlsvvval
   70. evlsscaval
   71. evlsvarval
   72. evlsbagval
   73. evlsexpval
   74. evlsaddval
   75. evlsmulval
   76. evlsmaprhm
   77. evlsevl
   78. evlcl
   79. evlvvval
   80. evlvvvallem
   81. evladdval
   82. evlmulval
   83. selvcllem1
   84. selvcllem2
   85. selvcllem3
   86. selvcllemh
   87. selvcllem4
   88. selvcllem5
   89. selvcl
   90. selvval2
   91. selvvvval
   92. evlselvlem
   93. evlselv
   94. selvadd
   95. selvmul
   96. fsuppind
   97. fsuppssindlem1
   98. fsuppssindlem2
   99. fsuppssind
   100. mhpind
   101. evlsmhpvvval
   102. mhphflem
   103. mhphf
   104. mhphf2
   105. mhphf3
   106. mhphf4
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. prjspnssbas
   22. prjspnn0
   23. 0prjspnlem
   24. prjspnfv01
   25. prjspner01
   26. prjspner1
   27. 0prjspnrel
   28. 0prjspn
   29. cprjcrv
   30. df-prjcrv
   31. prjcrvfval
   32. prjcrvval
   33. 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
9. Exemplar theorems
   1. iddii
   2. bicomdALT
   3. alan
   4. exor
   5. rexor
   6. ruvALT
   7. sn-wcdeq
   8. sq45
   9. sum9cubes
   10. sn-isghm
   11. aprilfools2025
   12. Standard replacements of ax-10 , ax-11 , ax-12