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

Metamath Proof Explorer

Theorem fsumdivc

Description: A finite sum divided by a constant. (Contributed by NM, 2-Jan-2006) (Revised by Mario Carneiro, 24-Apr-2014)

Ref Expression
Hypotheses fsummulc2.1 ⊢ φ → A ∈ Fin
fsummulc2.2 ⊢ φ → C ∈ ℂ
fsummulc2.3 ⊢ φ ∧ k ∈ A → B ∈ ℂ
fsumdivc.4 ⊢ φ → C ≠ 0
Assertion fsumdivc ⊢ φ → ∑ k ∈ A B C = ∑ k ∈ A B C

Proof

Step Hyp Ref Expression
1 fsummulc2.1 ⊢ φ → A ∈ Fin
2 fsummulc2.2 ⊢ φ → C ∈ ℂ
3 fsummulc2.3 ⊢ φ ∧ k ∈ A → B ∈ ℂ
4 fsumdivc.4 ⊢ φ → C ≠ 0
5 2 4 reccld ⊢ φ → 1 C ∈ ℂ
6 1 5 3 fsummulc1 ⊢ φ → ∑ k ∈ A B ⁢ 1 C = ∑ k ∈ A B ⁢ 1 C
7 1 3 fsumcl ⊢ φ → ∑ k ∈ A B ∈ ℂ
8 7 2 4 divrecd ⊢ φ → ∑ k ∈ A B C = ∑ k ∈ A B ⁢ 1 C
9 2 adantr ⊢ φ ∧ k ∈ A → C ∈ ℂ
10 4 adantr ⊢ φ ∧ k ∈ A → C ≠ 0
11 3 9 10 divrecd ⊢ φ ∧ k ∈ A → B C = B ⁢ 1 C
12 11 sumeq2dv ⊢ φ → ∑ k ∈ A B C = ∑ k ∈ A B ⁢ 1 C
13 6 8 12 3eqtr4d ⊢ φ → ∑ k ∈ A B C = ∑ k ∈ A B C