Metamath Proof Explorer

Theorem frgrreg

Description: If a finite nonempty friendship graph is K-regular, then K must be 2 (or 0 ). (Contributed by Alexander van der Vekens, 9-Oct-2018) (Revised by AV, 3-Jun-2021)

Ref Expression
Hypothesis frgrreggt1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion frgrreg ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) )

Proof

Step Hyp Ref Expression
1 frgrreggt1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 ancom ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ↔ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) )
3 ancom ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) ↔ ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) )
4 2 3 anbi12i ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) ) ↔ ( ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ∧ ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ) )
5 4 biimpi ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) ) → ( ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ∧ ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ) )
6 5 ancomd ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) ) → ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ) )
7 1 numclwwlk7lem ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ) → 𝐾 ∈ ℕ0 )
8 6 7 syl ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) ) → 𝐾 ∈ ℕ0 )
9 neanior ⊢ ( ( 𝐾 ≠ 0 ∧ 𝐾 ≠ 2 ) ↔ ¬ ( 𝐾 = 0 ∨ 𝐾 = 2 ) )
10 nn0re ⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℝ )
11 1re ⊢ 1 ∈ ℝ
12 lenlt ⊢ ( ( 𝐾 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝐾 ≤ 1 ↔ ¬ 1 < 𝐾 ) )
13 10 11 12 sylancl ⊢ ( 𝐾 ∈ ℕ0 → ( 𝐾 ≤ 1 ↔ ¬ 1 < 𝐾 ) )
14 13 adantl ⊢ ( ( ( 𝐾 ≠ 0 ∧ 𝐾 ≠ 2 ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝐾 ≤ 1 ↔ ¬ 1 < 𝐾 ) )
15 elnnne0 ⊢ ( 𝐾 ∈ ℕ ↔ ( 𝐾 ∈ ℕ0 ∧ 𝐾 ≠ 0 ) )
16 nnle1eq1 ⊢ ( 𝐾 ∈ ℕ → ( 𝐾 ≤ 1 ↔ 𝐾 = 1 ) )
17 16 biimpd ⊢ ( 𝐾 ∈ ℕ → ( 𝐾 ≤ 1 → 𝐾 = 1 ) )
18 15 17 sylbir ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐾 ≠ 0 ) → ( 𝐾 ≤ 1 → 𝐾 = 1 ) )
19 18 a1d ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐾 ≠ 0 ) → ( 𝐾 ≠ 2 → ( 𝐾 ≤ 1 → 𝐾 = 1 ) ) )
20 19 expimpd ⊢ ( 𝐾 ∈ ℕ0 → ( ( 𝐾 ≠ 0 ∧ 𝐾 ≠ 2 ) → ( 𝐾 ≤ 1 → 𝐾 = 1 ) ) )
21 20 impcom ⊢ ( ( ( 𝐾 ≠ 0 ∧ 𝐾 ≠ 2 ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝐾 ≤ 1 → 𝐾 = 1 ) )
22 14 21 sylbird ⊢ ( ( ( 𝐾 ≠ 0 ∧ 𝐾 ≠ 2 ) ∧ 𝐾 ∈ ℕ0 ) → ( ¬ 1 < 𝐾 → 𝐾 = 1 ) )
23 1 fveq2i ⊢ ( ♯ ‘ 𝑉 ) = ( ♯ ‘ ( Vtx ‘ 𝐺 ) )
24 23 eqeq1i ⊢ ( ( ♯ ‘ 𝑉 ) = 1 ↔ ( ♯ ‘ ( Vtx ‘ 𝐺 ) ) = 1 )
25 24 biimpi ⊢ ( ( ♯ ‘ 𝑉 ) = 1 → ( ♯ ‘ ( Vtx ‘ 𝐺 ) ) = 1 )
26 simpr ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) → 𝐺 RegUSGraph 𝐾 )
27 26 adantl ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) ) → 𝐺 RegUSGraph 𝐾 )
28 rusgr1vtx ⊢ ( ( ( ♯ ‘ ( Vtx ‘ 𝐺 ) ) = 1 ∧ 𝐺 RegUSGraph 𝐾 ) → 𝐾 = 0 )
29 25 27 28 syl2an ⊢ ( ( ( ♯ ‘ 𝑉 ) = 1 ∧ ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) ) ) → 𝐾 = 0 )
30 29 orcd ⊢ ( ( ( ♯ ‘ 𝑉 ) = 1 ∧ ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) ) ) → ( 𝐾 = 0 ∨ 𝐾 = 2 ) )
31 30 ex ⊢ ( ( ♯ ‘ 𝑉 ) = 1 → ( ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) ) → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) )
32 31 a1d ⊢ ( ( ♯ ‘ 𝑉 ) = 1 → ( 𝐾 = 1 → ( ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) ) → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) ) )
33 eqid ⊢ ( VtxDeg ‘ 𝐺 ) = ( VtxDeg ‘ 𝐺 )
34 1 33 rusgrprop0 ⊢ ( 𝐺 RegUSGraph 𝐾 → ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) )
35 simp2 ⊢ ( ( ¬ ( ♯ ‘ 𝑉 ) = 1 ∧ 𝐺 ∈ FriendGraph ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ) → 𝐺 ∈ FriendGraph )
36 hashnncl ⊢ ( 𝑉 ∈ Fin → ( ( ♯ ‘ 𝑉 ) ∈ ℕ ↔ 𝑉 ≠ ∅ ) )
37 df-ne ⊢ ( ( ♯ ‘ 𝑉 ) ≠ 1 ↔ ¬ ( ♯ ‘ 𝑉 ) = 1 )
38 nngt1ne1 ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℕ → ( 1 < ( ♯ ‘ 𝑉 ) ↔ ( ♯ ‘ 𝑉 ) ≠ 1 ) )
39 38 biimprd ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℕ → ( ( ♯ ‘ 𝑉 ) ≠ 1 → 1 < ( ♯ ‘ 𝑉 ) ) )
40 37 39 syl5bir ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℕ → ( ¬ ( ♯ ‘ 𝑉 ) = 1 → 1 < ( ♯ ‘ 𝑉 ) ) )
41 36 40 syl6bir ⊢ ( 𝑉 ∈ Fin → ( 𝑉 ≠ ∅ → ( ¬ ( ♯ ‘ 𝑉 ) = 1 → 1 < ( ♯ ‘ 𝑉 ) ) ) )
42 41 imp ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( ¬ ( ♯ ‘ 𝑉 ) = 1 → 1 < ( ♯ ‘ 𝑉 ) ) )
43 42 impcom ⊢ ( ( ¬ ( ♯ ‘ 𝑉 ) = 1 ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ) → 1 < ( ♯ ‘ 𝑉 ) )
44 1 vdgn1frgrv3 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 1 )
45 35 43 44 3imp3i2an ⊢ ( ( ¬ ( ♯ ‘ 𝑉 ) = 1 ∧ 𝐺 ∈ FriendGraph ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ) → ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 1 )
46 r19.26 ⊢ ( ∀ 𝑣 ∈ 𝑉 ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 1 ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) ↔ ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 1 ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) )
47 r19.2z ⊢ ( ( 𝑉 ≠ ∅ ∧ ∀ 𝑣 ∈ 𝑉 ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 1 ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) ) → ∃ 𝑣 ∈ 𝑉 ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 1 ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) )
48 neeq1 ⊢ ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 1 ↔ 𝐾 ≠ 1 ) )
49 48 biimpd ⊢ ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 1 → 𝐾 ≠ 1 ) )
50 49 impcom ⊢ ( ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 1 ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → 𝐾 ≠ 1 )
51 eqneqall ⊢ ( 𝐾 = 1 → ( 𝐾 ≠ 1 → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) )
52 51 com12 ⊢ ( 𝐾 ≠ 1 → ( 𝐾 = 1 → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) )
53 50 52 syl ⊢ ( ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 1 ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → ( 𝐾 = 1 → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) )
54 53 rexlimivw ⊢ ( ∃ 𝑣 ∈ 𝑉 ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 1 ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → ( 𝐾 = 1 → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) )
55 47 54 syl ⊢ ( ( 𝑉 ≠ ∅ ∧ ∀ 𝑣 ∈ 𝑉 ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 1 ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) ) → ( 𝐾 = 1 → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) )
56 55 ex ⊢ ( 𝑉 ≠ ∅ → ( ∀ 𝑣 ∈ 𝑉 ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 1 ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → ( 𝐾 = 1 → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) ) )
57 46 56 syl5bir ⊢ ( 𝑉 ≠ ∅ → ( ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 1 ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → ( 𝐾 = 1 → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) ) )
58 57 expd ⊢ ( 𝑉 ≠ ∅ → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 1 → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( 𝐾 = 1 → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) ) ) )
59 58 com34 ⊢ ( 𝑉 ≠ ∅ → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 1 → ( 𝐾 = 1 → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) ) ) )
60 59 adantl ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 1 → ( 𝐾 = 1 → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) ) ) )
61 60 3ad2ant3 ⊢ ( ( ¬ ( ♯ ‘ 𝑉 ) = 1 ∧ 𝐺 ∈ FriendGraph ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ) → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 1 → ( 𝐾 = 1 → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) ) ) )
62 45 61 mpd ⊢ ( ( ¬ ( ♯ ‘ 𝑉 ) = 1 ∧ 𝐺 ∈ FriendGraph ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ) → ( 𝐾 = 1 → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) ) )
63 62 3exp ⊢ ( ¬ ( ♯ ‘ 𝑉 ) = 1 → ( 𝐺 ∈ FriendGraph → ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( 𝐾 = 1 → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) ) ) ) )
64 63 com15 ⊢ ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( 𝐺 ∈ FriendGraph → ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( 𝐾 = 1 → ( ¬ ( ♯ ‘ 𝑉 ) = 1 → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) ) ) ) )
65 64 3ad2ant3 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → ( 𝐺 ∈ FriendGraph → ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( 𝐾 = 1 → ( ¬ ( ♯ ‘ 𝑉 ) = 1 → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) ) ) ) )
66 34 65 syl ⊢ ( 𝐺 RegUSGraph 𝐾 → ( 𝐺 ∈ FriendGraph → ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( 𝐾 = 1 → ( ¬ ( ♯ ‘ 𝑉 ) = 1 → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) ) ) ) )
67 66 impcom ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) → ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( 𝐾 = 1 → ( ¬ ( ♯ ‘ 𝑉 ) = 1 → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) ) ) )
68 67 impcom ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) ) → ( 𝐾 = 1 → ( ¬ ( ♯ ‘ 𝑉 ) = 1 → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) ) )
69 68 com13 ⊢ ( ¬ ( ♯ ‘ 𝑉 ) = 1 → ( 𝐾 = 1 → ( ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) ) → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) ) )
70 32 69 pm2.61i ⊢ ( 𝐾 = 1 → ( ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) ) → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) )
71 22 70 syl6 ⊢ ( ( ( 𝐾 ≠ 0 ∧ 𝐾 ≠ 2 ) ∧ 𝐾 ∈ ℕ0 ) → ( ¬ 1 < 𝐾 → ( ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) ) → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) ) )
72 71 ex ⊢ ( ( 𝐾 ≠ 0 ∧ 𝐾 ≠ 2 ) → ( 𝐾 ∈ ℕ0 → ( ¬ 1 < 𝐾 → ( ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) ) → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) ) ) )
73 72 com23 ⊢ ( ( 𝐾 ≠ 0 ∧ 𝐾 ≠ 2 ) → ( ¬ 1 < 𝐾 → ( 𝐾 ∈ ℕ0 → ( ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) ) → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) ) ) )
74 9 73 sylbir ⊢ ( ¬ ( 𝐾 = 0 ∨ 𝐾 = 2 ) → ( ¬ 1 < 𝐾 → ( 𝐾 ∈ ℕ0 → ( ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) ) → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) ) ) )
75 74 impcom ⊢ ( ( ¬ 1 < 𝐾 ∧ ¬ ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) → ( 𝐾 ∈ ℕ0 → ( ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) ) → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) ) )
76 75 com13 ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) ) → ( 𝐾 ∈ ℕ0 → ( ( ¬ 1 < 𝐾 ∧ ¬ ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) ) )
77 8 76 mpd ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) ) → ( ( ¬ 1 < 𝐾 ∧ ¬ ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) )
78 77 com12 ⊢ ( ( ¬ 1 < 𝐾 ∧ ¬ ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) → ( ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) ) → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) )
79 78 exp4b ⊢ ( ¬ 1 < 𝐾 → ( ¬ ( 𝐾 = 0 ∨ 𝐾 = 2 ) → ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) ) ) )
80 simprl ⊢ ( ( ( 1 < 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) ) → 𝐺 ∈ FriendGraph )
81 simpl ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → 𝑉 ∈ Fin )
82 81 ad2antlr ⊢ ( ( ( 1 < 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) ) → 𝑉 ∈ Fin )
83 simpr ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → 𝑉 ≠ ∅ )
84 83 ad2antlr ⊢ ( ( ( 1 < 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) ) → 𝑉 ≠ ∅ )
85 simpl ⊢ ( ( 1 < 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ) → 1 < 𝐾 )
86 85 26 anim12ci ⊢ ( ( ( 1 < 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) ) → ( 𝐺 RegUSGraph 𝐾 ∧ 1 < 𝐾 ) )
87 1 frgrreggt1 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( ( 𝐺 RegUSGraph 𝐾 ∧ 1 < 𝐾 ) → 𝐾 = 2 ) )
88 87 imp ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ ( 𝐺 RegUSGraph 𝐾 ∧ 1 < 𝐾 ) ) → 𝐾 = 2 )
89 80 82 84 86 88 syl31anc ⊢ ( ( ( 1 < 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) ) → 𝐾 = 2 )
90 89 olcd ⊢ ( ( ( 1 < 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) ) → ( 𝐾 = 0 ∨ 𝐾 = 2 ) )
91 90 exp31 ⊢ ( 1 < 𝐾 → ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) ) )
92 2a1 ⊢ ( ( 𝐾 = 0 ∨ 𝐾 = 2 ) → ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) ) )
93 79 91 92 pm2.61ii ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) )