Theorem iprodcl

Description: The product of a non-trivially converging infinite sequence is a complex number. (Contributed by Scott Fenton, 18-Dec-2017)

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

Proof

Step	Hyp	Ref	Expression
1		iprodcl.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		iprodcl.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		iprodcl.3	⊢ ( 𝜑 → ∃ 𝑛 ∈ 𝑍 ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) )
4		iprodcl.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
5		iprodcl.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
6	1 2 3 4 5	iprod	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑍 𝐴 = ( ⇝ ‘ seq 𝑀 ( · , 𝐹 ) ) )
7		fclim	⊢ ⇝ : dom ⇝ ⟶ ℂ
8	4 5	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
9	1 3 8	ntrivcvg	⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) ∈ dom ⇝ )
10		ffvelrn	⊢ ( ( ⇝ : dom ⇝ ⟶ ℂ ∧ seq 𝑀 ( · , 𝐹 ) ∈ dom ⇝ ) → ( ⇝ ‘ seq 𝑀 ( · , 𝐹 ) ) ∈ ℂ )
11	7 9 10	sylancr	⊢ ( 𝜑 → ( ⇝ ‘ seq 𝑀 ( · , 𝐹 ) ) ∈ ℂ )
12	6 11	eqeltrd	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑍 𝐴 ∈ ℂ )