# Metamath Proof Explorer

## Theorem climre

Description: Limit of the real part 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 ℂ$
climre.7 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {G}\left({k}\right)=\Re \left({F}\left({k}\right)\right)$
Assertion climre ${⊢}{\phi }\to {G}⇝\Re \left({A}\right)$

### 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 climre.7 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {G}\left({k}\right)=\Re \left({F}\left({k}\right)\right)$
7 ref ${⊢}\Re :ℂ⟶ℝ$
8 ax-resscn ${⊢}ℝ\subseteq ℂ$
9 fss ${⊢}\left(\Re :ℂ⟶ℝ\wedge ℝ\subseteq ℂ\right)\to \Re :ℂ⟶ℂ$
10 7 8 9 mp2an ${⊢}\Re :ℂ⟶ℂ$
11 recn2 ${⊢}\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|\Re \left({z}\right)-\Re \left({A}\right)\right|<{x}\right)$
12 1 2 3 4 5 10 11 6 climcn1lem ${⊢}{\phi }\to {G}⇝\Re \left({A}\right)$