This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ x = 0 → φ ↔ ψ
nn0ind.2 ⊢ x = y → φ ↔ χ
nn0ind.3 ⊢ x = y + 1 → φ ↔ θ
nn0ind.4 ⊢ x = A → φ ↔ τ
nn0ind.5 ⊢ ψ
nn0ind.6 ⊢ y ∈ ℕ 0 → χ → θ
Assertion nn0ind ⊢ A ∈ ℕ 0 → τ

Proof

Step Hyp Ref Expression
1 nn0ind.1 ⊢ x = 0 → φ ↔ ψ
2 nn0ind.2 ⊢ x = y → φ ↔ χ
3 nn0ind.3 ⊢ x = y + 1 → φ ↔ θ
4 nn0ind.4 ⊢ x = A → φ ↔ τ
5 nn0ind.5 ⊢ ψ
6 nn0ind.6 ⊢ y ∈ ℕ 0 → χ → θ
7 elnn0z ⊢ A ∈ ℕ 0 ↔ A ∈ ℤ ∧ 0 ≤ A
8 0z ⊢ 0 ∈ ℤ
9 5 a1i ⊢ 0 ∈ ℤ → ψ
10 elnn0z ⊢ y ∈ ℕ 0 ↔ y ∈ ℤ ∧ 0 ≤ y
11 10 6 sylbir ⊢ y ∈ ℤ ∧ 0 ≤ y → χ → θ
12 11 3adant1 ⊢ 0 ∈ ℤ ∧ y ∈ ℤ ∧ 0 ≤ y → χ → θ
13 1 2 3 4 9 12 uzind ⊢ 0 ∈ ℤ ∧ A ∈ ℤ ∧ 0 ≤ A → τ
14 8 13 mp3an1 ⊢ A ∈ ℤ ∧ 0 ≤ A → τ
15 7 14 sylbi ⊢ A ∈ ℕ 0 → τ