Metamath Proof Explorer

Theorem fsumsplitsnun

Description: Separate out a term in a finite sum by splitting the sum into two parts. (Contributed by Alexander van der Vekens, 1-Sep-2018) (Revised by AV, 17-Dec-2021)

Ref Expression
Assertion fsumsplitsnun ⊢A∈Fin∧Z∈V∧Z∉A∧∀k∈A∪ZB∈ℤ→∑k∈A∪ZB=∑k∈AB+⦋Z/k⦌B

Proof

Step Hyp Ref Expression
1 df-nel ⊢Z∉A↔¬Z∈A
2 disjsn ⊢A∩Z=∅↔¬Z∈A
3 1 2 sylbb2 ⊢Z∉A→A∩Z=∅
4 3 adantl ⊢Z∈V∧Z∉A→A∩Z=∅
5 4 3ad2ant2 ⊢A∈Fin∧Z∈V∧Z∉A∧∀k∈A∪ZB∈ℤ→A∩Z=∅
6 eqidd ⊢A∈Fin∧Z∈V∧Z∉A∧∀k∈A∪ZB∈ℤ→A∪Z=A∪Z
7 snfi ⊢Z∈Fin
8 unfi ⊢A∈Fin∧Z∈Fin→A∪Z∈Fin
9 7 8 mpan2 ⊢A∈Fin→A∪Z∈Fin
10 9 3ad2ant1 ⊢A∈Fin∧Z∈V∧Z∉A∧∀k∈A∪ZB∈ℤ→A∪Z∈Fin
11 rspcsbela ⊢x∈A∪Z∧∀k∈A∪ZB∈ℤ→⦋x/k⦌B∈ℤ
12 11 expcom ⊢∀k∈A∪ZB∈ℤ→x∈A∪Z→⦋x/k⦌B∈ℤ
13 12 3ad2ant3 ⊢A∈Fin∧Z∈V∧Z∉A∧∀k∈A∪ZB∈ℤ→x∈A∪Z→⦋x/k⦌B∈ℤ
14 13 imp ⊢A∈Fin∧Z∈V∧Z∉A∧∀k∈A∪ZB∈ℤ∧x∈A∪Z→⦋x/k⦌B∈ℤ
15 14 zcnd ⊢A∈Fin∧Z∈V∧Z∉A∧∀k∈A∪ZB∈ℤ∧x∈A∪Z→⦋x/k⦌B∈ℂ
16 5 6 10 15 fsumsplit ⊢A∈Fin∧Z∈V∧Z∉A∧∀k∈A∪ZB∈ℤ→∑x∈A∪Z⦋x/k⦌B=∑x∈A⦋x/k⦌B+∑x∈Z⦋x/k⦌B
17 nfcv ⊢Ⅎ_xB
18 nfcsb1v ⊢Ⅎ_k⦋x/k⦌B
19 csbeq1a ⊢k=x→B=⦋x/k⦌B
20 17 18 19 cbvsumi ⊢∑k∈A∪ZB=∑x∈A∪Z⦋x/k⦌B
21 17 18 19 cbvsumi ⊢∑k∈AB=∑x∈A⦋x/k⦌B
22 17 18 19 cbvsumi ⊢∑k∈ZB=∑x∈Z⦋x/k⦌B
23 21 22 oveq12i ⊢∑k∈AB+∑k∈ZB=∑x∈A⦋x/k⦌B+∑x∈Z⦋x/k⦌B
24 16 20 23 3eqtr4g ⊢A∈Fin∧Z∈V∧Z∉A∧∀k∈A∪ZB∈ℤ→∑k∈A∪ZB=∑k∈AB+∑k∈ZB
25 simp2l ⊢A∈Fin∧Z∈V∧Z∉A∧∀k∈A∪ZB∈ℤ→Z∈V
26 snidg ⊢Z∈V→Z∈Z
27 26 adantr ⊢Z∈V∧Z∉A→Z∈Z
28 27 3ad2ant2 ⊢A∈Fin∧Z∈V∧Z∉A∧∀k∈A∪ZB∈ℤ→Z∈Z
29 elun2 ⊢Z∈Z→Z∈A∪Z
30 28 29 syl ⊢A∈Fin∧Z∈V∧Z∉A∧∀k∈A∪ZB∈ℤ→Z∈A∪Z
31 simp3 ⊢A∈Fin∧Z∈V∧Z∉A∧∀k∈A∪ZB∈ℤ→∀k∈A∪ZB∈ℤ
32 rspcsbela ⊢Z∈A∪Z∧∀k∈A∪ZB∈ℤ→⦋Z/k⦌B∈ℤ
33 30 31 32 syl2anc ⊢A∈Fin∧Z∈V∧Z∉A∧∀k∈A∪ZB∈ℤ→⦋Z/k⦌B∈ℤ
34 33 zcnd ⊢A∈Fin∧Z∈V∧Z∉A∧∀k∈A∪ZB∈ℤ→⦋Z/k⦌B∈ℂ
35 sumsns ⊢Z∈V∧⦋Z/k⦌B∈ℂ→∑k∈ZB=⦋Z/k⦌B
36 25 34 35 syl2anc ⊢A∈Fin∧Z∈V∧Z∉A∧∀k∈A∪ZB∈ℤ→∑k∈ZB=⦋Z/k⦌B
37 36 oveq2d ⊢A∈Fin∧Z∈V∧Z∉A∧∀k∈A∪ZB∈ℤ→∑k∈AB+∑k∈ZB=∑k∈AB+⦋Z/k⦌B
38 24 37 eqtrd ⊢A∈Fin∧Z∈V∧Z∉A∧∀k∈A∪ZB∈ℤ→∑k∈A∪ZB=∑k∈AB+⦋Z/k⦌B