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

Metamath Proof Explorer

Theorem fsumre

Description: The real part of a sum. (Contributed by Paul Chapman, 9-Nov-2007) (Revised by Mario Carneiro, 25-Jul-2014)

Ref Expression
Hypotheses fsumre.1 ⊢ φ → A ∈ Fin
fsumre.2 ⊢ φ ∧ k ∈ A → B ∈ ℂ
Assertion fsumre ⊢ φ → ℜ ⁡ ∑ k ∈ A B = ∑ k ∈ A ℜ ⁡ B

Proof

Step Hyp Ref Expression
1 fsumre.1 ⊢ φ → A ∈ Fin
2 fsumre.2 ⊢ φ ∧ k ∈ A → B ∈ ℂ
3 ref ⊢ ℜ : ℂ ⟶ ℝ
4 ax-resscn ⊢ ℝ ⊆ ℂ
5 fss ⊢ ℜ : ℂ ⟶ ℝ ∧ ℝ ⊆ ℂ → ℜ : ℂ ⟶ ℂ
6 3 4 5 mp2an ⊢ ℜ : ℂ ⟶ ℂ
7 readd ⊢ x ∈ ℂ ∧ y ∈ ℂ → ℜ ⁡ x + y = ℜ ⁡ x + ℜ ⁡ y
8 1 2 6 7 fsumrelem ⊢ φ → ℜ ⁡ ∑ k ∈ A B = ∑ k ∈ A ℜ ⁡ B