Theorem 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	⊢ 𝐹 = ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) )
	prodmo.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
	prodrb.3	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
	fprodcvg.4	⊢ ( 𝜑 → 𝐴 ⊆ ( 𝑀 ... 𝑁 ) )
Assertion	fprodcvg	⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) ⇝ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		prodmo.1	⊢ 𝐹 = ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) )
2		prodmo.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
3		prodrb.3	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
4		fprodcvg.4	⊢ ( 𝜑 → 𝐴 ⊆ ( 𝑀 ... 𝑁 ) )
5		eqid	⊢ ( ℤ≥ ‘ 𝑁 ) = ( ℤ≥ ‘ 𝑁 )
6		eluzelz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
7	3 6	syl	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
8		seqex	⊢ seq 𝑀 ( · , 𝐹 ) ∈ V
9	8	a1i	⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) ∈ V )
10		eqid	⊢ ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑀 )
11		eluzel2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
12	3 11	syl	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
13		eluzelz	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑘 ∈ ℤ )
14	13	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑘 ∈ ℤ )
15		iftrue	⊢ ( 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) = 𝐵 )
16	15	adantl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑘 ∈ 𝐴 ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) = 𝐵 )
17	2	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
18	16 17	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑘 ∈ 𝐴 ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ∈ ℂ )
19	18	ex	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ∈ ℂ ) )
20		iffalse	⊢ ( ¬ 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) = 1 )
21		ax-1cn	⊢ 1 ∈ ℂ
22	20 21	eqeltrdi	⊢ ( ¬ 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ∈ ℂ )
23	19 22	pm2.61d1	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ∈ ℂ )
24	1	fvmpt2	⊢ ( ( 𝑘 ∈ ℤ ∧ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ∈ ℂ ) → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) )
25	14 23 24	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) )
26	25 23	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
27	10 12 26	prodf	⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) : ( ℤ≥ ‘ 𝑀 ) ⟶ ℂ )
28	27 3	ffvelrnd	⊢ ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ∈ ℂ )
29		mulid1	⊢ ( 𝑚 ∈ ℂ → ( 𝑚 · 1 ) = 𝑚 )
30	29	adantl	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑚 ∈ ℂ ) → ( 𝑚 · 1 ) = 𝑚 )
31	3	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
32		simpr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) )
33	12	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑀 ∈ ℤ )
34	26	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
35	10 33 34	prodf	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → seq 𝑀 ( · , 𝐹 ) : ( ℤ≥ ‘ 𝑀 ) ⟶ ℂ )
36	35 31	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ∈ ℂ )
37		elfzuz	⊢ ( 𝑚 ∈ ( ( 𝑁 + 1 ) ... 𝑛 ) → 𝑚 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) )
38		eluzelz	⊢ ( 𝑚 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) → 𝑚 ∈ ℤ )
39	38	adantl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑚 ∈ ℤ )
40	4	sseld	⊢ ( 𝜑 → ( 𝑚 ∈ 𝐴 → 𝑚 ∈ ( 𝑀 ... 𝑁 ) ) )
41		fznuz	⊢ ( 𝑚 ∈ ( 𝑀 ... 𝑁 ) → ¬ 𝑚 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) )
42	40 41	syl6	⊢ ( 𝜑 → ( 𝑚 ∈ 𝐴 → ¬ 𝑚 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )
43	42	con2d	⊢ ( 𝜑 → ( 𝑚 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) → ¬ 𝑚 ∈ 𝐴 ) )
44	43	imp	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ¬ 𝑚 ∈ 𝐴 )
45	39 44	eldifd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑚 ∈ ( ℤ ∖ 𝐴 ) )
46		fveqeq2	⊢ ( 𝑘 = 𝑚 → ( ( 𝐹 ‘ 𝑘 ) = 1 ↔ ( 𝐹 ‘ 𝑚 ) = 1 ) )
47		eldifi	⊢ ( 𝑘 ∈ ( ℤ ∖ 𝐴 ) → 𝑘 ∈ ℤ )
48		eldifn	⊢ ( 𝑘 ∈ ( ℤ ∖ 𝐴 ) → ¬ 𝑘 ∈ 𝐴 )
49	48 20	syl	⊢ ( 𝑘 ∈ ( ℤ ∖ 𝐴 ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) = 1 )
50	49 21	eqeltrdi	⊢ ( 𝑘 ∈ ( ℤ ∖ 𝐴 ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ∈ ℂ )
51	47 50 24	syl2anc	⊢ ( 𝑘 ∈ ( ℤ ∖ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) )
52	51 49	eqtrd	⊢ ( 𝑘 ∈ ( ℤ ∖ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) = 1 )
53	46 52	vtoclga	⊢ ( 𝑚 ∈ ( ℤ ∖ 𝐴 ) → ( 𝐹 ‘ 𝑚 ) = 1 )
54	45 53	syl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( 𝐹 ‘ 𝑚 ) = 1 )
55	37 54	sylan2	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( 𝑁 + 1 ) ... 𝑛 ) ) → ( 𝐹 ‘ 𝑚 ) = 1 )
56	55	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑚 ∈ ( ( 𝑁 + 1 ) ... 𝑛 ) ) → ( 𝐹 ‘ 𝑚 ) = 1 )
57	30 31 32 36 56	seqid2	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) = ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) )
58	57	eqcomd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) = ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) )
59	5 7 9 28 58	climconst	⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) ⇝ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) )