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