Theorem esumid

Description: Identify the extended sum as any limit points of the infinite sum. (Contributed by Thierry Arnoux, 9-May-2017)

	Ref	Expression
Hypotheses	esumid.p	|- F/ k ph
	esumid.0	|- F/_ k A
	esumid.1	|- ( ph -> A e. V )
	esumid.2	|- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
	esumid.3	|- ( ph -> C e. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) ) )
Assertion	esumid	|- ( ph -> sum* k e. A B = C )

Proof

Step	Hyp	Ref	Expression
1		esumid.p	|- F/ k ph
2		esumid.0	|- F/_ k A
3		esumid.1	|- ( ph -> A e. V )
4		esumid.2	|- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
5		esumid.3	|- ( ph -> C e. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) ) )
6		df-esum	|- sum* k e. A B = U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) )
7		eqid	|- ( RR*s |`s ( 0 [,] +oo ) ) = ( RR*s |`s ( 0 [,] +oo ) )
8		nfcv	|- F/_ k ( 0 [,] +oo )
9		eqid	|- ( k e. A |-> B ) = ( k e. A |-> B )
10	1 2 8 4 9	fmptdF	|- ( ph -> ( k e. A |-> B ) : A --> ( 0 [,] +oo ) )
11	7 3 10 5	xrge0tsmseq	|- ( ph -> C = U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) ) )
12	6 11	eqtr4id	|- ( ph -> sum* k e. A B = C )