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\to \left(\phi \leftrightarrow \psi \right)$$
	uzind4i.2	$$⊢j=k\to \left(\phi \leftrightarrow \chi \right)$$
	uzind4i.3	$$⊢j=k+1\to \left(\phi \leftrightarrow \theta \right)$$
	uzind4i.4	$$⊢j=N\to \left(\phi \leftrightarrow \tau \right)$$
	uzind4i.5	$$⊢\psi$$
	uzind4i.6	$$⊢k\in {\mathbb{Z}}_{\ge M}\to \left(\chi \to \theta \right)$$
Assertion	uzind4i	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \tau$$

Proof

Step	Hyp	Ref	Expression
1		uzind4i.1	$$⊢j=M\to \left(\phi \leftrightarrow \psi \right)$$
2		uzind4i.2	$$⊢j=k\to \left(\phi \leftrightarrow \chi \right)$$
3		uzind4i.3	$$⊢j=k+1\to \left(\phi \leftrightarrow \theta \right)$$
4		uzind4i.4	$$⊢j=N\to \left(\phi \leftrightarrow \tau \right)$$
5		uzind4i.5	$$⊢\psi$$
6		uzind4i.6	$$⊢k\in {\mathbb{Z}}_{\ge M}\to \left(\chi \to \theta \right)$$
7	5	a1i	$$⊢M\in \mathbb{Z}\to \psi$$
8	1 2 3 4 7 6	uzind4	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \tau$$