Step | Hyp | Ref
| Expression |
1 | | df-nel 2423 |
. . . . . . 7
⊢ (𝑍 ∉ 𝐴 ↔ ¬ 𝑍 ∈ 𝐴) |
2 | | disjsn 3621 |
. . . . . . 7
⊢ ((𝐴 ∩ {𝑍}) = ∅ ↔ ¬ 𝑍 ∈ 𝐴) |
3 | 1, 2 | sylbb2 137 |
. . . . . 6
⊢ (𝑍 ∉ 𝐴 → (𝐴 ∩ {𝑍}) = ∅) |
4 | 3 | adantl 275 |
. . . . 5
⊢ ((𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) → (𝐴 ∩ {𝑍}) = ∅) |
5 | 4 | 3ad2ant2 1004 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → (𝐴 ∩ {𝑍}) = ∅) |
6 | | eqidd 2158 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → (𝐴 ∪ {𝑍}) = (𝐴 ∪ {𝑍})) |
7 | | simp1 982 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → 𝐴 ∈ Fin) |
8 | | simp2l 1008 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → 𝑍 ∈ 𝑉) |
9 | | snfig 6759 |
. . . . . 6
⊢ (𝑍 ∈ 𝑉 → {𝑍} ∈ Fin) |
10 | 8, 9 | syl 14 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → {𝑍} ∈ Fin) |
11 | | unfidisj 6866 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ {𝑍} ∈ Fin ∧ (𝐴 ∩ {𝑍}) = ∅) → (𝐴 ∪ {𝑍}) ∈ Fin) |
12 | 7, 10, 5, 11 | syl3anc 1220 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → (𝐴 ∪ {𝑍}) ∈ Fin) |
13 | | rspcsbela 3090 |
. . . . . . . 8
⊢ ((𝑥 ∈ (𝐴 ∪ {𝑍}) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → ⦋𝑥 / 𝑘⦌𝐵 ∈ ℤ) |
14 | 13 | expcom 115 |
. . . . . . 7
⊢
(∀𝑘 ∈
(𝐴 ∪ {𝑍})𝐵 ∈ ℤ → (𝑥 ∈ (𝐴 ∪ {𝑍}) → ⦋𝑥 / 𝑘⦌𝐵 ∈ ℤ)) |
15 | 14 | 3ad2ant3 1005 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → (𝑥 ∈ (𝐴 ∪ {𝑍}) → ⦋𝑥 / 𝑘⦌𝐵 ∈ ℤ)) |
16 | 15 | imp 123 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) ∧ 𝑥 ∈ (𝐴 ∪ {𝑍})) → ⦋𝑥 / 𝑘⦌𝐵 ∈ ℤ) |
17 | 16 | zcnd 9287 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) ∧ 𝑥 ∈ (𝐴 ∪ {𝑍})) → ⦋𝑥 / 𝑘⦌𝐵 ∈ ℂ) |
18 | 5, 6, 12, 17 | fsumsplit 11304 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → Σ𝑥 ∈ (𝐴 ∪ {𝑍})⦋𝑥 / 𝑘⦌𝐵 = (Σ𝑥 ∈ 𝐴 ⦋𝑥 / 𝑘⦌𝐵 + Σ𝑥 ∈ {𝑍}⦋𝑥 / 𝑘⦌𝐵)) |
19 | | nfcv 2299 |
. . . 4
⊢
Ⅎ𝑥𝐵 |
20 | | nfcsb1v 3064 |
. . . 4
⊢
Ⅎ𝑘⦋𝑥 / 𝑘⦌𝐵 |
21 | | csbeq1a 3040 |
. . . 4
⊢ (𝑘 = 𝑥 → 𝐵 = ⦋𝑥 / 𝑘⦌𝐵) |
22 | 19, 20, 21 | cbvsumi 11259 |
. . 3
⊢
Σ𝑘 ∈
(𝐴 ∪ {𝑍})𝐵 = Σ𝑥 ∈ (𝐴 ∪ {𝑍})⦋𝑥 / 𝑘⦌𝐵 |
23 | 19, 20, 21 | cbvsumi 11259 |
. . . 4
⊢
Σ𝑘 ∈
𝐴 𝐵 = Σ𝑥 ∈ 𝐴 ⦋𝑥 / 𝑘⦌𝐵 |
24 | 19, 20, 21 | cbvsumi 11259 |
. . . 4
⊢
Σ𝑘 ∈
{𝑍}𝐵 = Σ𝑥 ∈ {𝑍}⦋𝑥 / 𝑘⦌𝐵 |
25 | 23, 24 | oveq12i 5836 |
. . 3
⊢
(Σ𝑘 ∈
𝐴 𝐵 + Σ𝑘 ∈ {𝑍}𝐵) = (Σ𝑥 ∈ 𝐴 ⦋𝑥 / 𝑘⦌𝐵 + Σ𝑥 ∈ {𝑍}⦋𝑥 / 𝑘⦌𝐵) |
26 | 18, 22, 25 | 3eqtr4g 2215 |
. 2
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → Σ𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 = (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ {𝑍}𝐵)) |
27 | | snidg 3589 |
. . . . . . . . 9
⊢ (𝑍 ∈ 𝑉 → 𝑍 ∈ {𝑍}) |
28 | 27 | adantr 274 |
. . . . . . . 8
⊢ ((𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) → 𝑍 ∈ {𝑍}) |
29 | 28 | 3ad2ant2 1004 |
. . . . . . 7
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → 𝑍 ∈ {𝑍}) |
30 | | elun2 3275 |
. . . . . . 7
⊢ (𝑍 ∈ {𝑍} → 𝑍 ∈ (𝐴 ∪ {𝑍})) |
31 | 29, 30 | syl 14 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → 𝑍 ∈ (𝐴 ∪ {𝑍})) |
32 | | simp3 984 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) |
33 | | rspcsbela 3090 |
. . . . . 6
⊢ ((𝑍 ∈ (𝐴 ∪ {𝑍}) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → ⦋𝑍 / 𝑘⦌𝐵 ∈ ℤ) |
34 | 31, 32, 33 | syl2anc 409 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → ⦋𝑍 / 𝑘⦌𝐵 ∈ ℤ) |
35 | 34 | zcnd 9287 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → ⦋𝑍 / 𝑘⦌𝐵 ∈ ℂ) |
36 | | sumsns 11312 |
. . . 4
⊢ ((𝑍 ∈ 𝑉 ∧ ⦋𝑍 / 𝑘⦌𝐵 ∈ ℂ) → Σ𝑘 ∈ {𝑍}𝐵 = ⦋𝑍 / 𝑘⦌𝐵) |
37 | 8, 35, 36 | syl2anc 409 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → Σ𝑘 ∈ {𝑍}𝐵 = ⦋𝑍 / 𝑘⦌𝐵) |
38 | 37 | oveq2d 5840 |
. 2
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ {𝑍}𝐵) = (Σ𝑘 ∈ 𝐴 𝐵 + ⦋𝑍 / 𝑘⦌𝐵)) |
39 | 26, 38 | eqtrd 2190 |
1
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → Σ𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 = (Σ𝑘 ∈ 𝐴 𝐵 + ⦋𝑍 / 𝑘⦌𝐵)) |