iprod

Description: Series product with an upper integer index set (i.e. an infinite product.) (Contributed by Scott Fenton, 5-Dec-2017)

	Ref	Expression
Hypotheses	zprod.1	$⊢ Z = ℤ_{\geq M}$
	zprod.2	$⊢ φ \to M \in ℤ$
	zprod.3	$⊢ φ \to \exists n \in Z \exists y (y \neq 0 \land seq n (\times F) ⇝ y)$
	iprod.4	$⊢ (φ \land k \in Z) \to F (k) = B$
	iprod.5	$⊢ (φ \land k \in Z) \to B \in ℂ$
Assertion	iprod	$⊢ φ \to \prod_{k \in Z} B = ⇝ (seq M (\times F))$

Step	Hyp	Ref	Expression
1		zprod.1	$⊢ Z = ℤ_{\geq M}$
2		zprod.2	$⊢ φ \to M \in ℤ$
3		zprod.3	$⊢ φ \to \exists n \in Z \exists y (y \neq 0 \land seq n (\times F) ⇝ y)$
4		iprod.4	$⊢ (φ \land k \in Z) \to F (k) = B$
5		iprod.5	$⊢ (φ \land k \in Z) \to B \in ℂ$
6		ssidd	$⊢ φ \to Z \subseteq Z$
7		iftrue	$⊢ k \in Z \to if (k \in Z, B, 1) = B$
8	7	adantl	$⊢ (φ \land k \in Z) \to if (k \in Z, B, 1) = B$
9	4 8	eqtr4d	$⊢ (φ \land k \in Z) \to F (k) = if (k \in Z, B, 1)$
10	1 2 3 6 9 5	zprod	$⊢ φ \to \prod_{k \in Z} B = ⇝ (seq M (\times F))$

Metamath Proof Explorer