Metamath Proof Explorer

Theorem isermulc2

Description: Multiplication of an infinite series by a constant. (Contributed by Paul Chapman, 14-Nov-2007) (Revised by Mario Carneiro, 1-Feb-2014)

Ref Expression
Hypotheses clim2ser.1 
|- Z = ( ZZ>= ` M )
isermulc2.2 
|- ( ph -> M e. ZZ )
isermulc2.4 
|- ( ph -> C e. CC )
isermulc2.5 
|- ( ph -> seq M ( + , F ) ~~> A )
isermulc2.6 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
isermulc2.7 
|- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( C x. ( F ` k ) ) )
Assertion isermulc2 
|- ( ph -> seq M ( + , G ) ~~> ( C x. A ) )

Proof

Step Hyp Ref Expression
1 clim2ser.1 
 |-  Z = ( ZZ>= ` M )
2 isermulc2.2 
 |-  ( ph -> M e. ZZ )
3 isermulc2.4 
 |-  ( ph -> C e. CC )
4 isermulc2.5 
 |-  ( ph -> seq M ( + , F ) ~~> A )
5 isermulc2.6 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
6 isermulc2.7 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) = ( C x. ( F ` k ) ) )
7 seqex 
 |-  seq M ( + , G ) e. _V
8 7 a1i 
 |-  ( ph -> seq M ( + , G ) e. _V )
9 1 2 5 serf 
 |-  ( ph -> seq M ( + , F ) : Z --> CC )
10 9 ffvelrnda 
 |-  ( ( ph /\ j e. Z ) -> ( seq M ( + , F ) ` j ) e. CC )
11 addcl 
 |-  ( ( k e. CC /\ x e. CC ) -> ( k + x ) e. CC )
12 11 adantl 
 |-  ( ( ( ph /\ j e. Z ) /\ ( k e. CC /\ x e. CC ) ) -> ( k + x ) e. CC )
13 3 adantr 
 |-  ( ( ph /\ j e. Z ) -> C e. CC )
14 adddi 
 |-  ( ( C e. CC /\ k e. CC /\ x e. CC ) -> ( C x. ( k + x ) ) = ( ( C x. k ) + ( C x. x ) ) )
15 14 3expb 
 |-  ( ( C e. CC /\ ( k e. CC /\ x e. CC ) ) -> ( C x. ( k + x ) ) = ( ( C x. k ) + ( C x. x ) ) )
16 13 15 sylan 
 |-  ( ( ( ph /\ j e. Z ) /\ ( k e. CC /\ x e. CC ) ) -> ( C x. ( k + x ) ) = ( ( C x. k ) + ( C x. x ) ) )
17 simpr 
 |-  ( ( ph /\ j e. Z ) -> j e. Z )
18 17 1 eleqtrdi 
 |-  ( ( ph /\ j e. Z ) -> j e. ( ZZ>= ` M ) )
19 elfzuz 
 |-  ( k e. ( M ... j ) -> k e. ( ZZ>= ` M ) )
20 19 1 eleqtrrdi 
 |-  ( k e. ( M ... j ) -> k e. Z )
21 20 5 sylan2 
 |-  ( ( ph /\ k e. ( M ... j ) ) -> ( F ` k ) e. CC )
22 21 adantlr 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( M ... j ) ) -> ( F ` k ) e. CC )
23 20 6 sylan2 
 |-  ( ( ph /\ k e. ( M ... j ) ) -> ( G ` k ) = ( C x. ( F ` k ) ) )
24 23 adantlr 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( M ... j ) ) -> ( G ` k ) = ( C x. ( F ` k ) ) )
25 12 16 18 22 24 seqdistr 
 |-  ( ( ph /\ j e. Z ) -> ( seq M ( + , G ) ` j ) = ( C x. ( seq M ( + , F ) ` j ) ) )
26 1 2 4 3 8 10 25 climmulc2 
 |-  ( ph -> seq M ( + , G ) ~~> ( C x. A ) )