Metamath Proof Explorer


Theorem fsumsplitsndif

Description: Separate out a term in a finite sum by splitting the sum into two parts. (Contributed by Alexander van der Vekens, 31-Aug-2018)

Ref Expression
Assertion fsumsplitsndif ( ( 𝐴 ∈ Fin ∧ 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐵 ∈ ℤ ) → Σ 𝑘𝐴 𝐵 = ( Σ 𝑘 ∈ ( 𝐴 ∖ { 𝑋 } ) 𝐵 + 𝑋 / 𝑘 𝐵 ) )

Proof

Step Hyp Ref Expression
1 neldifsnd ( ( 𝐴 ∈ Fin ∧ 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐵 ∈ ℤ ) → ¬ 𝑋 ∈ ( 𝐴 ∖ { 𝑋 } ) )
2 disjsn ( ( ( 𝐴 ∖ { 𝑋 } ) ∩ { 𝑋 } ) = ∅ ↔ ¬ 𝑋 ∈ ( 𝐴 ∖ { 𝑋 } ) )
3 1 2 sylibr ( ( 𝐴 ∈ Fin ∧ 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐵 ∈ ℤ ) → ( ( 𝐴 ∖ { 𝑋 } ) ∩ { 𝑋 } ) = ∅ )
4 uncom ( ( 𝐴 ∖ { 𝑋 } ) ∪ { 𝑋 } ) = ( { 𝑋 } ∪ ( 𝐴 ∖ { 𝑋 } ) )
5 simp2 ( ( 𝐴 ∈ Fin ∧ 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐵 ∈ ℤ ) → 𝑋𝐴 )
6 5 snssd ( ( 𝐴 ∈ Fin ∧ 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐵 ∈ ℤ ) → { 𝑋 } ⊆ 𝐴 )
7 undif ( { 𝑋 } ⊆ 𝐴 ↔ ( { 𝑋 } ∪ ( 𝐴 ∖ { 𝑋 } ) ) = 𝐴 )
8 6 7 sylib ( ( 𝐴 ∈ Fin ∧ 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐵 ∈ ℤ ) → ( { 𝑋 } ∪ ( 𝐴 ∖ { 𝑋 } ) ) = 𝐴 )
9 4 8 eqtr2id ( ( 𝐴 ∈ Fin ∧ 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐵 ∈ ℤ ) → 𝐴 = ( ( 𝐴 ∖ { 𝑋 } ) ∪ { 𝑋 } ) )
10 simp1 ( ( 𝐴 ∈ Fin ∧ 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐵 ∈ ℤ ) → 𝐴 ∈ Fin )
11 rspcsbela ( ( 𝑥𝐴 ∧ ∀ 𝑘𝐴 𝐵 ∈ ℤ ) → 𝑥 / 𝑘 𝐵 ∈ ℤ )
12 11 zcnd ( ( 𝑥𝐴 ∧ ∀ 𝑘𝐴 𝐵 ∈ ℤ ) → 𝑥 / 𝑘 𝐵 ∈ ℂ )
13 12 expcom ( ∀ 𝑘𝐴 𝐵 ∈ ℤ → ( 𝑥𝐴 𝑥 / 𝑘 𝐵 ∈ ℂ ) )
14 13 3ad2ant3 ( ( 𝐴 ∈ Fin ∧ 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐵 ∈ ℤ ) → ( 𝑥𝐴 𝑥 / 𝑘 𝐵 ∈ ℂ ) )
15 14 imp ( ( ( 𝐴 ∈ Fin ∧ 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐵 ∈ ℤ ) ∧ 𝑥𝐴 ) → 𝑥 / 𝑘 𝐵 ∈ ℂ )
16 3 9 10 15 fsumsplit ( ( 𝐴 ∈ Fin ∧ 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐵 ∈ ℤ ) → Σ 𝑥𝐴 𝑥 / 𝑘 𝐵 = ( Σ 𝑥 ∈ ( 𝐴 ∖ { 𝑋 } ) 𝑥 / 𝑘 𝐵 + Σ 𝑥 ∈ { 𝑋 } 𝑥 / 𝑘 𝐵 ) )
17 nfcv 𝑥 𝐵
18 nfcsb1v 𝑘 𝑥 / 𝑘 𝐵
19 csbeq1a ( 𝑘 = 𝑥𝐵 = 𝑥 / 𝑘 𝐵 )
20 17 18 19 cbvsumi Σ 𝑘𝐴 𝐵 = Σ 𝑥𝐴 𝑥 / 𝑘 𝐵
21 17 18 19 cbvsumi Σ 𝑘 ∈ ( 𝐴 ∖ { 𝑋 } ) 𝐵 = Σ 𝑥 ∈ ( 𝐴 ∖ { 𝑋 } ) 𝑥 / 𝑘 𝐵
22 17 18 19 cbvsumi Σ 𝑘 ∈ { 𝑋 } 𝐵 = Σ 𝑥 ∈ { 𝑋 } 𝑥 / 𝑘 𝐵
23 21 22 oveq12i ( Σ 𝑘 ∈ ( 𝐴 ∖ { 𝑋 } ) 𝐵 + Σ 𝑘 ∈ { 𝑋 } 𝐵 ) = ( Σ 𝑥 ∈ ( 𝐴 ∖ { 𝑋 } ) 𝑥 / 𝑘 𝐵 + Σ 𝑥 ∈ { 𝑋 } 𝑥 / 𝑘 𝐵 )
24 16 20 23 3eqtr4g ( ( 𝐴 ∈ Fin ∧ 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐵 ∈ ℤ ) → Σ 𝑘𝐴 𝐵 = ( Σ 𝑘 ∈ ( 𝐴 ∖ { 𝑋 } ) 𝐵 + Σ 𝑘 ∈ { 𝑋 } 𝐵 ) )
25 rspcsbela ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐵 ∈ ℤ ) → 𝑋 / 𝑘 𝐵 ∈ ℤ )
26 25 zcnd ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐵 ∈ ℤ ) → 𝑋 / 𝑘 𝐵 ∈ ℂ )
27 26 3adant1 ( ( 𝐴 ∈ Fin ∧ 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐵 ∈ ℤ ) → 𝑋 / 𝑘 𝐵 ∈ ℂ )
28 sumsns ( ( 𝑋𝐴 𝑋 / 𝑘 𝐵 ∈ ℂ ) → Σ 𝑘 ∈ { 𝑋 } 𝐵 = 𝑋 / 𝑘 𝐵 )
29 5 27 28 syl2anc ( ( 𝐴 ∈ Fin ∧ 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐵 ∈ ℤ ) → Σ 𝑘 ∈ { 𝑋 } 𝐵 = 𝑋 / 𝑘 𝐵 )
30 29 oveq2d ( ( 𝐴 ∈ Fin ∧ 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐵 ∈ ℤ ) → ( Σ 𝑘 ∈ ( 𝐴 ∖ { 𝑋 } ) 𝐵 + Σ 𝑘 ∈ { 𝑋 } 𝐵 ) = ( Σ 𝑘 ∈ ( 𝐴 ∖ { 𝑋 } ) 𝐵 + 𝑋 / 𝑘 𝐵 ) )
31 24 30 eqtrd ( ( 𝐴 ∈ Fin ∧ 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐵 ∈ ℤ ) → Σ 𝑘𝐴 𝐵 = ( Σ 𝑘 ∈ ( 𝐴 ∖ { 𝑋 } ) 𝐵 + 𝑋 / 𝑘 𝐵 ) )