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

Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 nn0indALT.6 ⊢ y ∈ ℕ 0 → χ → θ
2 nn0indALT.5 ⊢ ψ
3 nn0indALT.1 ⊢ x = 0 → φ ↔ ψ
4 nn0indALT.2 ⊢ x = y → φ ↔ χ
5 nn0indALT.3 ⊢ x = y + 1 → φ ↔ θ
6 nn0indALT.4 ⊢ x = A → φ ↔ τ
7 3 4 5 6 2 1 nn0ind ⊢ A ∈ ℕ 0 → τ