Metamath Proof Explorer

Theorem uzdisj

Description: The first N elements of an upper integer set are distinct from any later members. (Contributed by Mario Carneiro, 24-Apr-2014)

Ref Expression
Assertion uzdisj ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∩ ( ℤ≥ ‘ 𝑁 ) ) = ∅

Proof

Step Hyp Ref Expression
1 elinel2 ⊢ ( 𝑘 ∈ ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∩ ( ℤ≥ ‘ 𝑁 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) )
2 eluzle ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑁 ≤ 𝑘 )
3 1 2 syl ⊢ ( 𝑘 ∈ ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∩ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ≤ 𝑘 )
4 eluzel2 ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑁 ∈ ℤ )
5 1 4 syl ⊢ ( 𝑘 ∈ ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∩ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ∈ ℤ )
6 eluzelz ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑘 ∈ ℤ )
7 1 6 syl ⊢ ( 𝑘 ∈ ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∩ ( ℤ≥ ‘ 𝑁 ) ) → 𝑘 ∈ ℤ )
8 zlem1lt ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑁 ≤ 𝑘 ↔ ( 𝑁 − 1 ) < 𝑘 ) )
9 5 7 8 syl2anc ⊢ ( 𝑘 ∈ ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∩ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑁 ≤ 𝑘 ↔ ( 𝑁 − 1 ) < 𝑘 ) )
10 3 9 mpbid ⊢ ( 𝑘 ∈ ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∩ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑁 − 1 ) < 𝑘 )
11 7 zred ⊢ ( 𝑘 ∈ ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∩ ( ℤ≥ ‘ 𝑁 ) ) → 𝑘 ∈ ℝ )
12 peano2zm ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
13 5 12 syl ⊢ ( 𝑘 ∈ ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∩ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑁 − 1 ) ∈ ℤ )
14 13 zred ⊢ ( 𝑘 ∈ ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∩ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑁 − 1 ) ∈ ℝ )
15 elinel1 ⊢ ( 𝑘 ∈ ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∩ ( ℤ≥ ‘ 𝑁 ) ) → 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) )
16 elfzle2 ⊢ ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) → 𝑘 ≤ ( 𝑁 − 1 ) )
17 15 16 syl ⊢ ( 𝑘 ∈ ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∩ ( ℤ≥ ‘ 𝑁 ) ) → 𝑘 ≤ ( 𝑁 − 1 ) )
18 11 14 17 lensymd ⊢ ( 𝑘 ∈ ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∩ ( ℤ≥ ‘ 𝑁 ) ) → ¬ ( 𝑁 − 1 ) < 𝑘 )
19 10 18 pm2.21dd ⊢ ( 𝑘 ∈ ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∩ ( ℤ≥ ‘ 𝑁 ) ) → 𝑘 ∈ ∅ )
20 19 ssriv ⊢ ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∩ ( ℤ≥ ‘ 𝑁 ) ) ⊆ ∅
21 ss0 ⊢ ( ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∩ ( ℤ≥ ‘ 𝑁 ) ) ⊆ ∅ → ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∩ ( ℤ≥ ‘ 𝑁 ) ) = ∅ )
22 20 21 ax-mp ⊢ ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∩ ( ℤ≥ ‘ 𝑁 ) ) = ∅