Theorem uznfz

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

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

Proof

Step	Hyp	Ref	Expression
1		eluzle	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑁 ≤ 𝐾 )
2		eluzel2	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑁 ∈ ℤ )
3		elfzel1	⊢ ( 𝐾 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) → 𝑀 ∈ ℤ )
4		elfzm11	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ↔ ( 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁 ) ) )
5		simp3	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁 ) → 𝐾 < 𝑁 )
6	4 5	syl6bi	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) → 𝐾 < 𝑁 ) )
7	6	impancom	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝑁 ∈ ℤ → 𝐾 < 𝑁 ) )
8	3 7	mpancom	⊢ ( 𝐾 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) → ( 𝑁 ∈ ℤ → 𝐾 < 𝑁 ) )
9	2 8	syl5com	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝐾 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) → 𝐾 < 𝑁 ) )
10		eluzelz	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝐾 ∈ ℤ )
11		zre	⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
12		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
13		ltnle	⊢ ( ( 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝐾 < 𝑁 ↔ ¬ 𝑁 ≤ 𝐾 ) )
14	11 12 13	syl2an	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 < 𝑁 ↔ ¬ 𝑁 ≤ 𝐾 ) )
15	10 2 14	syl2anc	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝐾 < 𝑁 ↔ ¬ 𝑁 ≤ 𝐾 ) )
16	9 15	sylibd	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝐾 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) → ¬ 𝑁 ≤ 𝐾 ) )
17	1 16	mt2d	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) → ¬ 𝐾 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) )