fprodcvg

Description: The sequence of partial products of a finite product converges to the whole product. (Contributed by Scott Fenton, 4-Dec-2017)

	Ref	Expression
Hypotheses	prodmo.1	$⊢ F = (k \in ℤ ⟼ if (k \in A, B, 1))$
	prodmo.2	$⊢ (φ \land k \in A) \to B \in ℂ$
	prodrb.3	$⊢ φ \to N \in ℤ_{\geq M}$
	fprodcvg.4	$⊢ φ \to A \subseteq (M \dots N)$
Assertion	fprodcvg	$⊢ φ \to seq M (\times F) ⇝ seq M (\times F) (N)$

Proof

Step	Hyp	Ref	Expression
1		prodmo.1	$⊢ F = (k \in ℤ ⟼ if (k \in A, B, 1))$
2		prodmo.2	$⊢ (φ \land k \in A) \to B \in ℂ$
3		prodrb.3	$⊢ φ \to N \in ℤ_{\geq M}$
4		fprodcvg.4	$⊢ φ \to A \subseteq (M \dots N)$
5		eqid	$⊢ ℤ_{\geq N} = ℤ_{\geq N}$
6		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
7	3 6	syl	$⊢ φ \to N \in ℤ$
8		seqex	$⊢ seq M (\times F) \in V$
9	8	a1i	$⊢ φ \to seq M (\times F) \in V$
10		eqid	$⊢ ℤ_{\geq M} = ℤ_{\geq M}$
11		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
12	3 11	syl	$⊢ φ \to M \in ℤ$
13		eluzelz	$⊢ k \in ℤ_{\geq M} \to k \in ℤ$
14	13	adantl	$⊢ (φ \land k \in ℤ_{\geq M}) \to k \in ℤ$
15		iftrue	$⊢ k \in A \to if (k \in A, B, 1) = B$
16	15	adantl	$⊢ ((φ \land k \in ℤ_{\geq M}) \land k \in A) \to if (k \in A, B, 1) = B$
17	2	adantlr	$⊢ ((φ \land k \in ℤ_{\geq M}) \land k \in A) \to B \in ℂ$
18	16 17	eqeltrd	$⊢ ((φ \land k \in ℤ_{\geq M}) \land k \in A) \to if (k \in A, B, 1) \in ℂ$
19	18	ex	$⊢ (φ \land k \in ℤ_{\geq M}) \to (k \in A \to if (k \in A, B, 1) \in ℂ)$
20		iffalse	$⊢ \neg k \in A \to if (k \in A, B, 1) = 1$
21		ax-1cn	$⊢ 1 \in ℂ$
22	20 21	eqeltrdi	$⊢ \neg k \in A \to if (k \in A, B, 1) \in ℂ$
23	19 22	pm2.61d1	$⊢ (φ \land k \in ℤ_{\geq M}) \to if (k \in A, B, 1) \in ℂ$
24	1	fvmpt2	$⊢ (k \in ℤ \land if (k \in A, B, 1) \in ℂ) \to F (k) = if (k \in A, B, 1)$
25	14 23 24	syl2anc	$⊢ (φ \land k \in ℤ_{\geq M}) \to F (k) = if (k \in A, B, 1)$
26	25 23	eqeltrd	$⊢ (φ \land k \in ℤ_{\geq M}) \to F (k) \in ℂ$
27	10 12 26	prodf	$⊢ φ \to seq M (\times F) : ℤ_{\geq M} ⟶ ℂ$
28	27 3	ffvelrnd	$⊢ φ \to seq M (\times F) (N) \in ℂ$
29		mulid1	$⊢ m \in ℂ \to m \cdot 1 = m$
30	29	adantl	$⊢ ((φ \land n \in ℤ_{\geq N}) \land m \in ℂ) \to m \cdot 1 = m$
31	3	adantr	$⊢ (φ \land n \in ℤ_{\geq N}) \to N \in ℤ_{\geq M}$
32		simpr	$⊢ (φ \land n \in ℤ_{\geq N}) \to n \in ℤ_{\geq N}$
33	12	adantr	$⊢ (φ \land n \in ℤ_{\geq N}) \to M \in ℤ$
34	26	adantlr	$⊢ ((φ \land n \in ℤ_{\geq N}) \land k \in ℤ_{\geq M}) \to F (k) \in ℂ$
35	10 33 34	prodf	$⊢ (φ \land n \in ℤ_{\geq N}) \to seq M (\times F) : ℤ_{\geq M} ⟶ ℂ$
36	35 31	ffvelrnd	$⊢ (φ \land n \in ℤ_{\geq N}) \to seq M (\times F) (N) \in ℂ$
37		elfzuz	$⊢ m \in (N + 1 \dots n) \to m \in ℤ_{\geq (N + 1)}$
38		eluzelz	$⊢ m \in ℤ_{\geq (N + 1)} \to m \in ℤ$
39	38	adantl	$⊢ (φ \land m \in ℤ_{\geq (N + 1)}) \to m \in ℤ$
40	4	sseld	$⊢ φ \to (m \in A \to m \in (M \dots N))$
41		fznuz	$⊢ m \in (M \dots N) \to \neg m \in ℤ_{\geq (N + 1)}$
42	40 41	syl6	$⊢ φ \to (m \in A \to \neg m \in ℤ_{\geq (N + 1)})$
43	42	con2d	$⊢ φ \to (m \in ℤ_{\geq (N + 1)} \to \neg m \in A)$
44	43	imp	$⊢ (φ \land m \in ℤ_{\geq (N + 1)}) \to \neg m \in A$
45	39 44	eldifd	$⊢ (φ \land m \in ℤ_{\geq (N + 1)}) \to m \in (ℤ ∖ A)$
46		fveqeq2	$⊢ k = m \to (F (k) = 1 \leftrightarrow F (m) = 1)$
47		eldifi	$⊢ k \in (ℤ ∖ A) \to k \in ℤ$
48		eldifn	$⊢ k \in (ℤ ∖ A) \to \neg k \in A$
49	48 20	syl	$⊢ k \in (ℤ ∖ A) \to if (k \in A, B, 1) = 1$
50	49 21	eqeltrdi	$⊢ k \in (ℤ ∖ A) \to if (k \in A, B, 1) \in ℂ$
51	47 50 24	syl2anc	$⊢ k \in (ℤ ∖ A) \to F (k) = if (k \in A, B, 1)$
52	51 49	eqtrd	$⊢ k \in (ℤ ∖ A) \to F (k) = 1$
53	46 52	vtoclga	$⊢ m \in (ℤ ∖ A) \to F (m) = 1$
54	45 53	syl	$⊢ (φ \land m \in ℤ_{\geq (N + 1)}) \to F (m) = 1$
55	37 54	sylan2	$⊢ (φ \land m \in (N + 1 \dots n)) \to F (m) = 1$
56	55	adantlr	$⊢ ((φ \land n \in ℤ_{\geq N}) \land m \in (N + 1 \dots n)) \to F (m) = 1$
57	30 31 32 36 56	seqid2	$⊢ (φ \land n \in ℤ_{\geq N}) \to seq M (\times F) (N) = seq M (\times F) (n)$
58	57	eqcomd	$⊢ (φ \land n \in ℤ_{\geq N}) \to seq M (\times F) (n) = seq M (\times F) (N)$
59	5 7 9 28 58	climconst	$⊢ φ \to seq M (\times F) ⇝ seq M (\times F) (N)$

Metamath Proof Explorer

Theorem fprodcvg

Proof