Step | Hyp | Ref
| Expression |
1 | | numclwwlk6.v |
. . . . . 6
⊢ 𝑉 = (Vtx‘𝐺) |
2 | 1 | finrusgrfusgr 26913 |
. . . . 5
⊢ ((𝐺RegUSGraph𝐾 ∧ 𝑉 ∈ Fin) → 𝐺 ∈ FinUSGraph) |
3 | 2 | 3adant2 1122 |
. . . 4
⊢ ((𝐺RegUSGraph𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) → 𝐺 ∈ FinUSGraph) |
4 | | prmnn 15793 |
. . . . 5
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
5 | 4 | adantr 474 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)) → 𝑃 ∈ ℕ) |
6 | 1 | numclwwlk4 27818 |
. . . 4
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑃 ∈ ℕ) →
(♯‘(𝑃 ClWWalksN
𝐺)) = Σ𝑥 ∈ 𝑉 (♯‘(𝑥(ClWWalksNOn‘𝐺)𝑃))) |
7 | 3, 5, 6 | syl2an 589 |
. . 3
⊢ (((𝐺RegUSGraph𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (♯‘(𝑃 ClWWalksN 𝐺)) = Σ𝑥 ∈ 𝑉 (♯‘(𝑥(ClWWalksNOn‘𝐺)𝑃))) |
8 | 7 | oveq1d 6937 |
. 2
⊢ (((𝐺RegUSGraph𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((♯‘(𝑃 ClWWalksN 𝐺)) mod 𝑃) = (Σ𝑥 ∈ 𝑉 (♯‘(𝑥(ClWWalksNOn‘𝐺)𝑃)) mod 𝑃)) |
9 | 5 | adantl 475 |
. . . 4
⊢ (((𝐺RegUSGraph𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → 𝑃 ∈ ℕ) |
10 | | simp3 1129 |
. . . . 5
⊢ ((𝐺RegUSGraph𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) → 𝑉 ∈ Fin) |
11 | 10 | adantr 474 |
. . . 4
⊢ (((𝐺RegUSGraph𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → 𝑉 ∈ Fin) |
12 | 11 | adantr 474 |
. . . . . . 7
⊢ ((((𝐺RegUSGraph𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) ∧ 𝑥 ∈ 𝑉) → 𝑉 ∈ Fin) |
13 | 1 | clwwlknonfin 27496 |
. . . . . . 7
⊢ (𝑉 ∈ Fin → (𝑥(ClWWalksNOn‘𝐺)𝑃) ∈ Fin) |
14 | | hashcl 13462 |
. . . . . . 7
⊢ ((𝑥(ClWWalksNOn‘𝐺)𝑃) ∈ Fin → (♯‘(𝑥(ClWWalksNOn‘𝐺)𝑃)) ∈
ℕ0) |
15 | 12, 13, 14 | 3syl 18 |
. . . . . 6
⊢ ((((𝐺RegUSGraph𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) ∧ 𝑥 ∈ 𝑉) → (♯‘(𝑥(ClWWalksNOn‘𝐺)𝑃)) ∈
ℕ0) |
16 | 15 | nn0zd 11832 |
. . . . 5
⊢ ((((𝐺RegUSGraph𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) ∧ 𝑥 ∈ 𝑉) → (♯‘(𝑥(ClWWalksNOn‘𝐺)𝑃)) ∈ ℤ) |
17 | 16 | ralrimiva 3148 |
. . . 4
⊢ (((𝐺RegUSGraph𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ∀𝑥 ∈ 𝑉 (♯‘(𝑥(ClWWalksNOn‘𝐺)𝑃)) ∈ ℤ) |
18 | 9, 11, 17 | modfsummod 14930 |
. . 3
⊢ (((𝐺RegUSGraph𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (Σ𝑥 ∈ 𝑉 (♯‘(𝑥(ClWWalksNOn‘𝐺)𝑃)) mod 𝑃) = (Σ𝑥 ∈ 𝑉 ((♯‘(𝑥(ClWWalksNOn‘𝐺)𝑃)) mod 𝑃) mod 𝑃)) |
19 | | simpl 476 |
. . . . . 6
⊢ (((𝐺RegUSGraph𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (𝐺RegUSGraph𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin)) |
20 | | simpr 479 |
. . . . . . . . 9
⊢ (((𝐺RegUSGraph𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) |
21 | 20 | anim1i 608 |
. . . . . . . 8
⊢ ((((𝐺RegUSGraph𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) ∧ 𝑥 ∈ 𝑉) → ((𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)) ∧ 𝑥 ∈ 𝑉)) |
22 | 21 | ancomd 455 |
. . . . . . 7
⊢ ((((𝐺RegUSGraph𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) ∧ 𝑥 ∈ 𝑉) → (𝑥 ∈ 𝑉 ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)))) |
23 | | 3anass 1079 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)) ↔ (𝑥 ∈ 𝑉 ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)))) |
24 | 22, 23 | sylibr 226 |
. . . . . 6
⊢ ((((𝐺RegUSGraph𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) ∧ 𝑥 ∈ 𝑉) → (𝑥 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) |
25 | 1 | numclwwlk5 27820 |
. . . . . 6
⊢ (((𝐺RegUSGraph𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑥 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((♯‘(𝑥(ClWWalksNOn‘𝐺)𝑃)) mod 𝑃) = 1) |
26 | 19, 24, 25 | syl2an2r 675 |
. . . . 5
⊢ ((((𝐺RegUSGraph𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) ∧ 𝑥 ∈ 𝑉) → ((♯‘(𝑥(ClWWalksNOn‘𝐺)𝑃)) mod 𝑃) = 1) |
27 | 26 | sumeq2dv 14841 |
. . . 4
⊢ (((𝐺RegUSGraph𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → Σ𝑥 ∈ 𝑉 ((♯‘(𝑥(ClWWalksNOn‘𝐺)𝑃)) mod 𝑃) = Σ𝑥 ∈ 𝑉 1) |
28 | 27 | oveq1d 6937 |
. . 3
⊢ (((𝐺RegUSGraph𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (Σ𝑥 ∈ 𝑉 ((♯‘(𝑥(ClWWalksNOn‘𝐺)𝑃)) mod 𝑃) mod 𝑃) = (Σ𝑥 ∈ 𝑉 1 mod 𝑃)) |
29 | 18, 28 | eqtrd 2814 |
. 2
⊢ (((𝐺RegUSGraph𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (Σ𝑥 ∈ 𝑉 (♯‘(𝑥(ClWWalksNOn‘𝐺)𝑃)) mod 𝑃) = (Σ𝑥 ∈ 𝑉 1 mod 𝑃)) |
30 | | 1cnd 10371 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)) → 1 ∈
ℂ) |
31 | | fsumconst 14926 |
. . . . 5
⊢ ((𝑉 ∈ Fin ∧ 1 ∈
ℂ) → Σ𝑥
∈ 𝑉 1 =
((♯‘𝑉) ·
1)) |
32 | 10, 30, 31 | syl2an 589 |
. . . 4
⊢ (((𝐺RegUSGraph𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → Σ𝑥 ∈ 𝑉 1 = ((♯‘𝑉) · 1)) |
33 | | hashcl 13462 |
. . . . . . . 8
⊢ (𝑉 ∈ Fin →
(♯‘𝑉) ∈
ℕ0) |
34 | 33 | nn0red 11703 |
. . . . . . 7
⊢ (𝑉 ∈ Fin →
(♯‘𝑉) ∈
ℝ) |
35 | | ax-1rid 10342 |
. . . . . . 7
⊢
((♯‘𝑉)
∈ ℝ → ((♯‘𝑉) · 1) = (♯‘𝑉)) |
36 | 34, 35 | syl 17 |
. . . . . 6
⊢ (𝑉 ∈ Fin →
((♯‘𝑉) ·
1) = (♯‘𝑉)) |
37 | 36 | 3ad2ant3 1126 |
. . . . 5
⊢ ((𝐺RegUSGraph𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) → ((♯‘𝑉) · 1) =
(♯‘𝑉)) |
38 | 37 | adantr 474 |
. . . 4
⊢ (((𝐺RegUSGraph𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((♯‘𝑉) · 1) =
(♯‘𝑉)) |
39 | 32, 38 | eqtrd 2814 |
. . 3
⊢ (((𝐺RegUSGraph𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → Σ𝑥 ∈ 𝑉 1 = (♯‘𝑉)) |
40 | 39 | oveq1d 6937 |
. 2
⊢ (((𝐺RegUSGraph𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (Σ𝑥 ∈ 𝑉 1 mod 𝑃) = ((♯‘𝑉) mod 𝑃)) |
41 | 8, 29, 40 | 3eqtrd 2818 |
1
⊢ (((𝐺RegUSGraph𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((♯‘(𝑃 ClWWalksN 𝐺)) mod 𝑃) = ((♯‘𝑉) mod 𝑃)) |