Theorem esumcvg2

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

	Ref	Expression
Hypotheses	esumcvg2.j	|- J = ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) )
	esumcvg2.a	|- ( ( ph /\ k e. NN ) -> A e. ( 0 [,] +oo ) )
	esumcvg2.l	|- ( k = l -> A = B )
	esumcvg2.m	|- ( k = m -> A = C )
Assertion	esumcvg2	|- ( ph -> ( n e. NN |-> sum* k e. ( 1 ... n ) A ) ( ~~>t ` J ) sum* k e. NN A )

Proof

Step	Hyp	Ref	Expression
1		esumcvg2.j	|- J = ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) )
2		esumcvg2.a	|- ( ( ph /\ k e. NN ) -> A e. ( 0 [,] +oo ) )
3		esumcvg2.l	|- ( k = l -> A = B )
4		esumcvg2.m	|- ( k = m -> A = C )
5	4	cbvesumv	|- sum* k e. ( 1 ... i ) A = sum* m e. ( 1 ... i ) C
6		oveq2	|- ( i = n -> ( 1 ... i ) = ( 1 ... n ) )
7		esumeq1	|- ( ( 1 ... i ) = ( 1 ... n ) -> sum* k e. ( 1 ... i ) A = sum* k e. ( 1 ... n ) A )
8	6 7	syl	|- ( i = n -> sum* k e. ( 1 ... i ) A = sum* k e. ( 1 ... n ) A )
9	5 8	eqtr3id	|- ( i = n -> sum* m e. ( 1 ... i ) C = sum* k e. ( 1 ... n ) A )
10	9	cbvmptv	|- ( i e. NN |-> sum* m e. ( 1 ... i ) C ) = ( n e. NN |-> sum* k e. ( 1 ... n ) A )
11	1 10 2 3	esumcvg	|- ( ph -> ( i e. NN |-> sum* m e. ( 1 ... i ) C ) ( ~~>t ` J ) sum* k e. NN A )
12	10 11	eqbrtrrid	|- ( ph -> ( n e. NN |-> sum* k e. ( 1 ... n ) A ) ( ~~>t ` J ) sum* k e. NN A )