Description: A half-open integer interval is a set of integers. (Contributed by Glauco Siliprandi, 8-Apr-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | fzossz | ⊢ ( 𝑀 ..^ 𝑁 ) ⊆ ℤ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fzossfz | ⊢ ( 𝑀 ..^ 𝑁 ) ⊆ ( 𝑀 ... 𝑁 ) | |
2 | fzssz | ⊢ ( 𝑀 ... 𝑁 ) ⊆ ℤ | |
3 | 1 2 | sstri | ⊢ ( 𝑀 ..^ 𝑁 ) ⊆ ℤ |