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 \leftrightarrow \psi \right)$$
	nn0ind.2	$$⊢x=y\to \left(\phi \leftrightarrow \chi \right)$$
	nn0ind.3	$$⊢x=y+1\to \left(\phi \leftrightarrow \theta \right)$$
	nn0ind.4	$$⊢x=A\to \left(\phi \leftrightarrow \tau \right)$$
	nn0ind.5	$$⊢\psi$$
	nn0ind.6	$$⊢y\in {\mathbb{N}}_0\to \left(\chi \to \theta \right)$$
Assertion	nn0ind	$$⊢A\in {\mathbb{N}}_0\to \tau$$

Proof

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