Theorem iprodclim2

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

	Ref	Expression
Hypotheses	iprodclim.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	iprodclim.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	iprodclim.3	⊢ ( 𝜑 → ∃ 𝑛 ∈ 𝑍 ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) )
	iprodclim.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
	iprodclim.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
Assertion	iprodclim2	⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) ⇝ ∏ 𝑘 ∈ 𝑍 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		iprodclim.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		iprodclim.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		iprodclim.3	⊢ ( 𝜑 → ∃ 𝑛 ∈ 𝑍 ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) )
4		iprodclim.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
5		iprodclim.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
6	4 5	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
7	1 3 6	ntrivcvg	⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) ∈ dom ⇝ )
8		climdm	⊢ ( seq 𝑀 ( · , 𝐹 ) ∈ dom ⇝ ↔ seq 𝑀 ( · , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑀 ( · , 𝐹 ) ) )
9	7 8	sylib	⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑀 ( · , 𝐹 ) ) )
10	1 2 3 4 5	iprod	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑍 𝐴 = ( ⇝ ‘ seq 𝑀 ( · , 𝐹 ) ) )
11	9 10	breqtrrd	⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) ⇝ ∏ 𝑘 ∈ 𝑍 𝐴 )