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 ⊢ ( 𝑥 = 1 → ( 𝜓 ↔ 𝜒 ) )
nnindd.2 ⊢ ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜃 ) )
nnindd.3 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜓 ↔ 𝜏 ) )
nnindd.4 ⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜂 ) )
nnindd.5 ⊢ ( 𝜑 → 𝜒 )
nnindd.6 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ 𝜃 ) → 𝜏 )
Assertion nnindd ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) → 𝜂 )

Proof

Step Hyp Ref Expression
1 nnindd.1 ⊢ ( 𝑥 = 1 → ( 𝜓 ↔ 𝜒 ) )
2 nnindd.2 ⊢ ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜃 ) )
3 nnindd.3 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜓 ↔ 𝜏 ) )
4 nnindd.4 ⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜂 ) )
5 nnindd.5 ⊢ ( 𝜑 → 𝜒 )
6 nnindd.6 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ 𝜃 ) → 𝜏 )
7 1 imbi2d ⊢ ( 𝑥 = 1 → ( ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → 𝜒 ) ) )
8 2 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → 𝜃 ) ) )
9 3 imbi2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → 𝜏 ) ) )
10 4 imbi2d ⊢ ( 𝑥 = 𝐴 → ( ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → 𝜂 ) ) )
11 6 ex ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → ( 𝜃 → 𝜏 ) )
12 11 expcom ⊢ ( 𝑦 ∈ ℕ → ( 𝜑 → ( 𝜃 → 𝜏 ) ) )
13 12 a2d ⊢ ( 𝑦 ∈ ℕ → ( ( 𝜑 → 𝜃 ) → ( 𝜑 → 𝜏 ) ) )
14 7 8 9 10 5 13 nnind ⊢ ( 𝐴 ∈ ℕ → ( 𝜑 → 𝜂 ) )
15 14 impcom ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) → 𝜂 )