Metamath Proof Explorer

Theorem isummulc2

Description: An infinite sum multiplied by a constant. (Contributed by NM, 12-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 isummulc2 
|- ( ph -> ( B x. sum_ k e. Z A ) = sum_ k e. Z ( B x. A ) )

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 sumfc 
 |-  sum_ m e. Z ( ( k e. Z |-> ( B x. A ) ) ` m ) = sum_ k e. Z ( B x. A )
8 eqidd 
 |-  ( ( ph /\ m e. Z ) -> ( ( k e. Z |-> ( B x. A ) ) ` m ) = ( ( k e. Z |-> ( B x. A ) ) ` m ) )
9 6 adantr 
 |-  ( ( ph /\ k e. Z ) -> B e. CC )
10 9 4 mulcld 
 |-  ( ( ph /\ k e. Z ) -> ( B x. A ) e. CC )
11 10 fmpttd 
 |-  ( ph -> ( k e. Z |-> ( B x. A ) ) : Z --> CC )
12 11 ffvelrnda 
 |-  ( ( ph /\ m e. Z ) -> ( ( k e. Z |-> ( B x. A ) ) ` m ) e. CC )
13 1 2 3 4 5 isumclim2 
 |-  ( ph -> seq M ( + , F ) ~~> sum_ k e. Z A )
14 3 4 eqeltrd 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
15 14 ralrimiva 
 |-  ( ph -> A. k e. Z ( F ` k ) e. CC )
16 fveq2 
 |-  ( k = m -> ( F ` k ) = ( F ` m ) )
17 16 eleq1d 
 |-  ( k = m -> ( ( F ` k ) e. CC <-> ( F ` m ) e. CC ) )
18 17 rspccva 
 |-  ( ( A. k e. Z ( F ` k ) e. CC /\ m e. Z ) -> ( F ` m ) e. CC )
19 15 18 sylan 
 |-  ( ( ph /\ m e. Z ) -> ( F ` m ) e. CC )
20 simpr 
 |-  ( ( ph /\ k e. Z ) -> k e. Z )
21 ovex 
 |-  ( B x. A ) e. _V
22 eqid 
 |-  ( k e. Z |-> ( B x. A ) ) = ( k e. Z |-> ( B x. A ) )
23 22 fvmpt2 
 |-  ( ( k e. Z /\ ( B x. A ) e. _V ) -> ( ( k e. Z |-> ( B x. A ) ) ` k ) = ( B x. A ) )
24 20 21 23 sylancl 
 |-  ( ( ph /\ k e. Z ) -> ( ( k e. Z |-> ( B x. A ) ) ` k ) = ( B x. A ) )
25 3 oveq2d 
 |-  ( ( ph /\ k e. Z ) -> ( B x. ( F ` k ) ) = ( B x. A ) )
26 24 25 eqtr4d 
 |-  ( ( ph /\ k e. Z ) -> ( ( k e. Z |-> ( B x. A ) ) ` k ) = ( B x. ( F ` k ) ) )
27 26 ralrimiva 
 |-  ( ph -> A. k e. Z ( ( k e. Z |-> ( B x. A ) ) ` k ) = ( B x. ( F ` k ) ) )
28 nffvmpt1 
 |-  F/_ k ( ( k e. Z |-> ( B x. A ) ) ` m )
29 28 nfeq1 
 |-  F/ k ( ( k e. Z |-> ( B x. A ) ) ` m ) = ( B x. ( F ` m ) )
30 fveq2 
 |-  ( k = m -> ( ( k e. Z |-> ( B x. A ) ) ` k ) = ( ( k e. Z |-> ( B x. A ) ) ` m ) )
31 16 oveq2d 
 |-  ( k = m -> ( B x. ( F ` k ) ) = ( B x. ( F ` m ) ) )
32 30 31 eqeq12d 
 |-  ( k = m -> ( ( ( k e. Z |-> ( B x. A ) ) ` k ) = ( B x. ( F ` k ) ) <-> ( ( k e. Z |-> ( B x. A ) ) ` m ) = ( B x. ( F ` m ) ) ) )
33 29 32 rspc 
 |-  ( m e. Z -> ( A. k e. Z ( ( k e. Z |-> ( B x. A ) ) ` k ) = ( B x. ( F ` k ) ) -> ( ( k e. Z |-> ( B x. A ) ) ` m ) = ( B x. ( F ` m ) ) ) )
34 27 33 mpan9 
 |-  ( ( ph /\ m e. Z ) -> ( ( k e. Z |-> ( B x. A ) ) ` m ) = ( B x. ( F ` m ) ) )
35 1 2 6 13 19 34 isermulc2 
 |-  ( ph -> seq M ( + , ( k e. Z |-> ( B x. A ) ) ) ~~> ( B x. sum_ k e. Z A ) )
36 1 2 8 12 35 isumclim 
 |-  ( ph -> sum_ m e. Z ( ( k e. Z |-> ( B x. A ) ) ` m ) = ( B x. sum_ k e. Z A ) )
37 7 36 syl5reqr 
 |-  ( ph -> ( B x. sum_ k e. Z A ) = sum_ k e. Z ( B x. A ) )