# Metamath Proof Explorer

## Theorem prodfmul

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

Ref Expression
Hypotheses prodfmul.1 ${⊢}{\phi }\to {N}\in {ℤ}_{\ge {M}}$
prodfmul.2 ${⊢}\left({\phi }\wedge {k}\in \left({M}\dots {N}\right)\right)\to {F}\left({k}\right)\in ℂ$
prodfmul.3 ${⊢}\left({\phi }\wedge {k}\in \left({M}\dots {N}\right)\right)\to {G}\left({k}\right)\in ℂ$
prodfmul.4 ${⊢}\left({\phi }\wedge {k}\in \left({M}\dots {N}\right)\right)\to {H}\left({k}\right)={F}\left({k}\right){G}\left({k}\right)$
Assertion prodfmul ${⊢}{\phi }\to seq{M}\left(×,{H}\right)\left({N}\right)=seq{M}\left(×,{F}\right)\left({N}\right)seq{M}\left(×,{G}\right)\left({N}\right)$

### Proof

Step Hyp Ref Expression
1 prodfmul.1 ${⊢}{\phi }\to {N}\in {ℤ}_{\ge {M}}$
2 prodfmul.2 ${⊢}\left({\phi }\wedge {k}\in \left({M}\dots {N}\right)\right)\to {F}\left({k}\right)\in ℂ$
3 prodfmul.3 ${⊢}\left({\phi }\wedge {k}\in \left({M}\dots {N}\right)\right)\to {G}\left({k}\right)\in ℂ$
4 prodfmul.4 ${⊢}\left({\phi }\wedge {k}\in \left({M}\dots {N}\right)\right)\to {H}\left({k}\right)={F}\left({k}\right){G}\left({k}\right)$
5 mulcl ${⊢}\left({x}\in ℂ\wedge {y}\in ℂ\right)\to {x}{y}\in ℂ$
6 5 adantl ${⊢}\left({\phi }\wedge \left({x}\in ℂ\wedge {y}\in ℂ\right)\right)\to {x}{y}\in ℂ$
7 mulcom ${⊢}\left({x}\in ℂ\wedge {y}\in ℂ\right)\to {x}{y}={y}{x}$
8 7 adantl ${⊢}\left({\phi }\wedge \left({x}\in ℂ\wedge {y}\in ℂ\right)\right)\to {x}{y}={y}{x}$
9 mulass ${⊢}\left({x}\in ℂ\wedge {y}\in ℂ\wedge {z}\in ℂ\right)\to {x}{y}{z}={x}{y}{z}$
10 9 adantl ${⊢}\left({\phi }\wedge \left({x}\in ℂ\wedge {y}\in ℂ\wedge {z}\in ℂ\right)\right)\to {x}{y}{z}={x}{y}{z}$
11 6 8 10 1 2 3 4 seqcaopr ${⊢}{\phi }\to seq{M}\left(×,{H}\right)\left({N}\right)=seq{M}\left(×,{F}\right)\left({N}\right)seq{M}\left(×,{G}\right)\left({N}\right)$