Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nn0ind Structured version   Unicode version

Theorem nn0ind 10366
 Description: Principle of Mathematical Induction (inference schema) on nonnegative integers. The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction hypothesis. (Contributed by NM, 13-May-2004.)
Hypotheses
Ref Expression
nn0ind.1
nn0ind.2
nn0ind.3
nn0ind.4
nn0ind.5
nn0ind.6
Assertion
Ref Expression
nn0ind
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()   ()   ()   ()

Proof of Theorem nn0ind
StepHypRef Expression
1 elnn0z 10294 . 2
2 0z 10293 . . 3
3 nn0ind.1 . . . 4
4 nn0ind.2 . . . 4
5 nn0ind.3 . . . 4
6 nn0ind.4 . . . 4
7 nn0ind.5 . . . . 5
87a1i 11 . . . 4
9 elnn0z 10294 . . . . . 6
10 nn0ind.6 . . . . . 6
119, 10sylbir 205 . . . . 5
12113adant1 975 . . . 4
133, 4, 5, 6, 8, 12uzind 10361 . . 3
142, 13mp3an1 1266 . 2
151, 14sylbi 188 1