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

Proof

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