Step | Hyp | Ref
| Expression |
1 | | ancom 461 |
. . . . . . . . 9
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ↔ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin)) |
2 | | ancom 461 |
. . . . . . . . 9
⊢ ((𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾) ↔ (𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph )) |
3 | 1, 2 | anbi12i 627 |
. . . . . . . 8
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) ↔ ((𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ))) |
4 | 3 | biimpi 215 |
. . . . . . 7
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → ((𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ))) |
5 | 4 | ancomd 462 |
. . . . . 6
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → ((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin))) |
6 | | frgrreggt1.v |
. . . . . . 7
⊢ 𝑉 = (Vtx‘𝐺) |
7 | 6 | numclwwlk7lem 28740 |
. . . . . 6
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin)) → 𝐾 ∈
ℕ0) |
8 | 5, 7 | syl 17 |
. . . . 5
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → 𝐾 ∈
ℕ0) |
9 | | neanior 3037 |
. . . . . . . 8
⊢ ((𝐾 ≠ 0 ∧ 𝐾 ≠ 2) ↔ ¬ (𝐾 = 0 ∨ 𝐾 = 2)) |
10 | | nn0re 12231 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℝ) |
11 | | 1re 10964 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℝ |
12 | | lenlt 11042 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℝ ∧ 1 ∈
ℝ) → (𝐾 ≤ 1
↔ ¬ 1 < 𝐾)) |
13 | 10, 11, 12 | sylancl 586 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ ℕ0
→ (𝐾 ≤ 1 ↔
¬ 1 < 𝐾)) |
14 | 13 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝐾 ≠ 0 ∧ 𝐾 ≠ 2) ∧ 𝐾 ∈ ℕ0) → (𝐾 ≤ 1 ↔ ¬ 1 <
𝐾)) |
15 | | elnnne0 12236 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ ℕ ↔ (𝐾 ∈ ℕ0
∧ 𝐾 ≠
0)) |
16 | | nnle1eq1 11992 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐾 ∈ ℕ → (𝐾 ≤ 1 ↔ 𝐾 = 1)) |
17 | 16 | biimpd 228 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ ℕ → (𝐾 ≤ 1 → 𝐾 = 1)) |
18 | 15, 17 | sylbir 234 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ ℕ0
∧ 𝐾 ≠ 0) →
(𝐾 ≤ 1 → 𝐾 = 1)) |
19 | 18 | a1d 25 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℕ0
∧ 𝐾 ≠ 0) →
(𝐾 ≠ 2 → (𝐾 ≤ 1 → 𝐾 = 1))) |
20 | 19 | expimpd 454 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ ℕ0
→ ((𝐾 ≠ 0 ∧
𝐾 ≠ 2) → (𝐾 ≤ 1 → 𝐾 = 1))) |
21 | 20 | impcom 408 |
. . . . . . . . . . . 12
⊢ (((𝐾 ≠ 0 ∧ 𝐾 ≠ 2) ∧ 𝐾 ∈ ℕ0) → (𝐾 ≤ 1 → 𝐾 = 1)) |
22 | 14, 21 | sylbird 259 |
. . . . . . . . . . 11
⊢ (((𝐾 ≠ 0 ∧ 𝐾 ≠ 2) ∧ 𝐾 ∈ ℕ0) → (¬ 1
< 𝐾 → 𝐾 = 1)) |
23 | 6 | fveq2i 6771 |
. . . . . . . . . . . . . . . . . 18
⊢
(♯‘𝑉) =
(♯‘(Vtx‘𝐺)) |
24 | 23 | eqeq1i 2743 |
. . . . . . . . . . . . . . . . 17
⊢
((♯‘𝑉) =
1 ↔ (♯‘(Vtx‘𝐺)) = 1) |
25 | 24 | biimpi 215 |
. . . . . . . . . . . . . . . 16
⊢
((♯‘𝑉) =
1 → (♯‘(Vtx‘𝐺)) = 1) |
26 | | simpr 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾) → 𝐺 RegUSGraph 𝐾) |
27 | 26 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → 𝐺 RegUSGraph 𝐾) |
28 | | rusgr1vtx 27944 |
. . . . . . . . . . . . . . . 16
⊢
(((♯‘(Vtx‘𝐺)) = 1 ∧ 𝐺 RegUSGraph 𝐾) → 𝐾 = 0) |
29 | 25, 27, 28 | syl2an 596 |
. . . . . . . . . . . . . . 15
⊢
(((♯‘𝑉)
= 1 ∧ ((𝑉 ∈ Fin
∧ 𝑉 ≠ ∅) ∧
(𝐺 ∈ FriendGraph ∧
𝐺 RegUSGraph 𝐾))) → 𝐾 = 0) |
30 | 29 | orcd 870 |
. . . . . . . . . . . . . 14
⊢
(((♯‘𝑉)
= 1 ∧ ((𝑉 ∈ Fin
∧ 𝑉 ≠ ∅) ∧
(𝐺 ∈ FriendGraph ∧
𝐺 RegUSGraph 𝐾))) → (𝐾 = 0 ∨ 𝐾 = 2)) |
31 | 30 | ex 413 |
. . . . . . . . . . . . 13
⊢
((♯‘𝑉) =
1 → (((𝑉 ∈ Fin
∧ 𝑉 ≠ ∅) ∧
(𝐺 ∈ FriendGraph ∧
𝐺 RegUSGraph 𝐾)) → (𝐾 = 0 ∨ 𝐾 = 2))) |
32 | 31 | a1d 25 |
. . . . . . . . . . . 12
⊢
((♯‘𝑉) =
1 → (𝐾 = 1 →
(((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (𝐾 = 0 ∨ 𝐾 = 2)))) |
33 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢
(VtxDeg‘𝐺) =
(VtxDeg‘𝐺) |
34 | 6, 33 | rusgrprop0 27923 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0*
∧ ∀𝑣 ∈
𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾)) |
35 | | simp2 1136 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((¬
(♯‘𝑉) = 1 ∧
𝐺 ∈ FriendGraph ∧
(𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → 𝐺 ∈ FriendGraph
) |
36 | | hashnncl 14070 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑉 ∈ Fin →
((♯‘𝑉) ∈
ℕ ↔ 𝑉 ≠
∅)) |
37 | | df-ne 2944 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((♯‘𝑉)
≠ 1 ↔ ¬ (♯‘𝑉) = 1) |
38 | | nngt1ne1 11991 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((♯‘𝑉)
∈ ℕ → (1 < (♯‘𝑉) ↔ (♯‘𝑉) ≠ 1)) |
39 | 38 | biimprd 247 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((♯‘𝑉)
∈ ℕ → ((♯‘𝑉) ≠ 1 → 1 < (♯‘𝑉))) |
40 | 37, 39 | syl5bir 242 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((♯‘𝑉)
∈ ℕ → (¬ (♯‘𝑉) = 1 → 1 < (♯‘𝑉))) |
41 | 36, 40 | syl6bir 253 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑉 ∈ Fin → (𝑉 ≠ ∅ → (¬
(♯‘𝑉) = 1
→ 1 < (♯‘𝑉)))) |
42 | 41 | imp 407 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (¬
(♯‘𝑉) = 1
→ 1 < (♯‘𝑉))) |
43 | 42 | impcom 408 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((¬
(♯‘𝑉) = 1 ∧
(𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → 1 <
(♯‘𝑉)) |
44 | 6 | vdgn1frgrv3 28648 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐺 ∈ FriendGraph ∧ 1 <
(♯‘𝑉)) →
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 1) |
45 | 35, 43, 44 | 3imp3i2an 1344 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((¬
(♯‘𝑉) = 1 ∧
𝐺 ∈ FriendGraph ∧
(𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) →
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 1) |
46 | | r19.26 3095 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(∀𝑣 ∈
𝑉 (((VtxDeg‘𝐺)‘𝑣) ≠ 1 ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾) ↔ (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 1 ∧ ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾)) |
47 | | r19.2z 4427 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑉 ≠ ∅ ∧
∀𝑣 ∈ 𝑉 (((VtxDeg‘𝐺)‘𝑣) ≠ 1 ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾)) → ∃𝑣 ∈ 𝑉 (((VtxDeg‘𝐺)‘𝑣) ≠ 1 ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾)) |
48 | | neeq1 3006 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (((VtxDeg‘𝐺)‘𝑣) ≠ 1 ↔ 𝐾 ≠ 1)) |
49 | 48 | biimpd 228 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (((VtxDeg‘𝐺)‘𝑣) ≠ 1 → 𝐾 ≠ 1)) |
50 | 49 | impcom 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((VtxDeg‘𝐺)‘𝑣) ≠ 1 ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → 𝐾 ≠ 1) |
51 | | eqneqall 2954 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝐾 = 1 → (𝐾 ≠ 1 → (𝐾 = 0 ∨ 𝐾 = 2))) |
52 | 51 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐾 ≠ 1 → (𝐾 = 1 → (𝐾 = 0 ∨ 𝐾 = 2))) |
53 | 50, 52 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((VtxDeg‘𝐺)‘𝑣) ≠ 1 ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (𝐾 = 1 → (𝐾 = 0 ∨ 𝐾 = 2))) |
54 | 53 | rexlimivw 3210 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(∃𝑣 ∈
𝑉 (((VtxDeg‘𝐺)‘𝑣) ≠ 1 ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (𝐾 = 1 → (𝐾 = 0 ∨ 𝐾 = 2))) |
55 | 47, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑉 ≠ ∅ ∧
∀𝑣 ∈ 𝑉 (((VtxDeg‘𝐺)‘𝑣) ≠ 1 ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾)) → (𝐾 = 1 → (𝐾 = 0 ∨ 𝐾 = 2))) |
56 | 55 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑉 ≠ ∅ →
(∀𝑣 ∈ 𝑉 (((VtxDeg‘𝐺)‘𝑣) ≠ 1 ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (𝐾 = 1 → (𝐾 = 0 ∨ 𝐾 = 2)))) |
57 | 46, 56 | syl5bir 242 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑉 ≠ ∅ →
((∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 1 ∧ ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (𝐾 = 1 → (𝐾 = 0 ∨ 𝐾 = 2)))) |
58 | 57 | expd 416 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑉 ≠ ∅ →
(∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 1 → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (𝐾 = 1 → (𝐾 = 0 ∨ 𝐾 = 2))))) |
59 | 58 | com34 91 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑉 ≠ ∅ →
(∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 1 → (𝐾 = 1 → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (𝐾 = 0 ∨ 𝐾 = 2))))) |
60 | 59 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
(∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 1 → (𝐾 = 1 → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (𝐾 = 0 ∨ 𝐾 = 2))))) |
61 | 60 | 3ad2ant3 1134 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((¬
(♯‘𝑉) = 1 ∧
𝐺 ∈ FriendGraph ∧
(𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) →
(∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 1 → (𝐾 = 1 → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (𝐾 = 0 ∨ 𝐾 = 2))))) |
62 | 45, 61 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((¬
(♯‘𝑉) = 1 ∧
𝐺 ∈ FriendGraph ∧
(𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → (𝐾 = 1 → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (𝐾 = 0 ∨ 𝐾 = 2)))) |
63 | 62 | 3exp 1118 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
(♯‘𝑉) = 1
→ (𝐺 ∈
FriendGraph → ((𝑉
∈ Fin ∧ 𝑉 ≠
∅) → (𝐾 = 1
→ (∀𝑣 ∈
𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (𝐾 = 0 ∨ 𝐾 = 2)))))) |
64 | 63 | com15 101 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑣 ∈
𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (𝐺 ∈ FriendGraph → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 1 → (¬
(♯‘𝑉) = 1
→ (𝐾 = 0 ∨ 𝐾 = 2)))))) |
65 | 64 | 3ad2ant3 1134 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ∈ USGraph ∧ 𝐾 ∈
ℕ0* ∧ ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (𝐺 ∈ FriendGraph → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 1 → (¬
(♯‘𝑉) = 1
→ (𝐾 = 0 ∨ 𝐾 = 2)))))) |
66 | 34, 65 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ FriendGraph → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 1 → (¬
(♯‘𝑉) = 1
→ (𝐾 = 0 ∨ 𝐾 = 2)))))) |
67 | 66 | impcom 408 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 1 → (¬ (♯‘𝑉) = 1 → (𝐾 = 0 ∨ 𝐾 = 2))))) |
68 | 67 | impcom 408 |
. . . . . . . . . . . . 13
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (𝐾 = 1 → (¬ (♯‘𝑉) = 1 → (𝐾 = 0 ∨ 𝐾 = 2)))) |
69 | 68 | com13 88 |
. . . . . . . . . . . 12
⊢ (¬
(♯‘𝑉) = 1
→ (𝐾 = 1 →
(((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (𝐾 = 0 ∨ 𝐾 = 2)))) |
70 | 32, 69 | pm2.61i 182 |
. . . . . . . . . . 11
⊢ (𝐾 = 1 → (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (𝐾 = 0 ∨ 𝐾 = 2))) |
71 | 22, 70 | syl6 35 |
. . . . . . . . . 10
⊢ (((𝐾 ≠ 0 ∧ 𝐾 ≠ 2) ∧ 𝐾 ∈ ℕ0) → (¬ 1
< 𝐾 → (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (𝐾 = 0 ∨ 𝐾 = 2)))) |
72 | 71 | ex 413 |
. . . . . . . . 9
⊢ ((𝐾 ≠ 0 ∧ 𝐾 ≠ 2) → (𝐾 ∈ ℕ0 → (¬ 1
< 𝐾 → (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (𝐾 = 0 ∨ 𝐾 = 2))))) |
73 | 72 | com23 86 |
. . . . . . . 8
⊢ ((𝐾 ≠ 0 ∧ 𝐾 ≠ 2) → (¬ 1 < 𝐾 → (𝐾 ∈ ℕ0 → (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (𝐾 = 0 ∨ 𝐾 = 2))))) |
74 | 9, 73 | sylbir 234 |
. . . . . . 7
⊢ (¬
(𝐾 = 0 ∨ 𝐾 = 2) → (¬ 1 < 𝐾 → (𝐾 ∈ ℕ0 → (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (𝐾 = 0 ∨ 𝐾 = 2))))) |
75 | 74 | impcom 408 |
. . . . . 6
⊢ ((¬ 1
< 𝐾 ∧ ¬ (𝐾 = 0 ∨ 𝐾 = 2)) → (𝐾 ∈ ℕ0 → (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (𝐾 = 0 ∨ 𝐾 = 2)))) |
76 | 75 | com13 88 |
. . . . 5
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (𝐾 ∈ ℕ0 → ((¬ 1
< 𝐾 ∧ ¬ (𝐾 = 0 ∨ 𝐾 = 2)) → (𝐾 = 0 ∨ 𝐾 = 2)))) |
77 | 8, 76 | mpd 15 |
. . . 4
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → ((¬ 1 < 𝐾 ∧ ¬ (𝐾 = 0 ∨ 𝐾 = 2)) → (𝐾 = 0 ∨ 𝐾 = 2))) |
78 | 77 | com12 32 |
. . 3
⊢ ((¬ 1
< 𝐾 ∧ ¬ (𝐾 = 0 ∨ 𝐾 = 2)) → (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (𝐾 = 0 ∨ 𝐾 = 2))) |
79 | 78 | exp4b 431 |
. 2
⊢ (¬ 1
< 𝐾 → (¬ (𝐾 = 0 ∨ 𝐾 = 2) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾) → (𝐾 = 0 ∨ 𝐾 = 2))))) |
80 | | simprl 768 |
. . . . 5
⊢ (((1 <
𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → 𝐺 ∈ FriendGraph ) |
81 | | simpl 483 |
. . . . . 6
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → 𝑉 ∈ Fin) |
82 | 81 | ad2antlr 724 |
. . . . 5
⊢ (((1 <
𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → 𝑉 ∈ Fin) |
83 | | simpr 485 |
. . . . . 6
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → 𝑉 ≠ ∅) |
84 | 83 | ad2antlr 724 |
. . . . 5
⊢ (((1 <
𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → 𝑉 ≠ ∅) |
85 | | simpl 483 |
. . . . . 6
⊢ ((1 <
𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → 1 < 𝐾) |
86 | 85, 26 | anim12ci 614 |
. . . . 5
⊢ (((1 <
𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (𝐺 RegUSGraph 𝐾 ∧ 1 < 𝐾)) |
87 | 6 | frgrreggt1 28744 |
. . . . . 6
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((𝐺 RegUSGraph 𝐾 ∧ 1 < 𝐾) → 𝐾 = 2)) |
88 | 87 | imp 407 |
. . . . 5
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 RegUSGraph 𝐾 ∧ 1 < 𝐾)) → 𝐾 = 2) |
89 | 80, 82, 84, 86, 88 | syl31anc 1372 |
. . . 4
⊢ (((1 <
𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → 𝐾 = 2) |
90 | 89 | olcd 871 |
. . 3
⊢ (((1 <
𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (𝐾 = 0 ∨ 𝐾 = 2)) |
91 | 90 | exp31 420 |
. 2
⊢ (1 <
𝐾 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾) → (𝐾 = 0 ∨ 𝐾 = 2)))) |
92 | | 2a1 28 |
. 2
⊢ ((𝐾 = 0 ∨ 𝐾 = 2) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾) → (𝐾 = 0 ∨ 𝐾 = 2)))) |
93 | 79, 91, 92 | pm2.61ii 183 |
1
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾) → (𝐾 = 0 ∨ 𝐾 = 2))) |