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

Metamath Proof Explorer

Theorem nnindd

Description: Principle of Mathematical Induction (inference schema) on integers, a deduction version. (Contributed by Thierry Arnoux, 19-Jul-2020)

Ref Expression
Hypotheses nnindd.1 ⊢ x = 1 → ψ ↔ χ
nnindd.2 ⊢ x = y → ψ ↔ θ
nnindd.3 ⊢ x = y + 1 → ψ ↔ τ
nnindd.4 ⊢ x = A → ψ ↔ η
nnindd.5 ⊢ φ → χ
nnindd.6 ⊢ φ ∧ y ∈ ℕ ∧ θ → τ
Assertion nnindd ⊢ φ ∧ A ∈ ℕ → η

Proof

Step Hyp Ref Expression
1 nnindd.1 ⊢ x = 1 → ψ ↔ χ
2 nnindd.2 ⊢ x = y → ψ ↔ θ
3 nnindd.3 ⊢ x = y + 1 → ψ ↔ τ
4 nnindd.4 ⊢ x = A → ψ ↔ η
5 nnindd.5 ⊢ φ → χ
6 nnindd.6 ⊢ φ ∧ y ∈ ℕ ∧ θ → τ
7 1 imbi2d ⊢ x = 1 → φ → ψ ↔ φ → χ
8 2 imbi2d ⊢ x = y → φ → ψ ↔ φ → θ
9 3 imbi2d ⊢ x = y + 1 → φ → ψ ↔ φ → τ
10 4 imbi2d ⊢ x = A → φ → ψ ↔ φ → η
11 6 ex ⊢ φ ∧ y ∈ ℕ → θ → τ
12 11 expcom ⊢ y ∈ ℕ → φ → θ → τ
13 12 a2d ⊢ y ∈ ℕ → φ → θ → φ → τ
14 7 8 9 10 5 13 nnind ⊢ A ∈ ℕ → φ → η
15 14 impcom ⊢ φ ∧ A ∈ ℕ → η