Step | Hyp | Ref
| Expression |
1 | | nfcv 2902 |
. . . . . 6
⊢
Ⅎ𝑦𝐵 |
2 | | nfcv 2902 |
. . . . . 6
⊢
Ⅎ𝑥𝐵 |
3 | | nfv 1911 |
. . . . . 6
⊢
Ⅎ𝑥((od‘𝐺)‘𝑦) = 𝐷 |
4 | | nfv 1911 |
. . . . . 6
⊢
Ⅎ𝑦((od‘𝐺)‘𝑥) = 𝐷 |
5 | | fveqeq2 6915 |
. . . . . 6
⊢ (𝑦 = 𝑥 → (((od‘𝐺)‘𝑦) = 𝐷 ↔ ((od‘𝐺)‘𝑥) = 𝐷)) |
6 | 1, 2, 3, 4, 5 | cbvrabw 3470 |
. . . . 5
⊢ {𝑦 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} |
7 | 6 | fveq2i 6909 |
. . . 4
⊢
(♯‘{𝑦
∈ 𝐵 ∣
((od‘𝐺)‘𝑦) = 𝐷}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) |
8 | 7 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → (♯‘{𝑦 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})) |
9 | | unitscyglem4.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∥ (♯‘𝐵)) |
10 | 9 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → 𝐷 ∥ (♯‘𝐵)) |
11 | 10 | ex 412 |
. . . . . 6
⊢ (𝜑 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅ → 𝐷 ∥ (♯‘𝐵))) |
12 | 11 | ancrd 551 |
. . . . 5
⊢ (𝜑 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅ → (𝐷 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅))) |
13 | 12 | imdistani 568 |
. . . 4
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → (𝜑 ∧ (𝐷 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅))) |
14 | | breq1 5150 |
. . . . . . . 8
⊢ (𝑚 = 𝐷 → (𝑚 ∥ (♯‘𝐵) ↔ 𝐷 ∥ (♯‘𝐵))) |
15 | | eqeq2 2746 |
. . . . . . . . . 10
⊢ (𝑚 = 𝐷 → (((od‘𝐺)‘𝑥) = 𝑚 ↔ ((od‘𝐺)‘𝑥) = 𝐷)) |
16 | 15 | rabbidv 3440 |
. . . . . . . . 9
⊢ (𝑚 = 𝐷 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) |
17 | 16 | neeq1d 2997 |
. . . . . . . 8
⊢ (𝑚 = 𝐷 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅ ↔ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅)) |
18 | 14, 17 | anbi12d 632 |
. . . . . . 7
⊢ (𝑚 = 𝐷 → ((𝑚 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅) ↔ (𝐷 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅))) |
19 | 16 | fveq2d 6910 |
. . . . . . . 8
⊢ (𝑚 = 𝐷 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})) |
20 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑚 = 𝐷 → (ϕ‘𝑚) = (ϕ‘𝐷)) |
21 | 19, 20 | eqeq12d 2750 |
. . . . . . 7
⊢ (𝑚 = 𝐷 → ((♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚}) = (ϕ‘𝑚) ↔ (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) = (ϕ‘𝐷))) |
22 | 18, 21 | imbi12d 344 |
. . . . . 6
⊢ (𝑚 = 𝐷 → (((𝑚 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚}) = (ϕ‘𝑚)) ↔ ((𝐷 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) = (ϕ‘𝐷)))) |
23 | | unitscyglem1.1 |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐺) |
24 | | unitscyglem1.2 |
. . . . . . 7
⊢ ↑ =
(.g‘𝐺) |
25 | | unitscyglem1.3 |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ Grp) |
26 | | unitscyglem1.4 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ Fin) |
27 | | unitscyglem1.5 |
. . . . . . 7
⊢ (𝜑 → ∀𝑛 ∈ ℕ (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) ≤ 𝑛) |
28 | 23, 24, 25, 26, 27 | unitscyglem3 42178 |
. . . . . 6
⊢ (𝜑 → ∀𝑚 ∈ ℕ ((𝑚 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚}) = (ϕ‘𝑚))) |
29 | | unitscyglem4.1 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ ℕ) |
30 | 22, 28, 29 | rspcdva 3622 |
. . . . 5
⊢ (𝜑 → ((𝐷 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) = (ϕ‘𝐷))) |
31 | 30 | imp 406 |
. . . 4
⊢ ((𝜑 ∧ (𝐷 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅)) →
(♯‘{𝑥 ∈
𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) = (ϕ‘𝐷)) |
32 | 13, 31 | syl 17 |
. . 3
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) = (ϕ‘𝐷)) |
33 | 8, 32 | eqtrd 2774 |
. 2
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → (♯‘{𝑦 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷}) = (ϕ‘𝐷)) |
34 | | id 22 |
. . . . 5
⊢ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅ → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) |
35 | 34 | necon1bi 2966 |
. . . 4
⊢ (¬
{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅ → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) |
36 | 35 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) |
37 | 25 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → 𝐺 ∈ Grp) |
38 | 26 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → 𝐵 ∈ Fin) |
39 | 23, 37, 38 | hashfingrpnn 19002 |
. . . . . . . . 9
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∈
ℕ) |
40 | 23, 24, 37, 38, 39 | grpods 42175 |
. . . . . . . 8
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((♯‘𝐵) ↑ 𝑥) = (0g‘𝐺)})) |
41 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) ∧ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵)) → (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵)) |
42 | 41 | eqcomd 2740 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) ∧ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵)) → (♯‘𝐵) = (𝑙 · ((od‘𝐺)‘𝑥))) |
43 | 42 | oveq1d 7445 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) ∧ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵)) → ((♯‘𝐵) ↑ 𝑥) = ((𝑙 · ((od‘𝐺)‘𝑥)) ↑ 𝑥)) |
44 | 25 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐺 ∈ Grp) |
45 | 44 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → 𝐺 ∈ Grp) |
46 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → 𝑙 ∈ ℤ) |
47 | | eqid 2734 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(od‘𝐺) =
(od‘𝐺) |
48 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
49 | 23, 47, 48 | odcld 19584 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((od‘𝐺)‘𝑥) ∈
ℕ0) |
50 | 49 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → ((od‘𝐺)‘𝑥) ∈
ℕ0) |
51 | 50 | nn0zd 12636 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → ((od‘𝐺)‘𝑥) ∈ ℤ) |
52 | | simplr 769 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → 𝑥 ∈ 𝐵) |
53 | 46, 51, 52 | 3jca 1127 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → (𝑙 ∈ ℤ ∧ ((od‘𝐺)‘𝑥) ∈ ℤ ∧ 𝑥 ∈ 𝐵)) |
54 | 23, 24 | mulgass 19141 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ∈ Grp ∧ (𝑙 ∈ ℤ ∧
((od‘𝐺)‘𝑥) ∈ ℤ ∧ 𝑥 ∈ 𝐵)) → ((𝑙 · ((od‘𝐺)‘𝑥)) ↑ 𝑥) = (𝑙 ↑ (((od‘𝐺)‘𝑥) ↑ 𝑥))) |
55 | 45, 53, 54 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → ((𝑙 · ((od‘𝐺)‘𝑥)) ↑ 𝑥) = (𝑙 ↑ (((od‘𝐺)‘𝑥) ↑ 𝑥))) |
56 | | eqid 2734 |
. . . . . . . . . . . . . . . . . . 19
⊢
(0g‘𝐺) = (0g‘𝐺) |
57 | 23, 47, 24, 56 | odid 19570 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝐵 → (((od‘𝐺)‘𝑥) ↑ 𝑥) = (0g‘𝐺)) |
58 | 52, 57 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → (((od‘𝐺)‘𝑥) ↑ 𝑥) = (0g‘𝐺)) |
59 | 58 | oveq2d 7446 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → (𝑙 ↑ (((od‘𝐺)‘𝑥) ↑ 𝑥)) = (𝑙 ↑
(0g‘𝐺))) |
60 | 23, 24, 56 | mulgz 19132 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 ∈ Grp ∧ 𝑙 ∈ ℤ) → (𝑙 ↑
(0g‘𝐺)) =
(0g‘𝐺)) |
61 | 44, 60 | sylan 580 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → (𝑙 ↑
(0g‘𝐺)) =
(0g‘𝐺)) |
62 | 59, 61 | eqtrd 2774 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → (𝑙 ↑ (((od‘𝐺)‘𝑥) ↑ 𝑥)) = (0g‘𝐺)) |
63 | 55, 62 | eqtrd 2774 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → ((𝑙 · ((od‘𝐺)‘𝑥)) ↑ 𝑥) = (0g‘𝐺)) |
64 | 63 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) ∧ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵)) → ((𝑙 · ((od‘𝐺)‘𝑥)) ↑ 𝑥) = (0g‘𝐺)) |
65 | 43, 64 | eqtrd 2774 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) ∧ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵)) → ((♯‘𝐵) ↑ 𝑥) = (0g‘𝐺)) |
66 | 26 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐵 ∈ Fin) |
67 | 23, 47 | oddvds2 19598 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝑥 ∈ 𝐵) → ((od‘𝐺)‘𝑥) ∥ (♯‘𝐵)) |
68 | 44, 66, 48, 67 | syl3anc 1370 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((od‘𝐺)‘𝑥) ∥ (♯‘𝐵)) |
69 | 49 | nn0zd 12636 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((od‘𝐺)‘𝑥) ∈ ℤ) |
70 | | hashcl 14391 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ Fin →
(♯‘𝐵) ∈
ℕ0) |
71 | 66, 70 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (♯‘𝐵) ∈
ℕ0) |
72 | 71 | nn0zd 12636 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (♯‘𝐵) ∈ ℤ) |
73 | | divides 16288 |
. . . . . . . . . . . . . 14
⊢
((((od‘𝐺)‘𝑥) ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ) →
(((od‘𝐺)‘𝑥) ∥ (♯‘𝐵) ↔ ∃𝑙 ∈ ℤ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵))) |
74 | 69, 72, 73 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (((od‘𝐺)‘𝑥) ∥ (♯‘𝐵) ↔ ∃𝑙 ∈ ℤ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵))) |
75 | 68, 74 | mpbid 232 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑙 ∈ ℤ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵)) |
76 | 65, 75 | r19.29a 3159 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((♯‘𝐵) ↑ 𝑥) = (0g‘𝐺)) |
77 | 76 | rabeqcda 3444 |
. . . . . . . . . 10
⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ ((♯‘𝐵) ↑ 𝑥) = (0g‘𝐺)} = 𝐵) |
78 | 77 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → {𝑥 ∈ 𝐵 ∣ ((♯‘𝐵) ↑ 𝑥) = (0g‘𝐺)} = 𝐵) |
79 | 78 | fveq2d 6910 |
. . . . . . . 8
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((♯‘𝐵) ↑ 𝑥) = (0g‘𝐺)}) = (♯‘𝐵)) |
80 | 40, 79 | eqtr2d 2775 |
. . . . . . 7
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) = Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})) |
81 | | nfv 1911 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘(𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) |
82 | | nfcv 2902 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) |
83 | | fzfid 14010 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) →
(1...(♯‘𝐵))
∈ Fin) |
84 | | ssrab2 4089 |
. . . . . . . . . . . . 13
⊢ {𝑎 ∈
(1...(♯‘𝐵))
∣ 𝑎 ∥
(♯‘𝐵)} ⊆
(1...(♯‘𝐵)) |
85 | 84 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ (1...(♯‘𝐵))) |
86 | 83, 85 | ssfid 9298 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∈ Fin) |
87 | 38 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝐵 ∈ Fin) |
88 | | ssrab2 4089 |
. . . . . . . . . . . . . . 15
⊢ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ⊆ 𝐵 |
89 | 88 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ⊆ 𝐵) |
90 | 87, 89 | ssfid 9298 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∈ Fin) |
91 | | hashcl 14391 |
. . . . . . . . . . . . 13
⊢ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∈ Fin → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈
ℕ0) |
92 | 90, 91 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈
ℕ0) |
93 | 92 | nn0cnd 12586 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℂ) |
94 | | breq1 5150 |
. . . . . . . . . . . 12
⊢ (𝑎 = (♯‘𝐵) → (𝑎 ∥ (♯‘𝐵) ↔ (♯‘𝐵) ∥ (♯‘𝐵))) |
95 | | 1zzd 12645 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → 1 ∈
ℤ) |
96 | 39 | nnzd 12637 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∈
ℤ) |
97 | 39 | nnge1d 12311 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → 1 ≤
(♯‘𝐵)) |
98 | 39 | nnred 12278 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∈
ℝ) |
99 | 98 | leidd 11826 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ≤ (♯‘𝐵)) |
100 | 95, 96, 96, 97, 99 | elfzd 13551 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∈
(1...(♯‘𝐵))) |
101 | | iddvds 16303 |
. . . . . . . . . . . . 13
⊢
((♯‘𝐵)
∈ ℤ → (♯‘𝐵) ∥ (♯‘𝐵)) |
102 | 96, 101 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∥ (♯‘𝐵)) |
103 | 94, 100, 102 | elrabd 3696 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) |
104 | | eqeq2 2746 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (♯‘𝐵) → (((od‘𝐺)‘𝑥) = 𝑘 ↔ ((od‘𝐺)‘𝑥) = (♯‘𝐵))) |
105 | 104 | rabbidv 3440 |
. . . . . . . . . . . 12
⊢ (𝑘 = (♯‘𝐵) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) |
106 | 105 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (𝑘 = (♯‘𝐵) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)})) |
107 | 81, 82, 86, 93, 103, 106 | fsumsplit1 15777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = ((♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) + Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))) |
108 | | ssrab2 4089 |
. . . . . . . . . . . . . . . 16
⊢ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ⊆ 𝐵 |
109 | 108 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ⊆ 𝐵) |
110 | 38, 109 | ssfid 9298 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ∈ Fin) |
111 | | hashcl 14391 |
. . . . . . . . . . . . . 14
⊢ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ∈ Fin → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) ∈
ℕ0) |
112 | 110, 111 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) ∈
ℕ0) |
113 | 112 | nn0red 12585 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) ∈ ℝ) |
114 | | diffi 9213 |
. . . . . . . . . . . . . . 15
⊢ ({𝑎 ∈
(1...(♯‘𝐵))
∣ 𝑎 ∥
(♯‘𝐵)} ∈
Fin → ({𝑎 ∈
(1...(♯‘𝐵))
∣ 𝑎 ∥
(♯‘𝐵)} ∖
{(♯‘𝐵)}) ∈
Fin) |
115 | 86, 114 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}) ∈ Fin) |
116 | 38 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → 𝐵 ∈ Fin) |
117 | 88 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ⊆ 𝐵) |
118 | 116, 117 | ssfid 9298 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∈ Fin) |
119 | 118, 91 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈
ℕ0) |
120 | 115, 119 | fsumnn0cl 15768 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈
ℕ0) |
121 | 120 | nn0red 12585 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℝ) |
122 | 39 | phicld 16805 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) →
(ϕ‘(♯‘𝐵)) ∈ ℕ) |
123 | 122 | nnred 12278 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) →
(ϕ‘(♯‘𝐵)) ∈ ℝ) |
124 | | eldifi 4140 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}) → 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) |
125 | | breq1 5150 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 = 𝑘 → (𝑎 ∥ (♯‘𝐵) ↔ 𝑘 ∥ (♯‘𝐵))) |
126 | 125 | elrab 3694 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ↔ (𝑘 ∈ (1...(♯‘𝐵)) ∧ 𝑘 ∥ (♯‘𝐵))) |
127 | 126 | biimpi 216 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} → (𝑘 ∈ (1...(♯‘𝐵)) ∧ 𝑘 ∥ (♯‘𝐵))) |
128 | | elfzelz 13560 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈
(1...(♯‘𝐵))
→ 𝑘 ∈
ℤ) |
129 | | elfzle1 13563 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈
(1...(♯‘𝐵))
→ 1 ≤ 𝑘) |
130 | 128, 129 | jca 511 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈
(1...(♯‘𝐵))
→ (𝑘 ∈ ℤ
∧ 1 ≤ 𝑘)) |
131 | 130 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈
(1...(♯‘𝐵))
∧ 𝑘 ∥
(♯‘𝐵)) →
(𝑘 ∈ ℤ ∧ 1
≤ 𝑘)) |
132 | 127, 131 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘)) |
133 | 124, 132 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}) → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘)) |
134 | 133 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘)) |
135 | | elnnz1 12640 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ ↔ (𝑘 ∈ ℤ ∧ 1 ≤
𝑘)) |
136 | 134, 135 | sylibr 234 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → 𝑘 ∈ ℕ) |
137 | | phicl 16802 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ →
(ϕ‘𝑘) ∈
ℕ) |
138 | 136, 137 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → (ϕ‘𝑘) ∈ ℕ) |
139 | 138 | nnred 12278 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → (ϕ‘𝑘) ∈ ℝ) |
140 | 115, 139 | fsumrecl 15766 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘) ∈ ℝ) |
141 | | simplll 775 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅) ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝜑) |
142 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅) ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝑧 ∈ 𝐵) |
143 | 141, 142 | jca 511 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅) ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (𝜑 ∧ 𝑧 ∈ 𝐵)) |
144 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅) ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘𝑧) = (♯‘𝐵)) |
145 | 143, 144 | jca 511 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅) ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵))) |
146 | | fveqeq2 6915 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = (((♯‘𝐵) / 𝐷) ↑ 𝑧) → (((od‘𝐺)‘𝑥) = 𝐷 ↔ ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧)) = 𝐷)) |
147 | 25 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐺 ∈ Grp) |
148 | 9 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐷 ∥ (♯‘𝐵)) |
149 | 29 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐷 ∈ ℕ) |
150 | 149 | nnzd 12637 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐷 ∈ ℤ) |
151 | 149 | nnne0d 12313 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐷 ≠ 0) |
152 | 26 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐵 ∈ Fin) |
153 | 152, 70 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) ∈
ℕ0) |
154 | 153 | nn0zd 12636 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) ∈ ℤ) |
155 | | dvdsval2 16289 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ∧
(♯‘𝐵) ∈
ℤ) → (𝐷 ∥
(♯‘𝐵) ↔
((♯‘𝐵) / 𝐷) ∈
ℤ)) |
156 | 150, 151,
154, 155 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (𝐷 ∥ (♯‘𝐵) ↔ ((♯‘𝐵) / 𝐷) ∈ ℤ)) |
157 | 148, 156 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / 𝐷) ∈ ℤ) |
158 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝑧 ∈ 𝐵) |
159 | 23, 24, 147, 157, 158 | mulgcld 19126 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) ↑ 𝑧) ∈ 𝐵) |
160 | 153 | nn0cnd 12586 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) ∈ ℂ) |
161 | 29 | nncnd 12279 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝐷 ∈ ℂ) |
162 | 161 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐷 ∈ ℂ) |
163 | 23, 147, 152 | hashfingrpnn 19002 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) ∈ ℕ) |
164 | 163 | nnne0d 12313 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) ≠ 0) |
165 | 160, 160,
162, 164, 151 | divdiv2d 12072 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / ((♯‘𝐵) / 𝐷)) = (((♯‘𝐵) · 𝐷) / (♯‘𝐵))) |
166 | 162, 160,
164 | divcan3d 12045 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) · 𝐷) / (♯‘𝐵)) = 𝐷) |
167 | 165, 166 | eqtr2d 2775 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐷 = ((♯‘𝐵) / ((♯‘𝐵) / 𝐷))) |
168 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘𝑧) = (♯‘𝐵)) |
169 | 168 | oveq2d 7446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) = (((♯‘𝐵) / 𝐷) gcd (♯‘𝐵))) |
170 | 26, 70 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝜑 → (♯‘𝐵) ∈
ℕ0) |
171 | 170 | nn0cnd 12586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → (♯‘𝐵) ∈
ℂ) |
172 | 29 | nnne0d 12313 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → 𝐷 ≠ 0) |
173 | 171, 161,
172 | divcan2d 12042 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 → (𝐷 · ((♯‘𝐵) / 𝐷)) = (♯‘𝐵)) |
174 | 173 | eqcomd 2740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝜑 → (♯‘𝐵) = (𝐷 · ((♯‘𝐵) / 𝐷))) |
175 | 174 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (♯‘𝐵) = (𝐷 · ((♯‘𝐵) / 𝐷))) |
176 | 175 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) = (𝐷 · ((♯‘𝐵) / 𝐷))) |
177 | 176 | oveq2d 7446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd (♯‘𝐵)) = (((♯‘𝐵) / 𝐷) gcd (𝐷 · ((♯‘𝐵) / 𝐷)))) |
178 | | nndivdvds 16295 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((♯‘𝐵)
∈ ℕ ∧ 𝐷
∈ ℕ) → (𝐷
∥ (♯‘𝐵)
↔ ((♯‘𝐵) /
𝐷) ∈
ℕ)) |
179 | 163, 149,
178 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (𝐷 ∥ (♯‘𝐵) ↔ ((♯‘𝐵) / 𝐷) ∈ ℕ)) |
180 | 148, 179 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / 𝐷) ∈ ℕ) |
181 | 180 | nnnn0d 12584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / 𝐷) ∈
ℕ0) |
182 | 181, 150 | gcdmultipled 16567 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd (𝐷 · ((♯‘𝐵) / 𝐷))) = ((♯‘𝐵) / 𝐷)) |
183 | 177, 182 | eqtrd 2774 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd (♯‘𝐵)) = ((♯‘𝐵) / 𝐷)) |
184 | 169, 183 | eqtrd 2774 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) = ((♯‘𝐵) / 𝐷)) |
185 | 184 | eqcomd 2740 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / 𝐷) = (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧))) |
186 | 185 | oveq2d 7446 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / ((♯‘𝐵) / 𝐷)) = ((♯‘𝐵) / (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)))) |
187 | 167, 186 | eqtrd 2774 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐷 = ((♯‘𝐵) / (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)))) |
188 | 168 | eqcomd 2740 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) = ((od‘𝐺)‘𝑧)) |
189 | 23, 47, 24 | odmulg 19588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝐵 ∧ ((♯‘𝐵) / 𝐷) ∈ ℤ) → ((od‘𝐺)‘𝑧) = ((((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) · ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧)))) |
190 | 147, 158,
157, 189 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘𝑧) = ((((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) · ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧)))) |
191 | 188, 190 | eqtrd 2774 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) = ((((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) · ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧)))) |
192 | 191 | eqcomd 2740 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) · ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧))) = (♯‘𝐵)) |
193 | 157 | zcnd 12720 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / 𝐷) ∈ ℂ) |
194 | 184, 193 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) ∈ ℂ) |
195 | 23, 47, 159 | odcld 19584 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧)) ∈
ℕ0) |
196 | 195 | nn0cnd 12586 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧)) ∈ ℂ) |
197 | 168, 154 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘𝑧) ∈ ℤ) |
198 | 168, 164 | eqnetrd 3005 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘𝑧) ≠ 0) |
199 | 157, 197,
198 | 3jca 1127 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) ∈ ℤ ∧ ((od‘𝐺)‘𝑧) ∈ ℤ ∧ ((od‘𝐺)‘𝑧) ≠ 0)) |
200 | | gcd2n0cl 16542 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((♯‘𝐵)
/ 𝐷) ∈ ℤ ∧
((od‘𝐺)‘𝑧) ∈ ℤ ∧
((od‘𝐺)‘𝑧) ≠ 0) →
(((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) ∈ ℕ) |
201 | 199, 200 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) ∈ ℕ) |
202 | 201 | nnne0d 12313 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) ≠ 0) |
203 | 160, 194,
196, 202 | divmuld 12062 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧))) = ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧)) ↔ ((((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) · ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧))) = (♯‘𝐵))) |
204 | 192, 203 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧))) = ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧))) |
205 | 187, 204 | eqtr2d 2775 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧)) = 𝐷) |
206 | 146, 159,
205 | elrabd 3696 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) ↑ 𝑧) ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) |
207 | | ne0i 4346 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((♯‘𝐵)
/ 𝐷) ↑ 𝑧) ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) |
208 | 206, 207 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) |
209 | 145, 208 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅) ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) |
210 | | rabn0 4394 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅ ↔ ∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = (♯‘𝐵)) |
211 | | nfv 1911 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑧((od‘𝐺)‘𝑥) = (♯‘𝐵) |
212 | | nfv 1911 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑥((od‘𝐺)‘𝑧) = (♯‘𝐵) |
213 | | fveqeq2 6915 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑧 → (((od‘𝐺)‘𝑥) = (♯‘𝐵) ↔ ((od‘𝐺)‘𝑧) = (♯‘𝐵))) |
214 | 211, 212,
213 | cbvrexw 3304 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∃𝑥 ∈
𝐵 ((od‘𝐺)‘𝑥) = (♯‘𝐵) ↔ ∃𝑧 ∈ 𝐵 ((od‘𝐺)‘𝑧) = (♯‘𝐵)) |
215 | 210, 214 | bitri 275 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅ ↔ ∃𝑧 ∈ 𝐵 ((od‘𝐺)‘𝑧) = (♯‘𝐵)) |
216 | 215 | biimpi 216 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅ → ∃𝑧 ∈ 𝐵 ((od‘𝐺)‘𝑧) = (♯‘𝐵)) |
217 | 216 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅) → ∃𝑧 ∈ 𝐵 ((od‘𝐺)‘𝑧) = (♯‘𝐵)) |
218 | 209, 217 | r19.29a 3159 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) |
219 | 218 | ex 412 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅ → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅)) |
220 | 219 | necon4d 2961 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅ → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} = ∅)) |
221 | 220 | imp 406 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} = ∅) |
222 | 221 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) =
(♯‘∅)) |
223 | | hash0 14402 |
. . . . . . . . . . . . . . 15
⊢
(♯‘∅) = 0 |
224 | 223 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘∅)
= 0) |
225 | 222, 224 | eqtrd 2774 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) = 0) |
226 | 122 | nngt0d 12312 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → 0 <
(ϕ‘(♯‘𝐵))) |
227 | 225, 226 | eqbrtrd 5169 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) < (ϕ‘(♯‘𝐵))) |
228 | | eldif 3972 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}) ↔ (𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)})) |
229 | 228 | biimpi 216 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}) → (𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)})) |
230 | 229 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑧 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → (𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)})) |
231 | | breq1 5150 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑎 = 𝑧 → (𝑎 ∥ (♯‘𝐵) ↔ 𝑧 ∥ (♯‘𝐵))) |
232 | 231 | elrab 3694 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ↔ (𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵))) |
233 | 232 | biimpi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} → (𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵))) |
234 | 233 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)}) → (𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵))) |
235 | | velsn 4646 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑧 ∈ {(♯‘𝐵)} ↔ 𝑧 = (♯‘𝐵)) |
236 | 235 | bicomi 224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑧 = (♯‘𝐵) ↔ 𝑧 ∈ {(♯‘𝐵)}) |
237 | 236 | biimpi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 = (♯‘𝐵) → 𝑧 ∈ {(♯‘𝐵)}) |
238 | 237 | necon3bi 2964 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (¬
𝑧 ∈
{(♯‘𝐵)} →
𝑧 ≠ (♯‘𝐵)) |
239 | 238 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)}) → 𝑧 ≠ (♯‘𝐵)) |
240 | 234, 239 | jca 511 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)}) → ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) |
241 | 240 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)})) → ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) |
242 | | 1zzd 12645 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 1 ∈
ℤ) |
243 | 26 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝐵 ∈ Fin) |
244 | 243, 70 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → (♯‘𝐵) ∈
ℕ0) |
245 | 244 | nn0zd 12636 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → (♯‘𝐵) ∈ ℤ) |
246 | 245, 242 | zsubcld 12724 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → ((♯‘𝐵) − 1) ∈
ℤ) |
247 | | elfzelz 13560 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑧 ∈
(1...(♯‘𝐵))
→ 𝑧 ∈
ℤ) |
248 | 247 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑧 ∈
(1...(♯‘𝐵))
∧ 𝑧 ∥
(♯‘𝐵)) →
𝑧 ∈
ℤ) |
249 | 248 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑧 ∈
(1...(♯‘𝐵))
∧ 𝑧 ∥
(♯‘𝐵)) ∧
𝑧 ≠ (♯‘𝐵)) → 𝑧 ∈ ℤ) |
250 | 249 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ∈ ℤ) |
251 | | elfzle1 13563 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑧 ∈
(1...(♯‘𝐵))
→ 1 ≤ 𝑧) |
252 | 251 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑧 ∈
(1...(♯‘𝐵))
∧ 𝑧 ∥
(♯‘𝐵)) → 1
≤ 𝑧) |
253 | 252 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑧 ∈
(1...(♯‘𝐵))
∧ 𝑧 ∥
(♯‘𝐵)) ∧
𝑧 ≠ (♯‘𝐵)) → 1 ≤ 𝑧) |
254 | 253 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 1 ≤ 𝑧) |
255 | | elfzle2 13564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑧 ∈
(1...(♯‘𝐵))
→ 𝑧 ≤
(♯‘𝐵)) |
256 | 255 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑧 ∈
(1...(♯‘𝐵))
∧ 𝑧 ∥
(♯‘𝐵)) →
𝑧 ≤ (♯‘𝐵)) |
257 | 256 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑧 ∈
(1...(♯‘𝐵))
∧ 𝑧 ∥
(♯‘𝐵)) ∧
𝑧 ≠ (♯‘𝐵)) → 𝑧 ≤ (♯‘𝐵)) |
258 | 257 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ≤ (♯‘𝐵)) |
259 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ≠ (♯‘𝐵)) |
260 | 259 | necomd 2993 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → (♯‘𝐵) ≠ 𝑧) |
261 | 258, 260 | jca 511 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → (𝑧 ≤ (♯‘𝐵) ∧ (♯‘𝐵) ≠ 𝑧)) |
262 | 250 | zred 12719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ∈ ℝ) |
263 | 244 | nn0red 12585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → (♯‘𝐵) ∈ ℝ) |
264 | 262, 263 | ltlend 11403 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → (𝑧 < (♯‘𝐵) ↔ (𝑧 ≤ (♯‘𝐵) ∧ (♯‘𝐵) ≠ 𝑧))) |
265 | 261, 264 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 < (♯‘𝐵)) |
266 | 250, 245 | zltlem1d 12668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → (𝑧 < (♯‘𝐵) ↔ 𝑧 ≤ ((♯‘𝐵) − 1))) |
267 | 265, 266 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ≤ ((♯‘𝐵) − 1)) |
268 | 242, 246,
250, 254, 267 | elfzd 13551 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ∈ (1...((♯‘𝐵) − 1))) |
269 | | simprlr 780 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ∥ (♯‘𝐵)) |
270 | 231, 268,
269 | elrabd 3696 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) |
271 | 270 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵)) → 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)})) |
272 | 271 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)})) → (((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵)) → 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)})) |
273 | 241, 272 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)})) → 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) |
274 | 273 | ex 412 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)}) → 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)})) |
275 | 274 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑧 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → ((𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)}) → 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)})) |
276 | 230, 275 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) |
277 | 276 | ex 412 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑧 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}) → 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)})) |
278 | 277 | ssrdv 4000 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}) ⊆ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) |
279 | | 1zzd 12645 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → 1 ∈
ℤ) |
280 | 170 | nn0zd 12636 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (♯‘𝐵) ∈
ℤ) |
281 | 280 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) →
(♯‘𝐵) ∈
ℤ) |
282 | | elfzelz 13560 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 ∈
(1...((♯‘𝐵)
− 1)) → 𝑧 ∈
ℤ) |
283 | 282 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → 𝑧 ∈
ℤ) |
284 | | elfzle1 13563 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 ∈
(1...((♯‘𝐵)
− 1)) → 1 ≤ 𝑧) |
285 | 284 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → 1 ≤
𝑧) |
286 | 283 | zred 12719 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → 𝑧 ∈
ℝ) |
287 | 281 | zred 12719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) →
(♯‘𝐵) ∈
ℝ) |
288 | | 1red 11259 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → 1 ∈
ℝ) |
289 | 287, 288 | resubcld 11688 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) →
((♯‘𝐵) −
1) ∈ ℝ) |
290 | | elfzle2 13564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑧 ∈
(1...((♯‘𝐵)
− 1)) → 𝑧 ≤
((♯‘𝐵) −
1)) |
291 | 290 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → 𝑧 ≤ ((♯‘𝐵) − 1)) |
292 | 287 | lem1d 12198 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) →
((♯‘𝐵) −
1) ≤ (♯‘𝐵)) |
293 | 286, 289,
287, 291, 292 | letrd 11415 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → 𝑧 ≤ (♯‘𝐵)) |
294 | 279, 281,
283, 285, 293 | elfzd 13551 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → 𝑧 ∈
(1...(♯‘𝐵))) |
295 | 294 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑧 ∈ (1...((♯‘𝐵) − 1)) → 𝑧 ∈
(1...(♯‘𝐵)))) |
296 | 295 | ssrdv 4000 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (1...((♯‘𝐵) − 1)) ⊆
(1...(♯‘𝐵))) |
297 | | rabss2 4087 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((1...((♯‘𝐵) − 1)) ⊆
(1...(♯‘𝐵))
→ {𝑎 ∈
(1...((♯‘𝐵)
− 1)) ∣ 𝑎
∥ (♯‘𝐵)}
⊆ {𝑎 ∈
(1...(♯‘𝐵))
∣ 𝑎 ∥
(♯‘𝐵)}) |
298 | 296, 297 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) |
299 | 298 | sseld 3993 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} → 𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)})) |
300 | 299 | imp 406 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) |
301 | 170 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → (♯‘𝐵) ∈
ℕ0) |
302 | 301 | nn0red 12585 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → (♯‘𝐵) ∈ ℝ) |
303 | 302 | leidd 11826 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → (♯‘𝐵) ≤ (♯‘𝐵)) |
304 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → 𝑧 = (♯‘𝐵)) |
305 | 304 | eqcomd 2740 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → (♯‘𝐵) = 𝑧) |
306 | 231 | elrab 3694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ↔ (𝑧 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑧 ∥ (♯‘𝐵))) |
307 | 306 | biimpi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} → (𝑧 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑧 ∥ (♯‘𝐵))) |
308 | 307 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (𝑧 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑧 ∥ (♯‘𝐵))) |
309 | 291 | adantrr 717 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑧 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑧 ∥ (♯‘𝐵))) → 𝑧 ≤ ((♯‘𝐵) − 1)) |
310 | 309 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → ((𝑧 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑧 ∥ (♯‘𝐵)) → 𝑧 ≤ ((♯‘𝐵) − 1))) |
311 | 310 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → ((𝑧 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑧 ∥ (♯‘𝐵)) → 𝑧 ≤ ((♯‘𝐵) − 1))) |
312 | 308, 311 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝑧 ≤ ((♯‘𝐵) − 1)) |
313 | 300, 233,
248 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝑧 ∈ ℤ) |
314 | 280 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (♯‘𝐵) ∈
ℤ) |
315 | 313, 314 | zltlem1d 12668 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (𝑧 < (♯‘𝐵) ↔ 𝑧 ≤ ((♯‘𝐵) − 1))) |
316 | 312, 315 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝑧 < (♯‘𝐵)) |
317 | 316 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → 𝑧 < (♯‘𝐵)) |
318 | 305, 317 | eqbrtrd 5169 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → (♯‘𝐵) < (♯‘𝐵)) |
319 | 302, 302 | ltnled 11405 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → ((♯‘𝐵) < (♯‘𝐵) ↔ ¬ (♯‘𝐵) ≤ (♯‘𝐵))) |
320 | 318, 319 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → ¬ (♯‘𝐵) ≤ (♯‘𝐵)) |
321 | 303, 320 | pm2.21dd 195 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → 𝑧 ≠ (♯‘𝐵)) |
322 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 ≠ (♯‘𝐵)) → 𝑧 ≠ (♯‘𝐵)) |
323 | 321, 322 | pm2.61dane 3026 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝑧 ≠ (♯‘𝐵)) |
324 | 300, 323 | eldifsnd 4791 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝑧 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) |
325 | 324 | ex 412 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} → 𝑧 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}))) |
326 | 325 | ssrdv 4000 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) |
327 | 278, 326 | eqssd 4012 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}) = {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) |
328 | 327 | sumeq1d 15732 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = Σ𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})) |
329 | | fzfid 14010 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1...((♯‘𝐵) − 1)) ∈
Fin) |
330 | | ssrab2 4089 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑎 ∈
(1...((♯‘𝐵)
− 1)) ∣ 𝑎
∥ (♯‘𝐵)}
⊆ (1...((♯‘𝐵) − 1)) |
331 | 330 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆
(1...((♯‘𝐵)
− 1))) |
332 | 329, 331 | ssfid 9298 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ∈ Fin) |
333 | 26 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝐵 ∈ Fin) |
334 | 88 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ⊆ 𝐵) |
335 | 333, 334 | ssfid 9298 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∈ Fin) |
336 | 335, 91 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈
ℕ0) |
337 | 336 | nn0red 12585 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℝ) |
338 | 125 | elrab 3694 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ↔ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) |
339 | 338 | biimpi 216 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} → (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) |
340 | 339 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) |
341 | | elfzelz 13560 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 ∈
(1...((♯‘𝐵)
− 1)) → 𝑘 ∈
ℤ) |
342 | | elfzle1 13563 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 ∈
(1...((♯‘𝐵)
− 1)) → 1 ≤ 𝑘) |
343 | 341, 342 | jca 511 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 ∈
(1...((♯‘𝐵)
− 1)) → (𝑘
∈ ℤ ∧ 1 ≤ 𝑘)) |
344 | 343 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈
(1...((♯‘𝐵)
− 1)) ∧ 𝑘 ∥
(♯‘𝐵)) →
(𝑘 ∈ ℤ ∧ 1
≤ 𝑘)) |
345 | 344 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘)) |
346 | 345, 135 | sylibr 234 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) → 𝑘 ∈ ℕ) |
347 | 346 | ex 412 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵)) → 𝑘 ∈ ℕ)) |
348 | 347 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → ((𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵)) → 𝑘 ∈ ℕ)) |
349 | 340, 348 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝑘 ∈ ℕ) |
350 | 349 | phicld 16805 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (ϕ‘𝑘) ∈
ℕ) |
351 | 350 | nnred 12278 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (ϕ‘𝑘) ∈
ℝ) |
352 | | simpll 767 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → 𝜑) |
353 | 338 | biimpri 228 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑘 ∈
(1...((♯‘𝐵)
− 1)) ∧ 𝑘 ∥
(♯‘𝐵)) →
𝑘 ∈ {𝑎 ∈
(1...((♯‘𝐵)
− 1)) ∣ 𝑎
∥ (♯‘𝐵)}) |
354 | 353 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) → 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) |
355 | 354 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) |
356 | 352, 355 | jca 511 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)})) |
357 | 356, 337 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℝ) |
358 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) |
359 | 356, 358 | jca 511 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅)) |
360 | 340 | simprd 495 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝑘 ∥ (♯‘𝐵)) |
361 | 360 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → 𝑘 ∥ (♯‘𝐵)) |
362 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) |
363 | 361, 362 | jca 511 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅)) |
364 | | breq1 5150 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑚 = 𝑘 → (𝑚 ∥ (♯‘𝐵) ↔ 𝑘 ∥ (♯‘𝐵))) |
365 | | eqeq2 2746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑚 = 𝑘 → (((od‘𝐺)‘𝑥) = 𝑚 ↔ ((od‘𝐺)‘𝑥) = 𝑘)) |
366 | 365 | rabbidv 3440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑚 = 𝑘 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) |
367 | 366 | neeq1d 2997 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑚 = 𝑘 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅ ↔ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅)) |
368 | 364, 367 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑚 = 𝑘 → ((𝑚 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅) ↔ (𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅))) |
369 | 366 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑚 = 𝑘 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})) |
370 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑚 = 𝑘 → (ϕ‘𝑚) = (ϕ‘𝑘)) |
371 | 369, 370 | eqeq12d 2750 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑚 = 𝑘 → ((♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚}) = (ϕ‘𝑚) ↔ (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘))) |
372 | 368, 371 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑚 = 𝑘 → (((𝑚 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚}) = (ϕ‘𝑚)) ↔ ((𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘)))) |
373 | 28 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → ∀𝑚 ∈ ℕ ((𝑚 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚}) = (ϕ‘𝑚))) |
374 | 372, 373,
349 | rspcdva 3622 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → ((𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘))) |
375 | 374 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → ((𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘))) |
376 | 363, 375 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘)) |
377 | 359, 376 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘)) |
378 | 357, 377 | eqled 11361 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ (ϕ‘𝑘)) |
379 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅ → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) |
380 | 379 | necon1bi 2966 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (¬
{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅ → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} = ∅) |
381 | 380 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} = ∅) |
382 | 381 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) =
(♯‘∅)) |
383 | 223 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) →
(♯‘∅) = 0) |
384 | 382, 383 | eqtrd 2774 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = 0) |
385 | 346 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → 𝑘 ∈ ℕ) |
386 | 385 | phicld 16805 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (ϕ‘𝑘) ∈
ℕ) |
387 | 386 | nnnn0d 12584 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (ϕ‘𝑘) ∈
ℕ0) |
388 | 387 | nn0ge0d 12587 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → 0 ≤
(ϕ‘𝑘)) |
389 | 384, 388 | eqbrtrd 5169 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ (ϕ‘𝑘)) |
390 | 378, 389 | pm2.61dan 813 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ (ϕ‘𝑘)) |
391 | 390 | ex 412 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵)) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ (ϕ‘𝑘))) |
392 | 391 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → ((𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵)) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ (ϕ‘𝑘))) |
393 | 340, 392 | mpd 15 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ (ϕ‘𝑘)) |
394 | 332, 337,
351, 393 | fsumle 15831 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ Σ𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘)) |
395 | 327 | sumeq1d 15732 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘) = Σ𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘)) |
396 | 395 | eqcomd 2740 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘) = Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘)) |
397 | 394, 396 | breqtrd 5173 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘)) |
398 | 328, 397 | eqbrtrd 5169 |
. . . . . . . . . . . . 13
⊢ (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘)) |
399 | 398 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘)) |
400 | 113, 121,
123, 140, 227, 399 | ltleaddd 11881 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → ((♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) + Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})) < ((ϕ‘(♯‘𝐵)) + Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘))) |
401 | | nfcv 2902 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘(ϕ‘(♯‘𝐵)) |
402 | | simpll 767 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝜑) |
403 | 127 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (𝑘 ∈ (1...(♯‘𝐵)) ∧ 𝑘 ∥ (♯‘𝐵))) |
404 | 402, 403 | jca 511 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (𝜑 ∧ (𝑘 ∈ (1...(♯‘𝐵)) ∧ 𝑘 ∥ (♯‘𝐵)))) |
405 | 131 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑘 ∈ (1...(♯‘𝐵)) ∧ 𝑘 ∥ (♯‘𝐵))) → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘)) |
406 | 405 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ (𝜑 ∧ (𝑘 ∈ (1...(♯‘𝐵)) ∧ 𝑘 ∥ (♯‘𝐵)))) → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘)) |
407 | 406, 135 | sylibr 234 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ (𝜑 ∧ (𝑘 ∈ (1...(♯‘𝐵)) ∧ 𝑘 ∥ (♯‘𝐵)))) → 𝑘 ∈ ℕ) |
408 | 407 | ex 412 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → ((𝜑 ∧ (𝑘 ∈ (1...(♯‘𝐵)) ∧ 𝑘 ∥ (♯‘𝐵))) → 𝑘 ∈ ℕ)) |
409 | 404, 408 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝑘 ∈ ℕ) |
410 | 409 | phicld 16805 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (ϕ‘𝑘) ∈ ℕ) |
411 | 410 | nncnd 12279 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (ϕ‘𝑘) ∈ ℂ) |
412 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑘 = (♯‘𝐵) → (ϕ‘𝑘) =
(ϕ‘(♯‘𝐵))) |
413 | 81, 401, 86, 411, 103, 412 | fsumsplit1 15777 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘) = ((ϕ‘(♯‘𝐵)) + Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘))) |
414 | 400, 413 | breqtrrd 5175 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → ((♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) + Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})) < Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘)) |
415 | 107, 414 | eqbrtrd 5169 |
. . . . . . . . 9
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) < Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘)) |
416 | | elfzelz 13560 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈
(1...(♯‘𝐵))
→ 𝑎 ∈
ℤ) |
417 | | elfzle1 13563 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈
(1...(♯‘𝐵))
→ 1 ≤ 𝑎) |
418 | 416, 417 | jca 511 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈
(1...(♯‘𝐵))
→ (𝑎 ∈ ℤ
∧ 1 ≤ 𝑎)) |
419 | 418 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈
(1...(♯‘𝐵))
∧ 𝑎 ∥
(♯‘𝐵)) →
(𝑎 ∈ ℤ ∧ 1
≤ 𝑎)) |
420 | 419 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ (1...(♯‘𝐵)) ∧ 𝑎 ∥ (♯‘𝐵))) → (𝑎 ∈ ℤ ∧ 1 ≤ 𝑎)) |
421 | | elnnz1 12640 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ ℕ ↔ (𝑎 ∈ ℤ ∧ 1 ≤
𝑎)) |
422 | 420, 421 | sylibr 234 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ (1...(♯‘𝐵)) ∧ 𝑎 ∥ (♯‘𝐵))) → 𝑎 ∈ ℕ) |
423 | 422 | rabss3d 4090 |
. . . . . . . . . . . 12
⊢ (𝜑 → {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)}) |
424 | | simpl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑎 ∥ (♯‘𝐵))) → 𝜑) |
425 | | simprl 771 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑎 ∥ (♯‘𝐵))) → 𝑎 ∈ ℕ) |
426 | 424, 425 | jca 511 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑎 ∥ (♯‘𝐵))) → (𝜑 ∧ 𝑎 ∈ ℕ)) |
427 | | simprr 773 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑎 ∥ (♯‘𝐵))) → 𝑎 ∥ (♯‘𝐵)) |
428 | 426, 427 | jca 511 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑎 ∥ (♯‘𝐵))) → ((𝜑 ∧ 𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵))) |
429 | | 1zzd 12645 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)) → 1 ∈ ℤ) |
430 | 280 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ) → (♯‘𝐵) ∈
ℤ) |
431 | 430 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)) → (♯‘𝐵) ∈ ℤ) |
432 | 425 | anassrs 467 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)) → 𝑎 ∈ ℕ) |
433 | 432 | nnzd 12637 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)) → 𝑎 ∈ ℤ) |
434 | 432 | nnge1d 12311 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)) → 1 ≤ 𝑎) |
435 | | nnz 12631 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ∈ ℕ → 𝑎 ∈
ℤ) |
436 | 435 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ) → 𝑎 ∈ ℤ) |
437 | 23, 25, 26 | hashfingrpnn 19002 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (♯‘𝐵) ∈
ℕ) |
438 | 437 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ) → (♯‘𝐵) ∈
ℕ) |
439 | | dvdsle 16343 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ ℤ ∧
(♯‘𝐵) ∈
ℕ) → (𝑎 ∥
(♯‘𝐵) →
𝑎 ≤ (♯‘𝐵))) |
440 | 436, 438,
439 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ) → (𝑎 ∥ (♯‘𝐵) → 𝑎 ≤ (♯‘𝐵))) |
441 | 440 | imp 406 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)) → 𝑎 ≤ (♯‘𝐵)) |
442 | 429, 431,
433, 434, 441 | elfzd 13551 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)) → 𝑎 ∈ (1...(♯‘𝐵))) |
443 | 428, 442 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑎 ∥ (♯‘𝐵))) → 𝑎 ∈ (1...(♯‘𝐵))) |
444 | 443 | rabss3d 4090 |
. . . . . . . . . . . 12
⊢ (𝜑 → {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) |
445 | 423, 444 | eqssd 4012 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} = {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)}) |
446 | 445 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} = {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)}) |
447 | 446 | sumeq1d 15732 |
. . . . . . . . 9
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘) = Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘)) |
448 | 415, 447 | breqtrd 5173 |
. . . . . . . 8
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) < Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘)) |
449 | | phisum 16823 |
. . . . . . . . 9
⊢
((♯‘𝐵)
∈ ℕ → Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘) = (♯‘𝐵)) |
450 | 39, 449 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘) = (♯‘𝐵)) |
451 | 448, 450 | breqtrd 5173 |
. . . . . . 7
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) < (♯‘𝐵)) |
452 | 80, 451 | eqbrtrd 5169 |
. . . . . 6
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) < (♯‘𝐵)) |
453 | 170 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∈
ℕ0) |
454 | 453 | nn0red 12585 |
. . . . . . 7
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∈
ℝ) |
455 | 454 | ltnrd 11392 |
. . . . . 6
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → ¬
(♯‘𝐵) <
(♯‘𝐵)) |
456 | 452, 455 | pm2.21dd 195 |
. . . . 5
⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘{𝑦 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷}) = (ϕ‘𝐷)) |
457 | 456 | ex 412 |
. . . 4
⊢ (𝜑 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅ → (♯‘{𝑦 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷}) = (ϕ‘𝐷))) |
458 | 457 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅ → (♯‘{𝑦 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷}) = (ϕ‘𝐷))) |
459 | 36, 458 | mpd 15 |
. 2
⊢ ((𝜑 ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → (♯‘{𝑦 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷}) = (ϕ‘𝐷)) |
460 | 33, 459 | pm2.61dan 813 |
1
⊢ (𝜑 → (♯‘{𝑦 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷}) = (ϕ‘𝐷)) |