Metamath Proof Explorer

Table of Contents - 21.30. Mathbox for metakunt

1. Commutative Semiring
   1. ccsrg
   2. df-csring
   3. iscsrg
2. General helpful statements
   1. rhmzrhval
   2. zndvdchrrhm
   3. relogbcld
   4. relogbexpd
   5. relogbzexpd
   6. logblebd
   7. uzindd
   8. fzadd2d
   9. zltp1led
   10. fzne2d
   11. eqfnfv2d2
   12. fzsplitnd
   13. fzsplitnr
   14. addassnni
   15. addcomnni
   16. mulassnni
   17. mulcomnni
   18. gcdcomnni
   19. gcdnegnni
   20. neggcdnni
   21. bccl2d
   22. recbothd
   23. gcdmultiplei
   24. gcdaddmzz2nni
   25. gcdaddmzz2nncomi
   26. gcdnncli
   27. muldvds1d
   28. muldvds2d
   29. nndivdvdsd
   30. nnproddivdvdsd
   31. coprmdvds2d
   32. imadomfi
3. Some gcd and lcm results
   1. 12gcd5e1
   2. 60gcd6e6
   3. 60gcd7e1
   4. 420gcd8e4
   5. lcmeprodgcdi
   6. 12lcm5e60
   7. 60lcm6e60
   8. 60lcm7e420
   9. 420lcm8e840
   10. lcmfunnnd
   11. lcm1un
   12. lcm2un
   13. lcm3un
   14. lcm4un
   15. lcm5un
   16. lcm6un
   17. lcm7un
   18. lcm8un
4. Least common multiple inequality theorem
   1. 3factsumint1
   2. 3factsumint2
   3. 3factsumint3
   4. 3factsumint4
   5. 3factsumint
   6. resopunitintvd
   7. resclunitintvd
   8. resdvopclptsd
   9. lcmineqlem1
   10. lcmineqlem2
   11. lcmineqlem3
   12. lcmineqlem4
   13. lcmineqlem5
   14. lcmineqlem6
   15. lcmineqlem7
   16. lcmineqlem8
   17. lcmineqlem9
   18. lcmineqlem10
   19. lcmineqlem11
   20. lcmineqlem12
   21. lcmineqlem13
   22. lcmineqlem14
   23. lcmineqlem15
   24. lcmineqlem16
   25. lcmineqlem17
   26. lcmineqlem18
   27. lcmineqlem19
   28. lcmineqlem20
   29. lcmineqlem21
   30. lcmineqlem22
   31. lcmineqlem23
   32. lcmineqlem
5. Logarithm inequalities
   1. 3exp7
   2. 3lexlogpow5ineq1
   3. 3lexlogpow5ineq2
   4. 3lexlogpow5ineq4
   5. 3lexlogpow5ineq3
   6. 3lexlogpow2ineq1
   7. 3lexlogpow2ineq2
   8. 3lexlogpow5ineq5
6. Miscellaneous results for AKS formalisation
   1. intlewftc
   2. aks4d1lem1
   3. aks4d1p1p1
   4. dvrelog2
   5. dvrelog3
   6. dvrelog2b
   7. 0nonelalab
   8. dvrelogpow2b
   9. aks4d1p1p3
   10. aks4d1p1p2
   11. aks4d1p1p4
   12. dvle2
   13. aks4d1p1p6
   14. aks4d1p1p7
   15. aks4d1p1p5
   16. aks4d1p1
   17. aks4d1p2
   18. aks4d1p3
   19. aks4d1p4
   20. aks4d1p5
   21. aks4d1p6
   22. aks4d1p7d1
   23. aks4d1p7
   24. aks4d1p8d1
   25. aks4d1p8d2
   26. aks4d1p8d3
   27. aks4d1p8
   28. aks4d1p9
   29. aks4d1
   30. fldhmf1
   31. cprimroots
   32. df-primroots
   33. isprimroot
   34. isprimroot2
   35. mndmolinv
   36. linvh
   37. primrootsunit1
   38. primrootsunit
   39. primrootscoprmpow
   40. posbezout
   41. primrootscoprf
   42. primrootscoprbij
   43. primrootscoprbij2
   44. remexz
   45. primrootlekpowne0
   46. primrootspoweq0
   47. aks6d1c1p1
   48. aks6d1c1p1rcl
   49. aks6d1c1p2
   50. aks6d1c1p3
   51. aks6d1c1p4
   52. aks6d1c1p5
   53. aks6d1c1p7
   54. aks6d1c1p6
   55. aks6d1c1p8
   56. aks6d1c1
   57. evl1gprodd
   58. aks6d1c2p1
   59. aks6d1c2p2
   60. hashscontpowcl
   61. hashscontpow1
   62. hashscontpow
   63. aks6d1c3
   64. aks6d1c4
   65. aks6d1c1rh
   66. aks6d1c2lem3
   67. aks6d1c2lem4
   68. hashnexinj
   69. hashnexinjle
   70. aks6d1c2
   71. rspcsbnea
   72. idomnnzpownz
   73. idomnnzgmulnz
   74. ringexp0nn
   75. aks6d1c5lem0
   76. aks6d1c5lem1
   77. aks6d1c5lem3
   78. aks6d1c5lem2
   79. aks6d1c5
   80. deg1gprod
   81. deg1pow
   82. 5bc2eq10
   83. facp2
   84. 2np3bcnp1
   85. 2ap1caineq
7. Sticks and stones
   1. sticksstones1
   2. sticksstones2
   3. sticksstones3
   4. sticksstones4
   5. sticksstones5
   6. sticksstones6
   7. sticksstones7
   8. sticksstones8
   9. sticksstones9
   10. sticksstones10
   11. sticksstones11
   12. sticksstones12a
   13. sticksstones12
   14. sticksstones13
   15. sticksstones14
   16. sticksstones15
   17. sticksstones16
   18. sticksstones17
   19. sticksstones18
   20. sticksstones19
   21. sticksstones20
   22. sticksstones21
   23. sticksstones22
   24. sticksstones23
8. Continuation AKS
   1. aks6d1c6lem1
   2. aks6d1c6lem2
   3. aks6d1c6lem3
   4. aks6d1c6lem4
   5. aks6d1c6isolem1
   6. aks6d1c6isolem2
   7. aks6d1c6isolem3
   8. aks6d1c6lem5
   9. bcled
   10. bcle2d
   11. aks6d1c7lem1
   12. aks6d1c7lem2
   13. aks6d1c7lem3
   14. aks6d1c7lem4
   15. aks6d1c7
   16. rhmqusspan
   17. aks5lem1
   18. aks5lem2
   19. ply1asclzrhval
   20. aks5lem3a
   21. aks5lem4a
   22. aks5lem5a
   23. aks5lem6
   24. indstrd
   25. grpods
   26. unitscyglem1
   27. unitscyglem2
   28. unitscyglem3
   29. unitscyglem4
   30. unitscyglem5
   31. aks5lem7
   32. aks5lem8
   33. ax-exfinfld
   34. exfinfldd
   35. aks5