Metamath Proof Explorer
Table of Contents - 5.4.2. Principle of mathematical induction
- nnind
- nnindALT
- nnindd
- nn1m1nn
- nn1suc
- nnaddcl
- nnmulcl
- nnmulcli
- nnmtmip
- nn2ge
- nnge1
- nngt1ne1
- nnle1eq1
- nngt0
- nnnlt1
- nnnle0
- nnne0
- nnneneg
- 0nnn
- 0nnnALT
- nnne0ALT
- nngt0i
- nnne0i
- nndivre
- nnrecre
- nnrecgt0
- nnsub
- nnsubi
- nndiv
- nndivtr
- nnge1d
- nngt0d
- nnne0d
- nnrecred
- nnaddcld
- nnmulcld
- nndivred