Theorem nn0sinds

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

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

Proof

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