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