# Metamath Proof Explorer

## Theorem climcj

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 ) )`

### Proof

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 ) )`