prodfmul

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

	Ref	Expression
Hypotheses	prodfmul.1	$⊢ φ \to N \in ℤ_{\geq M}$
	prodfmul.2	$⊢ (φ \land k \in (M \dots N)) \to F (k) \in ℂ$
	prodfmul.3	$⊢ (φ \land k \in (M \dots N)) \to G (k) \in ℂ$
	prodfmul.4	$⊢ (φ \land k \in (M \dots N)) \to H (k) = F (k) G (k)$
Assertion	prodfmul	$⊢ φ \to seq M (\times H) (N) = seq M (\times F) (N) seq M (\times G) (N)$

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

Metamath Proof Explorer