Metamath Proof Explorer

Theorem fsumdifsnconst

Description: The sum of constant terms ( k is not free in C ) over an index set excluding a singleton. (Contributed by AV, 7-Jan-2022)

Ref Expression
Assertion fsumdifsnconst ⊢ A ∈ Fin ∧ B ∈ A ∧ C ∈ ℂ → ∑ k ∈ A ∖ B C = A − 1 ⁢ C

Proof

Step Hyp Ref Expression
1 diffi ⊢ A ∈ Fin → A ∖ B ∈ Fin
2 1 anim1i ⊢ A ∈ Fin ∧ C ∈ ℂ → A ∖ B ∈ Fin ∧ C ∈ ℂ
3 2 3adant2 ⊢ A ∈ Fin ∧ B ∈ A ∧ C ∈ ℂ → A ∖ B ∈ Fin ∧ C ∈ ℂ
4 fsumconst ⊢ A ∖ B ∈ Fin ∧ C ∈ ℂ → ∑ k ∈ A ∖ B C = A ∖ B ⁢ C
5 3 4 syl ⊢ A ∈ Fin ∧ B ∈ A ∧ C ∈ ℂ → ∑ k ∈ A ∖ B C = A ∖ B ⁢ C
6 hashdifsn ⊢ A ∈ Fin ∧ B ∈ A → A ∖ B = A − 1
7 6 3adant3 ⊢ A ∈ Fin ∧ B ∈ A ∧ C ∈ ℂ → A ∖ B = A − 1
8 7 oveq1d ⊢ A ∈ Fin ∧ B ∈ A ∧ C ∈ ℂ → A ∖ B ⁢ C = A − 1 ⁢ C
9 5 8 eqtrd ⊢ A ∈ Fin ∧ B ∈ A ∧ C ∈ ℂ → ∑ k ∈ A ∖ B C = A − 1 ⁢ C