Theorem rlimabs

Description: Limit of the absolute value 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	rlimabs	$$⊢\phi \to \left(k\in A⟼\left|B\right|\right)\underset{ℝ}{⇝}\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		absf	$$⊢\mathrm{abs}:ℂ⟶ℝ$$
7		ax-resscn	$$⊢ℝ\subseteq ℂ$$
8		fss	$$⊢\left(\mathrm{abs}:ℂ⟶ℝ\wedge ℝ\subseteq ℂ\right)\to \mathrm{abs}:ℂ⟶ℂ$$
9	6 7 8	mp2an	$$⊢\mathrm{abs}:ℂ⟶ℂ$$
10	9	a1i	$$⊢\phi \to \mathrm{abs}:ℂ⟶ℂ$$
11		abscn2	$$⊢\left(C\in ℂ\wedge x\in {ℝ}^{+}\right)\to \exists y\in {ℝ}^{+}\forall z\in ℂ\left(\left|z-C\right|<y\to \left|\left|z\right|-\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|\left|z\right|-\left|C\right|\right|<x\right)$$
13	3 5 2 10 12	rlimcn1b	$$⊢\phi \to \left(k\in A⟼\left|B\right|\right)\underset{ℝ}{⇝}\left|C\right|$$