Description: An upper set of integers is a subset of the reals. (Contributed by Glauco Siliprandi, 23-Oct-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | uzssre | |- ( ZZ>= ` M ) C_ RR |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uzssz | |- ( ZZ>= ` M ) C_ ZZ |
|
2 | zssre | |- ZZ C_ RR |
|
3 | 1 2 | sstri | |- ( ZZ>= ` M ) C_ RR |