Theorem prodf

Description: An infinite product of complex terms is a function from an upper set of integers to CC . (Contributed by Scott Fenton, 4-Dec-2017)

	Ref	Expression
Hypotheses	prodf.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	prodf.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	prodf.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
Assertion	prodf	⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) : 𝑍 ⟶ ℂ )

Proof

Step	Hyp	Ref	Expression
1		prodf.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		prodf.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		prodf.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
4		mulcl	⊢ ( ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑘 · 𝑥 ) ∈ ℂ )
5	4	adantl	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝑘 · 𝑥 ) ∈ ℂ )
6	1 2 3 5	seqf	⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) : 𝑍 ⟶ ℂ )