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	$⊢ (φ \land k \in A) \to B \in V$
	rlimabs.2	$⊢ φ \to (k \in A ⟼ B) \underset{ℝ}{⇝} C$
Assertion	rlimcj	$⊢ φ \to (k \in A ⟼ \overline{B}) \underset{ℝ}{⇝} \overline{C}$

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

Metamath Proof Explorer