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