Theorem 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	⊢ ( 𝑥 = 𝑀 → ( 𝜑 ↔ 𝜓 ) )
	fzind.2	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
	fzind.3	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜑 ↔ 𝜃 ) )
	fzind.4	⊢ ( 𝑥 = 𝐾 → ( 𝜑 ↔ 𝜏 ) )
	fzind.5	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) → 𝜓 )
	fzind.6	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) ) → ( 𝜒 → 𝜃 ) )
Assertion	fzind	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) → 𝜏 )

Proof

Step	Hyp	Ref	Expression
1		fzind.1	⊢ ( 𝑥 = 𝑀 → ( 𝜑 ↔ 𝜓 ) )
2		fzind.2	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
3		fzind.3	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜑 ↔ 𝜃 ) )
4		fzind.4	⊢ ( 𝑥 = 𝐾 → ( 𝜑 ↔ 𝜏 ) )
5		fzind.5	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) → 𝜓 )
6		fzind.6	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) ) → ( 𝜒 → 𝜃 ) )
7		breq1	⊢ ( 𝑥 = 𝑀 → ( 𝑥 ≤ 𝑁 ↔ 𝑀 ≤ 𝑁 ) )
8	7	anbi2d	⊢ ( 𝑥 = 𝑀 → ( ( 𝑁 ∈ ℤ ∧ 𝑥 ≤ 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) ) )
9	8 1	imbi12d	⊢ ( 𝑥 = 𝑀 → ( ( ( 𝑁 ∈ ℤ ∧ 𝑥 ≤ 𝑁 ) → 𝜑 ) ↔ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) → 𝜓 ) ) )
10		breq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≤ 𝑁 ↔ 𝑦 ≤ 𝑁 ) )
11	10	anbi2d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑁 ∈ ℤ ∧ 𝑥 ≤ 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝑦 ≤ 𝑁 ) ) )
12	11 2	imbi12d	⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑁 ∈ ℤ ∧ 𝑥 ≤ 𝑁 ) → 𝜑 ) ↔ ( ( 𝑁 ∈ ℤ ∧ 𝑦 ≤ 𝑁 ) → 𝜒 ) ) )
13		breq1	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 ≤ 𝑁 ↔ ( 𝑦 + 1 ) ≤ 𝑁 ) )
14	13	anbi2d	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑁 ∈ ℤ ∧ 𝑥 ≤ 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) ) )
15	14 3	imbi12d	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( 𝑁 ∈ ℤ ∧ 𝑥 ≤ 𝑁 ) → 𝜑 ) ↔ ( ( 𝑁 ∈ ℤ ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → 𝜃 ) ) )
16		breq1	⊢ ( 𝑥 = 𝐾 → ( 𝑥 ≤ 𝑁 ↔ 𝐾 ≤ 𝑁 ) )
17	16	anbi2d	⊢ ( 𝑥 = 𝐾 → ( ( 𝑁 ∈ ℤ ∧ 𝑥 ≤ 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝐾 ≤ 𝑁 ) ) )
18	17 4	imbi12d	⊢ ( 𝑥 = 𝐾 → ( ( ( 𝑁 ∈ ℤ ∧ 𝑥 ≤ 𝑁 ) → 𝜑 ) ↔ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ≤ 𝑁 ) → 𝜏 ) ) )
19	5	3expib	⊢ ( 𝑀 ∈ ℤ → ( ( 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) → 𝜓 ) )
20		zre	⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℝ )
21		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
22		p1le	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → 𝑦 ≤ 𝑁 )
23	22	3expia	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝑦 + 1 ) ≤ 𝑁 → 𝑦 ≤ 𝑁 ) )
24	20 21 23	syl2an	⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑦 + 1 ) ≤ 𝑁 → 𝑦 ≤ 𝑁 ) )
25	24	imdistanda	⊢ ( 𝑦 ∈ ℤ → ( ( 𝑁 ∈ ℤ ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → ( 𝑁 ∈ ℤ ∧ 𝑦 ≤ 𝑁 ) ) )
26	25	imim1d	⊢ ( 𝑦 ∈ ℤ → ( ( ( 𝑁 ∈ ℤ ∧ 𝑦 ≤ 𝑁 ) → 𝜒 ) → ( ( 𝑁 ∈ ℤ ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → 𝜒 ) ) )
27	26	3ad2ant2	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ) → ( ( ( 𝑁 ∈ ℤ ∧ 𝑦 ≤ 𝑁 ) → 𝜒 ) → ( ( 𝑁 ∈ ℤ ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → 𝜒 ) ) )
28		zltp1le	⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑦 < 𝑁 ↔ ( 𝑦 + 1 ) ≤ 𝑁 ) )
29	28	adantlr	⊢ ( ( ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ) ∧ 𝑁 ∈ ℤ ) → ( 𝑦 < 𝑁 ↔ ( 𝑦 + 1 ) ≤ 𝑁 ) )
30	29	expcom	⊢ ( 𝑁 ∈ ℤ → ( ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ) → ( 𝑦 < 𝑁 ↔ ( 𝑦 + 1 ) ≤ 𝑁 ) ) )
31	30	pm5.32d	⊢ ( 𝑁 ∈ ℤ → ( ( ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ) ∧ 𝑦 < 𝑁 ) ↔ ( ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ) ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) ) )
32	31	adantl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ) ∧ 𝑦 < 𝑁 ) ↔ ( ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ) ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) ) )
33	6	expcom	⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝜒 → 𝜃 ) ) )
34	33	3expa	⊢ ( ( ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ) ∧ 𝑦 < 𝑁 ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝜒 → 𝜃 ) ) )
35	34	com12	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ) ∧ 𝑦 < 𝑁 ) → ( 𝜒 → 𝜃 ) ) )
36	32 35	sylbird	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ) ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → ( 𝜒 → 𝜃 ) ) )
37	36	ex	⊢ ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ℤ → ( ( ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ) ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → ( 𝜒 → 𝜃 ) ) ) )
38	37	com23	⊢ ( 𝑀 ∈ ℤ → ( ( ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ) ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → ( 𝑁 ∈ ℤ → ( 𝜒 → 𝜃 ) ) ) )
39	38	expd	⊢ ( 𝑀 ∈ ℤ → ( ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ) → ( ( 𝑦 + 1 ) ≤ 𝑁 → ( 𝑁 ∈ ℤ → ( 𝜒 → 𝜃 ) ) ) ) )
40	39	3impib	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ) → ( ( 𝑦 + 1 ) ≤ 𝑁 → ( 𝑁 ∈ ℤ → ( 𝜒 → 𝜃 ) ) ) )
41	40	impcomd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ) → ( ( 𝑁 ∈ ℤ ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → ( 𝜒 → 𝜃 ) ) )
42	41	a2d	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ) → ( ( ( 𝑁 ∈ ℤ ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → 𝜒 ) → ( ( 𝑁 ∈ ℤ ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → 𝜃 ) ) )
43	27 42	syld	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ) → ( ( ( 𝑁 ∈ ℤ ∧ 𝑦 ≤ 𝑁 ) → 𝜒 ) → ( ( 𝑁 ∈ ℤ ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → 𝜃 ) ) )
44	9 12 15 18 19 43	uzind	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ) → ( ( 𝑁 ∈ ℤ ∧ 𝐾 ≤ 𝑁 ) → 𝜏 ) )
45	44	expcomd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ) → ( 𝐾 ≤ 𝑁 → ( 𝑁 ∈ ℤ → 𝜏 ) ) )
46	45	3expb	⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ) ) → ( 𝐾 ≤ 𝑁 → ( 𝑁 ∈ ℤ → 𝜏 ) ) )
47	46	expcom	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ) → ( 𝑀 ∈ ℤ → ( 𝐾 ≤ 𝑁 → ( 𝑁 ∈ ℤ → 𝜏 ) ) ) )
48	47	com23	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ) → ( 𝐾 ≤ 𝑁 → ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ℤ → 𝜏 ) ) ) )
49	48	3impia	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) → ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ℤ → 𝜏 ) ) )
50	49	impd	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝜏 ) )
51	50	impcom	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) → 𝜏 )