Theorem abscvgcvg

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

	Ref	Expression
Hypotheses	abscvgcvg.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	abscvgcvg.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	abscvgcvg.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) )
	abscvgcvg.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
	abscvgcvg.5	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
Assertion	abscvgcvg	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐺 ) ∈ dom ⇝ )

Proof

Step	Hyp	Ref	Expression
1		abscvgcvg.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		abscvgcvg.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		abscvgcvg.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) )
4		abscvgcvg.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
5		abscvgcvg.5	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
6		uzid	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
7	2 6	syl	⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
8	7 1	eleqtrrdi	⊢ ( 𝜑 → 𝑀 ∈ 𝑍 )
9	4	abscld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) ∈ ℝ )
10	3 9	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
11		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
12	1	eleq2i	⊢ ( 𝑘 ∈ 𝑍 ↔ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
13	3	eqcomd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) = ( 𝐹 ‘ 𝑘 ) )
14	9 13	eqled	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) ≤ ( 𝐹 ‘ 𝑘 ) )
15	10	recnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
16	15	mulid2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 1 · ( 𝐹 ‘ 𝑘 ) ) = ( 𝐹 ‘ 𝑘 ) )
17	14 16	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) ≤ ( 1 · ( 𝐹 ‘ 𝑘 ) ) )
18	12 17	sylan2br	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) ≤ ( 1 · ( 𝐹 ‘ 𝑘 ) ) )
19	1 8 10 4 5 11 18	cvgcmpce	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐺 ) ∈ dom ⇝ )