Theorem 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	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	iprodclim3.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	iprodclim3.3	⊢ ( 𝜑 → ∃ 𝑛 ∈ 𝑍 ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) ⇝ 𝑦 ) )
	iprodclim3.4	⊢ ( 𝜑 → 𝐹 ∈ dom ⇝ )
	iprodclim3.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
	iprodclim3.6	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑗 ) 𝐴 )
Assertion	iprodclim3	⊢ ( 𝜑 → 𝐹 ⇝ ∏ 𝑘 ∈ 𝑍 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		iprodclim3.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		iprodclim3.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		iprodclim3.3	⊢ ( 𝜑 → ∃ 𝑛 ∈ 𝑍 ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) ⇝ 𝑦 ) )
4		iprodclim3.4	⊢ ( 𝜑 → 𝐹 ∈ dom ⇝ )
5		iprodclim3.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
6		iprodclim3.6	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑗 ) 𝐴 )
7		climdm	⊢ ( 𝐹 ∈ dom ⇝ ↔ 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) )
8	4 7	sylib	⊢ ( 𝜑 → 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) )
9		prodfc	⊢ ∏ 𝑚 ∈ 𝑍 ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) = ∏ 𝑘 ∈ 𝑍 𝐴
10		eqidd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) )
11	5	fmpttd	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) : 𝑍 ⟶ ℂ )
12	11	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ∈ ℂ )
13	1 2 3 10 12	iprod	⊢ ( 𝜑 → ∏ 𝑚 ∈ 𝑍 ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) = ( ⇝ ‘ seq 𝑀 ( · , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) ) )
14	9 13	eqtr3id	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑍 𝐴 = ( ⇝ ‘ seq 𝑀 ( · , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) ) )
15		seqex	⊢ seq 𝑀 ( · , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) ∈ V
16	15	a1i	⊢ ( 𝜑 → seq 𝑀 ( · , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) ∈ V )
17		fvres	⊢ ( 𝑚 ∈ ( 𝑀 ... 𝑗 ) → ( ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ↾ ( 𝑀 ... 𝑗 ) ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) )
18		fzssuz	⊢ ( 𝑀 ... 𝑗 ) ⊆ ( ℤ≥ ‘ 𝑀 )
19	18 1	sseqtrri	⊢ ( 𝑀 ... 𝑗 ) ⊆ 𝑍
20		resmpt	⊢ ( ( 𝑀 ... 𝑗 ) ⊆ 𝑍 → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ↾ ( 𝑀 ... 𝑗 ) ) = ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) ↦ 𝐴 ) )
21	19 20	ax-mp	⊢ ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ↾ ( 𝑀 ... 𝑗 ) ) = ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) ↦ 𝐴 )
22	21	fveq1i	⊢ ( ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ↾ ( 𝑀 ... 𝑗 ) ) ‘ 𝑚 ) = ( ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) ↦ 𝐴 ) ‘ 𝑚 )
23	17 22	eqtr3di	⊢ ( 𝑚 ∈ ( 𝑀 ... 𝑗 ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) ↦ 𝐴 ) ‘ 𝑚 ) )
24	23	prodeq2i	⊢ ∏ 𝑚 ∈ ( 𝑀 ... 𝑗 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) = ∏ 𝑚 ∈ ( 𝑀 ... 𝑗 ) ( ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) ↦ 𝐴 ) ‘ 𝑚 )
25		prodfc	⊢ ∏ 𝑚 ∈ ( 𝑀 ... 𝑗 ) ( ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) ↦ 𝐴 ) ‘ 𝑚 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑗 ) 𝐴
26	24 25	eqtri	⊢ ∏ 𝑚 ∈ ( 𝑀 ... 𝑗 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑗 ) 𝐴
27		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑚 ∈ ( 𝑀 ... 𝑗 ) ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) )
28		simpr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ 𝑍 )
29	28 1	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
30		elfzuz	⊢ ( 𝑚 ∈ ( 𝑀 ... 𝑗 ) → 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) )
31	30 1	eleqtrrdi	⊢ ( 𝑚 ∈ ( 𝑀 ... 𝑗 ) → 𝑚 ∈ 𝑍 )
32	31 12	sylan2	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝑀 ... 𝑗 ) ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ∈ ℂ )
33	32	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑚 ∈ ( 𝑀 ... 𝑗 ) ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ∈ ℂ )
34	27 29 33	fprodser	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ∏ 𝑚 ∈ ( 𝑀 ... 𝑗 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) = ( seq 𝑀 ( · , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) ‘ 𝑗 ) )
35	26 34	eqtr3id	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ∏ 𝑘 ∈ ( 𝑀 ... 𝑗 ) 𝐴 = ( seq 𝑀 ( · , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) ‘ 𝑗 ) )
36	6 35	eqtr2d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( seq 𝑀 ( · , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) ‘ 𝑗 ) = ( 𝐹 ‘ 𝑗 ) )
37	1 16 4 2 36	climeq	⊢ ( 𝜑 → ( seq 𝑀 ( · , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) ⇝ 𝑥 ↔ 𝐹 ⇝ 𝑥 ) )
38	37	iotabidv	⊢ ( 𝜑 → ( ℩ 𝑥 seq 𝑀 ( · , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) ⇝ 𝑥 ) = ( ℩ 𝑥 𝐹 ⇝ 𝑥 ) )
39		df-fv	⊢ ( ⇝ ‘ seq 𝑀 ( · , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) ) = ( ℩ 𝑥 seq 𝑀 ( · , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) ⇝ 𝑥 )
40		df-fv	⊢ ( ⇝ ‘ 𝐹 ) = ( ℩ 𝑥 𝐹 ⇝ 𝑥 )
41	38 39 40	3eqtr4g	⊢ ( 𝜑 → ( ⇝ ‘ seq 𝑀 ( · , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) ) = ( ⇝ ‘ 𝐹 ) )
42	14 41	eqtrd	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑍 𝐴 = ( ⇝ ‘ 𝐹 ) )
43	8 42	breqtrrd	⊢ ( 𝜑 → 𝐹 ⇝ ∏ 𝑘 ∈ 𝑍 𝐴 )