Metamath Proof Explorer
Description: An upper set of integers is a subset of the Reals. (Contributed by Glauco Siliprandi, 23-Oct-2021)
|
|
Ref |
Expression |
|
Hypothesis |
uzssre2.1 |
|- Z = ( ZZ>= ` M ) |
|
Assertion |
uzssre2 |
|- Z C_ RR |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
uzssre2.1 |
|- Z = ( ZZ>= ` M ) |
2 |
|
uzssz |
|- ( ZZ>= ` M ) C_ ZZ |
3 |
|
zssre |
|- ZZ C_ RR |
4 |
2 3
|
sstri |
|- ( ZZ>= ` M ) C_ RR |
5 |
1 4
|
eqsstri |
|- Z C_ RR |