# 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}={ℤ}_{\ge {M}}$
climcn1lem.2 ${⊢}{\phi }\to {F}⇝{A}$
climcn1lem.4 ${⊢}{\phi }\to {G}\in {W}$
climcn1lem.5 ${⊢}{\phi }\to {M}\in ℤ$
climcn1lem.6 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right)\in ℂ$
climcj.7 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {G}\left({k}\right)=\stackrel{‾}{{F}\left({k}\right)}$
Assertion climcj ${⊢}{\phi }\to {G}⇝\stackrel{‾}{{A}}$

### Proof

Step Hyp Ref Expression
1 climcn1lem.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
2 climcn1lem.2 ${⊢}{\phi }\to {F}⇝{A}$
3 climcn1lem.4 ${⊢}{\phi }\to {G}\in {W}$
4 climcn1lem.5 ${⊢}{\phi }\to {M}\in ℤ$
5 climcn1lem.6 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right)\in ℂ$
6 climcj.7 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {G}\left({k}\right)=\stackrel{‾}{{F}\left({k}\right)}$
7 cjf ${⊢}*:ℂ⟶ℂ$
8 cjcn2 ${⊢}\left({A}\in ℂ\wedge {x}\in {ℝ}^{+}\right)\to \exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in ℂ\phantom{\rule{.4em}{0ex}}\left(\left|{z}-{A}\right|<{y}\to \left|\stackrel{‾}{{z}}-\stackrel{‾}{{A}}\right|<{x}\right)$
9 1 2 3 4 5 7 8 6 climcn1lem ${⊢}{\phi }\to {G}⇝\stackrel{‾}{{A}}$