Theorem isummulc1

Description: An infinite sum multiplied by a constant. (Contributed by NM, 13-Nov-2005) (Revised by Mario Carneiro, 23-Apr-2014)

	Ref	Expression
Hypotheses	isumcl.1	|- Z = ( ZZ>= ` M )
	isumcl.2	|- ( ph -> M e. ZZ )
	isumcl.3	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
	isumcl.4	|- ( ( ph /\ k e. Z ) -> A e. CC )
	isumcl.5	|- ( ph -> seq M ( + , F ) e. dom ~~> )
	summulc.6	|- ( ph -> B e. CC )
Assertion	isummulc1	|- ( ph -> ( sum_ k e. Z A x. B ) = sum_ k e. Z ( A x. B ) )

Proof

Step	Hyp	Ref	Expression
1		isumcl.1	|- Z = ( ZZ>= ` M )
2		isumcl.2	|- ( ph -> M e. ZZ )
3		isumcl.3	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
4		isumcl.4	|- ( ( ph /\ k e. Z ) -> A e. CC )
5		isumcl.5	|- ( ph -> seq M ( + , F ) e. dom ~~> )
6		summulc.6	|- ( ph -> B e. CC )
7	1 2 3 4 5 6	isummulc2	|- ( ph -> ( B x. sum_ k e. Z A ) = sum_ k e. Z ( B x. A ) )
8	1 2 3 4 5	isumcl	|- ( ph -> sum_ k e. Z A e. CC )
9	8 6	mulcomd	|- ( ph -> ( sum_ k e. Z A x. B ) = ( B x. sum_ k e. Z A ) )
10	6	adantr	|- ( ( ph /\ k e. Z ) -> B e. CC )
11	4 10	mulcomd	|- ( ( ph /\ k e. Z ) -> ( A x. B ) = ( B x. A ) )
12	11	sumeq2dv	|- ( ph -> sum_ k e. Z ( A x. B ) = sum_ k e. Z ( B x. A ) )
13	7 9 12	3eqtr4d	|- ( ph -> ( sum_ k e. Z A x. B ) = sum_ k e. Z ( A x. B ) )