| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ancom 460 | . . . . . . . . 9
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ↔ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin)) | 
| 2 |  | ancom 460 | . . . . . . . . 9
⊢ ((𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾) ↔ (𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph )) | 
| 3 | 1, 2 | anbi12i 628 | . . . . . . . 8
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) ↔ ((𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ))) | 
| 4 | 3 | biimpi 216 | . . . . . . 7
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → ((𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ))) | 
| 5 | 4 | ancomd 461 | . . . . . 6
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → ((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin))) | 
| 6 |  | frgrreggt1.v | . . . . . . 7
⊢ 𝑉 = (Vtx‘𝐺) | 
| 7 | 6 | numclwwlk7lem 30409 | . . . . . 6
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin)) → 𝐾 ∈
ℕ0) | 
| 8 | 5, 7 | syl 17 | . . . . 5
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → 𝐾 ∈
ℕ0) | 
| 9 |  | neanior 3034 | . . . . . . . 8
⊢ ((𝐾 ≠ 0 ∧ 𝐾 ≠ 2) ↔ ¬ (𝐾 = 0 ∨ 𝐾 = 2)) | 
| 10 |  | nn0re 12537 | . . . . . . . . . . . . . 14
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℝ) | 
| 11 |  | 1re 11262 | . . . . . . . . . . . . . 14
⊢ 1 ∈
ℝ | 
| 12 |  | lenlt 11340 | . . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℝ ∧ 1 ∈
ℝ) → (𝐾 ≤ 1
↔ ¬ 1 < 𝐾)) | 
| 13 | 10, 11, 12 | sylancl 586 | . . . . . . . . . . . . 13
⊢ (𝐾 ∈ ℕ0
→ (𝐾 ≤ 1 ↔
¬ 1 < 𝐾)) | 
| 14 | 13 | adantl 481 | . . . . . . . . . . . 12
⊢ (((𝐾 ≠ 0 ∧ 𝐾 ≠ 2) ∧ 𝐾 ∈ ℕ0) → (𝐾 ≤ 1 ↔ ¬ 1 <
𝐾)) | 
| 15 |  | elnnne0 12542 | . . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ ℕ ↔ (𝐾 ∈ ℕ0
∧ 𝐾 ≠
0)) | 
| 16 |  | nnle1eq1 12297 | . . . . . . . . . . . . . . . . 17
⊢ (𝐾 ∈ ℕ → (𝐾 ≤ 1 ↔ 𝐾 = 1)) | 
| 17 | 16 | biimpd 229 | . . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ ℕ → (𝐾 ≤ 1 → 𝐾 = 1)) | 
| 18 | 15, 17 | sylbir 235 | . . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ ℕ0
∧ 𝐾 ≠ 0) →
(𝐾 ≤ 1 → 𝐾 = 1)) | 
| 19 | 18 | a1d 25 | . . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℕ0
∧ 𝐾 ≠ 0) →
(𝐾 ≠ 2 → (𝐾 ≤ 1 → 𝐾 = 1))) | 
| 20 | 19 | expimpd 453 | . . . . . . . . . . . . 13
⊢ (𝐾 ∈ ℕ0
→ ((𝐾 ≠ 0 ∧
𝐾 ≠ 2) → (𝐾 ≤ 1 → 𝐾 = 1))) | 
| 21 | 20 | impcom 407 | . . . . . . . . . . . 12
⊢ (((𝐾 ≠ 0 ∧ 𝐾 ≠ 2) ∧ 𝐾 ∈ ℕ0) → (𝐾 ≤ 1 → 𝐾 = 1)) | 
| 22 | 14, 21 | sylbird 260 | . . . . . . . . . . 11
⊢ (((𝐾 ≠ 0 ∧ 𝐾 ≠ 2) ∧ 𝐾 ∈ ℕ0) → (¬ 1
< 𝐾 → 𝐾 = 1)) | 
| 23 | 6 | fveq2i 6908 | . . . . . . . . . . . . . . . . . 18
⊢
(♯‘𝑉) =
(♯‘(Vtx‘𝐺)) | 
| 24 | 23 | eqeq1i 2741 | . . . . . . . . . . . . . . . . 17
⊢
((♯‘𝑉) =
1 ↔ (♯‘(Vtx‘𝐺)) = 1) | 
| 25 | 24 | biimpi 216 | . . . . . . . . . . . . . . . 16
⊢
((♯‘𝑉) =
1 → (♯‘(Vtx‘𝐺)) = 1) | 
| 26 |  | simpr 484 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾) → 𝐺 RegUSGraph 𝐾) | 
| 27 | 26 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → 𝐺 RegUSGraph 𝐾) | 
| 28 |  | rusgr1vtx 29607 | . . . . . . . . . . . . . . . 16
⊢
(((♯‘(Vtx‘𝐺)) = 1 ∧ 𝐺 RegUSGraph 𝐾) → 𝐾 = 0) | 
| 29 | 25, 27, 28 | syl2an 596 | . . . . . . . . . . . . . . 15
⊢
(((♯‘𝑉)
= 1 ∧ ((𝑉 ∈ Fin
∧ 𝑉 ≠ ∅) ∧
(𝐺 ∈ FriendGraph ∧
𝐺 RegUSGraph 𝐾))) → 𝐾 = 0) | 
| 30 | 29 | orcd 873 | . . . . . . . . . . . . . 14
⊢
(((♯‘𝑉)
= 1 ∧ ((𝑉 ∈ Fin
∧ 𝑉 ≠ ∅) ∧
(𝐺 ∈ FriendGraph ∧
𝐺 RegUSGraph 𝐾))) → (𝐾 = 0 ∨ 𝐾 = 2)) | 
| 31 | 30 | ex 412 | . . . . . . . . . . . . 13
⊢
((♯‘𝑉) =
1 → (((𝑉 ∈ Fin
∧ 𝑉 ≠ ∅) ∧
(𝐺 ∈ FriendGraph ∧
𝐺 RegUSGraph 𝐾)) → (𝐾 = 0 ∨ 𝐾 = 2))) | 
| 32 | 31 | a1d 25 | . . . . . . . . . . . 12
⊢
((♯‘𝑉) =
1 → (𝐾 = 1 →
(((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (𝐾 = 0 ∨ 𝐾 = 2)))) | 
| 33 |  | eqid 2736 | . . . . . . . . . . . . . . . . 17
⊢
(VtxDeg‘𝐺) =
(VtxDeg‘𝐺) | 
| 34 | 6, 33 | rusgrprop0 29586 | . . . . . . . . . . . . . . . 16
⊢ (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0*
∧ ∀𝑣 ∈
𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾)) | 
| 35 |  | simp2 1137 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((¬
(♯‘𝑉) = 1 ∧
𝐺 ∈ FriendGraph ∧
(𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → 𝐺 ∈ FriendGraph
) | 
| 36 |  | hashnncl 14406 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑉 ∈ Fin →
((♯‘𝑉) ∈
ℕ ↔ 𝑉 ≠
∅)) | 
| 37 |  | df-ne 2940 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((♯‘𝑉)
≠ 1 ↔ ¬ (♯‘𝑉) = 1) | 
| 38 |  | nngt1ne1 12296 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((♯‘𝑉)
∈ ℕ → (1 < (♯‘𝑉) ↔ (♯‘𝑉) ≠ 1)) | 
| 39 | 38 | biimprd 248 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((♯‘𝑉)
∈ ℕ → ((♯‘𝑉) ≠ 1 → 1 < (♯‘𝑉))) | 
| 40 | 37, 39 | biimtrrid 243 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((♯‘𝑉)
∈ ℕ → (¬ (♯‘𝑉) = 1 → 1 < (♯‘𝑉))) | 
| 41 | 36, 40 | biimtrrdi 254 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑉 ∈ Fin → (𝑉 ≠ ∅ → (¬
(♯‘𝑉) = 1
→ 1 < (♯‘𝑉)))) | 
| 42 | 41 | imp 406 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (¬
(♯‘𝑉) = 1
→ 1 < (♯‘𝑉))) | 
| 43 | 42 | impcom 407 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((¬
(♯‘𝑉) = 1 ∧
(𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → 1 <
(♯‘𝑉)) | 
| 44 | 6 | vdgn1frgrv3 30317 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐺 ∈ FriendGraph ∧ 1 <
(♯‘𝑉)) →
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 1) | 
| 45 | 35, 43, 44 | 3imp3i2an 1345 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((¬
(♯‘𝑉) = 1 ∧
𝐺 ∈ FriendGraph ∧
(𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) →
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 1) | 
| 46 |  | r19.26 3110 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(∀𝑣 ∈
𝑉 (((VtxDeg‘𝐺)‘𝑣) ≠ 1 ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾) ↔ (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 1 ∧ ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾)) | 
| 47 |  | r19.2z 4494 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑉 ≠ ∅ ∧
∀𝑣 ∈ 𝑉 (((VtxDeg‘𝐺)‘𝑣) ≠ 1 ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾)) → ∃𝑣 ∈ 𝑉 (((VtxDeg‘𝐺)‘𝑣) ≠ 1 ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾)) | 
| 48 |  | neeq1 3002 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (((VtxDeg‘𝐺)‘𝑣) ≠ 1 ↔ 𝐾 ≠ 1)) | 
| 49 | 48 | biimpd 229 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (((VtxDeg‘𝐺)‘𝑣) ≠ 1 → 𝐾 ≠ 1)) | 
| 50 | 49 | impcom 407 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((VtxDeg‘𝐺)‘𝑣) ≠ 1 ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → 𝐾 ≠ 1) | 
| 51 |  | eqneqall 2950 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
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 3150 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(∃𝑣 ∈
𝑉 (((VtxDeg‘𝐺)‘𝑣) ≠ 1 ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (𝐾 = 1 → (𝐾 = 0 ∨ 𝐾 = 2))) | 
| 55 | 47, 54 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑉 ≠ ∅ ∧
∀𝑣 ∈ 𝑉 (((VtxDeg‘𝐺)‘𝑣) ≠ 1 ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾)) → (𝐾 = 1 → (𝐾 = 0 ∨ 𝐾 = 2))) | 
| 56 | 55 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑉 ≠ ∅ →
(∀𝑣 ∈ 𝑉 (((VtxDeg‘𝐺)‘𝑣) ≠ 1 ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (𝐾 = 1 → (𝐾 = 0 ∨ 𝐾 = 2)))) | 
| 57 | 46, 56 | biimtrrid 243 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑉 ≠ ∅ →
((∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 1 ∧ ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (𝐾 = 1 → (𝐾 = 0 ∨ 𝐾 = 2)))) | 
| 58 | 57 | expd 415 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑉 ≠ ∅ →
(∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 1 → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (𝐾 = 1 → (𝐾 = 0 ∨ 𝐾 = 2))))) | 
| 59 | 58 | com34 91 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑉 ≠ ∅ →
(∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 1 → (𝐾 = 1 → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (𝐾 = 0 ∨ 𝐾 = 2))))) | 
| 60 | 59 | adantl 481 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
(∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 1 → (𝐾 = 1 → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (𝐾 = 0 ∨ 𝐾 = 2))))) | 
| 61 | 60 | 3ad2ant3 1135 | . . . . . . . . . . . . . . . . . . . 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 1119 | . . . . . . . . . . . . . . . . . 18
⊢ (¬
(♯‘𝑉) = 1
→ (𝐺 ∈
FriendGraph → ((𝑉
∈ Fin ∧ 𝑉 ≠
∅) → (𝐾 = 1
→ (∀𝑣 ∈
𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (𝐾 = 0 ∨ 𝐾 = 2)))))) | 
| 64 | 63 | com15 101 | . . . . . . . . . . . . . . . . 17
⊢
(∀𝑣 ∈
𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (𝐺 ∈ FriendGraph → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 1 → (¬
(♯‘𝑉) = 1
→ (𝐾 = 0 ∨ 𝐾 = 2)))))) | 
| 65 | 64 | 3ad2ant3 1135 | . . . . . . . . . . . . . . . 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 407 | . . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 1 → (¬ (♯‘𝑉) = 1 → (𝐾 = 0 ∨ 𝐾 = 2))))) | 
| 68 | 67 | impcom 407 | . . . . . . . . . . . . 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 412 | . . . . . . . . 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 235 | . . . . . . 7
⊢ (¬
(𝐾 = 0 ∨ 𝐾 = 2) → (¬ 1 < 𝐾 → (𝐾 ∈ ℕ0 → (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (𝐾 = 0 ∨ 𝐾 = 2))))) | 
| 75 | 74 | impcom 407 | . . . . . 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 430 | . 2
⊢ (¬ 1
< 𝐾 → (¬ (𝐾 = 0 ∨ 𝐾 = 2) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾) → (𝐾 = 0 ∨ 𝐾 = 2))))) | 
| 80 |  | simprl 770 | . . . . 5
⊢ (((1 <
𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → 𝐺 ∈ FriendGraph ) | 
| 81 |  | simpl 482 | . . . . . 6
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → 𝑉 ∈ Fin) | 
| 82 | 81 | ad2antlr 727 | . . . . 5
⊢ (((1 <
𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → 𝑉 ∈ Fin) | 
| 83 |  | simpr 484 | . . . . . 6
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → 𝑉 ≠ ∅) | 
| 84 | 83 | ad2antlr 727 | . . . . 5
⊢ (((1 <
𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → 𝑉 ≠ ∅) | 
| 85 |  | simpl 482 | . . . . . 6
⊢ ((1 <
𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → 1 < 𝐾) | 
| 86 | 85, 26 | anim12ci 614 | . . . . 5
⊢ (((1 <
𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (𝐺 RegUSGraph 𝐾 ∧ 1 < 𝐾)) | 
| 87 | 6 | frgrreggt1 30413 | . . . . . 6
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((𝐺 RegUSGraph 𝐾 ∧ 1 < 𝐾) → 𝐾 = 2)) | 
| 88 | 87 | imp 406 | . . . . 5
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 RegUSGraph 𝐾 ∧ 1 < 𝐾)) → 𝐾 = 2) | 
| 89 | 80, 82, 84, 86, 88 | syl31anc 1374 | . . . 4
⊢ (((1 <
𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → 𝐾 = 2) | 
| 90 | 89 | olcd 874 | . . 3
⊢ (((1 <
𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (𝐾 = 0 ∨ 𝐾 = 2)) | 
| 91 | 90 | exp31 419 | . 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))) |