This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rlimcj

Description: Limit of the complex conjugate 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 rlimcj 
|- ( ph -> ( k e. A |-> ( * ` B ) ) ~~>r ( * ` 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 cjf 
 |-  * : CC --> CC
7 6 a1i 
 |-  ( ph -> * : CC --> CC )
8 cjcn2 
 |-  ( ( C e. CC /\ x e. RR+ ) -> E. y e. RR+ A. z e. CC ( ( abs ` ( z - C ) ) < y -> ( abs ` ( ( * ` z ) - ( * ` C ) ) ) < x ) )
9 5 8 sylan 
 |-  ( ( ph /\ x e. RR+ ) -> E. y e. RR+ A. z e. CC ( ( abs ` ( z - C ) ) < y -> ( abs ` ( ( * ` z ) - ( * ` C ) ) ) < x ) )
10 3 5 2 7 9 rlimcn1b 
 |-  ( ph -> ( k e. A |-> ( * ` B ) ) ~~>r ( * ` C ) )