Theorem climabs

Description: Limit of the absolute value of a sequence. Proposition 12-2.4(c) of Gleason p. 172. (Contributed by NM, 7-Jun-2006) (Revised by Mario Carneiro, 9-Feb-2014)

	Ref	Expression
Hypotheses	climcn1lem.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	climcn1lem.2	$$⊢\phi \to F⇝A$$
	climcn1lem.4	$$⊢\phi \to G\in W$$
	climcn1lem.5	$$⊢\phi \to M\in \mathbb{Z}$$
	climcn1lem.6	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℂ$$
	climabs.7	$$⊢\left(\phi \wedge k\in Z\right)\to G\left(k\right)=\left|F\left(k\right)\right|$$
Assertion	climabs	$$⊢\phi \to G⇝\left|A\right|$$

Proof

Step	Hyp	Ref	Expression
1		climcn1lem.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		climcn1lem.2	$$⊢\phi \to F⇝A$$
3		climcn1lem.4	$$⊢\phi \to G\in W$$
4		climcn1lem.5	$$⊢\phi \to M\in \mathbb{Z}$$
5		climcn1lem.6	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℂ$$
6		climabs.7	$$⊢\left(\phi \wedge k\in Z\right)\to G\left(k\right)=\left|F\left(k\right)\right|$$
7		absf	$$⊢\mathrm{abs}:ℂ⟶ℝ$$
8		ax-resscn	$$⊢ℝ\subseteq ℂ$$
9		fss	$$⊢\left(\mathrm{abs}:ℂ⟶ℝ\wedge ℝ\subseteq ℂ\right)\to \mathrm{abs}:ℂ⟶ℂ$$
10	7 8 9	mp2an	$$⊢\mathrm{abs}:ℂ⟶ℂ$$
11		abscn2	$$⊢\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\to \exists y\in {ℝ}^{+}\forall z\in ℂ\left(\left|z-A\right|<y\to \left|\left|z\right|-\left|A\right|\right|<x\right)$$
12	1 2 3 4 5 10 11 6	climcn1lem	$$⊢\phi \to G⇝\left|A\right|$$