Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Thierry Arnoux
Real and complex functions
Extended sum
esumcvg2
Next ⟩
esumcvgsum
Metamath Proof Explorer
Ascii
Unicode
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