fzind

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. (Contributed by Paul Chapman, 31-Mar-2011)

	Ref	Expression
Hypotheses	fzind.1	$⊢ x = M \to (φ \leftrightarrow ψ)$
	fzind.2	$⊢ x = y \to (φ \leftrightarrow χ)$
	fzind.3	$⊢ x = y + 1 \to (φ \leftrightarrow θ)$
	fzind.4	$⊢ x = K \to (φ \leftrightarrow τ)$
	fzind.5	$⊢ (M \in ℤ \land N \in ℤ \land M \leq N) \to ψ$
	fzind.6	$⊢ ((M \in ℤ \land N \in ℤ) \land (y \in ℤ \land M \leq y \land y < N)) \to (χ \to θ)$
Assertion	fzind	$⊢ ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land M \leq K \land K \leq N)) \to τ$

Proof

Step	Hyp	Ref	Expression
1		fzind.1	$⊢ x = M \to (φ \leftrightarrow ψ)$
2		fzind.2	$⊢ x = y \to (φ \leftrightarrow χ)$
3		fzind.3	$⊢ x = y + 1 \to (φ \leftrightarrow θ)$
4		fzind.4	$⊢ x = K \to (φ \leftrightarrow τ)$
5		fzind.5	$⊢ (M \in ℤ \land N \in ℤ \land M \leq N) \to ψ$
6		fzind.6	$⊢ ((M \in ℤ \land N \in ℤ) \land (y \in ℤ \land M \leq y \land y < N)) \to (χ \to θ)$
7		breq1	$⊢ x = M \to (x \leq N \leftrightarrow M \leq N)$
8	7	anbi2d	$⊢ x = M \to ((N \in ℤ \land x \leq N) \leftrightarrow (N \in ℤ \land M \leq N))$
9	8 1	imbi12d	$⊢ x = M \to (((N \in ℤ \land x \leq N) \to φ) \leftrightarrow ((N \in ℤ \land M \leq N) \to ψ))$
10		breq1	$⊢ x = y \to (x \leq N \leftrightarrow y \leq N)$
11	10	anbi2d	$⊢ x = y \to ((N \in ℤ \land x \leq N) \leftrightarrow (N \in ℤ \land y \leq N))$
12	11 2	imbi12d	$⊢ x = y \to (((N \in ℤ \land x \leq N) \to φ) \leftrightarrow ((N \in ℤ \land y \leq N) \to χ))$
13		breq1	$⊢ x = y + 1 \to (x \leq N \leftrightarrow y + 1 \leq N)$
14	13	anbi2d	$⊢ x = y + 1 \to ((N \in ℤ \land x \leq N) \leftrightarrow (N \in ℤ \land y + 1 \leq N))$
15	14 3	imbi12d	$⊢ x = y + 1 \to (((N \in ℤ \land x \leq N) \to φ) \leftrightarrow ((N \in ℤ \land y + 1 \leq N) \to θ))$
16		breq1	$⊢ x = K \to (x \leq N \leftrightarrow K \leq N)$
17	16	anbi2d	$⊢ x = K \to ((N \in ℤ \land x \leq N) \leftrightarrow (N \in ℤ \land K \leq N))$
18	17 4	imbi12d	$⊢ x = K \to (((N \in ℤ \land x \leq N) \to φ) \leftrightarrow ((N \in ℤ \land K \leq N) \to τ))$
19	5	3expib	$⊢ M \in ℤ \to ((N \in ℤ \land M \leq N) \to ψ)$
20		zre	$⊢ y \in ℤ \to y \in ℝ$
21		zre	$⊢ N \in ℤ \to N \in ℝ$
22		p1le	$⊢ (y \in ℝ \land N \in ℝ \land y + 1 \leq N) \to y \leq N$
23	22	3expia	$⊢ (y \in ℝ \land N \in ℝ) \to (y + 1 \leq N \to y \leq N)$
24	20 21 23	syl2an	$⊢ (y \in ℤ \land N \in ℤ) \to (y + 1 \leq N \to y \leq N)$
25	24	imdistanda	$⊢ y \in ℤ \to ((N \in ℤ \land y + 1 \leq N) \to (N \in ℤ \land y \leq N))$
26	25	imim1d	$⊢ y \in ℤ \to (((N \in ℤ \land y \leq N) \to χ) \to ((N \in ℤ \land y + 1 \leq N) \to χ))$
27	26	3ad2ant2	$⊢ (M \in ℤ \land y \in ℤ \land M \leq y) \to (((N \in ℤ \land y \leq N) \to χ) \to ((N \in ℤ \land y + 1 \leq N) \to χ))$
28		zltp1le	$⊢ (y \in ℤ \land N \in ℤ) \to (y < N \leftrightarrow y + 1 \leq N)$
29	28	adantlr	$⊢ ((y \in ℤ \land M \leq y) \land N \in ℤ) \to (y < N \leftrightarrow y + 1 \leq N)$
30	29	expcom	$⊢ N \in ℤ \to ((y \in ℤ \land M \leq y) \to (y < N \leftrightarrow y + 1 \leq N))$
31	30	pm5.32d	$⊢ N \in ℤ \to (((y \in ℤ \land M \leq y) \land y < N) \leftrightarrow ((y \in ℤ \land M \leq y) \land y + 1 \leq N))$
32	31	adantl	$⊢ (M \in ℤ \land N \in ℤ) \to (((y \in ℤ \land M \leq y) \land y < N) \leftrightarrow ((y \in ℤ \land M \leq y) \land y + 1 \leq N))$
33	6	expcom	$⊢ (y \in ℤ \land M \leq y \land y < N) \to ((M \in ℤ \land N \in ℤ) \to (χ \to θ))$
34	33	3expa	$⊢ ((y \in ℤ \land M \leq y) \land y < N) \to ((M \in ℤ \land N \in ℤ) \to (χ \to θ))$
35	34	com12	$⊢ (M \in ℤ \land N \in ℤ) \to (((y \in ℤ \land M \leq y) \land y < N) \to (χ \to θ))$
36	32 35	sylbird	$⊢ (M \in ℤ \land N \in ℤ) \to (((y \in ℤ \land M \leq y) \land y + 1 \leq N) \to (χ \to θ))$
37	36	ex	$⊢ M \in ℤ \to (N \in ℤ \to (((y \in ℤ \land M \leq y) \land y + 1 \leq N) \to (χ \to θ)))$
38	37	com23	$⊢ M \in ℤ \to (((y \in ℤ \land M \leq y) \land y + 1 \leq N) \to (N \in ℤ \to (χ \to θ)))$
39	38	expd	$⊢ M \in ℤ \to ((y \in ℤ \land M \leq y) \to (y + 1 \leq N \to (N \in ℤ \to (χ \to θ))))$
40	39	3impib	$⊢ (M \in ℤ \land y \in ℤ \land M \leq y) \to (y + 1 \leq N \to (N \in ℤ \to (χ \to θ)))$
41	40	impcomd	$⊢ (M \in ℤ \land y \in ℤ \land M \leq y) \to ((N \in ℤ \land y + 1 \leq N) \to (χ \to θ))$
42	41	a2d	$⊢ (M \in ℤ \land y \in ℤ \land M \leq y) \to (((N \in ℤ \land y + 1 \leq N) \to χ) \to ((N \in ℤ \land y + 1 \leq N) \to θ))$
43	27 42	syld	$⊢ (M \in ℤ \land y \in ℤ \land M \leq y) \to (((N \in ℤ \land y \leq N) \to χ) \to ((N \in ℤ \land y + 1 \leq N) \to θ))$
44	9 12 15 18 19 43	uzind	$⊢ (M \in ℤ \land K \in ℤ \land M \leq K) \to ((N \in ℤ \land K \leq N) \to τ)$
45	44	expcomd	$⊢ (M \in ℤ \land K \in ℤ \land M \leq K) \to (K \leq N \to (N \in ℤ \to τ))$
46	45	3expb	$⊢ (M \in ℤ \land (K \in ℤ \land M \leq K)) \to (K \leq N \to (N \in ℤ \to τ))$
47	46	expcom	$⊢ (K \in ℤ \land M \leq K) \to (M \in ℤ \to (K \leq N \to (N \in ℤ \to τ)))$
48	47	com23	$⊢ (K \in ℤ \land M \leq K) \to (K \leq N \to (M \in ℤ \to (N \in ℤ \to τ)))$
49	48	3impia	$⊢ (K \in ℤ \land M \leq K \land K \leq N) \to (M \in ℤ \to (N \in ℤ \to τ))$
50	49	impd	$⊢ (K \in ℤ \land M \leq K \land K \leq N) \to ((M \in ℤ \land N \in ℤ) \to τ)$
51	50	impcom	$⊢ ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land M \leq K \land K \leq N)) \to τ$

Metamath Proof Explorer

Theorem fzind

Proof