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