This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: An upper set of integers is a subset of the complex numbers.
(Contributed by Glauco Siliprandi, 5-Feb-2022)
|
|
Ref |
Expression |
|
Hypothesis |
uzsscn2.1 |
|- Z = ( ZZ>= ` M ) |
|
Assertion |
uzsscn2 |
|- Z C_ CC |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
uzsscn2.1 |
|- Z = ( ZZ>= ` M ) |
| 2 |
|
uzsscn |
|- ( ZZ>= ` M ) C_ CC |
| 3 |
1 2
|
eqsstri |
|- Z C_ CC |