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	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) → 𝜂 )