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 ∪ Z B ∈ ℤ → ∑ k ∈ A ∪ Z B = ∑ k ∈ A B + ⦋ 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 ∪ Z B ∈ ℤ → A ∩ Z = ∅
6 eqidd ⊢ A ∈ Fin ∧ Z ∈ V ∧ Z ∉ A ∧ ∀ k ∈ A ∪ Z B ∈ ℤ → 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 ∪ Z B ∈ ℤ → A ∪ Z ∈ Fin
11 rspcsbela ⊢ x ∈ A ∪ Z ∧ ∀ k ∈ A ∪ Z B ∈ ℤ → ⦋ x / k⦌ B ∈ ℤ
12 11 expcom ⊢ ∀ k ∈ A ∪ Z B ∈ ℤ → x ∈ A ∪ Z → ⦋ x / k⦌ B ∈ ℤ
13 12 3ad2ant3 ⊢ A ∈ Fin ∧ Z ∈ V ∧ Z ∉ A ∧ ∀ k ∈ A ∪ Z B ∈ ℤ → x ∈ A ∪ Z → ⦋ x / k⦌ B ∈ ℤ
14 13 imp ⊢ A ∈ Fin ∧ Z ∈ V ∧ Z ∉ A ∧ ∀ k ∈ A ∪ Z B ∈ ℤ ∧ x ∈ A ∪ Z → ⦋ x / k⦌ B ∈ ℤ
15 14 zcnd ⊢ A ∈ Fin ∧ Z ∈ V ∧ Z ∉ A ∧ ∀ k ∈ A ∪ Z B ∈ ℤ ∧ x ∈ A ∪ Z → ⦋ x / k⦌ B ∈ ℂ
16 5 6 10 15 fsumsplit ⊢ A ∈ Fin ∧ Z ∈ V ∧ Z ∉ A ∧ ∀ k ∈ A ∪ Z B ∈ ℤ → ∑ x ∈ A ∪ Z ⦋ x / k⦌ B = ∑ x ∈ A ⦋ x / k⦌ B + ∑ x ∈ Z ⦋ x / k⦌ B
17 csbeq1a ⊢ k = x → B = ⦋ x / k⦌ B
18 nfcv ⊢ Ⅎ _ x B
19 nfcsb1v ⊢ Ⅎ _ k ⦋ x / k⦌ B
20 17 18 19 cbvsum ⊢ ∑ k ∈ A ∪ Z B = ∑ x ∈ A ∪ Z ⦋ x / k⦌ B
21 17 18 19 cbvsum ⊢ ∑ k ∈ A B = ∑ x ∈ A ⦋ x / k⦌ B
22 17 18 19 cbvsum ⊢ ∑ k ∈ Z B = ∑ x ∈ Z ⦋ x / k⦌ B
23 21 22 oveq12i ⊢ ∑ k ∈ A B + ∑ k ∈ Z B = ∑ x ∈ A ⦋ x / k⦌ B + ∑ x ∈ Z ⦋ x / k⦌ B
24 16 20 23 3eqtr4g ⊢ A ∈ Fin ∧ Z ∈ V ∧ Z ∉ A ∧ ∀ k ∈ A ∪ Z B ∈ ℤ → ∑ k ∈ A ∪ Z B = ∑ k ∈ A B + ∑ k ∈ Z B
25 simp2l ⊢ A ∈ Fin ∧ Z ∈ V ∧ Z ∉ A ∧ ∀ k ∈ A ∪ Z B ∈ ℤ → 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 ∪ Z B ∈ ℤ → Z ∈ Z
29 elun2 ⊢ Z ∈ Z → Z ∈ A ∪ Z
30 28 29 syl ⊢ A ∈ Fin ∧ Z ∈ V ∧ Z ∉ A ∧ ∀ k ∈ A ∪ Z B ∈ ℤ → Z ∈ A ∪ Z
31 simp3 ⊢ A ∈ Fin ∧ Z ∈ V ∧ Z ∉ A ∧ ∀ k ∈ A ∪ Z B ∈ ℤ → ∀ k ∈ A ∪ Z B ∈ ℤ
32 rspcsbela ⊢ Z ∈ A ∪ Z ∧ ∀ k ∈ A ∪ Z B ∈ ℤ → ⦋ Z / k⦌ B ∈ ℤ
33 30 31 32 syl2anc ⊢ A ∈ Fin ∧ Z ∈ V ∧ Z ∉ A ∧ ∀ k ∈ A ∪ Z B ∈ ℤ → ⦋ Z / k⦌ B ∈ ℤ
34 33 zcnd ⊢ A ∈ Fin ∧ Z ∈ V ∧ Z ∉ A ∧ ∀ k ∈ A ∪ Z B ∈ ℤ → ⦋ Z / k⦌ B ∈ ℂ
35 sumsns ⊢ Z ∈ V ∧ ⦋ Z / k⦌ B ∈ ℂ → ∑ k ∈ Z B = ⦋ Z / k⦌ B
36 25 34 35 syl2anc ⊢ A ∈ Fin ∧ Z ∈ V ∧ Z ∉ A ∧ ∀ k ∈ A ∪ Z B ∈ ℤ → ∑ k ∈ Z B = ⦋ Z / k⦌ B
37 36 oveq2d ⊢ A ∈ Fin ∧ Z ∈ V ∧ Z ∉ A ∧ ∀ k ∈ A ∪ Z B ∈ ℤ → ∑ k ∈ A B + ∑ k ∈ Z B = ∑ k ∈ A B + ⦋ Z / k⦌ B
38 24 37 eqtrd ⊢ A ∈ Fin ∧ Z ∈ V ∧ Z ∉ A ∧ ∀ k ∈ A ∪ Z B ∈ ℤ → ∑ k ∈ A ∪ Z B = ∑ k ∈ A B + ⦋ Z / k⦌ B