This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem abscvgcvg

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

Ref Expression
Hypotheses abscvgcvg.1 ⊢ Z = ℤ ≥ M
abscvgcvg.2 ⊢ φ → M ∈ ℤ
abscvgcvg.3 ⊢ φ ∧ k ∈ Z → F ⁡ k = G ⁡ k
abscvgcvg.4 ⊢ φ ∧ k ∈ Z → G ⁡ k ∈ ℂ
abscvgcvg.5 ⊢ φ → seq M + F ∈ dom ⁡ ⇝
Assertion abscvgcvg ⊢ φ → seq M + G ∈ dom ⁡ ⇝

Proof

Step Hyp Ref Expression
1 abscvgcvg.1 ⊢ Z = ℤ ≥ M
2 abscvgcvg.2 ⊢ φ → M ∈ ℤ
3 abscvgcvg.3 ⊢ φ ∧ k ∈ Z → F ⁡ k = G ⁡ k
4 abscvgcvg.4 ⊢ φ ∧ k ∈ Z → G ⁡ k ∈ ℂ
5 abscvgcvg.5 ⊢ φ → seq M + F ∈ dom ⁡ ⇝
6 uzid ⊢ M ∈ ℤ → M ∈ ℤ ≥ M
7 2 6 syl ⊢ φ → M ∈ ℤ ≥ M
8 7 1 eleqtrrdi ⊢ φ → M ∈ Z
9 4 abscld ⊢ φ ∧ k ∈ Z → G ⁡ k ∈ ℝ
10 3 9 eqeltrd ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℝ
11 1red ⊢ φ → 1 ∈ ℝ
12 1 eleq2i ⊢ k ∈ Z ↔ k ∈ ℤ ≥ M
13 3 eqcomd ⊢ φ ∧ k ∈ Z → G ⁡ k = F ⁡ k
14 9 13 eqled ⊢ φ ∧ k ∈ Z → G ⁡ k ≤ F ⁡ k
15 10 recnd ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℂ
16 15 mullidd ⊢ φ ∧ k ∈ Z → 1 ⁢ F ⁡ k = F ⁡ k
17 14 16 breqtrrd ⊢ φ ∧ k ∈ Z → G ⁡ k ≤ 1 ⁢ F ⁡ k
18 12 17 sylan2br ⊢ φ ∧ k ∈ ℤ ≥ M → G ⁡ k ≤ 1 ⁢ F ⁡ k
19 1 8 10 4 5 11 18 cvgcmpce ⊢ φ → seq M + G ∈ dom ⁡ ⇝