Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . . . 5
⊢ (𝑥 = ∅ → (#‘𝑥) =
(#‘∅)) |
2 | | hash0 13019 |
. . . . 5
⊢
(#‘∅) = 0 |
3 | 1, 2 | syl6eq 2660 |
. . . 4
⊢ (𝑥 = ∅ → (#‘𝑥) = 0) |
4 | 3 | breq2d 4595 |
. . 3
⊢ (𝑥 = ∅ → (2 ∥
(#‘𝑥) ↔ 2
∥ 0)) |
5 | | sumeq1 14267 |
. . . . 5
⊢ (𝑥 = ∅ → Σ𝑘 ∈ 𝑥 𝐵 = Σ𝑘 ∈ ∅ 𝐵) |
6 | | sum0 14299 |
. . . . 5
⊢
Σ𝑘 ∈
∅ 𝐵 =
0 |
7 | 5, 6 | syl6eq 2660 |
. . . 4
⊢ (𝑥 = ∅ → Σ𝑘 ∈ 𝑥 𝐵 = 0) |
8 | 7 | breq2d 4595 |
. . 3
⊢ (𝑥 = ∅ → (2 ∥
Σ𝑘 ∈ 𝑥 𝐵 ↔ 2 ∥ 0)) |
9 | 4, 8 | bibi12d 334 |
. 2
⊢ (𝑥 = ∅ → ((2 ∥
(#‘𝑥) ↔ 2
∥ Σ𝑘 ∈
𝑥 𝐵) ↔ (2 ∥ 0 ↔ 2 ∥
0))) |
10 | | fveq2 6103 |
. . . 4
⊢ (𝑥 = 𝑦 → (#‘𝑥) = (#‘𝑦)) |
11 | 10 | breq2d 4595 |
. . 3
⊢ (𝑥 = 𝑦 → (2 ∥ (#‘𝑥) ↔ 2 ∥
(#‘𝑦))) |
12 | | sumeq1 14267 |
. . . 4
⊢ (𝑥 = 𝑦 → Σ𝑘 ∈ 𝑥 𝐵 = Σ𝑘 ∈ 𝑦 𝐵) |
13 | 12 | breq2d 4595 |
. . 3
⊢ (𝑥 = 𝑦 → (2 ∥ Σ𝑘 ∈ 𝑥 𝐵 ↔ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵)) |
14 | 11, 13 | bibi12d 334 |
. 2
⊢ (𝑥 = 𝑦 → ((2 ∥ (#‘𝑥) ↔ 2 ∥ Σ𝑘 ∈ 𝑥 𝐵) ↔ (2 ∥ (#‘𝑦) ↔ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵))) |
15 | | fveq2 6103 |
. . . 4
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (#‘𝑥) = (#‘(𝑦 ∪ {𝑧}))) |
16 | 15 | breq2d 4595 |
. . 3
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (2 ∥ (#‘𝑥) ↔ 2 ∥
(#‘(𝑦 ∪ {𝑧})))) |
17 | | sumeq1 14267 |
. . . 4
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → Σ𝑘 ∈ 𝑥 𝐵 = Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵) |
18 | 17 | breq2d 4595 |
. . 3
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (2 ∥ Σ𝑘 ∈ 𝑥 𝐵 ↔ 2 ∥ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵)) |
19 | 16, 18 | bibi12d 334 |
. 2
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((2 ∥ (#‘𝑥) ↔ 2 ∥ Σ𝑘 ∈ 𝑥 𝐵) ↔ (2 ∥ (#‘(𝑦 ∪ {𝑧})) ↔ 2 ∥ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵))) |
20 | | fveq2 6103 |
. . . 4
⊢ (𝑥 = 𝐴 → (#‘𝑥) = (#‘𝐴)) |
21 | 20 | breq2d 4595 |
. . 3
⊢ (𝑥 = 𝐴 → (2 ∥ (#‘𝑥) ↔ 2 ∥
(#‘𝐴))) |
22 | | sumeq1 14267 |
. . . 4
⊢ (𝑥 = 𝐴 → Σ𝑘 ∈ 𝑥 𝐵 = Σ𝑘 ∈ 𝐴 𝐵) |
23 | 22 | breq2d 4595 |
. . 3
⊢ (𝑥 = 𝐴 → (2 ∥ Σ𝑘 ∈ 𝑥 𝐵 ↔ 2 ∥ Σ𝑘 ∈ 𝐴 𝐵)) |
24 | 21, 23 | bibi12d 334 |
. 2
⊢ (𝑥 = 𝐴 → ((2 ∥ (#‘𝑥) ↔ 2 ∥ Σ𝑘 ∈ 𝑥 𝐵) ↔ (2 ∥ (#‘𝐴) ↔ 2 ∥ Σ𝑘 ∈ 𝐴 𝐵))) |
25 | | biidd 251 |
. 2
⊢ (𝜑 → (2 ∥ 0 ↔ 2
∥ 0)) |
26 | | eldifi 3694 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (𝐴 ∖ 𝑦) → 𝑧 ∈ 𝐴) |
27 | 26 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → 𝑧 ∈ 𝐴) |
28 | 27 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑧 ∈ 𝐴) |
29 | | sumeven.b |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℤ) |
30 | 29 | adantlr 747 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℤ) |
31 | 30 | ralrimiva 2949 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℤ) |
32 | | rspcsbela 3958 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ ℤ) → ⦋𝑧 / 𝑘⦌𝐵 ∈ ℤ) |
33 | 28, 31, 32 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ⦋𝑧 / 𝑘⦌𝐵 ∈ ℤ) |
34 | | sumodd.o |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ 2 ∥ 𝐵) |
35 | 34 | ralrimiva 2949 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 ¬ 2 ∥ 𝐵) |
36 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑘2 |
37 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑘
∥ |
38 | | nfcsb1v 3515 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑘⦋𝑧 / 𝑘⦌𝐵 |
39 | 36, 37, 38 | nfbr 4629 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘2 ∥
⦋𝑧 / 𝑘⦌𝐵 |
40 | 39 | nfn 1768 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘 ¬ 2
∥ ⦋𝑧 /
𝑘⦌𝐵 |
41 | | csbeq1a 3508 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑘⦌𝐵) |
42 | 41 | breq2d 4595 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑧 → (2 ∥ 𝐵 ↔ 2 ∥ ⦋𝑧 / 𝑘⦌𝐵)) |
43 | 42 | notbid 307 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑧 → (¬ 2 ∥ 𝐵 ↔ ¬ 2 ∥ ⦋𝑧 / 𝑘⦌𝐵)) |
44 | 40, 43 | rspc 3276 |
. . . . . . . . . . . . . . 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 448 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ¬ 2 ∥
⦋𝑧 / 𝑘⦌𝐵) |
49 | 33, 48 | jca 553 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (⦋𝑧 / 𝑘⦌𝐵 ∈ ℤ ∧ ¬ 2 ∥
⦋𝑧 / 𝑘⦌𝐵)) |
50 | 49 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → (⦋𝑧 / 𝑘⦌𝐵 ∈ ℤ ∧ ¬ 2 ∥
⦋𝑧 / 𝑘⦌𝐵)) |
51 | | sumeven.a |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ Fin) |
52 | | ssfi 8065 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ Fin ∧ 𝑦 ⊆ 𝐴) → 𝑦 ∈ Fin) |
53 | 52 | expcom 450 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ⊆ 𝐴 → (𝐴 ∈ Fin → 𝑦 ∈ Fin)) |
54 | 53 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → (𝐴 ∈ Fin → 𝑦 ∈ Fin)) |
55 | 51, 54 | syl5com 31 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → 𝑦 ∈ Fin)) |
56 | 55 | imp 444 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑦 ∈ Fin) |
57 | | simpll 786 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝑦) → 𝜑) |
58 | | ssel 3562 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ⊆ 𝐴 → (𝑘 ∈ 𝑦 → 𝑘 ∈ 𝐴)) |
59 | 58 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → (𝑘 ∈ 𝑦 → 𝑘 ∈ 𝐴)) |
60 | 59 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝑘 ∈ 𝑦 → 𝑘 ∈ 𝐴)) |
61 | 60 | imp 444 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ 𝐴) |
62 | 57, 61, 29 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝑦) → 𝐵 ∈ ℤ) |
63 | 56, 62 | fsumzcl 14313 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → Σ𝑘 ∈ 𝑦 𝐵 ∈ ℤ) |
64 | 63 | anim1i 590 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → (Σ𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵)) |
65 | | opeo 14927 |
. . . . . . . . 9
⊢
(((⦋𝑧
/ 𝑘⦌𝐵 ∈ ℤ ∧ ¬ 2
∥ ⦋𝑧 /
𝑘⦌𝐵) ∧ (Σ𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵)) → ¬ 2 ∥
(⦋𝑧 / 𝑘⦌𝐵 + Σ𝑘 ∈ 𝑦 𝐵)) |
66 | 50, 64, 65 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → ¬ 2 ∥
(⦋𝑧 / 𝑘⦌𝐵 + Σ𝑘 ∈ 𝑦 𝐵)) |
67 | 63 | zcnd 11359 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → Σ𝑘 ∈ 𝑦 𝐵 ∈ ℂ) |
68 | 33 | zcnd 11359 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ⦋𝑧 / 𝑘⦌𝐵 ∈ ℂ) |
69 | | addcom 10101 |
. . . . . . . . . . . 12
⊢
((Σ𝑘 ∈
𝑦 𝐵 ∈ ℂ ∧ ⦋𝑧 / 𝑘⦌𝐵 ∈ ℂ) → (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵) = (⦋𝑧 / 𝑘⦌𝐵 + Σ𝑘 ∈ 𝑦 𝐵)) |
70 | 69 | breq2d 4595 |
. . . . . . . . . . 11
⊢
((Σ𝑘 ∈
𝑦 𝐵 ∈ ℂ ∧ ⦋𝑧 / 𝑘⦌𝐵 ∈ ℂ) → (2 ∥
(Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵) ↔ 2 ∥ (⦋𝑧 / 𝑘⦌𝐵 + Σ𝑘 ∈ 𝑦 𝐵))) |
71 | 70 | notbid 307 |
. . . . . . . . . 10
⊢
((Σ𝑘 ∈
𝑦 𝐵 ∈ ℂ ∧ ⦋𝑧 / 𝑘⦌𝐵 ∈ ℂ) → (¬ 2 ∥
(Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵) ↔ ¬ 2 ∥
(⦋𝑧 / 𝑘⦌𝐵 + Σ𝑘 ∈ 𝑦 𝐵))) |
72 | 67, 68, 71 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵) ↔ ¬ 2 ∥
(⦋𝑧 / 𝑘⦌𝐵 + Σ𝑘 ∈ 𝑦 𝐵))) |
73 | 72 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → (¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵) ↔ ¬ 2 ∥
(⦋𝑧 / 𝑘⦌𝐵 + Σ𝑘 ∈ 𝑦 𝐵))) |
74 | 66, 73 | mpbird 246 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → ¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵)) |
75 | 74 | ex 449 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (2 ∥ Σ𝑘 ∈ 𝑦 𝐵 → ¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵))) |
76 | 63 | anim1i 590 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ ¬ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → (Σ𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ ¬ 2 ∥
Σ𝑘 ∈ 𝑦 𝐵)) |
77 | 49 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ ¬ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → (⦋𝑧 / 𝑘⦌𝐵 ∈ ℤ ∧ ¬ 2 ∥
⦋𝑧 / 𝑘⦌𝐵)) |
78 | | opoe 14925 |
. . . . . . . . 9
⊢
(((Σ𝑘 ∈
𝑦 𝐵 ∈ ℤ ∧ ¬ 2 ∥
Σ𝑘 ∈ 𝑦 𝐵) ∧ (⦋𝑧 / 𝑘⦌𝐵 ∈ ℤ ∧ ¬ 2 ∥
⦋𝑧 / 𝑘⦌𝐵)) → 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵)) |
79 | 76, 77, 78 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ ¬ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵)) |
80 | 79 | ex 449 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (¬ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵 → 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵))) |
81 | 80 | con1d 138 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵) → 2 ∥ Σ𝑘 ∈ 𝑦 𝐵)) |
82 | 75, 81 | impbid 201 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (2 ∥ Σ𝑘 ∈ 𝑦 𝐵 ↔ ¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵))) |
83 | | bitr3 341 |
. . . . 5
⊢ ((2
∥ Σ𝑘 ∈
𝑦 𝐵 ↔ ¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵)) → ((2 ∥ Σ𝑘 ∈ 𝑦 𝐵 ↔ ¬ 2 ∥ ((#‘𝑦) + 1)) → (¬ 2 ∥
(Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵) ↔ ¬ 2 ∥ ((#‘𝑦) + 1)))) |
84 | 82, 83 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ((2 ∥ Σ𝑘 ∈ 𝑦 𝐵 ↔ ¬ 2 ∥ ((#‘𝑦) + 1)) → (¬ 2 ∥
(Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵) ↔ ¬ 2 ∥ ((#‘𝑦) + 1)))) |
85 | | bicom 211 |
. . . 4
⊢ ((¬ 2
∥ ((#‘𝑦) + 1)
↔ 2 ∥ Σ𝑘
∈ 𝑦 𝐵) ↔ (2 ∥ Σ𝑘 ∈ 𝑦 𝐵 ↔ ¬ 2 ∥ ((#‘𝑦) + 1))) |
86 | | bicom 211 |
. . . 4
⊢ ((¬ 2
∥ ((#‘𝑦) + 1)
↔ ¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵)) ↔ (¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵) ↔ ¬ 2 ∥ ((#‘𝑦) + 1))) |
87 | 84, 85, 86 | 3imtr4g 284 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ((¬ 2 ∥ ((#‘𝑦) + 1) ↔ 2 ∥
Σ𝑘 ∈ 𝑦 𝐵) → (¬ 2 ∥ ((#‘𝑦) + 1) ↔ ¬ 2 ∥
(Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵)))) |
88 | | notnotb 303 |
. . . . 5
⊢ (2
∥ (#‘𝑦) ↔
¬ ¬ 2 ∥ (#‘𝑦)) |
89 | | hashcl 13009 |
. . . . . . . . 9
⊢ (𝑦 ∈ Fin →
(#‘𝑦) ∈
ℕ0) |
90 | 56, 89 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (#‘𝑦) ∈
ℕ0) |
91 | 90 | nn0zd 11356 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (#‘𝑦) ∈ ℤ) |
92 | | oddp1even 14906 |
. . . . . . 7
⊢
((#‘𝑦) ∈
ℤ → (¬ 2 ∥ (#‘𝑦) ↔ 2 ∥ ((#‘𝑦) + 1))) |
93 | 91, 92 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (¬ 2 ∥ (#‘𝑦) ↔ 2 ∥
((#‘𝑦) +
1))) |
94 | 93 | notbid 307 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (¬ ¬ 2 ∥
(#‘𝑦) ↔ ¬ 2
∥ ((#‘𝑦) +
1))) |
95 | 88, 94 | syl5bb 271 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (2 ∥ (#‘𝑦) ↔ ¬ 2 ∥
((#‘𝑦) +
1))) |
96 | 95 | bibi1d 332 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ((2 ∥ (#‘𝑦) ↔ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) ↔ (¬ 2 ∥ ((#‘𝑦) + 1) ↔ 2 ∥
Σ𝑘 ∈ 𝑦 𝐵))) |
97 | | simprr 792 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑧 ∈ (𝐴 ∖ 𝑦)) |
98 | | eldifn 3695 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (𝐴 ∖ 𝑦) → ¬ 𝑧 ∈ 𝑦) |
99 | 98 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → ¬ 𝑧 ∈ 𝑦) |
100 | 99 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ¬ 𝑧 ∈ 𝑦) |
101 | 56, 100 | jca 553 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) |
102 | | hashunsng 13042 |
. . . . . . 7
⊢ (𝑧 ∈ (𝐴 ∖ 𝑦) → ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (#‘(𝑦 ∪ {𝑧})) = ((#‘𝑦) + 1))) |
103 | 97, 101, 102 | sylc 63 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (#‘(𝑦 ∪ {𝑧})) = ((#‘𝑦) + 1)) |
104 | 103 | breq2d 4595 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (2 ∥ (#‘(𝑦 ∪ {𝑧})) ↔ 2 ∥ ((#‘𝑦) + 1))) |
105 | | df-nel 2783 |
. . . . . . . 8
⊢ (𝑧 ∉ 𝑦 ↔ ¬ 𝑧 ∈ 𝑦) |
106 | 100, 105 | sylibr 223 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑧 ∉ 𝑦) |
107 | | simpll 786 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ (𝑦 ∪ {𝑧})) → 𝜑) |
108 | | elun 3715 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (𝑦 ∪ {𝑧}) ↔ (𝑘 ∈ 𝑦 ∨ 𝑘 ∈ {𝑧})) |
109 | 59 | com12 32 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ 𝑦 → ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → 𝑘 ∈ 𝐴)) |
110 | | elsni 4142 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ {𝑧} → 𝑘 = 𝑧) |
111 | | eleq1 2676 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑧 → (𝑘 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)) |
112 | 27, 111 | syl5ibr 235 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑧 → ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → 𝑘 ∈ 𝐴)) |
113 | 110, 112 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ {𝑧} → ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → 𝑘 ∈ 𝐴)) |
114 | 109, 113 | jaoi 393 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ 𝑦 ∨ 𝑘 ∈ {𝑧}) → ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → 𝑘 ∈ 𝐴)) |
115 | 108, 114 | sylbi 206 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝑦 ∪ {𝑧}) → ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → 𝑘 ∈ 𝐴)) |
116 | 115 | com12 32 |
. . . . . . . . . . 11
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → (𝑘 ∈ (𝑦 ∪ {𝑧}) → 𝑘 ∈ 𝐴)) |
117 | 116 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝑘 ∈ (𝑦 ∪ {𝑧}) → 𝑘 ∈ 𝐴)) |
118 | 117 | imp 444 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ (𝑦 ∪ {𝑧})) → 𝑘 ∈ 𝐴) |
119 | 107, 118,
29 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ (𝑦 ∪ {𝑧})) → 𝐵 ∈ ℤ) |
120 | 119 | ralrimiva 2949 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ∀𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ ℤ) |
121 | | fsumsplitsnun 14328 |
. . . . . . 7
⊢ ((𝑦 ∈ Fin ∧ 𝑧 ∉ 𝑦 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ ℤ) → Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 = (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵)) |
122 | 56, 106, 120, 121 | syl3anc 1318 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 = (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵)) |
123 | 122 | breq2d 4595 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (2 ∥ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 ↔ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵))) |
124 | 104, 123 | bibi12d 334 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ((2 ∥ (#‘(𝑦 ∪ {𝑧})) ↔ 2 ∥ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵) ↔ (2 ∥ ((#‘𝑦) + 1) ↔ 2 ∥
(Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵)))) |
125 | | notbi 308 |
. . . 4
⊢ ((2
∥ ((#‘𝑦) + 1)
↔ 2 ∥ (Σ𝑘
∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵)) ↔ (¬ 2 ∥ ((#‘𝑦) + 1) ↔ ¬ 2 ∥
(Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵))) |
126 | 124, 125 | syl6bb 275 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ((2 ∥ (#‘(𝑦 ∪ {𝑧})) ↔ 2 ∥ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵) ↔ (¬ 2 ∥ ((#‘𝑦) + 1) ↔ ¬ 2 ∥
(Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵)))) |
127 | 87, 96, 126 | 3imtr4d 282 |
. 2
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ((2 ∥ (#‘𝑦) ↔ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → (2 ∥ (#‘(𝑦 ∪ {𝑧})) ↔ 2 ∥ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵))) |
128 | 9, 14, 19, 24, 25, 127, 51 | findcard2d 8087 |
1
⊢ (𝜑 → (2 ∥ (#‘𝐴) ↔ 2 ∥ Σ𝑘 ∈ 𝐴 𝐵)) |