Theorem rlimim

Description: Limit of the imaginary part 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	rlimim	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ⇝𝑟 ( ℑ ‘ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		rlimabs.1	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
2		rlimabs.2	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 )
3	1 2	rlimmptrcl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
4		rlimcl	⊢ ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 → 𝐶 ∈ ℂ )
5	2 4	syl	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
6		imf	⊢ ℑ : ℂ ⟶ ℝ
7		ax-resscn	⊢ ℝ ⊆ ℂ
8		fss	⊢ ( ( ℑ : ℂ ⟶ ℝ ∧ ℝ ⊆ ℂ ) → ℑ : ℂ ⟶ ℂ )
9	6 7 8	mp2an	⊢ ℑ : ℂ ⟶ ℂ
10	9	a1i	⊢ ( 𝜑 → ℑ : ℂ ⟶ ℂ )
11		imcn2	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ℂ ( ( abs ‘ ( 𝑧 − 𝐶 ) ) < 𝑦 → ( abs ‘ ( ( ℑ ‘ 𝑧 ) − ( ℑ ‘ 𝐶 ) ) ) < 𝑥 ) )
12	5 11	sylan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ℂ ( ( abs ‘ ( 𝑧 − 𝐶 ) ) < 𝑦 → ( abs ‘ ( ( ℑ ‘ 𝑧 ) − ( ℑ ‘ 𝐶 ) ) ) < 𝑥 ) )
13	3 5 2 10 12	rlimcn1b	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ⇝𝑟 ( ℑ ‘ 𝐶 ) )