Theorem isumdivc

Description: An infinite sum divided by a constant. (Contributed by NM, 2-Jan-2006) (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 )
	isumdivc.7	|- ( ph -> B =/= 0 )
Assertion	isumdivc	|- ( ph -> ( sum_ k e. Z A / B ) = sum_ k e. Z ( A / 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		isumdivc.7	|- ( ph -> B =/= 0 )
8	6 7	reccld	|- ( ph -> ( 1 / B ) e. CC )
9	1 2 3 4 5 8	isummulc1	|- ( ph -> ( sum_ k e. Z A x. ( 1 / B ) ) = sum_ k e. Z ( A x. ( 1 / B ) ) )
10	1 2 3 4 5	isumcl	|- ( ph -> sum_ k e. Z A e. CC )
11	10 6 7	divrecd	|- ( ph -> ( sum_ k e. Z A / B ) = ( sum_ k e. Z A x. ( 1 / B ) ) )
12	6	adantr	|- ( ( ph /\ k e. Z ) -> B e. CC )
13	7	adantr	|- ( ( ph /\ k e. Z ) -> B =/= 0 )
14	4 12 13	divrecd	|- ( ( ph /\ k e. Z ) -> ( A / B ) = ( A x. ( 1 / B ) ) )
15	14	sumeq2dv	|- ( ph -> sum_ k e. Z ( A / B ) = sum_ k e. Z ( A x. ( 1 / B ) ) )
16	9 11 15	3eqtr4d	|- ( ph -> ( sum_ k e. Z A / B ) = sum_ k e. Z ( A / B ) )