Metamath Proof Explorer


Table of Contents - 21.29. Mathbox for Steven Nguyen

  1. Utility theorems
    1. intnanrt
    2. ioin9i8
    3. jaodd
    4. syl3an12
    5. sbtd
    6. sbor2
    7. 19.9dev
    8. 3rspcedvdw
    9. 3rspcedvd
    10. sn-axrep5v
    11. sn-axprlem3
    12. sn-exelALT
    13. ss2ab1
    14. ssabdv
    15. sn-iotalem
    16. sn-iotalemcor
    17. abbi1sn
    18. brif2
    19. brif12
    20. pssexg
    21. pssn0
    22. psspwb
    23. xppss12
    24. coexd
    25. elpwbi
    26. imaopab
    27. fnsnbt
    28. fnimasnd
    29. eqresfnbd
    30. f1o2d2
    31. fmpocos
    32. ovmpogad
    33. ofun
    34. dfqs2
    35. dfqs3
    36. qseq12d
    37. qsalrel
    38. elmapssresd
    39. mapcod
    40. fzosumm1
    41. ccatcan2d
  2. Structures
    1. nelsubginvcld
    2. nelsubgcld
    3. nelsubgsubcld
    4. rnasclg
    5. frlmfielbas
    6. frlmfzwrd
    7. frlmfzowrd
    8. frlmfzolen
    9. frlmfzowrdb
    10. frlmfzoccat
    11. frlmvscadiccat
    12. grpasscan2d
    13. grpcominv1
    14. grpcominv2
    15. finsubmsubg
    16. imacrhmcl
    17. rimrcl1
    18. rimrcl2
    19. rimcnv
    20. rimco
    21. ricsym
    22. rictr
    23. riccrng1
    24. riccrng
    25. drnginvrn0d
    26. drngmulcanad
    27. drngmulcan2ad
    28. drnginvmuld
    29. ricdrng1
    30. ricdrng
    31. ricfld
    32. lvecgrp
    33. lvecring
    34. frlm0vald
    35. frlmsnic
    36. uvccl
    37. uvcn0
    38. pwselbasr
    39. pwsgprod
    40. psrmnd
    41. psrbagres
    42. mpllmodd
    43. mplringd
    44. mplcrngd
    45. mplsubrgcl
    46. mhmcopsr
    47. mhmcoaddpsr
    48. rhmcomulpsr
    49. rhmpsr
    50. mhmcompl
    51. mhmcoaddmpl
    52. rhmcomulmpl
    53. rhmmpl
    54. rhmpsr1
    55. mhmcoply1
    56. rhmply1
    57. rhmply1vr1
    58. ply1vscl
    59. rhmply1vsca
    60. rhmply1mon
    61. mplascl0
    62. mplascl1
    63. mplmapghm
    64. evl0
    65. evlscl
    66. evlsval3
    67. evlsvval
    68. evlsvvvallem
    69. evlsvvvallem2
    70. evlsvvval
    71. evlsscaval
    72. evlsvarval
    73. evlsbagval
    74. evlsexpval
    75. evlsaddval
    76. evlsmulval
    77. evlsmaprhm
    78. evlsevl
    79. evlcl
    80. evlvvval
    81. evlvvvallem
    82. evladdval
    83. evlmulval
    84. selvcllem1
    85. selvcllem2
    86. selvcllem3
    87. selvcllemh
    88. selvcllem4
    89. selvcllem5
    90. selvcl
    91. selvval2
    92. selvvvval
    93. evlselvlem
    94. evlselv
    95. selvadd
    96. selvmul
    97. fsuppind
    98. fsuppssindlem1
    99. fsuppssindlem2
    100. fsuppssind
    101. mhpind
    102. evlsmhpvvval
    103. mhphflem
    104. mhphf
    105. mhphf2
    106. mhphf3
    107. mhphf4
  3. Arithmetic theorems
    1. c0exALT
    2. 0cnALT3
    3. elre0re
    4. 1t1e1ALT
    5. remulcan2d
    6. readdridaddlidd
    7. sn-1ne2
    8. nnn1suc
    9. nnadd1com
    10. nnaddcom
    11. nnaddcomli
    12. nnadddir
    13. nnmul1com
    14. nnmulcom
    15. readdrcl2d
    16. mvrrsubd
    17. laddrotrd
    18. raddcom12d
    19. lsubrotld
    20. lsubcom23d
    21. addsubeq4com
    22. sqsumi
    23. negn0nposznnd
    24. sqmid3api
    25. decaddcom
    26. sqn5i
    27. sqn5ii
    28. decpmulnc
    29. decpmul
    30. sqdeccom12
    31. sq3deccom12
    32. 4t5e20
    33. sq9
    34. 235t711
    35. ex-decpmul
    36. fz1sumconst
    37. fz1sump1
    38. oddnumth
    39. nicomachus
    40. sumcubes
    41. pine0
    42. ine1
    43. 0tie0
    44. it1ei
    45. 1tiei
    46. itrere
    47. retire
  4. 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. zrtelqelz
    25. zrtdvds
    26. rtprmirr
    27. zdivgd
    28. efne0d
    29. efsubd
    30. ef11d
    31. logccne0d
    32. cxp112d
    33. cxp111d
    34. cxpi11d
    35. logne0d
    36. rxp112d
    37. log11d
    38. rplog11d
    39. rxp11d
  5. Real subtraction
    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. resubid
    45. readdrid
    46. resubid1
    47. renegneg
    48. readdcan2
    49. renegid2
    50. remulneg2d
    51. sn-it0e0
    52. sn-negex12
    53. sn-negex
    54. sn-negex2
    55. sn-addcand
    56. sn-addrid
    57. sn-addcan2d
    58. reixi
    59. rei4
    60. sn-addid0
    61. sn-mul01
    62. sn-subeu
    63. sn-subcl
    64. sn-subf
    65. resubeqsub
    66. subresre
    67. addinvcom
    68. remulinvcom
    69. remullid
    70. sn-1ticom
    71. sn-mullid
    72. sn-it1ei
    73. ipiiie0
    74. remulcand
    75. sn-0tie0
    76. sn-mul02
    77. sn-ltaddpos
    78. sn-ltaddneg
    79. reposdif
    80. relt0neg1
    81. relt0neg2
    82. sn-addlt0d
    83. sn-addgt0d
    84. sn-nnne0
    85. reelznn0nn
    86. nn0addcom
    87. zaddcomlem
    88. zaddcom
    89. renegmulnnass
    90. nn0mulcom
    91. zmulcomlem
    92. zmulcom
    93. mulgt0con1dlem
    94. mulgt0con1d
    95. mulgt0con2d
    96. mulgt0b2d
    97. sn-ltmul2d
    98. sn-0lt1
    99. sn-ltp1
    100. reneg1lt0
    101. sn-inelr
    102. sn-itrere
    103. sn-retire
    104. cnreeu
    105. sn-sup2
  6. 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
  7. 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
  8. Exemplar theorems
    1. iddii
    2. bicomdALT
    3. elabgw
    4. elab2gw
    5. elrab2w
    6. ruvALT
    7. sn-wcdeq
    8. sq45
    9. sum9cubes
    10. acos1half
    11. aprilfools2025