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

Metamath Proof Explorer

Theorem fsumcl

Description: Closure of a finite sum of complex numbers A ( k ) . (Contributed by NM, 9-Nov-2005) (Revised by Mario Carneiro, 22-Apr-2014)

Ref Expression
Hypotheses fsumcl.1 ⊢ φ → A ∈ Fin
fsumcl.2 ⊢ φ ∧ k ∈ A → B ∈ ℂ
Assertion fsumcl ⊢ φ → ∑ k ∈ A B ∈ ℂ

Proof

Step Hyp Ref Expression
1 fsumcl.1 ⊢ φ → A ∈ Fin
2 fsumcl.2 ⊢ φ ∧ k ∈ A → B ∈ ℂ
3 ssidd ⊢ φ → ℂ ⊆ ℂ
4 addcl ⊢ x ∈ ℂ ∧ y ∈ ℂ → x + y ∈ ℂ
5 4 adantl ⊢ φ ∧ x ∈ ℂ ∧ y ∈ ℂ → x + y ∈ ℂ
6 0cnd ⊢ φ → 0 ∈ ℂ
7 3 5 1 2 6 fsumcllem ⊢ φ → ∑ k ∈ A B ∈ ℂ