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 ⊢ V = Vtx ⁡ G
Assertion frgrreg ⊢ V ∈ Fin ∧ V ≠ ∅ → G ∈ FriendGraph ∧ G RegUSGraph K → K = 0 ∨ K = 2

Proof

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