Step | Hyp | Ref
| Expression |
1 | | sumeq1 14267 |
. . 3
⊢ (𝑥 = ∅ → Σ𝑘 ∈ 𝑥 𝐵 = Σ𝑘 ∈ ∅ 𝐵) |
2 | 1 | breq2d 4595 |
. 2
⊢ (𝑥 = ∅ → (2 ∥
Σ𝑘 ∈ 𝑥 𝐵 ↔ 2 ∥ Σ𝑘 ∈ ∅ 𝐵)) |
3 | | sumeq1 14267 |
. . 3
⊢ (𝑥 = 𝑦 → Σ𝑘 ∈ 𝑥 𝐵 = Σ𝑘 ∈ 𝑦 𝐵) |
4 | 3 | breq2d 4595 |
. 2
⊢ (𝑥 = 𝑦 → (2 ∥ Σ𝑘 ∈ 𝑥 𝐵 ↔ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵)) |
5 | | sumeq1 14267 |
. . 3
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → Σ𝑘 ∈ 𝑥 𝐵 = Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵) |
6 | 5 | breq2d 4595 |
. 2
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (2 ∥ Σ𝑘 ∈ 𝑥 𝐵 ↔ 2 ∥ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵)) |
7 | | sumeq1 14267 |
. . 3
⊢ (𝑥 = 𝐴 → Σ𝑘 ∈ 𝑥 𝐵 = Σ𝑘 ∈ 𝐴 𝐵) |
8 | 7 | breq2d 4595 |
. 2
⊢ (𝑥 = 𝐴 → (2 ∥ Σ𝑘 ∈ 𝑥 𝐵 ↔ 2 ∥ Σ𝑘 ∈ 𝐴 𝐵)) |
9 | | z0even 14941 |
. . . 4
⊢ 2 ∥
0 |
10 | | sum0 14299 |
. . . 4
⊢
Σ𝑘 ∈
∅ 𝐵 =
0 |
11 | 9, 10 | breqtrri 4610 |
. . 3
⊢ 2 ∥
Σ𝑘 ∈ ∅
𝐵 |
12 | 11 | a1i 11 |
. 2
⊢ (𝜑 → 2 ∥ Σ𝑘 ∈ ∅ 𝐵) |
13 | | 2z 11286 |
. . . . . . . 8
⊢ 2 ∈
ℤ |
14 | 13 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 2 ∈ ℤ) |
15 | | sumeven.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ Fin) |
16 | | ssfi 8065 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ Fin ∧ 𝑦 ⊆ 𝐴) → 𝑦 ∈ Fin) |
17 | 16 | expcom 450 |
. . . . . . . . . 10
⊢ (𝑦 ⊆ 𝐴 → (𝐴 ∈ Fin → 𝑦 ∈ Fin)) |
18 | 17 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → (𝐴 ∈ Fin → 𝑦 ∈ Fin)) |
19 | 15, 18 | mpan9 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑦 ∈ Fin) |
20 | | simpll 786 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝑦) → 𝜑) |
21 | | ssel 3562 |
. . . . . . . . . . . 12
⊢ (𝑦 ⊆ 𝐴 → (𝑘 ∈ 𝑦 → 𝑘 ∈ 𝐴)) |
22 | 21 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → (𝑘 ∈ 𝑦 → 𝑘 ∈ 𝐴)) |
23 | 22 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝑘 ∈ 𝑦 → 𝑘 ∈ 𝐴)) |
24 | 23 | imp 444 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ 𝐴) |
25 | | sumeven.b |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℤ) |
26 | 20, 24, 25 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝑦) → 𝐵 ∈ ℤ) |
27 | 19, 26 | fsumzcl 14313 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → Σ𝑘 ∈ 𝑦 𝐵 ∈ ℤ) |
28 | | eldifi 3694 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (𝐴 ∖ 𝑦) → 𝑧 ∈ 𝐴) |
29 | 28 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → 𝑧 ∈ 𝐴) |
30 | 29 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑧 ∈ 𝐴) |
31 | 25 | adantlr 747 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℤ) |
32 | 31 | ralrimiva 2949 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℤ) |
33 | | rspcsbela 3958 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ ℤ) → ⦋𝑧 / 𝑘⦌𝐵 ∈ ℤ) |
34 | 30, 32, 33 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ⦋𝑧 / 𝑘⦌𝐵 ∈ ℤ) |
35 | 14, 27, 34 | 3jca 1235 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (2 ∈ ℤ ∧
Σ𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ ⦋𝑧 / 𝑘⦌𝐵 ∈ ℤ)) |
36 | 35 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → (2 ∈ ℤ ∧
Σ𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ ⦋𝑧 / 𝑘⦌𝐵 ∈ ℤ)) |
37 | | sumeven.e |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 2 ∥ 𝐵) |
38 | 37 | ralrimiva 2949 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 2 ∥ 𝐵) |
39 | | nfcv 2751 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘2 |
40 | | nfcv 2751 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘
∥ |
41 | | nfcsb1v 3515 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘⦋𝑧 / 𝑘⦌𝐵 |
42 | 39, 40, 41 | nfbr 4629 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘2 ∥
⦋𝑧 / 𝑘⦌𝐵 |
43 | | csbeq1a 3508 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑘⦌𝐵) |
44 | 43 | breq2d 4595 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑧 → (2 ∥ 𝐵 ↔ 2 ∥ ⦋𝑧 / 𝑘⦌𝐵)) |
45 | 42, 44 | rspc 3276 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 2 ∥ 𝐵 → 2 ∥ ⦋𝑧 / 𝑘⦌𝐵)) |
46 | 28, 38, 45 | syl2imc 40 |
. . . . . . . . 9
⊢ (𝜑 → (𝑧 ∈ (𝐴 ∖ 𝑦) → 2 ∥ ⦋𝑧 / 𝑘⦌𝐵)) |
47 | 46 | a1d 25 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ⊆ 𝐴 → (𝑧 ∈ (𝐴 ∖ 𝑦) → 2 ∥ ⦋𝑧 / 𝑘⦌𝐵))) |
48 | 47 | imp32 448 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 2 ∥ ⦋𝑧 / 𝑘⦌𝐵) |
49 | 48 | anim1i 590 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → (2 ∥ ⦋𝑧 / 𝑘⦌𝐵 ∧ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵)) |
50 | 49 | ancomd 466 |
. . . . 5
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → (2 ∥ Σ𝑘 ∈ 𝑦 𝐵 ∧ 2 ∥ ⦋𝑧 / 𝑘⦌𝐵)) |
51 | | dvds2add 14853 |
. . . . 5
⊢ ((2
∈ ℤ ∧ Σ𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ ⦋𝑧 / 𝑘⦌𝐵 ∈ ℤ) → ((2 ∥
Σ𝑘 ∈ 𝑦 𝐵 ∧ 2 ∥ ⦋𝑧 / 𝑘⦌𝐵) → 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵))) |
52 | 36, 50, 51 | sylc 63 |
. . . 4
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵)) |
53 | 16 | ex 449 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Fin → (𝑦 ⊆ 𝐴 → 𝑦 ∈ Fin)) |
54 | 15, 53 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑦 ⊆ 𝐴 → 𝑦 ∈ Fin)) |
55 | 54 | com12 32 |
. . . . . . . 8
⊢ (𝑦 ⊆ 𝐴 → (𝜑 → 𝑦 ∈ Fin)) |
56 | 55 | adantr 480 |
. . . . . . 7
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → (𝜑 → 𝑦 ∈ Fin)) |
57 | 56 | impcom 445 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑦 ∈ Fin) |
58 | | eldif 3550 |
. . . . . . . . 9
⊢ (𝑧 ∈ (𝐴 ∖ 𝑦) ↔ (𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦)) |
59 | | df-nel 2783 |
. . . . . . . . . 10
⊢ (𝑧 ∉ 𝑦 ↔ ¬ 𝑧 ∈ 𝑦) |
60 | 59 | biimpri 217 |
. . . . . . . . 9
⊢ (¬
𝑧 ∈ 𝑦 → 𝑧 ∉ 𝑦) |
61 | 58, 60 | simplbiim 657 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝐴 ∖ 𝑦) → 𝑧 ∉ 𝑦) |
62 | 61 | adantl 481 |
. . . . . . 7
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → 𝑧 ∉ 𝑦) |
63 | 62 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑧 ∉ 𝑦) |
64 | | simpll 786 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ (𝑦 ∪ {𝑧})) → 𝜑) |
65 | | elun 3715 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (𝑦 ∪ {𝑧}) ↔ (𝑘 ∈ 𝑦 ∨ 𝑘 ∈ {𝑧})) |
66 | 22 | com12 32 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ 𝑦 → ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → 𝑘 ∈ 𝐴)) |
67 | | elsni 4142 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ {𝑧} → 𝑘 = 𝑧) |
68 | | eleq1 2676 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑧 → (𝑘 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)) |
69 | 29, 68 | syl5ibr 235 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑧 → ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → 𝑘 ∈ 𝐴)) |
70 | 67, 69 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ {𝑧} → ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → 𝑘 ∈ 𝐴)) |
71 | 66, 70 | jaoi 393 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ 𝑦 ∨ 𝑘 ∈ {𝑧}) → ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → 𝑘 ∈ 𝐴)) |
72 | 71 | com12 32 |
. . . . . . . . . . 11
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → ((𝑘 ∈ 𝑦 ∨ 𝑘 ∈ {𝑧}) → 𝑘 ∈ 𝐴)) |
73 | 65, 72 | syl5bi 231 |
. . . . . . . . . 10
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → (𝑘 ∈ (𝑦 ∪ {𝑧}) → 𝑘 ∈ 𝐴)) |
74 | 73 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝑘 ∈ (𝑦 ∪ {𝑧}) → 𝑘 ∈ 𝐴)) |
75 | 74 | imp 444 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ (𝑦 ∪ {𝑧})) → 𝑘 ∈ 𝐴) |
76 | 64, 75, 25 | syl2anc 691 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ (𝑦 ∪ {𝑧})) → 𝐵 ∈ ℤ) |
77 | 76 | ralrimiva 2949 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ∀𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ ℤ) |
78 | | fsumsplitsnun 14328 |
. . . . . 6
⊢ ((𝑦 ∈ Fin ∧ 𝑧 ∉ 𝑦 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ ℤ) → Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 = (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵)) |
79 | 57, 63, 77, 78 | syl3anc 1318 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 = (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵)) |
80 | 79 | adantr 480 |
. . . 4
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 = (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵)) |
81 | 52, 80 | breqtrrd 4611 |
. . 3
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → 2 ∥ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵) |
82 | 81 | ex 449 |
. 2
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (2 ∥ Σ𝑘 ∈ 𝑦 𝐵 → 2 ∥ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵)) |
83 | 2, 4, 6, 8, 12, 82, 15 | findcard2d 8087 |
1
⊢ (𝜑 → 2 ∥ Σ𝑘 ∈ 𝐴 𝐵) |