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. nnadd1com
10. nnaddcom
11. nnaddcomli
12. nnmtmip
13. nn2ge
14. nnge1
15. nngt1ne1
16. nnle1eq1
17. nngt0
18. nnnlt1
19. nnnle0
20. nnne0
21. nnneneg
22. 0nnn
23. 0nnnALT
24. nnne0ALT
25. nngt0i
26. nnne0i
27. nndivre
28. nnrecre
29. nnrecgt0
30. nnsub
31. nnsubi
32. nndiv
33. nndivtr
34. nnge1d
35. nngt0d
36. nnne0d
37. nnrecred
38. nnaddcld
39. nnmulcld
40. nndivred
41. 1t1e1ALT
42. nnadddir
43. nnmul1com
44. nnmulcom