Metamath Proof Explorer


Table of Contents - 5.4.2. Principle of mathematical induction

  1. nnind
  2. nnindALT
  3. nnindd
  4. nn1m1nn
  5. nn1suc
  6. nnaddcl
  7. nnmulcl
  8. nnmulcli
  9. nnmtmip
  10. nn2ge
  11. nnge1
  12. nngt1ne1
  13. nnle1eq1
  14. nngt0
  15. nnnlt1
  16. nnnle0
  17. nnne0
  18. nnneneg
  19. 0nnn
  20. 0nnnALT
  21. nnne0ALT
  22. nngt0i
  23. nnne0i
  24. nndivre
  25. nnrecre
  26. nnrecgt0
  27. nnsub
  28. nnsubi
  29. nndiv
  30. nndivtr
  31. nnge1d
  32. nngt0d
  33. nnne0d
  34. nnrecred
  35. nnaddcld
  36. nnmulcld
  37. nndivred