This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )