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 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 ⇝ )