Description: An upper set of integers is a subset of the reals. (Contributed by Glauco Siliprandi, 23-Oct-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | uzssre | ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℝ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uzssz | ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ | |
2 | zssre | ⊢ ℤ ⊆ ℝ | |
3 | 1 2 | sstri | ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℝ |