iprodclim3

Description: The sequence of partial finite product of a converging infinite product converge to the infinite product of the series. Note that j must not occur in A . (Contributed by Scott Fenton, 18-Dec-2017)

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

Proof

Step	Hyp	Ref	Expression
1		iprodclim3.1	$⊢ Z = ℤ_{\geq M}$
2		iprodclim3.2	$⊢ φ \to M \in ℤ$
3		iprodclim3.3	$⊢ φ \to \exists n \in Z \exists y (y \neq 0 \land seq n (\times (k \in Z ⟼ A)) ⇝ y)$
4		iprodclim3.4	$⊢ φ \to F \in dom ⇝$
5		iprodclim3.5	$⊢ (φ \land k \in Z) \to A \in ℂ$
6		iprodclim3.6	$⊢ (φ \land j \in Z) \to F (j) = \prod_{k = M}^{j} A$
7		climdm	$⊢ F \in dom ⇝ \leftrightarrow F ⇝ ⇝ (F)$
8	4 7	sylib	$⊢ φ \to F ⇝ ⇝ (F)$
9		prodfc	$⊢ \prod_{m \in Z} (k \in Z ⟼ A) (m) = \prod_{k \in Z} A$
10		eqidd	$⊢ (φ \land m \in Z) \to (k \in Z ⟼ A) (m) = (k \in Z ⟼ A) (m)$
11	5	fmpttd	$⊢ φ \to (k \in Z ⟼ A) : Z ⟶ ℂ$
12	11	ffvelrnda	$⊢ (φ \land m \in Z) \to (k \in Z ⟼ A) (m) \in ℂ$
13	1 2 3 10 12	iprod	$⊢ φ \to \prod_{m \in Z} (k \in Z ⟼ A) (m) = ⇝ (seq M (\times (k \in Z ⟼ A)))$
14	9 13	syl5eqr	$⊢ φ \to \prod_{k \in Z} A = ⇝ (seq M (\times (k \in Z ⟼ A)))$
15		seqex	$⊢ seq M (\times (k \in Z ⟼ A)) \in V$
16	15	a1i	$⊢ φ \to seq M (\times (k \in Z ⟼ A)) \in V$
17		fzssuz	$⊢ (M \dots j) \subseteq ℤ_{\geq M}$
18	17 1	sseqtrri	$⊢ (M \dots j) \subseteq Z$
19		resmpt	$⊢ (M \dots j) \subseteq Z \to {(k \in Z ⟼ A) ↾}_{(M \dots j)} = (k \in (M \dots j) ⟼ A)$
20	18 19	ax-mp	$⊢ {(k \in Z ⟼ A) ↾}_{(M \dots j)} = (k \in (M \dots j) ⟼ A)$
21	20	fveq1i	$⊢ ({(k \in Z ⟼ A) ↾}_{(M \dots j)}) (m) = (k \in (M \dots j) ⟼ A) (m)$
22		fvres	$⊢ m \in (M \dots j) \to ({(k \in Z ⟼ A) ↾}_{(M \dots j)}) (m) = (k \in Z ⟼ A) (m)$
23	21 22	syl5reqr	$⊢ m \in (M \dots j) \to (k \in Z ⟼ A) (m) = (k \in (M \dots j) ⟼ A) (m)$
24	23	prodeq2i	$⊢ \prod_{m = M}^{j} (k \in Z ⟼ A) (m) = \prod_{m = M}^{j} (k \in (M \dots j) ⟼ A) (m)$
25		prodfc	$⊢ \prod_{m = M}^{j} (k \in (M \dots j) ⟼ A) (m) = \prod_{k = M}^{j} A$
26	24 25	eqtri	$⊢ \prod_{m = M}^{j} (k \in Z ⟼ A) (m) = \prod_{k = M}^{j} A$
27		eqidd	$⊢ ((φ \land j \in Z) \land m \in (M \dots j)) \to (k \in Z ⟼ A) (m) = (k \in Z ⟼ A) (m)$
28		simpr	$⊢ (φ \land j \in Z) \to j \in Z$
29	28 1	eleqtrdi	$⊢ (φ \land j \in Z) \to j \in ℤ_{\geq M}$
30		elfzuz	$⊢ m \in (M \dots j) \to m \in ℤ_{\geq M}$
31	30 1	eleqtrrdi	$⊢ m \in (M \dots j) \to m \in Z$
32	31 12	sylan2	$⊢ (φ \land m \in (M \dots j)) \to (k \in Z ⟼ A) (m) \in ℂ$
33	32	adantlr	$⊢ ((φ \land j \in Z) \land m \in (M \dots j)) \to (k \in Z ⟼ A) (m) \in ℂ$
34	27 29 33	fprodser	$⊢ (φ \land j \in Z) \to \prod_{m = M}^{j} (k \in Z ⟼ A) (m) = seq M (\times (k \in Z ⟼ A)) (j)$
35	26 34	syl5eqr	$⊢ (φ \land j \in Z) \to \prod_{k = M}^{j} A = seq M (\times (k \in Z ⟼ A)) (j)$
36	6 35	eqtr2d	$⊢ (φ \land j \in Z) \to seq M (\times (k \in Z ⟼ A)) (j) = F (j)$
37	1 16 4 2 36	climeq	$⊢ φ \to (seq M (\times (k \in Z ⟼ A)) ⇝ x \leftrightarrow F ⇝ x)$
38	37	iotabidv	$⊢ φ \to (ι x \| seq M (\times (k \in Z ⟼ A)) ⇝ x) = (ι x \| F ⇝ x)$
39		df-fv	$⊢ ⇝ (seq M (\times (k \in Z ⟼ A))) = (ι x \| seq M (\times (k \in Z ⟼ A)) ⇝ x)$
40		df-fv	$⊢ ⇝ (F) = (ι x \| F ⇝ x)$
41	38 39 40	3eqtr4g	$⊢ φ \to ⇝ (seq M (\times (k \in Z ⟼ A))) = ⇝ (F)$
42	14 41	eqtrd	$⊢ φ \to \prod_{k \in Z} A = ⇝ (F)$
43	8 42	breqtrrd	$⊢ φ \to F ⇝ \prod_{k \in Z} A$

Metamath Proof Explorer

Theorem iprodclim3

Proof