Metamath Proof Explorer


Theorem rlimre

Description: Limit of the real part of a sequence. Proposition 12-2.4(c) of Gleason p. 172. (Contributed by Mario Carneiro, 10-May-2016)

Ref Expression
Hypotheses rlimabs.1
|- ( ( ph /\ k e. A ) -> B e. V )
rlimabs.2
|- ( ph -> ( k e. A |-> B ) ~~>r C )
Assertion rlimre
|- ( ph -> ( k e. A |-> ( Re ` B ) ) ~~>r ( Re ` C ) )

Proof

Step Hyp Ref Expression
1 rlimabs.1
 |-  ( ( ph /\ k e. A ) -> B e. V )
2 rlimabs.2
 |-  ( ph -> ( k e. A |-> B ) ~~>r C )
3 1 2 rlimmptrcl
 |-  ( ( ph /\ k e. A ) -> B e. CC )
4 rlimcl
 |-  ( ( k e. A |-> B ) ~~>r C -> C e. CC )
5 2 4 syl
 |-  ( ph -> C e. CC )
6 ref
 |-  Re : CC --> RR
7 ax-resscn
 |-  RR C_ CC
8 fss
 |-  ( ( Re : CC --> RR /\ RR C_ CC ) -> Re : CC --> CC )
9 6 7 8 mp2an
 |-  Re : CC --> CC
10 9 a1i
 |-  ( ph -> Re : CC --> CC )
11 recn2
 |-  ( ( C e. CC /\ x e. RR+ ) -> E. y e. RR+ A. z e. CC ( ( abs ` ( z - C ) ) < y -> ( abs ` ( ( Re ` z ) - ( Re ` C ) ) ) < x ) )
12 5 11 sylan
 |-  ( ( ph /\ x e. RR+ ) -> E. y e. RR+ A. z e. CC ( ( abs ` ( z - C ) ) < y -> ( abs ` ( ( Re ` z ) - ( Re ` C ) ) ) < x ) )
13 3 5 2 10 12 rlimcn1b
 |-  ( ph -> ( k e. A |-> ( Re ` B ) ) ~~>r ( Re ` C ) )