Description: Limit of the complex conjugate of a sequence. Proposition 122.4(c) of Gleason p. 172. (Contributed by NM, 7Jun2006) (Revised by Mario Carneiro, 9Feb2014)
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 ) ) 