| Step | Hyp | Ref
| Expression |
| 1 | | simp1 1137 |
. . . . 5
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → 𝐺 ∈ FriendGraph
) |
| 2 | 1 | anim1ci 616 |
. . . 4
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾) → (𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph )) |
| 3 | | simp3 1139 |
. . . . . 6
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → 𝑉 ≠ ∅) |
| 4 | | simp2 1138 |
. . . . . 6
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → 𝑉 ∈ Fin) |
| 5 | 3, 4 | jca 511 |
. . . . 5
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin)) |
| 6 | 5 | adantr 480 |
. . . 4
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾) → (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin)) |
| 7 | | frgrreggt1.v |
. . . . 5
⊢ 𝑉 = (Vtx‘𝐺) |
| 8 | 7 | numclwwlk7lem 30408 |
. . . 4
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin)) → 𝐾 ∈
ℕ0) |
| 9 | 2, 6, 8 | syl2anc 584 |
. . 3
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾) → 𝐾 ∈
ℕ0) |
| 10 | | 2z 12649 |
. . . . . . . . . 10
⊢ 2 ∈
ℤ |
| 11 | 10 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℕ0
∧ 2 < 𝐾) → 2
∈ ℤ) |
| 12 | | nn0z 12638 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℤ) |
| 13 | 12 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℕ0
∧ 2 < 𝐾) →
𝐾 ∈
ℤ) |
| 14 | | peano2zm 12660 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℤ → (𝐾 − 1) ∈
ℤ) |
| 15 | 13, 14 | syl 17 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℕ0
∧ 2 < 𝐾) →
(𝐾 − 1) ∈
ℤ) |
| 16 | | zltlem1 12670 |
. . . . . . . . . . 11
⊢ ((2
∈ ℤ ∧ 𝐾
∈ ℤ) → (2 < 𝐾 ↔ 2 ≤ (𝐾 − 1))) |
| 17 | 10, 12, 16 | sylancr 587 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℕ0
→ (2 < 𝐾 ↔ 2
≤ (𝐾 −
1))) |
| 18 | 17 | biimpa 476 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℕ0
∧ 2 < 𝐾) → 2
≤ (𝐾 −
1)) |
| 19 | | eluz2 12884 |
. . . . . . . . 9
⊢ ((𝐾 − 1) ∈
(ℤ≥‘2) ↔ (2 ∈ ℤ ∧ (𝐾 − 1) ∈ ℤ ∧
2 ≤ (𝐾 −
1))) |
| 20 | 11, 15, 18, 19 | syl3anbrc 1344 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℕ0
∧ 2 < 𝐾) →
(𝐾 − 1) ∈
(ℤ≥‘2)) |
| 21 | | exprmfct 16741 |
. . . . . . . 8
⊢ ((𝐾 − 1) ∈
(ℤ≥‘2) → ∃𝑝 ∈ ℙ 𝑝 ∥ (𝐾 − 1)) |
| 22 | 20, 21 | syl 17 |
. . . . . . 7
⊢ ((𝐾 ∈ ℕ0
∧ 2 < 𝐾) →
∃𝑝 ∈ ℙ
𝑝 ∥ (𝐾 − 1)) |
| 23 | 4 | anim1ci 616 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾) → (𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin)) |
| 24 | 7 | finrusgrfusgr 29583 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin) → 𝐺 ∈ FinUSGraph) |
| 25 | 23, 24 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾) → 𝐺 ∈ FinUSGraph) |
| 26 | 25 | 3ad2ant3 1136 |
. . . . . . . . . . . 12
⊢ (((𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1)) ∧ (𝐾 ∈ ℕ0 ∧ 2 <
𝐾) ∧ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾)) → 𝐺 ∈ FinUSGraph) |
| 27 | | simp1l 1198 |
. . . . . . . . . . . 12
⊢ (((𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1)) ∧ (𝐾 ∈ ℕ0 ∧ 2 <
𝐾) ∧ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾)) → 𝑝 ∈ ℙ) |
| 28 | | numclwwlk8 30411 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑝 ∈ ℙ) →
((♯‘(𝑝
ClWWalksN 𝐺)) mod 𝑝) = 0) |
| 29 | 26, 27, 28 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1)) ∧ (𝐾 ∈ ℕ0 ∧ 2 <
𝐾) ∧ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾)) → ((♯‘(𝑝 ClWWalksN 𝐺)) mod 𝑝) = 0) |
| 30 | 2 | 3ad2ant3 1136 |
. . . . . . . . . . . 12
⊢ (((𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1)) ∧ (𝐾 ∈ ℕ0 ∧ 2 <
𝐾) ∧ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾)) → (𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph )) |
| 31 | | pm3.22 459 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin)) |
| 32 | 31 | 3adant1 1131 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin)) |
| 33 | 32 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾) → (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin)) |
| 34 | 33 | 3ad2ant3 1136 |
. . . . . . . . . . . 12
⊢ (((𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1)) ∧ (𝐾 ∈ ℕ0 ∧ 2 <
𝐾) ∧ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾)) → (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin)) |
| 35 | | simp1 1137 |
. . . . . . . . . . . 12
⊢ (((𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1)) ∧ (𝐾 ∈ ℕ0 ∧ 2 <
𝐾) ∧ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾)) → (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1))) |
| 36 | 7 | numclwwlk7 30410 |
. . . . . . . . . . . 12
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1))) → ((♯‘(𝑝 ClWWalksN 𝐺)) mod 𝑝) = 1) |
| 37 | 30, 34, 35, 36 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (((𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1)) ∧ (𝐾 ∈ ℕ0 ∧ 2 <
𝐾) ∧ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾)) → ((♯‘(𝑝 ClWWalksN 𝐺)) mod 𝑝) = 1) |
| 38 | | eqeq1 2741 |
. . . . . . . . . . . 12
⊢
(((♯‘(𝑝
ClWWalksN 𝐺)) mod 𝑝) = 0 →
(((♯‘(𝑝
ClWWalksN 𝐺)) mod 𝑝) = 1 ↔ 0 =
1)) |
| 39 | | ax-1ne0 11224 |
. . . . . . . . . . . . . 14
⊢ 1 ≠
0 |
| 40 | 39 | nesymi 2998 |
. . . . . . . . . . . . 13
⊢ ¬ 0
= 1 |
| 41 | 40 | pm2.21i 119 |
. . . . . . . . . . . 12
⊢ (0 = 1
→ 𝐾 =
2) |
| 42 | 38, 41 | biimtrdi 253 |
. . . . . . . . . . 11
⊢
(((♯‘(𝑝
ClWWalksN 𝐺)) mod 𝑝) = 0 →
(((♯‘(𝑝
ClWWalksN 𝐺)) mod 𝑝) = 1 → 𝐾 = 2)) |
| 43 | 29, 37, 42 | sylc 65 |
. . . . . . . . . 10
⊢ (((𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1)) ∧ (𝐾 ∈ ℕ0 ∧ 2 <
𝐾) ∧ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾)) → 𝐾 = 2) |
| 44 | 43 | a1d 25 |
. . . . . . . . 9
⊢ (((𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1)) ∧ (𝐾 ∈ ℕ0 ∧ 2 <
𝐾) ∧ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾)) → (1 < 𝐾 → 𝐾 = 2)) |
| 45 | 44 | 3exp 1120 |
. . . . . . . 8
⊢ ((𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1)) → ((𝐾 ∈ ℕ0 ∧ 2 <
𝐾) → (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾) → (1 < 𝐾 → 𝐾 = 2)))) |
| 46 | 45 | rexlimiva 3147 |
. . . . . . 7
⊢
(∃𝑝 ∈
ℙ 𝑝 ∥ (𝐾 − 1) → ((𝐾 ∈ ℕ0
∧ 2 < 𝐾) →
(((𝐺 ∈ FriendGraph
∧ 𝑉 ∈ Fin ∧
𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾) → (1 < 𝐾 → 𝐾 = 2)))) |
| 47 | 22, 46 | mpcom 38 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 2 < 𝐾) →
(((𝐺 ∈ FriendGraph
∧ 𝑉 ∈ Fin ∧
𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾) → (1 < 𝐾 → 𝐾 = 2))) |
| 48 | 47 | expcom 413 |
. . . . 5
⊢ (2 <
𝐾 → (𝐾 ∈ ℕ0 → (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾) → (1 < 𝐾 → 𝐾 = 2)))) |
| 49 | 48 | com23 86 |
. . . 4
⊢ (2 <
𝐾 → (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾) → (𝐾 ∈ ℕ0 → (1 <
𝐾 → 𝐾 = 2)))) |
| 50 | | 1red 11262 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℕ0
→ 1 ∈ ℝ) |
| 51 | | nn0re 12535 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℝ) |
| 52 | 50, 51 | ltnled 11408 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ0
→ (1 < 𝐾 ↔
¬ 𝐾 ≤
1)) |
| 53 | | 1e2m1 12393 |
. . . . . . . . . . 11
⊢ 1 = (2
− 1) |
| 54 | 53 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℕ0
→ 1 = (2 − 1)) |
| 55 | 54 | breq2d 5155 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℕ0
→ (𝐾 ≤ 1 ↔
𝐾 ≤ (2 −
1))) |
| 56 | 55 | notbid 318 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ0
→ (¬ 𝐾 ≤ 1
↔ ¬ 𝐾 ≤ (2
− 1))) |
| 57 | | zltlem1 12670 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ ℤ ∧ 2 ∈
ℤ) → (𝐾 < 2
↔ 𝐾 ≤ (2 −
1))) |
| 58 | 12, 10, 57 | sylancl 586 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℕ0
→ (𝐾 < 2 ↔
𝐾 ≤ (2 −
1))) |
| 59 | 58 | bicomd 223 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℕ0
→ (𝐾 ≤ (2 −
1) ↔ 𝐾 <
2)) |
| 60 | 59 | notbid 318 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ0
→ (¬ 𝐾 ≤ (2
− 1) ↔ ¬ 𝐾
< 2)) |
| 61 | 52, 56, 60 | 3bitrd 305 |
. . . . . . 7
⊢ (𝐾 ∈ ℕ0
→ (1 < 𝐾 ↔
¬ 𝐾 <
2)) |
| 62 | | 2re 12340 |
. . . . . . . . 9
⊢ 2 ∈
ℝ |
| 63 | | lttri3 11344 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℝ ∧ 2 ∈
ℝ) → (𝐾 = 2
↔ (¬ 𝐾 < 2
∧ ¬ 2 < 𝐾))) |
| 64 | 63 | biimprd 248 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℝ ∧ 2 ∈
ℝ) → ((¬ 𝐾
< 2 ∧ ¬ 2 < 𝐾) → 𝐾 = 2)) |
| 65 | 51, 62, 64 | sylancl 586 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ0
→ ((¬ 𝐾 < 2
∧ ¬ 2 < 𝐾)
→ 𝐾 =
2)) |
| 66 | 65 | expd 415 |
. . . . . . 7
⊢ (𝐾 ∈ ℕ0
→ (¬ 𝐾 < 2
→ (¬ 2 < 𝐾
→ 𝐾 =
2))) |
| 67 | 61, 66 | sylbid 240 |
. . . . . 6
⊢ (𝐾 ∈ ℕ0
→ (1 < 𝐾 →
(¬ 2 < 𝐾 →
𝐾 = 2))) |
| 68 | 67 | com3r 87 |
. . . . 5
⊢ (¬ 2
< 𝐾 → (𝐾 ∈ ℕ0
→ (1 < 𝐾 →
𝐾 = 2))) |
| 69 | 68 | a1d 25 |
. . . 4
⊢ (¬ 2
< 𝐾 → (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾) → (𝐾 ∈ ℕ0 → (1 <
𝐾 → 𝐾 = 2)))) |
| 70 | 49, 69 | pm2.61i 182 |
. . 3
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾) → (𝐾 ∈ ℕ0 → (1 <
𝐾 → 𝐾 = 2))) |
| 71 | 9, 70 | mpd 15 |
. 2
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾) → (1 < 𝐾 → 𝐾 = 2)) |
| 72 | 71 | expimpd 453 |
1
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((𝐺 RegUSGraph 𝐾 ∧ 1 < 𝐾) → 𝐾 = 2)) |