Theorem uzind4ALT

Description: Induction on the upper set of integers that starts at an integer M . The last four hypotheses give us the substitution instances we need; the first two are the basis and the induction step. Either uzind4 or uzind4ALT may be used; see comment for nnind . (Contributed by NM, 7-Sep-2005) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	uzind4ALT.5	|- ( M e. ZZ -> ps )
	uzind4ALT.6	|- ( k e. ( ZZ>= ` M ) -> ( ch -> th ) )
	uzind4ALT.1	|- ( j = M -> ( ph <-> ps ) )
	uzind4ALT.2	|- ( j = k -> ( ph <-> ch ) )
	uzind4ALT.3	|- ( j = ( k + 1 ) -> ( ph <-> th ) )
	uzind4ALT.4	|- ( j = N -> ( ph <-> ta ) )
Assertion	uzind4ALT	|- ( N e. ( ZZ>= ` M ) -> ta )

Proof

Step	Hyp	Ref	Expression
1		uzind4ALT.5	|- ( M e. ZZ -> ps )
2		uzind4ALT.6	|- ( k e. ( ZZ>= ` M ) -> ( ch -> th ) )
3		uzind4ALT.1	|- ( j = M -> ( ph <-> ps ) )
4		uzind4ALT.2	|- ( j = k -> ( ph <-> ch ) )
5		uzind4ALT.3	|- ( j = ( k + 1 ) -> ( ph <-> th ) )
6		uzind4ALT.4	|- ( j = N -> ( ph <-> ta ) )
7	3 4 5 6 1 2	uzind4	|- ( N e. ( ZZ>= ` M ) -> ta )