Theorem nnindALT

Description: Principle of Mathematical Induction (inference schema). The last four hypotheses give us the substitution instances we need; the first two are the induction step and the basis.

This ALT version of nnind has a different hypothesis order. It may be easier to use with the Metamath program Proof Assistant, because "MM-PA> ASSIGN LAST" will be applied to the substitution instances first. We may eventually use this one as the official version. You may use either version. After the proof is complete, the ALT version can be changed to the non-ALT version with "MM-PA> MINIMIZE__WITH nnind / MAY_GROW". (Contributed by NM, 7-Dec-2005) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	nnindALT.6	$$⊢y\in \mathbb{N}\to \left(\chi \to \theta \right)$$
	nnindALT.5	$$⊢\psi$$
	nnindALT.1	$$⊢x=1\to \left(\phi \leftrightarrow \psi \right)$$
	nnindALT.2	$$⊢x=y\to \left(\phi \leftrightarrow \chi \right)$$
	nnindALT.3	$$⊢x=y+1\to \left(\phi \leftrightarrow \theta \right)$$
	nnindALT.4	$$⊢x=A\to \left(\phi \leftrightarrow \tau \right)$$
Assertion	nnindALT	$$⊢A\in \mathbb{N}\to \tau$$

Proof

Step	Hyp	Ref	Expression
1		nnindALT.6	$$⊢y\in \mathbb{N}\to \left(\chi \to \theta \right)$$
2		nnindALT.5	$$⊢\psi$$
3		nnindALT.1	$$⊢x=1\to \left(\phi \leftrightarrow \psi \right)$$
4		nnindALT.2	$$⊢x=y\to \left(\phi \leftrightarrow \chi \right)$$
5		nnindALT.3	$$⊢x=y+1\to \left(\phi \leftrightarrow \theta \right)$$
6		nnindALT.4	$$⊢x=A\to \left(\phi \leftrightarrow \tau \right)$$
7	3 4 5 6 2 1	nnind	$$⊢A\in \mathbb{N}\to \tau$$