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 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
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 mullidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 1 · ( 𝐹 ‘ 𝑘 ) ) = ( 𝐹 ‘ 𝑘 ) )
17 14 16 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) ≤ ( 1 · ( 𝐹 ‘ 𝑘 ) ) )
18 12 17 sylan2br ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) ≤ ( 1 · ( 𝐹 ‘ 𝑘 ) ) )
19 1 8 10 4 5 11 18 cvgcmpce ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐺 ) ∈ dom ⇝ )