Step | Hyp | Ref
| Expression |
1 | | rusgraprop 26456 |
. . . . 5
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (𝑉 USGrph 𝐸 ∧ 𝐾 ∈ ℕ0 ∧
∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾)) |
2 | | 2z 11286 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℤ |
3 | 2 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ ℕ0
∧ 2 < 𝐾) → 2
∈ ℤ) |
4 | | nn0z 11277 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℤ) |
5 | | peano2zm 11297 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ ℤ → (𝐾 − 1) ∈
ℤ) |
6 | 4, 5 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ ℕ0
→ (𝐾 − 1) ∈
ℤ) |
7 | 6 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ ℕ0
∧ 2 < 𝐾) →
(𝐾 − 1) ∈
ℤ) |
8 | | zltlem1 11307 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℤ ∧ 𝐾
∈ ℤ) → (2 < 𝐾 ↔ 2 ≤ (𝐾 − 1))) |
9 | 2, 4, 8 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ ℕ0
→ (2 < 𝐾 ↔ 2
≤ (𝐾 −
1))) |
10 | 9 | biimpa 500 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ ℕ0
∧ 2 < 𝐾) → 2
≤ (𝐾 −
1)) |
11 | | eluz2 11569 |
. . . . . . . . . . 11
⊢ ((𝐾 − 1) ∈
(ℤ≥‘2) ↔ (2 ∈ ℤ ∧ (𝐾 − 1) ∈ ℤ ∧
2 ≤ (𝐾 −
1))) |
12 | 3, 7, 10, 11 | syl3anbrc 1239 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℕ0
∧ 2 < 𝐾) →
(𝐾 − 1) ∈
(ℤ≥‘2)) |
13 | | exprmfct 15254 |
. . . . . . . . . 10
⊢ ((𝐾 − 1) ∈
(ℤ≥‘2) → ∃𝑝 ∈ ℙ 𝑝 ∥ (𝐾 − 1)) |
14 | 12, 13 | syl 17 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℕ0
∧ 2 < 𝐾) →
∃𝑝 ∈ ℙ
𝑝 ∥ (𝐾 − 1)) |
15 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ (((𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1)) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → 〈𝑉, 𝐸〉 RegUSGrph 𝐾) |
16 | | simp1 1054 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → 𝑉 FriendGrph 𝐸) |
17 | 15, 16 | anim12i 588 |
. . . . . . . . . . . . . 14
⊢ ((((𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1)) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸)) |
18 | | pm3.22 464 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin)) |
19 | 18 | 3adant1 1072 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin)) |
20 | 19 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1)) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin)) |
21 | | simpll 786 |
. . . . . . . . . . . . . 14
⊢ ((((𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1)) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1))) |
22 | | numclwwlk7 26641 |
. . . . . . . . . . . . . 14
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1))) → ((#‘((𝑉 ClWWalksN 𝐸)‘𝑝)) mod 𝑝) = 1) |
23 | 17, 20, 21, 22 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((((𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1)) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → ((#‘((𝑉 ClWWalksN 𝐸)‘𝑝)) mod 𝑝) = 1) |
24 | | frisusgra 26519 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑉 FriendGrph 𝐸 → 𝑉 USGrph 𝐸) |
25 | 24 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → 𝑉 USGrph 𝐸) |
26 | 25 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1)) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → 𝑉 USGrph 𝐸) |
27 | | simpr2 1061 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1)) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → 𝑉 ∈ Fin) |
28 | | simplll 794 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1)) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → 𝑝 ∈ ℙ) |
29 | | numclwwlk8 26642 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑝 ∈ ℙ) → ((#‘((𝑉 ClWWalksN 𝐸)‘𝑝)) mod 𝑝) = 0) |
30 | 26, 27, 28, 29 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1)) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → ((#‘((𝑉 ClWWalksN 𝐸)‘𝑝)) mod 𝑝) = 0) |
31 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . 17
⊢
(((#‘((𝑉
ClWWalksN 𝐸)‘𝑝)) mod 𝑝) = 0 → (((#‘((𝑉 ClWWalksN 𝐸)‘𝑝)) mod 𝑝) = 1 ↔ 0 = 1)) |
32 | | ax-1ne0 9884 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ≠
0 |
33 | 32 | nesymi 2839 |
. . . . . . . . . . . . . . . . . 18
⊢ ¬ 0
= 1 |
34 | 33 | pm2.21i 115 |
. . . . . . . . . . . . . . . . 17
⊢ (0 = 1
→ 𝐾 =
2) |
35 | 31, 34 | syl6bi 242 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘((𝑉
ClWWalksN 𝐸)‘𝑝)) mod 𝑝) = 0 → (((#‘((𝑉 ClWWalksN 𝐸)‘𝑝)) mod 𝑝) = 1 → 𝐾 = 2)) |
36 | 30, 35 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1)) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → (((#‘((𝑉 ClWWalksN 𝐸)‘𝑝)) mod 𝑝) = 1 → 𝐾 = 2)) |
37 | 36 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℕ0
∧ 2 < 𝐾) →
((((𝑝 ∈ ℙ ∧
𝑝 ∥ (𝐾 − 1)) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → (((#‘((𝑉 ClWWalksN 𝐸)‘𝑝)) mod 𝑝) = 1 → 𝐾 = 2))) |
38 | 37 | com13 86 |
. . . . . . . . . . . . 13
⊢
(((#‘((𝑉
ClWWalksN 𝐸)‘𝑝)) mod 𝑝) = 1 → ((((𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1)) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → ((𝐾 ∈ ℕ0 ∧ 2 <
𝐾) → 𝐾 = 2))) |
39 | 23, 38 | mpcom 37 |
. . . . . . . . . . . 12
⊢ ((((𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1)) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → ((𝐾 ∈ ℕ0 ∧ 2 <
𝐾) → 𝐾 = 2)) |
40 | 39 | exp31 628 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1)) → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((𝐾 ∈ ℕ0 ∧ 2 <
𝐾) → 𝐾 = 2)))) |
41 | 40 | com24 93 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1)) → ((𝐾 ∈ ℕ0 ∧ 2 <
𝐾) → ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → 𝐾 = 2)))) |
42 | 41 | rexlimiva 3010 |
. . . . . . . . 9
⊢
(∃𝑝 ∈
ℙ 𝑝 ∥ (𝐾 − 1) → ((𝐾 ∈ ℕ0
∧ 2 < 𝐾) →
((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → 𝐾 = 2)))) |
43 | 14, 42 | mpcom 37 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℕ0
∧ 2 < 𝐾) →
((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → 𝐾 = 2))) |
44 | 43 | ex 449 |
. . . . . . 7
⊢ (𝐾 ∈ ℕ0
→ (2 < 𝐾 →
((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → 𝐾 = 2)))) |
45 | 44 | com24 93 |
. . . . . 6
⊢ (𝐾 ∈ ℕ0
→ (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (2 < 𝐾 → 𝐾 = 2)))) |
46 | 45 | 3ad2ant2 1076 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ 𝐾 ∈ ℕ0 ∧
∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (2 < 𝐾 → 𝐾 = 2)))) |
47 | 1, 46 | mpcom 37 |
. . . 4
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (2 < 𝐾 → 𝐾 = 2))) |
48 | 47 | adantr 480 |
. . 3
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 1 < 𝐾) → ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (2 < 𝐾 → 𝐾 = 2))) |
49 | 48 | com13 86 |
. 2
⊢ (2 <
𝐾 → ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 1 < 𝐾) → 𝐾 = 2))) |
50 | | 1red 9934 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℕ0
→ 1 ∈ ℝ) |
51 | | nn0re 11178 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℝ) |
52 | 50, 51 | ltnled 10063 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℕ0
→ (1 < 𝐾 ↔
¬ 𝐾 ≤
1)) |
53 | | 1e2m1 11013 |
. . . . . . . . . . . 12
⊢ 1 = (2
− 1) |
54 | 53 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ℕ0
→ 1 = (2 − 1)) |
55 | 54 | breq2d 4595 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℕ0
→ (𝐾 ≤ 1 ↔
𝐾 ≤ (2 −
1))) |
56 | 55 | notbid 307 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℕ0
→ (¬ 𝐾 ≤ 1
↔ ¬ 𝐾 ≤ (2
− 1))) |
57 | | zltlem1 11307 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ ℤ ∧ 2 ∈
ℤ) → (𝐾 < 2
↔ 𝐾 ≤ (2 −
1))) |
58 | 4, 2, 57 | sylancl 693 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ℕ0
→ (𝐾 < 2 ↔
𝐾 ≤ (2 −
1))) |
59 | 58 | bicomd 212 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℕ0
→ (𝐾 ≤ (2 −
1) ↔ 𝐾 <
2)) |
60 | 59 | notbid 307 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℕ0
→ (¬ 𝐾 ≤ (2
− 1) ↔ ¬ 𝐾
< 2)) |
61 | 52, 56, 60 | 3bitrd 293 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ0
→ (1 < 𝐾 ↔
¬ 𝐾 <
2)) |
62 | | 2re 10967 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
63 | | lttri3 10000 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ ℝ ∧ 2 ∈
ℝ) → (𝐾 = 2
↔ (¬ 𝐾 < 2
∧ ¬ 2 < 𝐾))) |
64 | 63 | biimprd 237 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℝ ∧ 2 ∈
ℝ) → ((¬ 𝐾
< 2 ∧ ¬ 2 < 𝐾) → 𝐾 = 2)) |
65 | 51, 62, 64 | sylancl 693 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℕ0
→ ((¬ 𝐾 < 2
∧ ¬ 2 < 𝐾)
→ 𝐾 =
2)) |
66 | 65 | expd 451 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ0
→ (¬ 𝐾 < 2
→ (¬ 2 < 𝐾
→ 𝐾 =
2))) |
67 | 61, 66 | sylbid 229 |
. . . . . . 7
⊢ (𝐾 ∈ ℕ0
→ (1 < 𝐾 →
(¬ 2 < 𝐾 →
𝐾 = 2))) |
68 | 67 | 3ad2ant2 1076 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ 𝐾 ∈ ℕ0 ∧
∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → (1 < 𝐾 → (¬ 2 < 𝐾 → 𝐾 = 2))) |
69 | 1, 68 | syl 17 |
. . . . 5
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (1 < 𝐾 → (¬ 2 < 𝐾 → 𝐾 = 2))) |
70 | 69 | imp 444 |
. . . 4
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 1 < 𝐾) → (¬ 2 < 𝐾 → 𝐾 = 2)) |
71 | 70 | com12 32 |
. . 3
⊢ (¬ 2
< 𝐾 → ((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 1 < 𝐾) → 𝐾 = 2)) |
72 | 71 | a1d 25 |
. 2
⊢ (¬ 2
< 𝐾 → ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 1 < 𝐾) → 𝐾 = 2))) |
73 | 49, 72 | pm2.61i 175 |
1
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 1 < 𝐾) → 𝐾 = 2)) |