Step | Hyp | Ref
| Expression |
1 | | df-nel 2436 |
. . . . . . 7
⊢ (𝑍 ∉ 𝐴 ↔ ¬ 𝑍 ∈ 𝐴) |
2 | | disjsn 3645 |
. . . . . . 7
⊢ ((𝐴 ∩ {𝑍}) = ∅ ↔ ¬ 𝑍 ∈ 𝐴) |
3 | 1, 2 | sylbb2 137 |
. . . . . 6
⊢ (𝑍 ∉ 𝐴 → (𝐴 ∩ {𝑍}) = ∅) |
4 | 3 | adantl 275 |
. . . . 5
⊢ ((𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) → (𝐴 ∩ {𝑍}) = ∅) |
5 | 4 | 3ad2ant2 1014 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → (𝐴 ∩ {𝑍}) = ∅) |
6 | | eqidd 2171 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → (𝐴 ∪ {𝑍}) = (𝐴 ∪ {𝑍})) |
7 | | simp1 992 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → 𝐴 ∈ Fin) |
8 | | simp2l 1018 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → 𝑍 ∈ 𝑉) |
9 | | snfig 6792 |
. . . . . 6
⊢ (𝑍 ∈ 𝑉 → {𝑍} ∈ Fin) |
10 | 8, 9 | syl 14 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → {𝑍} ∈ Fin) |
11 | | unfidisj 6899 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ {𝑍} ∈ Fin ∧ (𝐴 ∩ {𝑍}) = ∅) → (𝐴 ∪ {𝑍}) ∈ Fin) |
12 | 7, 10, 5, 11 | syl3anc 1233 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → (𝐴 ∪ {𝑍}) ∈ Fin) |
13 | | rspcsbela 3108 |
. . . . . . . 8
⊢ ((𝑥 ∈ (𝐴 ∪ {𝑍}) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → ⦋𝑥 / 𝑘⦌𝐵 ∈ ℤ) |
14 | 13 | expcom 115 |
. . . . . . 7
⊢
(∀𝑘 ∈
(𝐴 ∪ {𝑍})𝐵 ∈ ℤ → (𝑥 ∈ (𝐴 ∪ {𝑍}) → ⦋𝑥 / 𝑘⦌𝐵 ∈ ℤ)) |
15 | 14 | 3ad2ant3 1015 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → (𝑥 ∈ (𝐴 ∪ {𝑍}) → ⦋𝑥 / 𝑘⦌𝐵 ∈ ℤ)) |
16 | 15 | imp 123 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) ∧ 𝑥 ∈ (𝐴 ∪ {𝑍})) → ⦋𝑥 / 𝑘⦌𝐵 ∈ ℤ) |
17 | 16 | zcnd 9335 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) ∧ 𝑥 ∈ (𝐴 ∪ {𝑍})) → ⦋𝑥 / 𝑘⦌𝐵 ∈ ℂ) |
18 | 5, 6, 12, 17 | fsumsplit 11370 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → Σ𝑥 ∈ (𝐴 ∪ {𝑍})⦋𝑥 / 𝑘⦌𝐵 = (Σ𝑥 ∈ 𝐴 ⦋𝑥 / 𝑘⦌𝐵 + Σ𝑥 ∈ {𝑍}⦋𝑥 / 𝑘⦌𝐵)) |
19 | | nfcv 2312 |
. . . 4
⊢
Ⅎ𝑥𝐵 |
20 | | nfcsb1v 3082 |
. . . 4
⊢
Ⅎ𝑘⦋𝑥 / 𝑘⦌𝐵 |
21 | | csbeq1a 3058 |
. . . 4
⊢ (𝑘 = 𝑥 → 𝐵 = ⦋𝑥 / 𝑘⦌𝐵) |
22 | 19, 20, 21 | cbvsumi 11325 |
. . 3
⊢
Σ𝑘 ∈
(𝐴 ∪ {𝑍})𝐵 = Σ𝑥 ∈ (𝐴 ∪ {𝑍})⦋𝑥 / 𝑘⦌𝐵 |
23 | 19, 20, 21 | cbvsumi 11325 |
. . . 4
⊢
Σ𝑘 ∈
𝐴 𝐵 = Σ𝑥 ∈ 𝐴 ⦋𝑥 / 𝑘⦌𝐵 |
24 | 19, 20, 21 | cbvsumi 11325 |
. . . 4
⊢
Σ𝑘 ∈
{𝑍}𝐵 = Σ𝑥 ∈ {𝑍}⦋𝑥 / 𝑘⦌𝐵 |
25 | 23, 24 | oveq12i 5865 |
. . 3
⊢
(Σ𝑘 ∈
𝐴 𝐵 + Σ𝑘 ∈ {𝑍}𝐵) = (Σ𝑥 ∈ 𝐴 ⦋𝑥 / 𝑘⦌𝐵 + Σ𝑥 ∈ {𝑍}⦋𝑥 / 𝑘⦌𝐵) |
26 | 18, 22, 25 | 3eqtr4g 2228 |
. 2
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → Σ𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 = (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ {𝑍}𝐵)) |
27 | | snidg 3612 |
. . . . . . . . 9
⊢ (𝑍 ∈ 𝑉 → 𝑍 ∈ {𝑍}) |
28 | 27 | adantr 274 |
. . . . . . . 8
⊢ ((𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) → 𝑍 ∈ {𝑍}) |
29 | 28 | 3ad2ant2 1014 |
. . . . . . 7
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → 𝑍 ∈ {𝑍}) |
30 | | elun2 3295 |
. . . . . . 7
⊢ (𝑍 ∈ {𝑍} → 𝑍 ∈ (𝐴 ∪ {𝑍})) |
31 | 29, 30 | syl 14 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → 𝑍 ∈ (𝐴 ∪ {𝑍})) |
32 | | simp3 994 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) |
33 | | rspcsbela 3108 |
. . . . . 6
⊢ ((𝑍 ∈ (𝐴 ∪ {𝑍}) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → ⦋𝑍 / 𝑘⦌𝐵 ∈ ℤ) |
34 | 31, 32, 33 | syl2anc 409 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → ⦋𝑍 / 𝑘⦌𝐵 ∈ ℤ) |
35 | 34 | zcnd 9335 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → ⦋𝑍 / 𝑘⦌𝐵 ∈ ℂ) |
36 | | sumsns 11378 |
. . . 4
⊢ ((𝑍 ∈ 𝑉 ∧ ⦋𝑍 / 𝑘⦌𝐵 ∈ ℂ) → Σ𝑘 ∈ {𝑍}𝐵 = ⦋𝑍 / 𝑘⦌𝐵) |
37 | 8, 35, 36 | syl2anc 409 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → Σ𝑘 ∈ {𝑍}𝐵 = ⦋𝑍 / 𝑘⦌𝐵) |
38 | 37 | oveq2d 5869 |
. 2
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ {𝑍}𝐵) = (Σ𝑘 ∈ 𝐴 𝐵 + ⦋𝑍 / 𝑘⦌𝐵)) |
39 | 26, 38 | eqtrd 2203 |
1
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → Σ𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 = (Σ𝑘 ∈ 𝐴 𝐵 + ⦋𝑍 / 𝑘⦌𝐵)) |