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

Metamath Proof Explorer

Theorem nn0disj

Description: The first N + 1 elements of the set of nonnegative integers are distinct from any later members. (Contributed by AV, 8-Nov-2019)

Ref Expression
Assertion nn0disj ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = ∅

Proof

Step Hyp Ref Expression
1 elinel2 ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) )
2 eluzle ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) → ( 𝑁 + 1 ) ≤ 𝑘 )
3 1 2 syl ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( 𝑁 + 1 ) ≤ 𝑘 )
4 eluzel2 ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) → ( 𝑁 + 1 ) ∈ ℤ )
5 1 4 syl ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( 𝑁 + 1 ) ∈ ℤ )
6 eluzelz ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) → 𝑘 ∈ ℤ )
7 1 6 syl ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑘 ∈ ℤ )
8 zlem1lt ⊢ ( ( ( 𝑁 + 1 ) ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( 𝑁 + 1 ) ≤ 𝑘 ↔ ( ( 𝑁 + 1 ) − 1 ) < 𝑘 ) )
9 5 7 8 syl2anc ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( ( 𝑁 + 1 ) ≤ 𝑘 ↔ ( ( 𝑁 + 1 ) − 1 ) < 𝑘 ) )
10 3 9 mpbid ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( ( 𝑁 + 1 ) − 1 ) < 𝑘 )
11 elinel1 ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑘 ∈ ( 0 ... 𝑁 ) )
12 elfzle2 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ≤ 𝑁 )
13 11 12 syl ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑘 ≤ 𝑁 )
14 7 zred ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑘 ∈ ℝ )
15 elin ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ↔ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )
16 elfzel2 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℤ )
17 16 adantr ⊢ ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑁 ∈ ℤ )
18 15 17 sylbi ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑁 ∈ ℤ )
19 18 zred ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑁 ∈ ℝ )
20 14 19 lenltd ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( 𝑘 ≤ 𝑁 ↔ ¬ 𝑁 < 𝑘 ) )
21 18 zcnd ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑁 ∈ ℂ )
22 pncan1 ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
23 21 22 syl ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
24 23 eqcomd ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑁 = ( ( 𝑁 + 1 ) − 1 ) )
25 24 breq1d ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( 𝑁 < 𝑘 ↔ ( ( 𝑁 + 1 ) − 1 ) < 𝑘 ) )
26 25 notbid ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( ¬ 𝑁 < 𝑘 ↔ ¬ ( ( 𝑁 + 1 ) − 1 ) < 𝑘 ) )
27 20 26 bitrd ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( 𝑘 ≤ 𝑁 ↔ ¬ ( ( 𝑁 + 1 ) − 1 ) < 𝑘 ) )
28 13 27 mpbid ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ¬ ( ( 𝑁 + 1 ) − 1 ) < 𝑘 )
29 10 28 pm2.21dd ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑘 ∈ ∅ )
30 29 ssriv ⊢ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ⊆ ∅
31 ss0 ⊢ ( ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ⊆ ∅ → ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = ∅ )
32 30 31 ax-mp ⊢ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = ∅