Step | Hyp | Ref
| Expression |
1 | | prmnn 15226 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
2 | 1 | nnnn0d 11228 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ0) |
3 | 2 | adantr 480 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)) → 𝑃 ∈
ℕ0) |
4 | 3 | 3ad2ant3 1077 |
. . . . . 6
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → 𝑃 ∈
ℕ0) |
5 | | eqid 2610 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ0
↦ ((𝑉 ClWWalksN 𝐸)‘𝑛)) = (𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛)) |
6 | 5 | numclwwlkfvc 26604 |
. . . . . 6
⊢ (𝑃 ∈ ℕ0
→ ((𝑛 ∈
ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛))‘𝑃) = ((𝑉 ClWWalksN 𝐸)‘𝑃)) |
7 | 4, 6 | syl 17 |
. . . . 5
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛))‘𝑃) = ((𝑉 ClWWalksN 𝐸)‘𝑃)) |
8 | 7 | eqcomd 2616 |
. . . 4
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((𝑉 ClWWalksN 𝐸)‘𝑃) = ((𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛))‘𝑃)) |
9 | 8 | fveq2d 6107 |
. . 3
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (#‘((𝑉 ClWWalksN 𝐸)‘𝑃)) = (#‘((𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛))‘𝑃))) |
10 | 9 | oveq1d 6564 |
. 2
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((#‘((𝑉 ClWWalksN 𝐸)‘𝑃)) mod 𝑃) = ((#‘((𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛))‘𝑃)) mod 𝑃)) |
11 | | simpr 476 |
. . . . 5
⊢ ((𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) → 𝑉 ∈ Fin) |
12 | 11 | anim2i 591 |
. . . 4
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin)) → ((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ 𝑉 ∈ Fin)) |
13 | | df-3an 1033 |
. . . 4
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ↔ ((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ 𝑉 ∈ Fin)) |
14 | 12, 13 | sylibr 223 |
. . 3
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin)) → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin)) |
15 | | fveq2 6103 |
. . . . 5
⊢ (𝑛 = 𝑚 → ((𝑉 ClWWalksN 𝐸)‘𝑛) = ((𝑉 ClWWalksN 𝐸)‘𝑚)) |
16 | 15 | cbvmptv 4678 |
. . . 4
⊢ (𝑛 ∈ ℕ0
↦ ((𝑉 ClWWalksN 𝐸)‘𝑛)) = (𝑚 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑚)) |
17 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑝 = 𝑞 → (𝑝‘0) = (𝑞‘0)) |
18 | 17 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑝 = 𝑞 → ((𝑝‘0) = 𝑣 ↔ (𝑞‘0) = 𝑣)) |
19 | 18 | cbvrabv 3172 |
. . . . . 6
⊢ {𝑝 ∈ ((𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛))‘𝑚) ∣ (𝑝‘0) = 𝑣} = {𝑞 ∈ ((𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛))‘𝑚) ∣ (𝑞‘0) = 𝑣} |
20 | 19 | a1i 11 |
. . . . 5
⊢ ((𝑣 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) → {𝑝 ∈ ((𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛))‘𝑚) ∣ (𝑝‘0) = 𝑣} = {𝑞 ∈ ((𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛))‘𝑚) ∣ (𝑞‘0) = 𝑣}) |
21 | 20 | mpt2eq3ia 6618 |
. . . 4
⊢ (𝑣 ∈ 𝑉, 𝑚 ∈ ℕ0 ↦ {𝑝 ∈ ((𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛))‘𝑚) ∣ (𝑝‘0) = 𝑣}) = (𝑣 ∈ 𝑉, 𝑚 ∈ ℕ0 ↦ {𝑞 ∈ ((𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛))‘𝑚) ∣ (𝑞‘0) = 𝑣}) |
22 | 16, 21 | numclwwlk6 26640 |
. . 3
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((#‘((𝑛 ∈ ℕ0
↦ ((𝑉 ClWWalksN 𝐸)‘𝑛))‘𝑃)) mod 𝑃) = ((#‘𝑉) mod 𝑃)) |
23 | 14, 22 | stoic3 1692 |
. 2
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((#‘((𝑛 ∈ ℕ0
↦ ((𝑉 ClWWalksN 𝐸)‘𝑛))‘𝑃)) mod 𝑃) = ((#‘𝑉) mod 𝑃)) |
24 | | simp2 1055 |
. . . . . 6
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin)) |
25 | 24 | ancomd 466 |
. . . . 5
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) |
26 | | simp1 1054 |
. . . . . 6
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸)) |
27 | 26 | ancomd 466 |
. . . . 5
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾)) |
28 | | frrusgraord 26598 |
. . . . 5
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1))) |
29 | 25, 27, 28 | sylc 63 |
. . . 4
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1)) |
30 | 29 | oveq1d 6564 |
. . 3
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((#‘𝑉) mod 𝑃) = (((𝐾 · (𝐾 − 1)) + 1) mod 𝑃)) |
31 | | rusgraprop 26456 |
. . . . . . 7
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (𝑉 USGrph 𝐸 ∧ 𝐾 ∈ ℕ0 ∧
∀𝑥 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑥) = 𝐾)) |
32 | | nn0cn 11179 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℂ) |
33 | | peano2cnm 10226 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐾 ∈ ℂ → (𝐾 − 1) ∈
ℂ) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ ℕ0
→ (𝐾 − 1) ∈
ℂ) |
35 | 32, 34 | mulcomd 9940 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ ℕ0
→ (𝐾 · (𝐾 − 1)) = ((𝐾 − 1) · 𝐾)) |
36 | 35 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ ℕ0
→ ((𝐾 · (𝐾 − 1)) mod 𝑃) = (((𝐾 − 1) · 𝐾) mod 𝑃)) |
37 | 36 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ ℕ0
∧ (𝑃 ∈ ℙ
∧ 𝑃 ∥ (𝐾 − 1))) → ((𝐾 · (𝐾 − 1)) mod 𝑃) = (((𝐾 − 1) · 𝐾) mod 𝑃)) |
38 | 1 | ad2antrl 760 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ ℕ0
∧ (𝑃 ∈ ℙ
∧ 𝑃 ∥ (𝐾 − 1))) → 𝑃 ∈
ℕ) |
39 | | nn0z 11277 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℤ) |
40 | | peano2zm 11297 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐾 ∈ ℤ → (𝐾 − 1) ∈
ℤ) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ ℕ0
→ (𝐾 − 1) ∈
ℤ) |
42 | 41 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ ℕ0
∧ (𝑃 ∈ ℙ
∧ 𝑃 ∥ (𝐾 − 1))) → (𝐾 − 1) ∈
ℤ) |
43 | 39 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ ℕ0
∧ (𝑃 ∈ ℙ
∧ 𝑃 ∥ (𝐾 − 1))) → 𝐾 ∈
ℤ) |
44 | 38, 42, 43 | 3jca 1235 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℕ0
∧ (𝑃 ∈ ℙ
∧ 𝑃 ∥ (𝐾 − 1))) → (𝑃 ∈ ℕ ∧ (𝐾 − 1) ∈ ℤ ∧
𝐾 ∈
ℤ)) |
45 | | simprr 792 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℕ0
∧ (𝑃 ∈ ℙ
∧ 𝑃 ∥ (𝐾 − 1))) → 𝑃 ∥ (𝐾 − 1)) |
46 | | mulmoddvds 14889 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℕ ∧ (𝐾 − 1) ∈ ℤ ∧
𝐾 ∈ ℤ) →
(𝑃 ∥ (𝐾 − 1) → (((𝐾 − 1) · 𝐾) mod 𝑃) = 0)) |
47 | 44, 45, 46 | sylc 63 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ ℕ0
∧ (𝑃 ∈ ℙ
∧ 𝑃 ∥ (𝐾 − 1))) → (((𝐾 − 1) · 𝐾) mod 𝑃) = 0) |
48 | 37, 47 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ ℕ0
∧ (𝑃 ∈ ℙ
∧ 𝑃 ∥ (𝐾 − 1))) → ((𝐾 · (𝐾 − 1)) mod 𝑃) = 0) |
49 | 1 | nnred 10912 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℝ) |
50 | | prmgt1 15247 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ ℙ → 1 <
𝑃) |
51 | 49, 50 | jca 553 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℙ → (𝑃 ∈ ℝ ∧ 1 <
𝑃)) |
52 | 51 | ad2antrl 760 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ ℕ0
∧ (𝑃 ∈ ℙ
∧ 𝑃 ∥ (𝐾 − 1))) → (𝑃 ∈ ℝ ∧ 1 <
𝑃)) |
53 | | 1mod 12564 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℝ ∧ 1 <
𝑃) → (1 mod 𝑃) = 1) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ ℕ0
∧ (𝑃 ∈ ℙ
∧ 𝑃 ∥ (𝐾 − 1))) → (1 mod
𝑃) = 1) |
55 | 48, 54 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ ℕ0
∧ (𝑃 ∈ ℙ
∧ 𝑃 ∥ (𝐾 − 1))) → (((𝐾 · (𝐾 − 1)) mod 𝑃) + (1 mod 𝑃)) = (0 + 1)) |
56 | 55 | oveq1d 6564 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℕ0
∧ (𝑃 ∈ ℙ
∧ 𝑃 ∥ (𝐾 − 1))) → ((((𝐾 · (𝐾 − 1)) mod 𝑃) + (1 mod 𝑃)) mod 𝑃) = ((0 + 1) mod 𝑃)) |
57 | | nn0re 11178 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℝ) |
58 | | peano2rem 10227 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ ℝ → (𝐾 − 1) ∈
ℝ) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ ℕ0
→ (𝐾 − 1) ∈
ℝ) |
60 | 57, 59 | remulcld 9949 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ ℕ0
→ (𝐾 · (𝐾 − 1)) ∈
ℝ) |
61 | 60 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ ℕ0
∧ (𝑃 ∈ ℙ
∧ 𝑃 ∥ (𝐾 − 1))) → (𝐾 · (𝐾 − 1)) ∈
ℝ) |
62 | | 1red 9934 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ ℕ0
∧ (𝑃 ∈ ℙ
∧ 𝑃 ∥ (𝐾 − 1))) → 1 ∈
ℝ) |
63 | 1 | nnrpd 11746 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℝ+) |
64 | 63 | ad2antrl 760 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ ℕ0
∧ (𝑃 ∈ ℙ
∧ 𝑃 ∥ (𝐾 − 1))) → 𝑃 ∈
ℝ+) |
65 | | modaddabs 12570 |
. . . . . . . . . . 11
⊢ (((𝐾 · (𝐾 − 1)) ∈ ℝ ∧ 1 ∈
ℝ ∧ 𝑃 ∈
ℝ+) → ((((𝐾 · (𝐾 − 1)) mod 𝑃) + (1 mod 𝑃)) mod 𝑃) = (((𝐾 · (𝐾 − 1)) + 1) mod 𝑃)) |
66 | 61, 62, 64, 65 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℕ0
∧ (𝑃 ∈ ℙ
∧ 𝑃 ∥ (𝐾 − 1))) → ((((𝐾 · (𝐾 − 1)) mod 𝑃) + (1 mod 𝑃)) mod 𝑃) = (((𝐾 · (𝐾 − 1)) + 1) mod 𝑃)) |
67 | | 0p1e1 11009 |
. . . . . . . . . . . 12
⊢ (0 + 1) =
1 |
68 | 67 | oveq1i 6559 |
. . . . . . . . . . 11
⊢ ((0 + 1)
mod 𝑃) = (1 mod 𝑃) |
69 | 49, 50, 53 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ ℙ → (1 mod
𝑃) = 1) |
70 | 69 | ad2antrl 760 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ ℕ0
∧ (𝑃 ∈ ℙ
∧ 𝑃 ∥ (𝐾 − 1))) → (1 mod
𝑃) = 1) |
71 | 68, 70 | syl5eq 2656 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℕ0
∧ (𝑃 ∈ ℙ
∧ 𝑃 ∥ (𝐾 − 1))) → ((0 + 1)
mod 𝑃) =
1) |
72 | 56, 66, 71 | 3eqtr3d 2652 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℕ0
∧ (𝑃 ∈ ℙ
∧ 𝑃 ∥ (𝐾 − 1))) → (((𝐾 · (𝐾 − 1)) + 1) mod 𝑃) = 1) |
73 | 72 | ex 449 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ0
→ ((𝑃 ∈ ℙ
∧ 𝑃 ∥ (𝐾 − 1)) → (((𝐾 · (𝐾 − 1)) + 1) mod 𝑃) = 1)) |
74 | 73 | 3ad2ant2 1076 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ 𝐾 ∈ ℕ0 ∧
∀𝑥 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑥) = 𝐾) → ((𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)) → (((𝐾 · (𝐾 − 1)) + 1) mod 𝑃) = 1)) |
75 | 31, 74 | syl 17 |
. . . . . 6
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)) → (((𝐾 · (𝐾 − 1)) + 1) mod 𝑃) = 1)) |
76 | 75 | adantr 480 |
. . . . 5
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) → ((𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)) → (((𝐾 · (𝐾 − 1)) + 1) mod 𝑃) = 1)) |
77 | 76 | imp 444 |
. . . 4
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (((𝐾 · (𝐾 − 1)) + 1) mod 𝑃) = 1) |
78 | 77 | 3adant2 1073 |
. . 3
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (((𝐾 · (𝐾 − 1)) + 1) mod 𝑃) = 1) |
79 | 30, 78 | eqtrd 2644 |
. 2
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((#‘𝑉) mod 𝑃) = 1) |
80 | 10, 23, 79 | 3eqtrd 2648 |
1
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((#‘((𝑉 ClWWalksN 𝐸)‘𝑃)) mod 𝑃) = 1) |