Theorem nn0indALT

Description: Principle of Mathematical Induction (inference schema) on nonnegative integers. The last four hypotheses give us the substitution instances we need; the first two are the basis and the induction step. Either nn0ind or nn0indALT may be used; see comment for nnind . (Contributed by NM, 28-Nov-2005) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

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