This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ Z = ℤ ≥ M
prodf.2 ⊢ φ → M ∈ ℤ
prodf.3 ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℂ
Assertion prodf ⊢ φ → seq M × F : Z ⟶ ℂ

Proof

Step Hyp Ref Expression
1 prodf.1 ⊢ Z = ℤ ≥ M
2 prodf.2 ⊢ φ → M ∈ ℤ
3 prodf.3 ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℂ
4 mulcl ⊢ k ∈ ℂ ∧ x ∈ ℂ → k ⁢ x ∈ ℂ
5 4 adantl ⊢ φ ∧ k ∈ ℂ ∧ x ∈ ℂ → k ⁢ x ∈ ℂ
6 1 2 3 5 seqf ⊢ φ → seq M × F : Z ⟶ ℂ