Step | Hyp | Ref
| Expression |
1 | | simp1 1135 |
. . . . 5
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → 𝐺 ∈ FriendGraph
) |
2 | 1 | anim1ci 616 |
. . . 4
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾) → (𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph )) |
3 | | simp3 1137 |
. . . . . 6
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → 𝑉 ≠ ∅) |
4 | | simp2 1136 |
. . . . . 6
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → 𝑉 ∈ Fin) |
5 | 3, 4 | jca 512 |
. . . . 5
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin)) |
6 | 5 | adantr 481 |
. . . 4
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾) → (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin)) |
7 | | frgrreggt1.v |
. . . . 5
⊢ 𝑉 = (Vtx‘𝐺) |
8 | 7 | numclwwlk7lem 28753 |
. . . 4
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin)) → 𝐾 ∈
ℕ0) |
9 | 2, 6, 8 | syl2anc 584 |
. . 3
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾) → 𝐾 ∈
ℕ0) |
10 | | 2z 12352 |
. . . . . . . . . 10
⊢ 2 ∈
ℤ |
11 | 10 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℕ0
∧ 2 < 𝐾) → 2
∈ ℤ) |
12 | | nn0z 12343 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℤ) |
13 | 12 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℕ0
∧ 2 < 𝐾) →
𝐾 ∈
ℤ) |
14 | | peano2zm 12363 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℤ → (𝐾 − 1) ∈
ℤ) |
15 | 13, 14 | syl 17 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℕ0
∧ 2 < 𝐾) →
(𝐾 − 1) ∈
ℤ) |
16 | | zltlem1 12373 |
. . . . . . . . . . 11
⊢ ((2
∈ ℤ ∧ 𝐾
∈ ℤ) → (2 < 𝐾 ↔ 2 ≤ (𝐾 − 1))) |
17 | 10, 12, 16 | sylancr 587 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℕ0
→ (2 < 𝐾 ↔ 2
≤ (𝐾 −
1))) |
18 | 17 | biimpa 477 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℕ0
∧ 2 < 𝐾) → 2
≤ (𝐾 −
1)) |
19 | | eluz2 12588 |
. . . . . . . . 9
⊢ ((𝐾 − 1) ∈
(ℤ≥‘2) ↔ (2 ∈ ℤ ∧ (𝐾 − 1) ∈ ℤ ∧
2 ≤ (𝐾 −
1))) |
20 | 11, 15, 18, 19 | syl3anbrc 1342 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℕ0
∧ 2 < 𝐾) →
(𝐾 − 1) ∈
(ℤ≥‘2)) |
21 | | exprmfct 16409 |
. . . . . . . 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 27932 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin) → 𝐺 ∈ FinUSGraph) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾) → 𝐺 ∈ FinUSGraph) |
26 | 25 | 3ad2ant3 1134 |
. . . . . . . . . . . 12
⊢ (((𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1)) ∧ (𝐾 ∈ ℕ0 ∧ 2 <
𝐾) ∧ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾)) → 𝐺 ∈ FinUSGraph) |
27 | | simp1l 1196 |
. . . . . . . . . . . 12
⊢ (((𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1)) ∧ (𝐾 ∈ ℕ0 ∧ 2 <
𝐾) ∧ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾)) → 𝑝 ∈ ℙ) |
28 | | numclwwlk8 28756 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑝 ∈ ℙ) →
((♯‘(𝑝
ClWWalksN 𝐺)) mod 𝑝) = 0) |
29 | 26, 27, 28 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1)) ∧ (𝐾 ∈ ℕ0 ∧ 2 <
𝐾) ∧ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾)) → ((♯‘(𝑝 ClWWalksN 𝐺)) mod 𝑝) = 0) |
30 | 2 | 3ad2ant3 1134 |
. . . . . . . . . . . 12
⊢ (((𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1)) ∧ (𝐾 ∈ ℕ0 ∧ 2 <
𝐾) ∧ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾)) → (𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph )) |
31 | | pm3.22 460 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin)) |
32 | 31 | 3adant1 1129 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin)) |
33 | 32 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾) → (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin)) |
34 | 33 | 3ad2ant3 1134 |
. . . . . . . . . . . 12
⊢ (((𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1)) ∧ (𝐾 ∈ ℕ0 ∧ 2 <
𝐾) ∧ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾)) → (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin)) |
35 | | simp1 1135 |
. . . . . . . . . . . 12
⊢ (((𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1)) ∧ (𝐾 ∈ ℕ0 ∧ 2 <
𝐾) ∧ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾)) → (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1))) |
36 | 7 | numclwwlk7 28755 |
. . . . . . . . . . . 12
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1))) → ((♯‘(𝑝 ClWWalksN 𝐺)) mod 𝑝) = 1) |
37 | 30, 34, 35, 36 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ (((𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1)) ∧ (𝐾 ∈ ℕ0 ∧ 2 <
𝐾) ∧ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾)) → ((♯‘(𝑝 ClWWalksN 𝐺)) mod 𝑝) = 1) |
38 | | eqeq1 2742 |
. . . . . . . . . . . 12
⊢
(((♯‘(𝑝
ClWWalksN 𝐺)) mod 𝑝) = 0 →
(((♯‘(𝑝
ClWWalksN 𝐺)) mod 𝑝) = 1 ↔ 0 =
1)) |
39 | | ax-1ne0 10940 |
. . . . . . . . . . . . . 14
⊢ 1 ≠
0 |
40 | 39 | nesymi 3001 |
. . . . . . . . . . . . 13
⊢ ¬ 0
= 1 |
41 | 40 | pm2.21i 119 |
. . . . . . . . . . . 12
⊢ (0 = 1
→ 𝐾 =
2) |
42 | 38, 41 | syl6bi 252 |
. . . . . . . . . . 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 1118 |
. . . . . . . 8
⊢ ((𝑝 ∈ ℙ ∧ 𝑝 ∥ (𝐾 − 1)) → ((𝐾 ∈ ℕ0 ∧ 2 <
𝐾) → (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾) → (1 < 𝐾 → 𝐾 = 2)))) |
46 | 45 | rexlimiva 3210 |
. . . . . . 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 414 |
. . . . 5
⊢ (2 <
𝐾 → (𝐾 ∈ ℕ0 → (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾) → (1 < 𝐾 → 𝐾 = 2)))) |
49 | 48 | com23 86 |
. . . 4
⊢ (2 <
𝐾 → (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝐾) → (𝐾 ∈ ℕ0 → (1 <
𝐾 → 𝐾 = 2)))) |
50 | | 1red 10976 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℕ0
→ 1 ∈ ℝ) |
51 | | nn0re 12242 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℝ) |
52 | 50, 51 | ltnled 11122 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ0
→ (1 < 𝐾 ↔
¬ 𝐾 ≤
1)) |
53 | | 1e2m1 12100 |
. . . . . . . . . . 11
⊢ 1 = (2
− 1) |
54 | 53 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℕ0
→ 1 = (2 − 1)) |
55 | 54 | breq2d 5086 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℕ0
→ (𝐾 ≤ 1 ↔
𝐾 ≤ (2 −
1))) |
56 | 55 | notbid 318 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ0
→ (¬ 𝐾 ≤ 1
↔ ¬ 𝐾 ≤ (2
− 1))) |
57 | | zltlem1 12373 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ ℤ ∧ 2 ∈
ℤ) → (𝐾 < 2
↔ 𝐾 ≤ (2 −
1))) |
58 | 12, 10, 57 | sylancl 586 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℕ0
→ (𝐾 < 2 ↔
𝐾 ≤ (2 −
1))) |
59 | 58 | bicomd 222 |
. . . . . . . . 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 12047 |
. . . . . . . . 9
⊢ 2 ∈
ℝ |
63 | | lttri3 11058 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℝ ∧ 2 ∈
ℝ) → (𝐾 = 2
↔ (¬ 𝐾 < 2
∧ ¬ 2 < 𝐾))) |
64 | 63 | biimprd 247 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℝ ∧ 2 ∈
ℝ) → ((¬ 𝐾
< 2 ∧ ¬ 2 < 𝐾) → 𝐾 = 2)) |
65 | 51, 62, 64 | sylancl 586 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ0
→ ((¬ 𝐾 < 2
∧ ¬ 2 < 𝐾)
→ 𝐾 =
2)) |
66 | 65 | expd 416 |
. . . . . . 7
⊢ (𝐾 ∈ ℕ0
→ (¬ 𝐾 < 2
→ (¬ 2 < 𝐾
→ 𝐾 =
2))) |
67 | 61, 66 | sylbid 239 |
. . . . . 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 454 |
1
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((𝐺 RegUSGraph 𝐾 ∧ 1 < 𝐾) → 𝐾 = 2)) |