Description: Principle of Mathematical Induction (inference schema) on nonnegative integers. The last four hypotheses give us the substitution instances we need; the first two are the basis and the induction step. Either nn0ind or nn0indALT may be used; see comment for nnind . (Contributed by NM, 28-Nov-2005) (New usage is discouraged.) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | nn0indALT.6 | |- ( y e. NN0 -> ( ch -> th ) ) |
|
| nn0indALT.5 | |- ps |
||
| nn0indALT.1 | |- ( x = 0 -> ( ph <-> ps ) ) |
||
| nn0indALT.2 | |- ( x = y -> ( ph <-> ch ) ) |
||
| nn0indALT.3 | |- ( x = ( y + 1 ) -> ( ph <-> th ) ) |
||
| nn0indALT.4 | |- ( x = A -> ( ph <-> ta ) ) |
||
| Assertion | nn0indALT | |- ( A e. NN0 -> ta ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nn0indALT.6 | |- ( y e. NN0 -> ( ch -> th ) ) |
|
| 2 | nn0indALT.5 | |- ps |
|
| 3 | nn0indALT.1 | |- ( x = 0 -> ( ph <-> ps ) ) |
|
| 4 | nn0indALT.2 | |- ( x = y -> ( ph <-> ch ) ) |
|
| 5 | nn0indALT.3 | |- ( x = ( y + 1 ) -> ( ph <-> th ) ) |
|
| 6 | nn0indALT.4 | |- ( x = A -> ( ph <-> ta ) ) |
|
| 7 | 3 4 5 6 2 1 | nn0ind | |- ( A e. NN0 -> ta ) |