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 -> ( ph <-> ps ) )
	nn0ind.2	|- ( x = y -> ( ph <-> ch ) )
	nn0ind.3	|- ( x = ( y + 1 ) -> ( ph <-> th ) )
	nn0ind.4	|- ( x = A -> ( ph <-> ta ) )
	nn0ind.5	|- ps
	nn0ind.6	|- ( y e. NN0 -> ( ch -> th ) )
Assertion	nn0ind	|- ( A e. NN0 -> ta )

Proof

Step	Hyp	Ref	Expression
1		nn0ind.1	|- ( x = 0 -> ( ph <-> ps ) )
2		nn0ind.2	|- ( x = y -> ( ph <-> ch ) )
3		nn0ind.3	|- ( x = ( y + 1 ) -> ( ph <-> th ) )
4		nn0ind.4	|- ( x = A -> ( ph <-> ta ) )
5		nn0ind.5	|- ps
6		nn0ind.6	|- ( y e. NN0 -> ( ch -> th ) )
7		elnn0z	|- ( A e. NN0 <-> ( A e. ZZ /\ 0 <_ A ) )
8		0z	|- 0 e. ZZ
9	5	a1i	|- ( 0 e. ZZ -> ps )
10		elnn0z	|- ( y e. NN0 <-> ( y e. ZZ /\ 0 <_ y ) )
11	10 6	sylbir	|- ( ( y e. ZZ /\ 0 <_ y ) -> ( ch -> th ) )
12	11	3adant1	|- ( ( 0 e. ZZ /\ y e. ZZ /\ 0 <_ y ) -> ( ch -> th ) )
13	1 2 3 4 9 12	uzind	|- ( ( 0 e. ZZ /\ A e. ZZ /\ 0 <_ A ) -> ta )
14	8 13	mp3an1	|- ( ( A e. ZZ /\ 0 <_ A ) -> ta )
15	7 14	sylbi	|- ( A e. NN0 -> ta )