| Step | Hyp | Ref
| Expression |
| 1 | | df-nel 3047 |
. . . . . . 7
⊢ (𝑍 ∉ 𝐴 ↔ ¬ 𝑍 ∈ 𝐴) |
| 2 | | disjsn 4711 |
. . . . . . 7
⊢ ((𝐴 ∩ {𝑍}) = ∅ ↔ ¬ 𝑍 ∈ 𝐴) |
| 3 | 1, 2 | sylbb2 238 |
. . . . . 6
⊢ (𝑍 ∉ 𝐴 → (𝐴 ∩ {𝑍}) = ∅) |
| 4 | 3 | adantl 481 |
. . . . 5
⊢ ((𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) → (𝐴 ∩ {𝑍}) = ∅) |
| 5 | 4 | 3ad2ant2 1135 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → (𝐴 ∩ {𝑍}) = ∅) |
| 6 | | eqidd 2738 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → (𝐴 ∪ {𝑍}) = (𝐴 ∪ {𝑍})) |
| 7 | | snfi 9083 |
. . . . . 6
⊢ {𝑍} ∈ Fin |
| 8 | | unfi 9211 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ {𝑍} ∈ Fin) → (𝐴 ∪ {𝑍}) ∈ Fin) |
| 9 | 7, 8 | mpan2 691 |
. . . . 5
⊢ (𝐴 ∈ Fin → (𝐴 ∪ {𝑍}) ∈ Fin) |
| 10 | 9 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → (𝐴 ∪ {𝑍}) ∈ Fin) |
| 11 | | rspcsbela 4438 |
. . . . . . . 8
⊢ ((𝑥 ∈ (𝐴 ∪ {𝑍}) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → ⦋𝑥 / 𝑘⦌𝐵 ∈ ℤ) |
| 12 | 11 | expcom 413 |
. . . . . . 7
⊢
(∀𝑘 ∈
(𝐴 ∪ {𝑍})𝐵 ∈ ℤ → (𝑥 ∈ (𝐴 ∪ {𝑍}) → ⦋𝑥 / 𝑘⦌𝐵 ∈ ℤ)) |
| 13 | 12 | 3ad2ant3 1136 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → (𝑥 ∈ (𝐴 ∪ {𝑍}) → ⦋𝑥 / 𝑘⦌𝐵 ∈ ℤ)) |
| 14 | 13 | imp 406 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) ∧ 𝑥 ∈ (𝐴 ∪ {𝑍})) → ⦋𝑥 / 𝑘⦌𝐵 ∈ ℤ) |
| 15 | 14 | zcnd 12723 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) ∧ 𝑥 ∈ (𝐴 ∪ {𝑍})) → ⦋𝑥 / 𝑘⦌𝐵 ∈ ℂ) |
| 16 | 5, 6, 10, 15 | fsumsplit 15777 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → Σ𝑥 ∈ (𝐴 ∪ {𝑍})⦋𝑥 / 𝑘⦌𝐵 = (Σ𝑥 ∈ 𝐴 ⦋𝑥 / 𝑘⦌𝐵 + Σ𝑥 ∈ {𝑍}⦋𝑥 / 𝑘⦌𝐵)) |
| 17 | | csbeq1a 3913 |
. . . 4
⊢ (𝑘 = 𝑥 → 𝐵 = ⦋𝑥 / 𝑘⦌𝐵) |
| 18 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑥𝐵 |
| 19 | | nfcsb1v 3923 |
. . . 4
⊢
Ⅎ𝑘⦋𝑥 / 𝑘⦌𝐵 |
| 20 | 17, 18, 19 | cbvsum 15731 |
. . 3
⊢
Σ𝑘 ∈
(𝐴 ∪ {𝑍})𝐵 = Σ𝑥 ∈ (𝐴 ∪ {𝑍})⦋𝑥 / 𝑘⦌𝐵 |
| 21 | 17, 18, 19 | cbvsum 15731 |
. . . 4
⊢
Σ𝑘 ∈
𝐴 𝐵 = Σ𝑥 ∈ 𝐴 ⦋𝑥 / 𝑘⦌𝐵 |
| 22 | 17, 18, 19 | cbvsum 15731 |
. . . 4
⊢
Σ𝑘 ∈
{𝑍}𝐵 = Σ𝑥 ∈ {𝑍}⦋𝑥 / 𝑘⦌𝐵 |
| 23 | 21, 22 | oveq12i 7443 |
. . 3
⊢
(Σ𝑘 ∈
𝐴 𝐵 + Σ𝑘 ∈ {𝑍}𝐵) = (Σ𝑥 ∈ 𝐴 ⦋𝑥 / 𝑘⦌𝐵 + Σ𝑥 ∈ {𝑍}⦋𝑥 / 𝑘⦌𝐵) |
| 24 | 16, 20, 23 | 3eqtr4g 2802 |
. 2
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → Σ𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 = (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ {𝑍}𝐵)) |
| 25 | | simp2l 1200 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → 𝑍 ∈ 𝑉) |
| 26 | | snidg 4660 |
. . . . . . . . 9
⊢ (𝑍 ∈ 𝑉 → 𝑍 ∈ {𝑍}) |
| 27 | 26 | adantr 480 |
. . . . . . . 8
⊢ ((𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) → 𝑍 ∈ {𝑍}) |
| 28 | 27 | 3ad2ant2 1135 |
. . . . . . 7
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → 𝑍 ∈ {𝑍}) |
| 29 | | elun2 4183 |
. . . . . . 7
⊢ (𝑍 ∈ {𝑍} → 𝑍 ∈ (𝐴 ∪ {𝑍})) |
| 30 | 28, 29 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → 𝑍 ∈ (𝐴 ∪ {𝑍})) |
| 31 | | simp3 1139 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) |
| 32 | | rspcsbela 4438 |
. . . . . 6
⊢ ((𝑍 ∈ (𝐴 ∪ {𝑍}) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → ⦋𝑍 / 𝑘⦌𝐵 ∈ ℤ) |
| 33 | 30, 31, 32 | syl2anc 584 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → ⦋𝑍 / 𝑘⦌𝐵 ∈ ℤ) |
| 34 | 33 | zcnd 12723 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → ⦋𝑍 / 𝑘⦌𝐵 ∈ ℂ) |
| 35 | | sumsns 15786 |
. . . 4
⊢ ((𝑍 ∈ 𝑉 ∧ ⦋𝑍 / 𝑘⦌𝐵 ∈ ℂ) → Σ𝑘 ∈ {𝑍}𝐵 = ⦋𝑍 / 𝑘⦌𝐵) |
| 36 | 25, 34, 35 | syl2anc 584 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → Σ𝑘 ∈ {𝑍}𝐵 = ⦋𝑍 / 𝑘⦌𝐵) |
| 37 | 36 | oveq2d 7447 |
. 2
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ {𝑍}𝐵) = (Σ𝑘 ∈ 𝐴 𝐵 + ⦋𝑍 / 𝑘⦌𝐵)) |
| 38 | 24, 37 | eqtrd 2777 |
1
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → Σ𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 = (Σ𝑘 ∈ 𝐴 𝐵 + ⦋𝑍 / 𝑘⦌𝐵)) |