Description: A sequence of extended reals that converges to a real w.r.t. the standard topology on the extended reals, also converges w.r.t. to the standard topology on the complex numbers. (Contributed by Glauco Siliprandi, 23-Apr-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | xlimclimdm.1 | |- ( ph -> M e. ZZ ) |
|
| xlimclimdm.2 | |- Z = ( ZZ>= ` M ) |
||
| xlimclimdm.3 | |- ( ph -> F : Z --> RR* ) |
||
| xlimclimdm.4 | |- ( ph -> F ~~>* A ) |
||
| xlimclimdm.5 | |- ( ph -> A e. RR ) |
||
| Assertion | xlimclimdm | |- ( ph -> F e. dom ~~> ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | xlimclimdm.1 | |- ( ph -> M e. ZZ ) |
|
| 2 | xlimclimdm.2 | |- Z = ( ZZ>= ` M ) |
|
| 3 | xlimclimdm.3 | |- ( ph -> F : Z --> RR* ) |
|
| 4 | xlimclimdm.4 | |- ( ph -> F ~~>* A ) |
|
| 5 | xlimclimdm.5 | |- ( ph -> A e. RR ) |
|
| 6 | climrel | |- Rel ~~> |
|
| 7 | 1 2 3 5 | xlimclim2 | |- ( ph -> ( F ~~>* A <-> F ~~> A ) ) |
| 8 | 4 7 | mpbid | |- ( ph -> F ~~> A ) |
| 9 | releldm | |- ( ( Rel ~~> /\ F ~~> A ) -> F e. dom ~~> ) |
|
| 10 | 6 8 9 | sylancr | |- ( ph -> F e. dom ~~> ) |