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

Metamath Proof Explorer

Theorem prodfmul

Description: The product of two infinite products. (Contributed by Scott Fenton, 18-Dec-2017)

Ref Expression
Hypotheses prodfmul.1 
|- ( ph -> N e. ( ZZ>= ` M ) )
prodfmul.2 
|- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. CC )
prodfmul.3 
|- ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) e. CC )
prodfmul.4 
|- ( ( ph /\ k e. ( M ... N ) ) -> ( H ` k ) = ( ( F ` k ) x. ( G ` k ) ) )
Assertion prodfmul 
|- ( ph -> ( seq M ( x. , H ) ` N ) = ( ( seq M ( x. , F ) ` N ) x. ( seq M ( x. , G ) ` N ) ) )

Proof

Step Hyp Ref Expression
1 prodfmul.1 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
2 prodfmul.2 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. CC )
3 prodfmul.3 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) e. CC )
4 prodfmul.4 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( H ` k ) = ( ( F ` k ) x. ( G ` k ) ) )
5 mulcl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x x. y ) e. CC )
6 5 adantl 
 |-  ( ( ph /\ ( x e. CC /\ y e. CC ) ) -> ( x x. y ) e. CC )
7 mulcom 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x x. y ) = ( y x. x ) )
8 7 adantl 
 |-  ( ( ph /\ ( x e. CC /\ y e. CC ) ) -> ( x x. y ) = ( y x. x ) )
9 mulass 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( ( x x. y ) x. z ) = ( x x. ( y x. z ) ) )
10 9 adantl 
 |-  ( ( ph /\ ( x e. CC /\ y e. CC /\ z e. CC ) ) -> ( ( x x. y ) x. z ) = ( x x. ( y x. z ) ) )
11 6 8 10 1 2 3 4 seqcaopr 
 |-  ( ph -> ( seq M ( x. , H ) ` N ) = ( ( seq M ( x. , F ) ` N ) x. ( seq M ( x. , G ) ` N ) ) )