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 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
rlimabs.2 ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 )
Assertion rlimcj ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ ( ∗ ‘ 𝐵 ) ) ⇝𝑟 ( ∗ ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 rlimabs.1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
2 rlimabs.2 ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 )
3 1 2 rlimmptrcl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
4 rlimcl ⊢ ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 → 𝐶 ∈ ℂ )
5 2 4 syl ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
6 cjf ⊢ ∗ : ℂ ⟶ ℂ
7 6 a1i ⊢ ( 𝜑 → ∗ : ℂ ⟶ ℂ )
8 cjcn2 ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ℂ ( ( abs ‘ ( 𝑧 − 𝐶 ) ) < 𝑦 → ( abs ‘ ( ( ∗ ‘ 𝑧 ) − ( ∗ ‘ 𝐶 ) ) ) < 𝑥 ) )
9 5 8 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ℂ ( ( abs ‘ ( 𝑧 − 𝐶 ) ) < 𝑦 → ( abs ‘ ( ( ∗ ‘ 𝑧 ) − ( ∗ ‘ 𝐶 ) ) ) < 𝑥 ) )
10 3 5 2 7 9 rlimcn1b ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ ( ∗ ‘ 𝐵 ) ) ⇝𝑟 ( ∗ ‘ 𝐶 ) )