Theorem uzind4i

Description: Induction on the upper integers that start at M . The first four give us the substitution instances we need, and the last two are the basis and the induction step. This is a stronger version of uzind4 assuming that ps holds unconditionally. Notice that N e. ( ZZ>=M ) implies that the lower bound M is an integer ( M e. ZZ , see eluzel2 ). (Contributed by NM, 4-Sep-2005) (Revised by AV, 13-Jul-2022)

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

Proof

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