This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrdi ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ( 𝑀 ... ( 𝑁 − 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 ) ) )