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

Metamath Proof Explorer

Theorem nnuzdisj

Description: The first N elements of the set of nonnegative integers are distinct from any later members. (Contributed by Glauco Siliprandi, 21-Nov-2020)

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

Proof

Step Hyp Ref Expression
1 fz1ssfz0 ⊢ ( 1 ... 𝑁 ) ⊆ ( 0 ... 𝑁 )
2 ssrin ⊢ ( ( 1 ... 𝑁 ) ⊆ ( 0 ... 𝑁 ) → ( ( 1 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ⊆ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )
3 1 2 ax-mp ⊢ ( ( 1 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ⊆ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) )
4 nn0disj ⊢ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = ∅
5 sseq0 ⊢ ( ( ( ( 1 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ⊆ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = ∅ ) → ( ( 1 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = ∅ )
6 3 4 5 mp2an ⊢ ( ( 1 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = ∅