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

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		imf	$$⊢\Im :ℂ⟶ℝ$$
7		ax-resscn	$$⊢ℝ\subseteq ℂ$$
8		fss	$$⊢\left(\Im :ℂ⟶ℝ\wedge ℝ\subseteq ℂ\right)\to \Im :ℂ⟶ℂ$$
9	6 7 8	mp2an	$$⊢\Im :ℂ⟶ℂ$$
10	9	a1i	$$⊢\phi \to \Im :ℂ⟶ℂ$$
11		imcn2	$$⊢\left(C\in ℂ\wedge x\in {ℝ}^{+}\right)\to \exists y\in {ℝ}^{+}\forall z\in ℂ\left(\left|z-C\right|<y\to \left|\Im \left(z\right)-\Im \left(C\right)\right|<x\right)$$
12	5 11	sylan	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to \exists y\in {ℝ}^{+}\forall z\in ℂ\left(\left|z-C\right|<y\to \left|\Im \left(z\right)-\Im \left(C\right)\right|<x\right)$$
13	3 5 2 10 12	rlimcn1b	$$⊢\phi \to \left(k\in A⟼\Im \left(B\right)\right)\underset{ℝ}{⇝}\Im \left(C\right)$$