Step | Hyp | Ref
| Expression |
1 | | simpl1 1057 |
. . . . 5
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 2 ∈ ℙ ∧ 2 ∥
(𝐾 − 1))) →
〈𝑉, 𝐸〉 RegUSGrph 𝐾) |
2 | | simpr3 1062 |
. . . . 5
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 2 ∈ ℙ ∧ 2 ∥
(𝐾 − 1))) → 2
∥ (𝐾 −
1)) |
3 | | simpr1 1060 |
. . . . 5
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 2 ∈ ℙ ∧ 2 ∥
(𝐾 − 1))) →
𝑋 ∈ 𝑉) |
4 | | numclwwlk.c |
. . . . . 6
⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛)) |
5 | | numclwwlk.f |
. . . . . 6
⊢ 𝐹 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝐶‘𝑛) ∣ (𝑤‘0) = 𝑣}) |
6 | 4, 5 | numclwwlk5lem 26638 |
. . . . 5
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 2 ∥ (𝐾 − 1) ∧ 𝑋 ∈ 𝑉) → ((#‘(𝑋𝐹2)) mod 2) = 1) |
7 | 1, 2, 3, 6 | syl3anc 1318 |
. . . 4
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 2 ∈ ℙ ∧ 2 ∥
(𝐾 − 1))) →
((#‘(𝑋𝐹2)) mod 2) = 1) |
8 | 7 | a1i 11 |
. . 3
⊢ (𝑃 = 2 → (((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 2 ∈ ℙ ∧ 2 ∥
(𝐾 − 1))) →
((#‘(𝑋𝐹2)) mod 2) =
1)) |
9 | | eleq1 2676 |
. . . . 5
⊢ (𝑃 = 2 → (𝑃 ∈ ℙ ↔ 2 ∈
ℙ)) |
10 | | breq1 4586 |
. . . . 5
⊢ (𝑃 = 2 → (𝑃 ∥ (𝐾 − 1) ↔ 2 ∥ (𝐾 − 1))) |
11 | 9, 10 | 3anbi23d 1394 |
. . . 4
⊢ (𝑃 = 2 → ((𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)) ↔ (𝑋 ∈ 𝑉 ∧ 2 ∈ ℙ ∧ 2 ∥
(𝐾 −
1)))) |
12 | 11 | anbi2d 736 |
. . 3
⊢ (𝑃 = 2 → (((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) ↔ ((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 2 ∈ ℙ ∧ 2 ∥
(𝐾 −
1))))) |
13 | | oveq2 6557 |
. . . . . 6
⊢ (𝑃 = 2 → (𝑋𝐹𝑃) = (𝑋𝐹2)) |
14 | 13 | fveq2d 6107 |
. . . . 5
⊢ (𝑃 = 2 → (#‘(𝑋𝐹𝑃)) = (#‘(𝑋𝐹2))) |
15 | | id 22 |
. . . . 5
⊢ (𝑃 = 2 → 𝑃 = 2) |
16 | 14, 15 | oveq12d 6567 |
. . . 4
⊢ (𝑃 = 2 → ((#‘(𝑋𝐹𝑃)) mod 𝑃) = ((#‘(𝑋𝐹2)) mod 2)) |
17 | 16 | eqeq1d 2612 |
. . 3
⊢ (𝑃 = 2 → (((#‘(𝑋𝐹𝑃)) mod 𝑃) = 1 ↔ ((#‘(𝑋𝐹2)) mod 2) = 1)) |
18 | 8, 12, 17 | 3imtr4d 282 |
. 2
⊢ (𝑃 = 2 → (((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((#‘(𝑋𝐹𝑃)) mod 𝑃) = 1)) |
19 | | 3simpa 1051 |
. . . . . . . 8
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸)) |
20 | 19 | adantr 480 |
. . . . . . 7
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸)) |
21 | 20 | adantl 481 |
. . . . . 6
⊢ ((𝑃 ≠ 2 ∧ ((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)))) → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸)) |
22 | | simprl3 1101 |
. . . . . 6
⊢ ((𝑃 ≠ 2 ∧ ((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)))) → 𝑉 ∈ Fin) |
23 | | simprr1 1102 |
. . . . . 6
⊢ ((𝑃 ≠ 2 ∧ ((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)))) → 𝑋 ∈ 𝑉) |
24 | | eldifsn 4260 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ (ℙ ∖ {2})
↔ (𝑃 ∈ ℙ
∧ 𝑃 ≠
2)) |
25 | | oddprmge3 15250 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
(ℤ≥‘3)) |
26 | 24, 25 | sylbir 224 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝑃 ≠ 2) → 𝑃 ∈
(ℤ≥‘3)) |
27 | 26 | ex 449 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℙ → (𝑃 ≠ 2 → 𝑃 ∈
(ℤ≥‘3))) |
28 | 27 | 3ad2ant2 1076 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)) → (𝑃 ≠ 2 → 𝑃 ∈
(ℤ≥‘3))) |
29 | 28 | adantl 481 |
. . . . . . 7
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (𝑃 ≠ 2 → 𝑃 ∈
(ℤ≥‘3))) |
30 | 29 | impcom 445 |
. . . . . 6
⊢ ((𝑃 ≠ 2 ∧ ((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)))) → 𝑃 ∈
(ℤ≥‘3)) |
31 | | fveq1 6102 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑤 → (𝑢‘0) = (𝑤‘0)) |
32 | 31 | eqeq1d 2612 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑤 → ((𝑢‘0) = 𝑣 ↔ (𝑤‘0) = 𝑣)) |
33 | | fveq1 6102 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑤 → (𝑢‘(𝑛 − 2)) = (𝑤‘(𝑛 − 2))) |
34 | 33, 31 | eqeq12d 2625 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑤 → ((𝑢‘(𝑛 − 2)) = (𝑢‘0) ↔ (𝑤‘(𝑛 − 2)) = (𝑤‘0))) |
35 | 32, 34 | anbi12d 743 |
. . . . . . . . . 10
⊢ (𝑢 = 𝑤 → (((𝑢‘0) = 𝑣 ∧ (𝑢‘(𝑛 − 2)) = (𝑢‘0)) ↔ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) = (𝑤‘0)))) |
36 | 35 | cbvrabv 3172 |
. . . . . . . . 9
⊢ {𝑢 ∈ (𝐶‘𝑛) ∣ ((𝑢‘0) = 𝑣 ∧ (𝑢‘(𝑛 − 2)) = (𝑢‘0))} = {𝑤 ∈ (𝐶‘𝑛) ∣ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) = (𝑤‘0))} |
37 | 36 | a1i 11 |
. . . . . . . 8
⊢ ((𝑣 ∈ 𝑉 ∧ 𝑛 ∈ (ℤ≥‘2))
→ {𝑢 ∈ (𝐶‘𝑛) ∣ ((𝑢‘0) = 𝑣 ∧ (𝑢‘(𝑛 − 2)) = (𝑢‘0))} = {𝑤 ∈ (𝐶‘𝑛) ∣ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) = (𝑤‘0))}) |
38 | 37 | mpt2eq3ia 6618 |
. . . . . . 7
⊢ (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑢 ∈ (𝐶‘𝑛) ∣ ((𝑢‘0) = 𝑣 ∧ (𝑢‘(𝑛 − 2)) = (𝑢‘0))}) = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝐶‘𝑛) ∣ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) = (𝑤‘0))}) |
39 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑤 → ( lastS ‘𝑢) = ( lastS ‘𝑤)) |
40 | 39 | neeq1d 2841 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑤 → (( lastS ‘𝑢) ≠ 𝑣 ↔ ( lastS ‘𝑤) ≠ 𝑣)) |
41 | 32, 40 | anbi12d 743 |
. . . . . . . . . 10
⊢ (𝑢 = 𝑤 → (((𝑢‘0) = 𝑣 ∧ ( lastS ‘𝑢) ≠ 𝑣) ↔ ((𝑤‘0) = 𝑣 ∧ ( lastS ‘𝑤) ≠ 𝑣))) |
42 | 41 | cbvrabv 3172 |
. . . . . . . . 9
⊢ {𝑢 ∈ ((𝑉 WWalksN 𝐸)‘𝑛) ∣ ((𝑢‘0) = 𝑣 ∧ ( lastS ‘𝑢) ≠ 𝑣)} = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑛) ∣ ((𝑤‘0) = 𝑣 ∧ ( lastS ‘𝑤) ≠ 𝑣)} |
43 | 42 | a1i 11 |
. . . . . . . 8
⊢ ((𝑣 ∈ 𝑉 ∧ 𝑛 ∈ ℕ0) → {𝑢 ∈ ((𝑉 WWalksN 𝐸)‘𝑛) ∣ ((𝑢‘0) = 𝑣 ∧ ( lastS ‘𝑢) ≠ 𝑣)} = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑛) ∣ ((𝑤‘0) = 𝑣 ∧ ( lastS ‘𝑤) ≠ 𝑣)}) |
44 | 43 | mpt2eq3ia 6618 |
. . . . . . 7
⊢ (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ {𝑢 ∈ ((𝑉 WWalksN 𝐸)‘𝑛) ∣ ((𝑢‘0) = 𝑣 ∧ ( lastS ‘𝑢) ≠ 𝑣)}) = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑛) ∣ ((𝑤‘0) = 𝑣 ∧ ( lastS ‘𝑤) ≠ 𝑣)}) |
45 | | eqeq2 2621 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑣 → ((𝑢‘0) = 𝑧 ↔ (𝑢‘0) = 𝑣)) |
46 | 45 | anbi1d 737 |
. . . . . . . . 9
⊢ (𝑧 = 𝑣 → (((𝑢‘0) = 𝑧 ∧ (𝑢‘(𝑚 − 2)) ≠ (𝑢‘0)) ↔ ((𝑢‘0) = 𝑣 ∧ (𝑢‘(𝑚 − 2)) ≠ (𝑢‘0)))) |
47 | 46 | rabbidv 3164 |
. . . . . . . 8
⊢ (𝑧 = 𝑣 → {𝑢 ∈ (𝐶‘𝑚) ∣ ((𝑢‘0) = 𝑧 ∧ (𝑢‘(𝑚 − 2)) ≠ (𝑢‘0))} = {𝑢 ∈ (𝐶‘𝑚) ∣ ((𝑢‘0) = 𝑣 ∧ (𝑢‘(𝑚 − 2)) ≠ (𝑢‘0))}) |
48 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (𝐶‘𝑚) = (𝐶‘𝑛)) |
49 | | oveq1 6556 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → (𝑚 − 2) = (𝑛 − 2)) |
50 | 49 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → (𝑢‘(𝑚 − 2)) = (𝑢‘(𝑛 − 2))) |
51 | 50 | neeq1d 2841 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → ((𝑢‘(𝑚 − 2)) ≠ (𝑢‘0) ↔ (𝑢‘(𝑛 − 2)) ≠ (𝑢‘0))) |
52 | 51 | anbi2d 736 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (((𝑢‘0) = 𝑣 ∧ (𝑢‘(𝑚 − 2)) ≠ (𝑢‘0)) ↔ ((𝑢‘0) = 𝑣 ∧ (𝑢‘(𝑛 − 2)) ≠ (𝑢‘0)))) |
53 | 48, 52 | rabeqbidv 3168 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → {𝑢 ∈ (𝐶‘𝑚) ∣ ((𝑢‘0) = 𝑣 ∧ (𝑢‘(𝑚 − 2)) ≠ (𝑢‘0))} = {𝑢 ∈ (𝐶‘𝑛) ∣ ((𝑢‘0) = 𝑣 ∧ (𝑢‘(𝑛 − 2)) ≠ (𝑢‘0))}) |
54 | 33, 31 | neeq12d 2843 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑤 → ((𝑢‘(𝑛 − 2)) ≠ (𝑢‘0) ↔ (𝑤‘(𝑛 − 2)) ≠ (𝑤‘0))) |
55 | 32, 54 | anbi12d 743 |
. . . . . . . . . 10
⊢ (𝑢 = 𝑤 → (((𝑢‘0) = 𝑣 ∧ (𝑢‘(𝑛 − 2)) ≠ (𝑢‘0)) ↔ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) ≠ (𝑤‘0)))) |
56 | 55 | cbvrabv 3172 |
. . . . . . . . 9
⊢ {𝑢 ∈ (𝐶‘𝑛) ∣ ((𝑢‘0) = 𝑣 ∧ (𝑢‘(𝑛 − 2)) ≠ (𝑢‘0))} = {𝑤 ∈ (𝐶‘𝑛) ∣ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) ≠ (𝑤‘0))} |
57 | 53, 56 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → {𝑢 ∈ (𝐶‘𝑚) ∣ ((𝑢‘0) = 𝑣 ∧ (𝑢‘(𝑚 − 2)) ≠ (𝑢‘0))} = {𝑤 ∈ (𝐶‘𝑛) ∣ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) ≠ (𝑤‘0))}) |
58 | 47, 57 | cbvmpt2v 6633 |
. . . . . . 7
⊢ (𝑧 ∈ 𝑉, 𝑚 ∈ ℕ0 ↦ {𝑢 ∈ (𝐶‘𝑚) ∣ ((𝑢‘0) = 𝑧 ∧ (𝑢‘(𝑚 − 2)) ≠ (𝑢‘0))}) = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝐶‘𝑛) ∣ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) ≠ (𝑤‘0))}) |
59 | 4, 5, 38, 44, 58 | numclwwlk3 26636 |
. . . . . 6
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑃 ∈ (ℤ≥‘3)))
→ (#‘(𝑋𝐹𝑃)) = (((𝐾 − 1) · (#‘(𝑋𝐹(𝑃 − 2)))) + (𝐾↑(𝑃 − 2)))) |
60 | 21, 22, 23, 30, 59 | syl13anc 1320 |
. . . . 5
⊢ ((𝑃 ≠ 2 ∧ ((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)))) → (#‘(𝑋𝐹𝑃)) = (((𝐾 − 1) · (#‘(𝑋𝐹(𝑃 − 2)))) + (𝐾↑(𝑃 − 2)))) |
61 | 60 | oveq1d 6564 |
. . . 4
⊢ ((𝑃 ≠ 2 ∧ ((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)))) → ((#‘(𝑋𝐹𝑃)) mod 𝑃) = ((((𝐾 − 1) · (#‘(𝑋𝐹(𝑃 − 2)))) + (𝐾↑(𝑃 − 2))) mod 𝑃)) |
62 | | rusgraprop 26456 |
. . . . . . . . . . . . 13
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (𝑉 USGrph 𝐸 ∧ 𝐾 ∈ ℕ0 ∧
∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾)) |
63 | | nn0z 11277 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℤ) |
64 | 63 | 3ad2ant2 1076 |
. . . . . . . . . . . . 13
⊢ ((𝑉 USGrph 𝐸 ∧ 𝐾 ∈ ℕ0 ∧
∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → 𝐾 ∈ ℤ) |
65 | 62, 64 | syl 17 |
. . . . . . . . . . . 12
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → 𝐾 ∈ ℤ) |
66 | 65 | zred 11358 |
. . . . . . . . . . 11
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → 𝐾 ∈ ℝ) |
67 | | peano2rem 10227 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ℝ → (𝐾 − 1) ∈
ℝ) |
68 | 66, 67 | syl 17 |
. . . . . . . . . 10
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (𝐾 − 1) ∈ ℝ) |
69 | 68 | 3ad2ant1 1075 |
. . . . . . . . 9
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) → (𝐾 − 1) ∈ ℝ) |
70 | 69 | adantr 480 |
. . . . . . . 8
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (𝐾 − 1) ∈ ℝ) |
71 | | rusisusgra 26458 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → 𝑉 USGrph 𝐸) |
72 | | usgrav 25867 |
. . . . . . . . . . . . . . . 16
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
73 | 72 | simprd 478 |
. . . . . . . . . . . . . . 15
⊢ (𝑉 USGrph 𝐸 → 𝐸 ∈ V) |
74 | 71, 73 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → 𝐸 ∈ V) |
75 | 74 | anim1i 590 |
. . . . . . . . . . . . 13
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 ∈ Fin) → (𝐸 ∈ V ∧ 𝑉 ∈ Fin)) |
76 | 75 | ancomd 466 |
. . . . . . . . . . . 12
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 ∈ Fin) → (𝑉 ∈ Fin ∧ 𝐸 ∈ V)) |
77 | 76 | 3adant2 1073 |
. . . . . . . . . . 11
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) → (𝑉 ∈ Fin ∧ 𝐸 ∈ V)) |
78 | | prmm2nn0 15248 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ → (𝑃 − 2) ∈
ℕ0) |
79 | 78 | anim2i 591 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ) → (𝑋 ∈ 𝑉 ∧ (𝑃 − 2) ∈
ℕ0)) |
80 | 79 | 3adant3 1074 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)) → (𝑋 ∈ 𝑉 ∧ (𝑃 − 2) ∈
ℕ0)) |
81 | 4, 5 | numclwwlkffin 26609 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ Fin ∧ 𝐸 ∈ V) ∧ (𝑋 ∈ 𝑉 ∧ (𝑃 − 2) ∈ ℕ0))
→ (𝑋𝐹(𝑃 − 2)) ∈ Fin) |
82 | 77, 80, 81 | syl2an 493 |
. . . . . . . . . 10
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (𝑋𝐹(𝑃 − 2)) ∈ Fin) |
83 | | hashcl 13009 |
. . . . . . . . . 10
⊢ ((𝑋𝐹(𝑃 − 2)) ∈ Fin →
(#‘(𝑋𝐹(𝑃 − 2))) ∈
ℕ0) |
84 | 82, 83 | syl 17 |
. . . . . . . . 9
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (#‘(𝑋𝐹(𝑃 − 2))) ∈
ℕ0) |
85 | 84 | nn0red 11229 |
. . . . . . . 8
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (#‘(𝑋𝐹(𝑃 − 2))) ∈
ℝ) |
86 | 70, 85 | remulcld 9949 |
. . . . . . 7
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((𝐾 − 1) · (#‘(𝑋𝐹(𝑃 − 2)))) ∈
ℝ) |
87 | 66 | 3ad2ant1 1075 |
. . . . . . . 8
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) → 𝐾 ∈ ℝ) |
88 | 78 | 3ad2ant2 1076 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)) → (𝑃 − 2) ∈
ℕ0) |
89 | | reexpcl 12739 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℝ ∧ (𝑃 − 2) ∈
ℕ0) → (𝐾↑(𝑃 − 2)) ∈
ℝ) |
90 | 87, 88, 89 | syl2an 493 |
. . . . . . 7
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (𝐾↑(𝑃 − 2)) ∈
ℝ) |
91 | | prmnn 15226 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
92 | 91 | nnrpd 11746 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℝ+) |
93 | 92 | 3ad2ant2 1076 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)) → 𝑃 ∈
ℝ+) |
94 | 93 | adantl 481 |
. . . . . . 7
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → 𝑃 ∈
ℝ+) |
95 | 86, 90, 94 | 3jca 1235 |
. . . . . 6
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (((𝐾 − 1) · (#‘(𝑋𝐹(𝑃 − 2)))) ∈ ℝ ∧ (𝐾↑(𝑃 − 2)) ∈ ℝ ∧ 𝑃 ∈
ℝ+)) |
96 | 95 | adantl 481 |
. . . . 5
⊢ ((𝑃 ≠ 2 ∧ ((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)))) → (((𝐾 − 1) · (#‘(𝑋𝐹(𝑃 − 2)))) ∈ ℝ ∧ (𝐾↑(𝑃 − 2)) ∈ ℝ ∧ 𝑃 ∈
ℝ+)) |
97 | | modaddabs 12570 |
. . . . . 6
⊢ ((((𝐾 − 1) ·
(#‘(𝑋𝐹(𝑃 − 2)))) ∈ ℝ ∧ (𝐾↑(𝑃 − 2)) ∈ ℝ ∧ 𝑃 ∈ ℝ+)
→ (((((𝐾 − 1)
· (#‘(𝑋𝐹(𝑃 − 2)))) mod 𝑃) + ((𝐾↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = ((((𝐾 − 1) · (#‘(𝑋𝐹(𝑃 − 2)))) + (𝐾↑(𝑃 − 2))) mod 𝑃)) |
98 | 97 | eqcomd 2616 |
. . . . 5
⊢ ((((𝐾 − 1) ·
(#‘(𝑋𝐹(𝑃 − 2)))) ∈ ℝ ∧ (𝐾↑(𝑃 − 2)) ∈ ℝ ∧ 𝑃 ∈ ℝ+)
→ ((((𝐾 − 1)
· (#‘(𝑋𝐹(𝑃 − 2)))) + (𝐾↑(𝑃 − 2))) mod 𝑃) = (((((𝐾 − 1) · (#‘(𝑋𝐹(𝑃 − 2)))) mod 𝑃) + ((𝐾↑(𝑃 − 2)) mod 𝑃)) mod 𝑃)) |
99 | 96, 98 | syl 17 |
. . . 4
⊢ ((𝑃 ≠ 2 ∧ ((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)))) → ((((𝐾 − 1) · (#‘(𝑋𝐹(𝑃 − 2)))) + (𝐾↑(𝑃 − 2))) mod 𝑃) = (((((𝐾 − 1) · (#‘(𝑋𝐹(𝑃 − 2)))) mod 𝑃) + ((𝐾↑(𝑃 − 2)) mod 𝑃)) mod 𝑃)) |
100 | 91 | 3ad2ant2 1076 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)) → 𝑃 ∈ ℕ) |
101 | 100 | adantl 481 |
. . . . . . . . . 10
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → 𝑃 ∈ ℕ) |
102 | | peano2zm 11297 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ ℤ → (𝐾 − 1) ∈
ℤ) |
103 | 65, 102 | syl 17 |
. . . . . . . . . . . 12
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (𝐾 − 1) ∈ ℤ) |
104 | 103 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) → (𝐾 − 1) ∈ ℤ) |
105 | 104 | adantr 480 |
. . . . . . . . . 10
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (𝐾 − 1) ∈ ℤ) |
106 | 84 | nn0zd 11356 |
. . . . . . . . . 10
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (#‘(𝑋𝐹(𝑃 − 2))) ∈
ℤ) |
107 | 101, 105,
106 | 3jca 1235 |
. . . . . . . . 9
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (𝑃 ∈ ℕ ∧ (𝐾 − 1) ∈ ℤ ∧
(#‘(𝑋𝐹(𝑃 − 2))) ∈
ℤ)) |
108 | | simpr3 1062 |
. . . . . . . . 9
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → 𝑃 ∥ (𝐾 − 1)) |
109 | | mulmoddvds 14889 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℕ ∧ (𝐾 − 1) ∈ ℤ ∧
(#‘(𝑋𝐹(𝑃 − 2))) ∈ ℤ) → (𝑃 ∥ (𝐾 − 1) → (((𝐾 − 1) · (#‘(𝑋𝐹(𝑃 − 2)))) mod 𝑃) = 0)) |
110 | 107, 108,
109 | sylc 63 |
. . . . . . . 8
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (((𝐾 − 1) · (#‘(𝑋𝐹(𝑃 − 2)))) mod 𝑃) = 0) |
111 | 65 | 3ad2ant1 1075 |
. . . . . . . . . 10
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) → 𝐾 ∈ ℤ) |
112 | | simp2 1055 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)) → 𝑃 ∈ ℙ) |
113 | 111, 112 | anim12ci 589 |
. . . . . . . . 9
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (𝑃 ∈ ℙ ∧ 𝐾 ∈ ℤ)) |
114 | | powm2modprm 15346 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℤ) → (𝑃 ∥ (𝐾 − 1) → ((𝐾↑(𝑃 − 2)) mod 𝑃) = 1)) |
115 | 113, 108,
114 | sylc 63 |
. . . . . . . 8
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((𝐾↑(𝑃 − 2)) mod 𝑃) = 1) |
116 | 110, 115 | oveq12d 6567 |
. . . . . . 7
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((((𝐾 − 1) · (#‘(𝑋𝐹(𝑃 − 2)))) mod 𝑃) + ((𝐾↑(𝑃 − 2)) mod 𝑃)) = (0 + 1)) |
117 | 116 | oveq1d 6564 |
. . . . . 6
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (((((𝐾 − 1) · (#‘(𝑋𝐹(𝑃 − 2)))) mod 𝑃) + ((𝐾↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = ((0 + 1) mod 𝑃)) |
118 | | 0p1e1 11009 |
. . . . . . . . . 10
⊢ (0 + 1) =
1 |
119 | 118 | oveq1i 6559 |
. . . . . . . . 9
⊢ ((0 + 1)
mod 𝑃) = (1 mod 𝑃) |
120 | 91 | nnred 10912 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℝ) |
121 | | prmgt1 15247 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 1 <
𝑃) |
122 | | 1mod 12564 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℝ ∧ 1 <
𝑃) → (1 mod 𝑃) = 1) |
123 | 120, 121,
122 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℙ → (1 mod
𝑃) = 1) |
124 | 119, 123 | syl5eq 2656 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → ((0 + 1)
mod 𝑃) =
1) |
125 | 124 | 3ad2ant2 1076 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)) → ((0 + 1) mod 𝑃) = 1) |
126 | 125 | adantl 481 |
. . . . . 6
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((0 + 1) mod 𝑃) = 1) |
127 | 117, 126 | eqtrd 2644 |
. . . . 5
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (((((𝐾 − 1) · (#‘(𝑋𝐹(𝑃 − 2)))) mod 𝑃) + ((𝐾↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = 1) |
128 | 127 | adantl 481 |
. . . 4
⊢ ((𝑃 ≠ 2 ∧ ((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)))) → (((((𝐾 − 1) · (#‘(𝑋𝐹(𝑃 − 2)))) mod 𝑃) + ((𝐾↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = 1) |
129 | 61, 99, 128 | 3eqtrd 2648 |
. . 3
⊢ ((𝑃 ≠ 2 ∧ ((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)))) → ((#‘(𝑋𝐹𝑃)) mod 𝑃) = 1) |
130 | 129 | ex 449 |
. 2
⊢ (𝑃 ≠ 2 → (((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((#‘(𝑋𝐹𝑃)) mod 𝑃) = 1)) |
131 | 18, 130 | pm2.61ine 2865 |
1
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((#‘(𝑋𝐹𝑃)) mod 𝑃) = 1) |