Theorem nnsinds

Description: Strong (or "total") induction principle over the naturals. (Contributed by Scott Fenton, 16-May-2014)

	Ref	Expression
Hypotheses	nnsinds.1	|- ( x = y -> ( ph <-> ps ) )
	nnsinds.2	|- ( x = N -> ( ph <-> ch ) )
	nnsinds.3	|- ( x e. NN -> ( A. y e. ( 1 ... ( x - 1 ) ) ps -> ph ) )
Assertion	nnsinds	|- ( N e. NN -> ch )

Proof

Step	Hyp	Ref	Expression
1		nnsinds.1	|- ( x = y -> ( ph <-> ps ) )
2		nnsinds.2	|- ( x = N -> ( ph <-> ch ) )
3		nnsinds.3	|- ( x e. NN -> ( A. y e. ( 1 ... ( x - 1 ) ) ps -> ph ) )
4		elnnuz	|- ( N e. NN <-> N e. ( ZZ>= ` 1 ) )
5		elnnuz	|- ( x e. NN <-> x e. ( ZZ>= ` 1 ) )
6	5 3	sylbir	|- ( x e. ( ZZ>= ` 1 ) -> ( A. y e. ( 1 ... ( x - 1 ) ) ps -> ph ) )
7	1 2 6	uzsinds	|- ( N e. ( ZZ>= ` 1 ) -> ch )
8	4 7	sylbi	|- ( N e. NN -> ch )