Theorem fzindd

Description: Induction on the integers from M to N inclusive, a deduction version. (Contributed by metakunt, 12-May-2024)

	Ref	Expression
Hypotheses	fzindd.1	⊢ ( 𝑥 = 𝑀 → ( 𝜓 ↔ 𝜒 ) )
	fzindd.2	⊢ ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜃 ) )
	fzindd.3	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜓 ↔ 𝜏 ) )
	fzindd.4	⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜂 ) )
	fzindd.5	⊢ ( 𝜑 → 𝜒 )
	fzindd.6	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) ∧ 𝜃 ) → 𝜏 )
	fzindd.7	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	fzindd.8	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
	fzindd.9	⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
Assertion	fzindd	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ℤ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁 ) ) → 𝜂 )

Proof

Step	Hyp	Ref	Expression
1		fzindd.1	⊢ ( 𝑥 = 𝑀 → ( 𝜓 ↔ 𝜒 ) )
2		fzindd.2	⊢ ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜃 ) )
3		fzindd.3	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜓 ↔ 𝜏 ) )
4		fzindd.4	⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜂 ) )
5		fzindd.5	⊢ ( 𝜑 → 𝜒 )
6		fzindd.6	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) ∧ 𝜃 ) → 𝜏 )
7		fzindd.7	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
8		fzindd.8	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
9		fzindd.9	⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
10	7 8	jca	⊢ ( 𝜑 → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
11	1	imbi2d	⊢ ( 𝑥 = 𝑀 → ( ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → 𝜒 ) ) )
12	2	imbi2d	⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → 𝜃 ) ) )
13	3	imbi2d	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → 𝜏 ) ) )
14	4	imbi2d	⊢ ( 𝑥 = 𝐴 → ( ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → 𝜂 ) ) )
15	5	a1i	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) → ( 𝜑 → 𝜒 ) )
16	6	3expa	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) ) ∧ 𝜃 ) → 𝜏 )
17	16	ex	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) ) → ( 𝜃 → 𝜏 ) )
18	17	expcom	⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) → ( 𝜑 → ( 𝜃 → 𝜏 ) ) )
19	18	a2d	⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) → ( ( 𝜑 → 𝜃 ) → ( 𝜑 → 𝜏 ) ) )
20	19	adantl	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) ) → ( ( 𝜑 → 𝜃 ) → ( 𝜑 → 𝜏 ) ) )
21	11 12 13 14 15 20	fzind	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ∈ ℤ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁 ) ) → ( 𝜑 → 𝜂 ) )
22	10 21	sylan	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ℤ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁 ) ) → ( 𝜑 → 𝜂 ) )
23	22	imp	⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ ℤ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁 ) ) ∧ 𝜑 ) → 𝜂 )
24	23	anabss1	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ℤ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁 ) ) → 𝜂 )