# Metamath Proof Explorer

## Theorem nn0ind

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 step. (Contributed by NM, 13-May-2004)

Ref Expression
Hypotheses nn0ind.1 ${⊢}{x}=0\to \left({\phi }↔{\psi }\right)$
nn0ind.2 ${⊢}{x}={y}\to \left({\phi }↔{\chi }\right)$
nn0ind.3 ${⊢}{x}={y}+1\to \left({\phi }↔{\theta }\right)$
nn0ind.4 ${⊢}{x}={A}\to \left({\phi }↔{\tau }\right)$
nn0ind.5 ${⊢}{\psi }$
nn0ind.6 ${⊢}{y}\in {ℕ}_{0}\to \left({\chi }\to {\theta }\right)$
Assertion nn0ind ${⊢}{A}\in {ℕ}_{0}\to {\tau }$

### Proof

Step Hyp Ref Expression
1 nn0ind.1 ${⊢}{x}=0\to \left({\phi }↔{\psi }\right)$
2 nn0ind.2 ${⊢}{x}={y}\to \left({\phi }↔{\chi }\right)$
3 nn0ind.3 ${⊢}{x}={y}+1\to \left({\phi }↔{\theta }\right)$
4 nn0ind.4 ${⊢}{x}={A}\to \left({\phi }↔{\tau }\right)$
5 nn0ind.5 ${⊢}{\psi }$
6 nn0ind.6 ${⊢}{y}\in {ℕ}_{0}\to \left({\chi }\to {\theta }\right)$
7 elnn0z ${⊢}{A}\in {ℕ}_{0}↔\left({A}\in ℤ\wedge 0\le {A}\right)$
8 0z ${⊢}0\in ℤ$
9 5 a1i ${⊢}0\in ℤ\to {\psi }$
10 elnn0z ${⊢}{y}\in {ℕ}_{0}↔\left({y}\in ℤ\wedge 0\le {y}\right)$
11 10 6 sylbir ${⊢}\left({y}\in ℤ\wedge 0\le {y}\right)\to \left({\chi }\to {\theta }\right)$
12 11 3adant1 ${⊢}\left(0\in ℤ\wedge {y}\in ℤ\wedge 0\le {y}\right)\to \left({\chi }\to {\theta }\right)$
13 1 2 3 4 9 12 uzind ${⊢}\left(0\in ℤ\wedge {A}\in ℤ\wedge 0\le {A}\right)\to {\tau }$
14 8 13 mp3an1 ${⊢}\left({A}\in ℤ\wedge 0\le {A}\right)\to {\tau }$
15 7 14 sylbi ${⊢}{A}\in {ℕ}_{0}\to {\tau }$