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

Metamath Proof Explorer

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 ⊢ x = M → ψ ↔ χ
fzindd.2 ⊢ x = y → ψ ↔ θ
fzindd.3 ⊢ x = y + 1 → ψ ↔ τ
fzindd.4 ⊢ x = A → ψ ↔ η
fzindd.5 ⊢ φ → χ
fzindd.6 ⊢ φ ∧ y ∈ ℤ ∧ M ≤ y ∧ y < N ∧ θ → τ
fzindd.7 ⊢ φ → M ∈ ℤ
fzindd.8 ⊢ φ → N ∈ ℤ
fzindd.9 ⊢ φ → M ≤ N
Assertion fzindd ⊢ φ ∧ A ∈ ℤ ∧ M ≤ A ∧ A ≤ N → η

Proof

Step Hyp Ref Expression
1 fzindd.1 ⊢ x = M → ψ ↔ χ
2 fzindd.2 ⊢ x = y → ψ ↔ θ
3 fzindd.3 ⊢ x = y + 1 → ψ ↔ τ
4 fzindd.4 ⊢ x = A → ψ ↔ η
5 fzindd.5 ⊢ φ → χ
6 fzindd.6 ⊢ φ ∧ y ∈ ℤ ∧ M ≤ y ∧ y < N ∧ θ → τ
7 fzindd.7 ⊢ φ → M ∈ ℤ
8 fzindd.8 ⊢ φ → N ∈ ℤ
9 fzindd.9 ⊢ φ → M ≤ N
10 7 8 jca ⊢ φ → M ∈ ℤ ∧ N ∈ ℤ
11 1 imbi2d ⊢ x = M → φ → ψ ↔ φ → χ
12 2 imbi2d ⊢ x = y → φ → ψ ↔ φ → θ
13 3 imbi2d ⊢ x = y + 1 → φ → ψ ↔ φ → τ
14 4 imbi2d ⊢ x = A → φ → ψ ↔ φ → η
15 5 a1i ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M ≤ N → φ → χ
16 6 3expa ⊢ φ ∧ y ∈ ℤ ∧ M ≤ y ∧ y < N ∧ θ → τ
17 16 ex ⊢ φ ∧ y ∈ ℤ ∧ M ≤ y ∧ y < N → θ → τ
18 17 expcom ⊢ y ∈ ℤ ∧ M ≤ y ∧ y < N → φ → θ → τ
19 18 a2d ⊢ y ∈ ℤ ∧ M ≤ y ∧ y < N → φ → θ → φ → τ
20 19 adantl ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ y ∈ ℤ ∧ M ≤ y ∧ y < N → φ → θ → φ → τ
21 11 12 13 14 15 20 fzind ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ A ∈ ℤ ∧ M ≤ A ∧ A ≤ N → φ → η
22 10 21 sylan ⊢ φ ∧ A ∈ ℤ ∧ M ≤ A ∧ A ≤ N → φ → η
23 22 imp ⊢ φ ∧ A ∈ ℤ ∧ M ≤ A ∧ A ≤ N ∧ φ → η
24 23 anabss1 ⊢ φ ∧ A ∈ ℤ ∧ M ≤ A ∧ A ≤ N → η