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	$$⊢\left(\phi \wedge k\in A\right)\to B\in V$$
	rlimabs.2	$$⊢\phi \to \left(k\in A⟼B\right)\underset{ℝ}{⇝}C$$
Assertion	rlimcj	$$⊢\phi \to \left(k\in A⟼\bar{B}\right)\underset{ℝ}{⇝}\bar{C}$$

Proof

Step	Hyp	Ref	Expression
1		rlimabs.1	$$⊢\left(\phi \wedge k\in A\right)\to B\in V$$
2		rlimabs.2	$$⊢\phi \to \left(k\in A⟼B\right)\underset{ℝ}{⇝}C$$
3	1 2	rlimmptrcl	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℂ$$
4		rlimcl	$$⊢\left(k\in A⟼B\right)\underset{ℝ}{⇝}C\to C\in ℂ$$
5	2 4	syl	$$⊢\phi \to C\in ℂ$$
6		cjf	$$⊢*:ℂ⟶ℂ$$
7	6	a1i	$$⊢\phi \to *:ℂ⟶ℂ$$
8		cjcn2	$$⊢\left(C\in ℂ\wedge x\in {ℝ}^{+}\right)\to \exists y\in {ℝ}^{+}\forall z\in ℂ\left(\left|z-C\right|<y\to \left|\bar{z}-\bar{C}\right|<x\right)$$
9	5 8	sylan	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to \exists y\in {ℝ}^{+}\forall z\in ℂ\left(\left|z-C\right|<y\to \left|\bar{z}-\bar{C}\right|<x\right)$$
10	3 5 2 7 9	rlimcn1b	$$⊢\phi \to \left(k\in A⟼\bar{B}\right)\underset{ℝ}{⇝}\bar{C}$$