Description: An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | climreu | |- ( F ~~> A -> E! x e. CC F ~~> x ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | climeu | |- ( F ~~> A -> E! x F ~~> x ) |
|
| 2 | climcl | |- ( F ~~> x -> x e. CC ) |
|
| 3 | 2 | pm4.71ri | |- ( F ~~> x <-> ( x e. CC /\ F ~~> x ) ) |
| 4 | 3 | eubii | |- ( E! x F ~~> x <-> E! x ( x e. CC /\ F ~~> x ) ) |
| 5 | df-reu | |- ( E! x e. CC F ~~> x <-> E! x ( x e. CC /\ F ~~> x ) ) |
|
| 6 | 4 5 | bitr4i | |- ( E! x F ~~> x <-> E! x e. CC F ~~> x ) |
| 7 | 1 6 | sylib | |- ( F ~~> A -> E! x e. CC F ~~> x ) |