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	⊢ ( 𝑦 ∈ ℕ0 → ( 𝜒 → 𝜃 ) )
	nn0indALT.5	⊢ 𝜓
	nn0indALT.1	⊢ ( 𝑥 = 0 → ( 𝜑 ↔ 𝜓 ) )
	nn0indALT.2	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
	nn0indALT.3	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜑 ↔ 𝜃 ) )
	nn0indALT.4	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
Assertion	nn0indALT	⊢ ( 𝐴 ∈ ℕ0 → 𝜏 )

Proof

Step	Hyp	Ref	Expression
1		nn0indALT.6	⊢ ( 𝑦 ∈ ℕ0 → ( 𝜒 → 𝜃 ) )
2		nn0indALT.5	⊢ 𝜓
3		nn0indALT.1	⊢ ( 𝑥 = 0 → ( 𝜑 ↔ 𝜓 ) )
4		nn0indALT.2	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
5		nn0indALT.3	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜑 ↔ 𝜃 ) )
6		nn0indALT.4	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
7	3 4 5 6 2 1	nn0ind	⊢ ( 𝐴 ∈ ℕ0 → 𝜏 )