Description: A function mapping from an upper set of integers to the extended reals is a partial map on the complex numbers. (Contributed by Glauco Siliprandi, 5-Feb-2022)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | fuzxrpmcn.1 | |- Z = ( ZZ>= ` M ) |
|
| fuzxrpmcn.2 | |- ( ph -> F : Z --> RR* ) |
||
| Assertion | fuzxrpmcn | |- ( ph -> F e. ( RR* ^pm CC ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fuzxrpmcn.1 | |- Z = ( ZZ>= ` M ) |
|
| 2 | fuzxrpmcn.2 | |- ( ph -> F : Z --> RR* ) |
|
| 3 | cnex | |- CC e. _V |
|
| 4 | 3 | a1i | |- ( ph -> CC e. _V ) |
| 5 | xrex | |- RR* e. _V |
|
| 6 | 5 | a1i | |- ( ph -> RR* e. _V ) |
| 7 | 1 | uzsscn2 | |- Z C_ CC |
| 8 | 7 | a1i | |- ( ph -> Z C_ CC ) |
| 9 | 4 6 8 2 | fpmd | |- ( ph -> F e. ( RR* ^pm CC ) ) |