Step | Hyp | Ref
| Expression |
1 | | rusisusgra 26458 |
. . . . . 6
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → 𝑉 USGrph 𝐸) |
2 | 1 | 3ad2ant1 1075 |
. . . . 5
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) → 𝑉 USGrph 𝐸) |
3 | 2 | adantr 480 |
. . . 4
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → 𝑉 USGrph 𝐸) |
4 | | simp3 1056 |
. . . . 5
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) → 𝑉 ∈ Fin) |
5 | 4 | adantr 480 |
. . . 4
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → 𝑉 ∈ Fin) |
6 | | prmnn 15226 |
. . . . . 6
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
7 | 6 | nnnn0d 11228 |
. . . . 5
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ0) |
8 | 7 | ad2antrl 760 |
. . . 4
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → 𝑃 ∈
ℕ0) |
9 | | numclwwlk.c |
. . . . 5
⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛)) |
10 | | numclwwlk.f |
. . . . 5
⊢ 𝐹 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝐶‘𝑛) ∣ (𝑤‘0) = 𝑣}) |
11 | 9, 10 | numclwwlk4 26637 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑃 ∈ ℕ0) →
(#‘(𝐶‘𝑃)) = Σ𝑥 ∈ 𝑉 (#‘(𝑥𝐹𝑃))) |
12 | 3, 5, 8, 11 | syl3anc 1318 |
. . 3
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (#‘(𝐶‘𝑃)) = Σ𝑥 ∈ 𝑉 (#‘(𝑥𝐹𝑃))) |
13 | 12 | oveq1d 6564 |
. 2
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((#‘(𝐶‘𝑃)) mod 𝑃) = (Σ𝑥 ∈ 𝑉 (#‘(𝑥𝐹𝑃)) mod 𝑃)) |
14 | 6 | ad2antrl 760 |
. . . 4
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → 𝑃 ∈ ℕ) |
15 | | usgrav 25867 |
. . . . . . . . . . . . . . 15
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
16 | 15 | simprd 478 |
. . . . . . . . . . . . . 14
⊢ (𝑉 USGrph 𝐸 → 𝐸 ∈ V) |
17 | 1, 16 | syl 17 |
. . . . . . . . . . . . 13
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → 𝐸 ∈ V) |
18 | 17 | anim1i 590 |
. . . . . . . . . . . 12
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 ∈ Fin) → (𝐸 ∈ V ∧ 𝑉 ∈ Fin)) |
19 | 18 | ancomd 466 |
. . . . . . . . . . 11
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 ∈ Fin) → (𝑉 ∈ Fin ∧ 𝐸 ∈ V)) |
20 | 19 | 3adant2 1073 |
. . . . . . . . . 10
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) → (𝑉 ∈ Fin ∧ 𝐸 ∈ V)) |
21 | 20 | adantr 480 |
. . . . . . . . 9
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (𝑉 ∈ Fin ∧ 𝐸 ∈ V)) |
22 | 21 | adantr 480 |
. . . . . . . 8
⊢
((((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) ∧ 𝑥 ∈ 𝑉) → (𝑉 ∈ Fin ∧ 𝐸 ∈ V)) |
23 | 8 | anim1i 590 |
. . . . . . . . 9
⊢
((((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) ∧ 𝑥 ∈ 𝑉) → (𝑃 ∈ ℕ0 ∧ 𝑥 ∈ 𝑉)) |
24 | 23 | ancomd 466 |
. . . . . . . 8
⊢
((((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) ∧ 𝑥 ∈ 𝑉) → (𝑥 ∈ 𝑉 ∧ 𝑃 ∈
ℕ0)) |
25 | 9, 10 | numclwwlkffin 26609 |
. . . . . . . 8
⊢ (((𝑉 ∈ Fin ∧ 𝐸 ∈ V) ∧ (𝑥 ∈ 𝑉 ∧ 𝑃 ∈ ℕ0)) → (𝑥𝐹𝑃) ∈ Fin) |
26 | 22, 24, 25 | syl2anc 691 |
. . . . . . 7
⊢
((((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) ∧ 𝑥 ∈ 𝑉) → (𝑥𝐹𝑃) ∈ Fin) |
27 | | hashcl 13009 |
. . . . . . 7
⊢ ((𝑥𝐹𝑃) ∈ Fin → (#‘(𝑥𝐹𝑃)) ∈
ℕ0) |
28 | 26, 27 | syl 17 |
. . . . . 6
⊢
((((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) ∧ 𝑥 ∈ 𝑉) → (#‘(𝑥𝐹𝑃)) ∈
ℕ0) |
29 | 28 | nn0zd 11356 |
. . . . 5
⊢
((((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) ∧ 𝑥 ∈ 𝑉) → (#‘(𝑥𝐹𝑃)) ∈ ℤ) |
30 | 29 | ralrimiva 2949 |
. . . 4
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ∀𝑥 ∈ 𝑉 (#‘(𝑥𝐹𝑃)) ∈ ℤ) |
31 | 14, 5, 30 | modfsummod 14367 |
. . 3
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (Σ𝑥 ∈ 𝑉 (#‘(𝑥𝐹𝑃)) mod 𝑃) = (Σ𝑥 ∈ 𝑉 ((#‘(𝑥𝐹𝑃)) mod 𝑃) mod 𝑃)) |
32 | | simpll 786 |
. . . . . 6
⊢
((((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) ∧ 𝑥 ∈ 𝑉) → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin)) |
33 | | simpr 476 |
. . . . . 6
⊢
((((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ 𝑉) |
34 | | simplrl 796 |
. . . . . 6
⊢
((((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) ∧ 𝑥 ∈ 𝑉) → 𝑃 ∈ ℙ) |
35 | | simplrr 797 |
. . . . . 6
⊢
((((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) ∧ 𝑥 ∈ 𝑉) → 𝑃 ∥ (𝐾 − 1)) |
36 | 9, 10 | numclwwlk5 26639 |
. . . . . 6
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑥 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((#‘(𝑥𝐹𝑃)) mod 𝑃) = 1) |
37 | 32, 33, 34, 35, 36 | syl13anc 1320 |
. . . . 5
⊢
((((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) ∧ 𝑥 ∈ 𝑉) → ((#‘(𝑥𝐹𝑃)) mod 𝑃) = 1) |
38 | 37 | sumeq2dv 14281 |
. . . 4
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → Σ𝑥 ∈ 𝑉 ((#‘(𝑥𝐹𝑃)) mod 𝑃) = Σ𝑥 ∈ 𝑉 1) |
39 | 38 | oveq1d 6564 |
. . 3
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (Σ𝑥 ∈ 𝑉 ((#‘(𝑥𝐹𝑃)) mod 𝑃) mod 𝑃) = (Σ𝑥 ∈ 𝑉 1 mod 𝑃)) |
40 | 31, 39 | eqtrd 2644 |
. 2
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (Σ𝑥 ∈ 𝑉 (#‘(𝑥𝐹𝑃)) mod 𝑃) = (Σ𝑥 ∈ 𝑉 1 mod 𝑃)) |
41 | | ax-1cn 9873 |
. . . . . . 7
⊢ 1 ∈
ℂ |
42 | 4, 41 | jctir 559 |
. . . . . 6
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) → (𝑉 ∈ Fin ∧ 1 ∈
ℂ)) |
43 | 42 | adantr 480 |
. . . . 5
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (𝑉 ∈ Fin ∧ 1 ∈
ℂ)) |
44 | | fsumconst 14364 |
. . . . 5
⊢ ((𝑉 ∈ Fin ∧ 1 ∈
ℂ) → Σ𝑥
∈ 𝑉 1 =
((#‘𝑉) ·
1)) |
45 | 43, 44 | syl 17 |
. . . 4
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → Σ𝑥 ∈ 𝑉 1 = ((#‘𝑉) · 1)) |
46 | | hashcl 13009 |
. . . . . . . 8
⊢ (𝑉 ∈ Fin →
(#‘𝑉) ∈
ℕ0) |
47 | 46 | nn0red 11229 |
. . . . . . 7
⊢ (𝑉 ∈ Fin →
(#‘𝑉) ∈
ℝ) |
48 | 47 | 3ad2ant3 1077 |
. . . . . 6
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) → (#‘𝑉) ∈
ℝ) |
49 | 48 | adantr 480 |
. . . . 5
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (#‘𝑉) ∈
ℝ) |
50 | | ax-1rid 9885 |
. . . . 5
⊢
((#‘𝑉) ∈
ℝ → ((#‘𝑉)
· 1) = (#‘𝑉)) |
51 | 49, 50 | syl 17 |
. . . 4
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((#‘𝑉) · 1) = (#‘𝑉)) |
52 | 45, 51 | eqtrd 2644 |
. . 3
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → Σ𝑥 ∈ 𝑉 1 = (#‘𝑉)) |
53 | 52 | oveq1d 6564 |
. 2
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (Σ𝑥 ∈ 𝑉 1 mod 𝑃) = ((#‘𝑉) mod 𝑃)) |
54 | 13, 40, 53 | 3eqtrd 2648 |
1
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((#‘(𝐶‘𝑃)) mod 𝑃) = ((#‘𝑉) mod 𝑃)) |