Step | Hyp | Ref
| Expression |
1 | | fveq2 6674 |
. . . . 5
⊢ (𝑥 = ∅ →
(♯‘𝑥) =
(♯‘∅)) |
2 | | hash0 13820 |
. . . . 5
⊢
(♯‘∅) = 0 |
3 | 1, 2 | eqtrdi 2789 |
. . . 4
⊢ (𝑥 = ∅ →
(♯‘𝑥) =
0) |
4 | 3 | breq2d 5042 |
. . 3
⊢ (𝑥 = ∅ → (2 ∥
(♯‘𝑥) ↔ 2
∥ 0)) |
5 | | sumeq1 15138 |
. . . . 5
⊢ (𝑥 = ∅ → Σ𝑘 ∈ 𝑥 𝐵 = Σ𝑘 ∈ ∅ 𝐵) |
6 | | sum0 15171 |
. . . . 5
⊢
Σ𝑘 ∈
∅ 𝐵 =
0 |
7 | 5, 6 | eqtrdi 2789 |
. . . 4
⊢ (𝑥 = ∅ → Σ𝑘 ∈ 𝑥 𝐵 = 0) |
8 | 7 | breq2d 5042 |
. . 3
⊢ (𝑥 = ∅ → (2 ∥
Σ𝑘 ∈ 𝑥 𝐵 ↔ 2 ∥ 0)) |
9 | 4, 8 | bibi12d 349 |
. 2
⊢ (𝑥 = ∅ → ((2 ∥
(♯‘𝑥) ↔ 2
∥ Σ𝑘 ∈
𝑥 𝐵) ↔ (2 ∥ 0 ↔ 2 ∥
0))) |
10 | | fveq2 6674 |
. . . 4
⊢ (𝑥 = 𝑦 → (♯‘𝑥) = (♯‘𝑦)) |
11 | 10 | breq2d 5042 |
. . 3
⊢ (𝑥 = 𝑦 → (2 ∥ (♯‘𝑥) ↔ 2 ∥
(♯‘𝑦))) |
12 | | sumeq1 15138 |
. . . 4
⊢ (𝑥 = 𝑦 → Σ𝑘 ∈ 𝑥 𝐵 = Σ𝑘 ∈ 𝑦 𝐵) |
13 | 12 | breq2d 5042 |
. . 3
⊢ (𝑥 = 𝑦 → (2 ∥ Σ𝑘 ∈ 𝑥 𝐵 ↔ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵)) |
14 | 11, 13 | bibi12d 349 |
. 2
⊢ (𝑥 = 𝑦 → ((2 ∥ (♯‘𝑥) ↔ 2 ∥ Σ𝑘 ∈ 𝑥 𝐵) ↔ (2 ∥ (♯‘𝑦) ↔ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵))) |
15 | | fveq2 6674 |
. . . 4
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (♯‘𝑥) = (♯‘(𝑦 ∪ {𝑧}))) |
16 | 15 | breq2d 5042 |
. . 3
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (2 ∥ (♯‘𝑥) ↔ 2 ∥
(♯‘(𝑦 ∪
{𝑧})))) |
17 | | sumeq1 15138 |
. . . 4
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → Σ𝑘 ∈ 𝑥 𝐵 = Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵) |
18 | 17 | breq2d 5042 |
. . 3
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (2 ∥ Σ𝑘 ∈ 𝑥 𝐵 ↔ 2 ∥ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵)) |
19 | 16, 18 | bibi12d 349 |
. 2
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((2 ∥ (♯‘𝑥) ↔ 2 ∥ Σ𝑘 ∈ 𝑥 𝐵) ↔ (2 ∥ (♯‘(𝑦 ∪ {𝑧})) ↔ 2 ∥ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵))) |
20 | | fveq2 6674 |
. . . 4
⊢ (𝑥 = 𝐴 → (♯‘𝑥) = (♯‘𝐴)) |
21 | 20 | breq2d 5042 |
. . 3
⊢ (𝑥 = 𝐴 → (2 ∥ (♯‘𝑥) ↔ 2 ∥
(♯‘𝐴))) |
22 | | sumeq1 15138 |
. . . 4
⊢ (𝑥 = 𝐴 → Σ𝑘 ∈ 𝑥 𝐵 = Σ𝑘 ∈ 𝐴 𝐵) |
23 | 22 | breq2d 5042 |
. . 3
⊢ (𝑥 = 𝐴 → (2 ∥ Σ𝑘 ∈ 𝑥 𝐵 ↔ 2 ∥ Σ𝑘 ∈ 𝐴 𝐵)) |
24 | 21, 23 | bibi12d 349 |
. 2
⊢ (𝑥 = 𝐴 → ((2 ∥ (♯‘𝑥) ↔ 2 ∥ Σ𝑘 ∈ 𝑥 𝐵) ↔ (2 ∥ (♯‘𝐴) ↔ 2 ∥ Σ𝑘 ∈ 𝐴 𝐵))) |
25 | | biidd 265 |
. 2
⊢ (𝜑 → (2 ∥ 0 ↔ 2
∥ 0)) |
26 | | eldifi 4017 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (𝐴 ∖ 𝑦) → 𝑧 ∈ 𝐴) |
27 | 26 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → 𝑧 ∈ 𝐴) |
28 | 27 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑧 ∈ 𝐴) |
29 | | sumeven.b |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℤ) |
30 | 29 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℤ) |
31 | 30 | ralrimiva 3096 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℤ) |
32 | | rspcsbela 4325 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ ℤ) → ⦋𝑧 / 𝑘⦌𝐵 ∈ ℤ) |
33 | 28, 31, 32 | syl2anc 587 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ⦋𝑧 / 𝑘⦌𝐵 ∈ ℤ) |
34 | | sumodd.o |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ 2 ∥ 𝐵) |
35 | 34 | ralrimiva 3096 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 ¬ 2 ∥ 𝐵) |
36 | | nfcv 2899 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑘2 |
37 | | nfcv 2899 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑘
∥ |
38 | | nfcsb1v 3814 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑘⦋𝑧 / 𝑘⦌𝐵 |
39 | 36, 37, 38 | nfbr 5077 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘2 ∥
⦋𝑧 / 𝑘⦌𝐵 |
40 | 39 | nfn 1864 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘 ¬ 2
∥ ⦋𝑧 /
𝑘⦌𝐵 |
41 | | csbeq1a 3804 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑘⦌𝐵) |
42 | 41 | breq2d 5042 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑧 → (2 ∥ 𝐵 ↔ 2 ∥ ⦋𝑧 / 𝑘⦌𝐵)) |
43 | 42 | notbid 321 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑧 → (¬ 2 ∥ 𝐵 ↔ ¬ 2 ∥ ⦋𝑧 / 𝑘⦌𝐵)) |
44 | 40, 43 | rspc 3514 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 ¬ 2 ∥ 𝐵 → ¬ 2 ∥ ⦋𝑧 / 𝑘⦌𝐵)) |
45 | 26, 44 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (𝐴 ∖ 𝑦) → (∀𝑘 ∈ 𝐴 ¬ 2 ∥ 𝐵 → ¬ 2 ∥ ⦋𝑧 / 𝑘⦌𝐵)) |
46 | 35, 45 | syl5com 31 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑧 ∈ (𝐴 ∖ 𝑦) → ¬ 2 ∥ ⦋𝑧 / 𝑘⦌𝐵)) |
47 | 46 | a1d 25 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑦 ⊆ 𝐴 → (𝑧 ∈ (𝐴 ∖ 𝑦) → ¬ 2 ∥ ⦋𝑧 / 𝑘⦌𝐵))) |
48 | 47 | imp32 422 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ¬ 2 ∥
⦋𝑧 / 𝑘⦌𝐵) |
49 | 33, 48 | jca 515 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (⦋𝑧 / 𝑘⦌𝐵 ∈ ℤ ∧ ¬ 2 ∥
⦋𝑧 / 𝑘⦌𝐵)) |
50 | 49 | adantr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → (⦋𝑧 / 𝑘⦌𝐵 ∈ ℤ ∧ ¬ 2 ∥
⦋𝑧 / 𝑘⦌𝐵)) |
51 | | sumeven.a |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ Fin) |
52 | | ssfi 8772 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ Fin ∧ 𝑦 ⊆ 𝐴) → 𝑦 ∈ Fin) |
53 | 52 | expcom 417 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ⊆ 𝐴 → (𝐴 ∈ Fin → 𝑦 ∈ Fin)) |
54 | 53 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → (𝐴 ∈ Fin → 𝑦 ∈ Fin)) |
55 | 51, 54 | syl5com 31 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → 𝑦 ∈ Fin)) |
56 | 55 | imp 410 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑦 ∈ Fin) |
57 | | simpll 767 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝑦) → 𝜑) |
58 | | ssel 3870 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ⊆ 𝐴 → (𝑘 ∈ 𝑦 → 𝑘 ∈ 𝐴)) |
59 | 58 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → (𝑘 ∈ 𝑦 → 𝑘 ∈ 𝐴)) |
60 | 59 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝑘 ∈ 𝑦 → 𝑘 ∈ 𝐴)) |
61 | 60 | imp 410 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ 𝐴) |
62 | 57, 61, 29 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝑦) → 𝐵 ∈ ℤ) |
63 | 56, 62 | fsumzcl 15185 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → Σ𝑘 ∈ 𝑦 𝐵 ∈ ℤ) |
64 | 63 | anim1i 618 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → (Σ𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵)) |
65 | | opeo 15810 |
. . . . . . . . 9
⊢
(((⦋𝑧
/ 𝑘⦌𝐵 ∈ ℤ ∧ ¬ 2
∥ ⦋𝑧 /
𝑘⦌𝐵) ∧ (Σ𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵)) → ¬ 2 ∥
(⦋𝑧 / 𝑘⦌𝐵 + Σ𝑘 ∈ 𝑦 𝐵)) |
66 | 50, 64, 65 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → ¬ 2 ∥
(⦋𝑧 / 𝑘⦌𝐵 + Σ𝑘 ∈ 𝑦 𝐵)) |
67 | 63 | zcnd 12169 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → Σ𝑘 ∈ 𝑦 𝐵 ∈ ℂ) |
68 | 33 | zcnd 12169 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ⦋𝑧 / 𝑘⦌𝐵 ∈ ℂ) |
69 | | addcom 10904 |
. . . . . . . . . . . 12
⊢
((Σ𝑘 ∈
𝑦 𝐵 ∈ ℂ ∧ ⦋𝑧 / 𝑘⦌𝐵 ∈ ℂ) → (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵) = (⦋𝑧 / 𝑘⦌𝐵 + Σ𝑘 ∈ 𝑦 𝐵)) |
70 | 69 | breq2d 5042 |
. . . . . . . . . . 11
⊢
((Σ𝑘 ∈
𝑦 𝐵 ∈ ℂ ∧ ⦋𝑧 / 𝑘⦌𝐵 ∈ ℂ) → (2 ∥
(Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵) ↔ 2 ∥ (⦋𝑧 / 𝑘⦌𝐵 + Σ𝑘 ∈ 𝑦 𝐵))) |
71 | 70 | notbid 321 |
. . . . . . . . . 10
⊢
((Σ𝑘 ∈
𝑦 𝐵 ∈ ℂ ∧ ⦋𝑧 / 𝑘⦌𝐵 ∈ ℂ) → (¬ 2 ∥
(Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵) ↔ ¬ 2 ∥
(⦋𝑧 / 𝑘⦌𝐵 + Σ𝑘 ∈ 𝑦 𝐵))) |
72 | 67, 68, 71 | syl2anc 587 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵) ↔ ¬ 2 ∥
(⦋𝑧 / 𝑘⦌𝐵 + Σ𝑘 ∈ 𝑦 𝐵))) |
73 | 72 | adantr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → (¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵) ↔ ¬ 2 ∥
(⦋𝑧 / 𝑘⦌𝐵 + Σ𝑘 ∈ 𝑦 𝐵))) |
74 | 66, 73 | mpbird 260 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → ¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵)) |
75 | 74 | ex 416 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (2 ∥ Σ𝑘 ∈ 𝑦 𝐵 → ¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵))) |
76 | 63 | anim1i 618 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ ¬ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → (Σ𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ ¬ 2 ∥
Σ𝑘 ∈ 𝑦 𝐵)) |
77 | 49 | adantr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ ¬ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → (⦋𝑧 / 𝑘⦌𝐵 ∈ ℤ ∧ ¬ 2 ∥
⦋𝑧 / 𝑘⦌𝐵)) |
78 | | opoe 15808 |
. . . . . . . . 9
⊢
(((Σ𝑘 ∈
𝑦 𝐵 ∈ ℤ ∧ ¬ 2 ∥
Σ𝑘 ∈ 𝑦 𝐵) ∧ (⦋𝑧 / 𝑘⦌𝐵 ∈ ℤ ∧ ¬ 2 ∥
⦋𝑧 / 𝑘⦌𝐵)) → 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵)) |
79 | 76, 77, 78 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ ¬ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵)) |
80 | 79 | ex 416 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (¬ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵 → 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵))) |
81 | 80 | con1d 147 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵) → 2 ∥ Σ𝑘 ∈ 𝑦 𝐵)) |
82 | 75, 81 | impbid 215 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (2 ∥ Σ𝑘 ∈ 𝑦 𝐵 ↔ ¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵))) |
83 | | bitr3 356 |
. . . . 5
⊢ ((2
∥ Σ𝑘 ∈
𝑦 𝐵 ↔ ¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵)) → ((2 ∥ Σ𝑘 ∈ 𝑦 𝐵 ↔ ¬ 2 ∥
((♯‘𝑦) + 1))
→ (¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵) ↔ ¬ 2 ∥
((♯‘𝑦) +
1)))) |
84 | 82, 83 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ((2 ∥ Σ𝑘 ∈ 𝑦 𝐵 ↔ ¬ 2 ∥
((♯‘𝑦) + 1))
→ (¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵) ↔ ¬ 2 ∥
((♯‘𝑦) +
1)))) |
85 | | bicom 225 |
. . . 4
⊢ ((¬ 2
∥ ((♯‘𝑦)
+ 1) ↔ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) ↔ (2 ∥ Σ𝑘 ∈ 𝑦 𝐵 ↔ ¬ 2 ∥
((♯‘𝑦) +
1))) |
86 | | bicom 225 |
. . . 4
⊢ ((¬ 2
∥ ((♯‘𝑦)
+ 1) ↔ ¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵)) ↔ (¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵) ↔ ¬ 2 ∥
((♯‘𝑦) +
1))) |
87 | 84, 85, 86 | 3imtr4g 299 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ((¬ 2 ∥
((♯‘𝑦) + 1)
↔ 2 ∥ Σ𝑘
∈ 𝑦 𝐵) → (¬ 2 ∥
((♯‘𝑦) + 1)
↔ ¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵)))) |
88 | | notnotb 318 |
. . . . 5
⊢ (2
∥ (♯‘𝑦)
↔ ¬ ¬ 2 ∥ (♯‘𝑦)) |
89 | | hashcl 13809 |
. . . . . . . . 9
⊢ (𝑦 ∈ Fin →
(♯‘𝑦) ∈
ℕ0) |
90 | 56, 89 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (♯‘𝑦) ∈
ℕ0) |
91 | 90 | nn0zd 12166 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (♯‘𝑦) ∈ ℤ) |
92 | | oddp1even 15789 |
. . . . . . 7
⊢
((♯‘𝑦)
∈ ℤ → (¬ 2 ∥ (♯‘𝑦) ↔ 2 ∥ ((♯‘𝑦) + 1))) |
93 | 91, 92 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (¬ 2 ∥
(♯‘𝑦) ↔ 2
∥ ((♯‘𝑦)
+ 1))) |
94 | 93 | notbid 321 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (¬ ¬ 2 ∥
(♯‘𝑦) ↔
¬ 2 ∥ ((♯‘𝑦) + 1))) |
95 | 88, 94 | syl5bb 286 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (2 ∥ (♯‘𝑦) ↔ ¬ 2 ∥
((♯‘𝑦) +
1))) |
96 | 95 | bibi1d 347 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ((2 ∥ (♯‘𝑦) ↔ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) ↔ (¬ 2 ∥
((♯‘𝑦) + 1)
↔ 2 ∥ Σ𝑘
∈ 𝑦 𝐵))) |
97 | | simprr 773 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑧 ∈ (𝐴 ∖ 𝑦)) |
98 | | eldifn 4018 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (𝐴 ∖ 𝑦) → ¬ 𝑧 ∈ 𝑦) |
99 | 98 | adantl 485 |
. . . . . . . . 9
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → ¬ 𝑧 ∈ 𝑦) |
100 | 99 | adantl 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ¬ 𝑧 ∈ 𝑦) |
101 | 56, 100 | jca 515 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) |
102 | | hashunsng 13845 |
. . . . . . 7
⊢ (𝑧 ∈ (𝐴 ∖ 𝑦) → ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1))) |
103 | 97, 101, 102 | sylc 65 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1)) |
104 | 103 | breq2d 5042 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (2 ∥ (♯‘(𝑦 ∪ {𝑧})) ↔ 2 ∥ ((♯‘𝑦) + 1))) |
105 | | vex 3402 |
. . . . . . . 8
⊢ 𝑧 ∈ V |
106 | 105 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑧 ∈ V) |
107 | | df-nel 3039 |
. . . . . . . 8
⊢ (𝑧 ∉ 𝑦 ↔ ¬ 𝑧 ∈ 𝑦) |
108 | 100, 107 | sylibr 237 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑧 ∉ 𝑦) |
109 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ (𝑦 ∪ {𝑧})) → 𝜑) |
110 | | elun 4039 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (𝑦 ∪ {𝑧}) ↔ (𝑘 ∈ 𝑦 ∨ 𝑘 ∈ {𝑧})) |
111 | 59 | com12 32 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ 𝑦 → ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → 𝑘 ∈ 𝐴)) |
112 | | elsni 4533 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ {𝑧} → 𝑘 = 𝑧) |
113 | | eleq1w 2815 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑧 → (𝑘 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)) |
114 | 27, 113 | syl5ibr 249 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑧 → ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → 𝑘 ∈ 𝐴)) |
115 | 112, 114 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ {𝑧} → ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → 𝑘 ∈ 𝐴)) |
116 | 111, 115 | jaoi 856 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ 𝑦 ∨ 𝑘 ∈ {𝑧}) → ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → 𝑘 ∈ 𝐴)) |
117 | 110, 116 | sylbi 220 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝑦 ∪ {𝑧}) → ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → 𝑘 ∈ 𝐴)) |
118 | 117 | com12 32 |
. . . . . . . . . . 11
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → (𝑘 ∈ (𝑦 ∪ {𝑧}) → 𝑘 ∈ 𝐴)) |
119 | 118 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝑘 ∈ (𝑦 ∪ {𝑧}) → 𝑘 ∈ 𝐴)) |
120 | 119 | imp 410 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ (𝑦 ∪ {𝑧})) → 𝑘 ∈ 𝐴) |
121 | 109, 120,
29 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ (𝑦 ∪ {𝑧})) → 𝐵 ∈ ℤ) |
122 | 121 | ralrimiva 3096 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ∀𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ ℤ) |
123 | | fsumsplitsnun 15203 |
. . . . . . 7
⊢ ((𝑦 ∈ Fin ∧ (𝑧 ∈ V ∧ 𝑧 ∉ 𝑦) ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ ℤ) → Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 = (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵)) |
124 | 56, 106, 108, 122, 123 | syl121anc 1376 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 = (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵)) |
125 | 124 | breq2d 5042 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (2 ∥ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 ↔ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵))) |
126 | 104, 125 | bibi12d 349 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ((2 ∥ (♯‘(𝑦 ∪ {𝑧})) ↔ 2 ∥ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵) ↔ (2 ∥ ((♯‘𝑦) + 1) ↔ 2 ∥
(Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵)))) |
127 | | notbi 322 |
. . . 4
⊢ ((2
∥ ((♯‘𝑦)
+ 1) ↔ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵)) ↔ (¬ 2 ∥
((♯‘𝑦) + 1)
↔ ¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵))) |
128 | 126, 127 | bitrdi 290 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ((2 ∥ (♯‘(𝑦 ∪ {𝑧})) ↔ 2 ∥ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵) ↔ (¬ 2 ∥
((♯‘𝑦) + 1)
↔ ¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵)))) |
129 | 87, 96, 128 | 3imtr4d 297 |
. 2
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ((2 ∥ (♯‘𝑦) ↔ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → (2 ∥ (♯‘(𝑦 ∪ {𝑧})) ↔ 2 ∥ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵))) |
130 | 9, 14, 19, 24, 25, 129, 51 | findcard2d 8765 |
1
⊢ (𝜑 → (2 ∥
(♯‘𝐴) ↔ 2
∥ Σ𝑘 ∈
𝐴 𝐵)) |