Theorem fznuz

Description: Disjointness of the upper integers and a finite sequence. (Contributed by Mario Carneiro, 30-Jun-2013) (Revised by Mario Carneiro, 24-Aug-2013)

	Ref	Expression
Assertion	fznuz	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ¬ 𝐾 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elfzle2	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝐾 ≤ 𝑁 )
2		elfzel2	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ℤ )
3		eluzp1l	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑁 < 𝐾 )
4	3	ex	⊢ ( 𝑁 ∈ ℤ → ( 𝐾 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) → 𝑁 < 𝐾 ) )
5	2 4	syl	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) → 𝑁 < 𝐾 ) )
6		elfzelz	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝐾 ∈ ℤ )
7		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
8		zre	⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
9		ltnle	⊢ ( ( 𝑁 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( 𝑁 < 𝐾 ↔ ¬ 𝐾 ≤ 𝑁 ) )
10	7 8 9	syl2an	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑁 < 𝐾 ↔ ¬ 𝐾 ≤ 𝑁 ) )
11	2 6 10	syl2anc	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝑁 < 𝐾 ↔ ¬ 𝐾 ≤ 𝑁 ) )
12	5 11	sylibd	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) → ¬ 𝐾 ≤ 𝑁 ) )
13	1 12	mt2d	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ¬ 𝐾 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) )