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

Metamath Proof Explorer

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 ) ) )