Metamath Proof Explorer

Table of Contents - 20.34. Mathbox for Stanislas Polu

  1. inductionexd
  2. IMO Problems
    1. IMO 1972 B2
  3. INT Inequalities Proof Generator
    1. int-addcomd
    2. int-addassocd
    3. int-addsimpd
    4. int-mulcomd
    5. int-mulassocd
    6. int-mulsimpd
    7. int-leftdistd
    8. int-rightdistd
    9. int-sqdefd
    10. int-mul11d
    11. int-mul12d
    12. int-add01d
    13. int-add02d
    14. int-sqgeq0d
    15. int-eqprincd
    16. int-eqtransd
    17. int-eqmvtd
    18. int-eqineqd
    19. int-ineqmvtd
    20. int-ineq1stprincd
    21. int-ineq2ndprincd
    22. int-ineqtransd
  4. N-Digit Addition Proof Generator
    1. unitadd
  5. AM-GM (for k = 2,3,4)
    1. gsumws3
    2. gsumws4
    3. amgm2d
    4. amgm3d
    5. amgm4d