Description: Limit of the complex conjugate of a sequence. Proposition 12-2.4(c) of Gleason p. 172. (Contributed by NM, 7-Jun-2006) (Revised by Mario Carneiro, 9-Feb-2014)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | climcn1lem.1 | |- Z = ( ZZ>= ` M ) |
|
| climcn1lem.2 | |- ( ph -> F ~~> A ) |
||
| climcn1lem.4 | |- ( ph -> G e. W ) |
||
| climcn1lem.5 | |- ( ph -> M e. ZZ ) |
||
| climcn1lem.6 | |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC ) |
||
| climcj.7 | |- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( * ` ( F ` k ) ) ) |
||
| Assertion | climcj | |- ( ph -> G ~~> ( * ` A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | climcn1lem.1 | |- Z = ( ZZ>= ` M ) |
|
| 2 | climcn1lem.2 | |- ( ph -> F ~~> A ) |
|
| 3 | climcn1lem.4 | |- ( ph -> G e. W ) |
|
| 4 | climcn1lem.5 | |- ( ph -> M e. ZZ ) |
|
| 5 | climcn1lem.6 | |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC ) |
|
| 6 | climcj.7 | |- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( * ` ( F ` k ) ) ) |
|
| 7 | cjf | |- * : CC --> CC |
|
| 8 | cjcn2 | |- ( ( A e. CC /\ x e. RR+ ) -> E. y e. RR+ A. z e. CC ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( * ` z ) - ( * ` A ) ) ) < x ) ) |
|
| 9 | 1 2 3 4 5 7 8 6 | climcn1lem | |- ( ph -> G ~~> ( * ` A ) ) |