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 \to (ψ \leftrightarrow χ)$
	fzindd.2	$⊢ x = y \to (ψ \leftrightarrow θ)$
	fzindd.3	$⊢ x = y + 1 \to (ψ \leftrightarrow τ)$
	fzindd.4	$⊢ x = A \to (ψ \leftrightarrow η)$
	fzindd.5	$⊢ φ \to χ$
	fzindd.6	$⊢ (φ \land (y \in ℤ \land M \leq y \land y < N) \land θ) \to τ$
	fzindd.7	$⊢ φ \to M \in ℤ$
	fzindd.8	$⊢ φ \to N \in ℤ$
	fzindd.9	$⊢ φ \to M \leq N$
Assertion	fzindd	$⊢ (φ \land (A \in ℤ \land M \leq A \land A \leq N)) \to η$

Proof

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

Metamath Proof Explorer

Theorem fzindd

Proof