Metamath Proof Explorer


Theorem esumcvg2

Description: Simpler version of esumcvg . (Contributed by Thierry Arnoux, 5-Sep-2017)

Ref Expression
Hypotheses esumcvg2.j J = TopOpen 𝑠 * 𝑠 0 +∞
esumcvg2.a φ k A 0 +∞
esumcvg2.l k = l A = B
esumcvg2.m k = m A = C
Assertion esumcvg2 φ n * k = 1 n A t J * k A

Proof

Step Hyp Ref Expression
1 esumcvg2.j J = TopOpen 𝑠 * 𝑠 0 +∞
2 esumcvg2.a φ k A 0 +∞
3 esumcvg2.l k = l A = B
4 esumcvg2.m k = m A = C
5 4 cbvesumv * k = 1 i A = * m = 1 i C
6 oveq2 i = n 1 i = 1 n
7 esumeq1 1 i = 1 n * k = 1 i A = * k = 1 n A
8 6 7 syl i = n * k = 1 i A = * k = 1 n A
9 5 8 eqtr3id i = n * m = 1 i C = * k = 1 n A
10 9 cbvmptv i * m = 1 i C = n * k = 1 n A
11 1 10 2 3 esumcvg φ i * m = 1 i C t J * k A
12 10 11 eqbrtrrid φ n * k = 1 n A t J * k A