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	⊢ ( 𝑥 = 𝑀 → ( 𝜑 ↔ 𝜓 ) )
	fzind2.2	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
	fzind2.3	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜑 ↔ 𝜃 ) )
	fzind2.4	⊢ ( 𝑥 = 𝐾 → ( 𝜑 ↔ 𝜏 ) )
	fzind2.5	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 𝑀 ) → 𝜓 )
	fzind2.6	⊢ ( 𝑦 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝜒 → 𝜃 ) )
Assertion	fzind2	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝜏 )

Proof

Step	Hyp	Ref	Expression
1		fzind2.1	⊢ ( 𝑥 = 𝑀 → ( 𝜑 ↔ 𝜓 ) )
2		fzind2.2	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
3		fzind2.3	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜑 ↔ 𝜃 ) )
4		fzind2.4	⊢ ( 𝑥 = 𝐾 → ( 𝜑 ↔ 𝜏 ) )
5		fzind2.5	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 𝑀 ) → 𝜓 )
6		fzind2.6	⊢ ( 𝑦 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝜒 → 𝜃 ) )
7		elfz2	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) )
8		anass	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) ↔ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) ) )
9		df-3an	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ↔ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∈ ℤ ) )
10	9	anbi1i	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) ↔ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) )
11		3anass	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ↔ ( 𝐾 ∈ ℤ ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) )
12	11	anbi2i	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) ↔ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) ) )
13	8 10 12	3bitr4i	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) ↔ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) )
14	7 13	bitri	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) )
15		eluz2	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) )
16	15 5	sylbir	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) → 𝜓 )
17		3anass	⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) ↔ ( 𝑦 ∈ ℤ ∧ ( 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) ) )
18		elfzo	⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑦 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) ) )
19	18 6	syl6bir	⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) → ( 𝜒 → 𝜃 ) ) )
20	19	3coml	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) → ( 𝜒 → 𝜃 ) ) )
21	20	3expa	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) → ( ( 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) → ( 𝜒 → 𝜃 ) ) )
22	21	impr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ ℤ ∧ ( 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) ) ) → ( 𝜒 → 𝜃 ) )
23	17 22	sylan2b	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) ) → ( 𝜒 → 𝜃 ) )
24	1 2 3 4 16 23	fzind	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) → 𝜏 )
25	14 24	sylbi	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝜏 )

Metamath Proof Explorer

Theorem fzind2

Proof