Theorem abscvgcvg

Description: An absolutely convergent series is convergent. (Contributed by Mario Carneiro, 28-Apr-2014)

	Ref	Expression
Hypotheses	abscvgcvg.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	abscvgcvg.2	$$⊢\phi \to M\in \mathbb{Z}$$
	abscvgcvg.3	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=\left|G\left(k\right)\right|$$
	abscvgcvg.4	$$⊢\left(\phi \wedge k\in Z\right)\to G\left(k\right)\in ℂ$$
	abscvgcvg.5	$$⊢\phi \to seqM\left(+,F\right)\in \mathrm{dom}⇝$$
Assertion	abscvgcvg	$$⊢\phi \to seqM\left(+,G\right)\in \mathrm{dom}⇝$$

Proof

Step	Hyp	Ref	Expression
1		abscvgcvg.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		abscvgcvg.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		abscvgcvg.3	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=\left|G\left(k\right)\right|$$
4		abscvgcvg.4	$$⊢\left(\phi \wedge k\in Z\right)\to G\left(k\right)\in ℂ$$
5		abscvgcvg.5	$$⊢\phi \to seqM\left(+,F\right)\in \mathrm{dom}⇝$$
6		uzid	$$⊢M\in \mathbb{Z}\to M\in {\mathbb{Z}}_{\ge M}$$
7	2 6	syl	$$⊢\phi \to M\in {\mathbb{Z}}_{\ge M}$$
8	7 1	eleqtrrdi	$$⊢\phi \to M\in Z$$
9	4	abscld	$$⊢\left(\phi \wedge k\in Z\right)\to \left|G\left(k\right)\right|\in ℝ$$
10	3 9	eqeltrd	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℝ$$
11		1red	$$⊢\phi \to 1\in ℝ$$
12	1	eleq2i	$$⊢k\in Z\leftrightarrow k\in {\mathbb{Z}}_{\ge M}$$
13	3	eqcomd	$$⊢\left(\phi \wedge k\in Z\right)\to \left|G\left(k\right)\right|=F\left(k\right)$$
14	9 13	eqled	$$⊢\left(\phi \wedge k\in Z\right)\to \left|G\left(k\right)\right|\le F\left(k\right)$$
15	10	recnd	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℂ$$
16	15	mullidd	$$⊢\left(\phi \wedge k\in Z\right)\to 1F\left(k\right)=F\left(k\right)$$
17	14 16	breqtrrd	$$⊢\left(\phi \wedge k\in Z\right)\to \left|G\left(k\right)\right|\le 1F\left(k\right)$$
18	12 17	sylan2br	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge M}\right)\to \left|G\left(k\right)\right|\le 1F\left(k\right)$$
19	1 8 10 4 5 11 18	cvgcmpce	$$⊢\phi \to seqM\left(+,G\right)\in \mathrm{dom}⇝$$