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