fzind2

Description: Induction on the integers from M to N inclusive. The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. Version of fzind using integer range definitions. (Contributed by Mario Carneiro, 6-Feb-2016)

	Ref	Expression
Hypotheses	fzind2.1	$⊢ x = M \to (φ \leftrightarrow ψ)$
	fzind2.2	$⊢ x = y \to (φ \leftrightarrow χ)$
	fzind2.3	$⊢ x = y + 1 \to (φ \leftrightarrow θ)$
	fzind2.4	$⊢ x = K \to (φ \leftrightarrow τ)$
	fzind2.5	$⊢ N \in ℤ_{\geq M} \to ψ$
	fzind2.6	$⊢ y \in (M ..^N) \to (χ \to θ)$
Assertion	fzind2	$⊢ K \in (M \dots N) \to τ$

Proof

Step	Hyp	Ref	Expression
1		fzind2.1	$⊢ x = M \to (φ \leftrightarrow ψ)$
2		fzind2.2	$⊢ x = y \to (φ \leftrightarrow χ)$
3		fzind2.3	$⊢ x = y + 1 \to (φ \leftrightarrow θ)$
4		fzind2.4	$⊢ x = K \to (φ \leftrightarrow τ)$
5		fzind2.5	$⊢ N \in ℤ_{\geq M} \to ψ$
6		fzind2.6	$⊢ y \in (M ..^N) \to (χ \to θ)$
7		elfz2	$⊢ K \in (M \dots N) \leftrightarrow ((M \in ℤ \land N \in ℤ \land K \in ℤ) \land (M \leq K \land K \leq N))$
8		anass	$⊢ (((M \in ℤ \land N \in ℤ) \land K \in ℤ) \land (M \leq K \land K \leq N)) \leftrightarrow ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land (M \leq K \land K \leq N)))$
9		df-3an	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \leftrightarrow ((M \in ℤ \land N \in ℤ) \land K \in ℤ)$
10	9	anbi1i	$⊢ ((M \in ℤ \land N \in ℤ \land K \in ℤ) \land (M \leq K \land K \leq N)) \leftrightarrow (((M \in ℤ \land N \in ℤ) \land K \in ℤ) \land (M \leq K \land K \leq N))$
11		3anass	$⊢ (K \in ℤ \land M \leq K \land K \leq N) \leftrightarrow (K \in ℤ \land (M \leq K \land K \leq N))$
12	11	anbi2i	$⊢ ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land M \leq K \land K \leq N)) \leftrightarrow ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land (M \leq K \land K \leq N)))$
13	8 10 12	3bitr4i	$⊢ ((M \in ℤ \land N \in ℤ \land K \in ℤ) \land (M \leq K \land K \leq N)) \leftrightarrow ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land M \leq K \land K \leq N))$
14	7 13	bitri	$⊢ K \in (M \dots N) \leftrightarrow ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land M \leq K \land K \leq N))$
15		eluz2	$⊢ N \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land N \in ℤ \land M \leq N)$
16	15 5	sylbir	$⊢ (M \in ℤ \land N \in ℤ \land M \leq N) \to ψ$
17		3anass	$⊢ (y \in ℤ \land M \leq y \land y < N) \leftrightarrow (y \in ℤ \land (M \leq y \land y < N))$
18		elfzo	$⊢ (y \in ℤ \land M \in ℤ \land N \in ℤ) \to (y \in (M ..^N) \leftrightarrow (M \leq y \land y < N))$
19	18 6	syl6bir	$⊢ (y \in ℤ \land M \in ℤ \land N \in ℤ) \to ((M \leq y \land y < N) \to (χ \to θ))$
20	19	3coml	$⊢ (M \in ℤ \land N \in ℤ \land y \in ℤ) \to ((M \leq y \land y < N) \to (χ \to θ))$
21	20	3expa	$⊢ ((M \in ℤ \land N \in ℤ) \land y \in ℤ) \to ((M \leq y \land y < N) \to (χ \to θ))$
22	21	impr	$⊢ ((M \in ℤ \land N \in ℤ) \land (y \in ℤ \land (M \leq y \land y < N))) \to (χ \to θ)$
23	17 22	sylan2b	$⊢ ((M \in ℤ \land N \in ℤ) \land (y \in ℤ \land M \leq y \land y < N)) \to (χ \to θ)$
24	1 2 3 4 16 23	fzind	$⊢ ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land M \leq K \land K \leq N)) \to τ$
25	14 24	sylbi	$⊢ K \in (M \dots N) \to τ$

Metamath Proof Explorer

Theorem fzind2

Proof