iprodclim2

Description: A converging product converges to its infinite product. (Contributed by Scott Fenton, 18-Dec-2017)

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

Step	Hyp	Ref	Expression
1		iprodclim.1	$⊢ Z = ℤ_{\geq M}$
2		iprodclim.2	$⊢ φ \to M \in ℤ$
3		iprodclim.3	$⊢ φ \to \exists n \in Z \exists y (y \neq 0 \land seq n (\times F) ⇝ y)$
4		iprodclim.4	$⊢ (φ \land k \in Z) \to F (k) = A$
5		iprodclim.5	$⊢ (φ \land k \in Z) \to A \in ℂ$
6	4 5	eqeltrd	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
7	1 3 6	ntrivcvg	$⊢ φ \to seq M (\times F) \in dom ⇝$
8		climdm	$⊢ seq M (\times F) \in dom ⇝ \leftrightarrow seq M (\times F) ⇝ ⇝ (seq M (\times F))$
9	7 8	sylib	$⊢ φ \to seq M (\times F) ⇝ ⇝ (seq M (\times F))$
10	1 2 3 4 5	iprod	$⊢ φ \to \prod_{k \in Z} A = ⇝ (seq M (\times F))$
11	9 10	breqtrrd	$⊢ φ \to seq M (\times F) ⇝ \prod_{k \in Z} A$

Metamath Proof Explorer