Description: The upper integers function needs to be applied to an integer, in order to return a nonempty set. (Contributed by Glauco Siliprandi, 2-Jan-2022)
Ref | Expression | ||
---|---|---|---|
Assertion | uzn0bi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uz0 | |
|
2 | 1 | adantl | |
3 | neneq | |
|
4 | 3 | adantr | |
5 | 2 4 | condan | |
6 | id | |
|
7 | eqid | |
|
8 | 6 7 | uzn0d | |
9 | 5 8 | impbii | |