Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nn0ind Structured version   Visualization version   GIF version

Theorem nn0ind 11664
 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.)
Hypotheses
Ref Expression
nn0ind.1 (𝑥 = 0 → (𝜑𝜓))
nn0ind.2 (𝑥 = 𝑦 → (𝜑𝜒))
nn0ind.3 (𝑥 = (𝑦 + 1) → (𝜑𝜃))
nn0ind.4 (𝑥 = 𝐴 → (𝜑𝜏))
nn0ind.5 𝜓
nn0ind.6 (𝑦 ∈ ℕ0 → (𝜒𝜃))
Assertion
Ref Expression
nn0ind (𝐴 ∈ ℕ0𝜏)
Distinct variable groups:   𝑥,𝑦   𝑥,𝐴   𝜓,𝑥   𝜒,𝑥   𝜃,𝑥   𝜏,𝑥   𝜑,𝑦
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)   𝜒(𝑦)   𝜃(𝑦)   𝜏(𝑦)   𝐴(𝑦)

Proof of Theorem nn0ind
StepHypRef Expression
1 elnn0z 11582 . 2 (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴))
2 0z 11580 . . 3 0 ∈ ℤ
3 nn0ind.1 . . . 4 (𝑥 = 0 → (𝜑𝜓))
4 nn0ind.2 . . . 4 (𝑥 = 𝑦 → (𝜑𝜒))
5 nn0ind.3 . . . 4 (𝑥 = (𝑦 + 1) → (𝜑𝜃))
6 nn0ind.4 . . . 4 (𝑥 = 𝐴 → (𝜑𝜏))
7 nn0ind.5 . . . . 5 𝜓
87a1i 11 . . . 4 (0 ∈ ℤ → 𝜓)
9 elnn0z 11582 . . . . . 6 (𝑦 ∈ ℕ0 ↔ (𝑦 ∈ ℤ ∧ 0 ≤ 𝑦))
10 nn0ind.6 . . . . . 6 (𝑦 ∈ ℕ0 → (𝜒𝜃))
119, 10sylbir 225 . . . . 5 ((𝑦 ∈ ℤ ∧ 0 ≤ 𝑦) → (𝜒𝜃))
12113adant1 1125 . . . 4 ((0 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 0 ≤ 𝑦) → (𝜒𝜃))
133, 4, 5, 6, 8, 12uzind 11661 . . 3 ((0 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 0 ≤ 𝐴) → 𝜏)
142, 13mp3an1 1560 . 2 ((𝐴 ∈ ℤ ∧ 0 ≤ 𝐴) → 𝜏)
151, 14sylbi 207 1 (𝐴 ∈ ℕ0𝜏)