Theorem nn0ind

Description: Principle of Mathematical Induction (inference schema) on nonnegative integers. The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. (Contributed by NM, 13-May-2004)

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

Proof

Step	Hyp	Ref	Expression
1		nn0ind.1	⊢ ( 𝑥 = 0 → ( 𝜑 ↔ 𝜓 ) )
2		nn0ind.2	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
3		nn0ind.3	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜑 ↔ 𝜃 ) )
4		nn0ind.4	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
5		nn0ind.5	⊢ 𝜓
6		nn0ind.6	⊢ ( 𝑦 ∈ ℕ0 → ( 𝜒 → 𝜃 ) )
7		elnn0z	⊢ ( 𝐴 ∈ ℕ0 ↔ ( 𝐴 ∈ ℤ ∧ 0 ≤ 𝐴 ) )
8		0z	⊢ 0 ∈ ℤ
9	5	a1i	⊢ ( 0 ∈ ℤ → 𝜓 )
10		elnn0z	⊢ ( 𝑦 ∈ ℕ0 ↔ ( 𝑦 ∈ ℤ ∧ 0 ≤ 𝑦 ) )
11	10 6	sylbir	⊢ ( ( 𝑦 ∈ ℤ ∧ 0 ≤ 𝑦 ) → ( 𝜒 → 𝜃 ) )
12	11	3adant1	⊢ ( ( 0 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 0 ≤ 𝑦 ) → ( 𝜒 → 𝜃 ) )
13	1 2 3 4 9 12	uzind	⊢ ( ( 0 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 0 ≤ 𝐴 ) → 𝜏 )
14	8 13	mp3an1	⊢ ( ( 𝐴 ∈ ℤ ∧ 0 ≤ 𝐴 ) → 𝜏 )
15	7 14	sylbi	⊢ ( 𝐴 ∈ ℕ0 → 𝜏 )