Description: Principle of Mathematical Induction (inference schema) on nonnegative integers, a deduction version. (Contributed by Thierry Arnoux, 23-Mar-2018)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nn0indd.1 | |
|
nn0indd.2 | |
||
nn0indd.3 | |
||
nn0indd.4 | |
||
nn0indd.5 | |
||
nn0indd.6 | |
||
Assertion | nn0indd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nn0indd.1 | |
|
2 | nn0indd.2 | |
|
3 | nn0indd.3 | |
|
4 | nn0indd.4 | |
|
5 | nn0indd.5 | |
|
6 | nn0indd.6 | |
|
7 | 1 | imbi2d | |
8 | 2 | imbi2d | |
9 | 3 | imbi2d | |
10 | 4 | imbi2d | |
11 | 6 | ex | |
12 | 11 | expcom | |
13 | 12 | a2d | |
14 | 7 8 9 10 5 13 | nn0ind | |
15 | 14 | impcom | |