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 ⊢ ( 𝑦 ∈ ℕ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 → 𝜏 )