Metamath Proof Explorer

Theorem frgrreggt1

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

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

Proof

Step Hyp Ref Expression
1 frgrreggt1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 simp1 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → 𝐺 ∈ FriendGraph )
3 2 anim1ci ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) )
4 simp3 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → 𝑉 ≠ ∅ )
5 simp2 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → 𝑉 ∈ Fin )
6 4 5 jca ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) )
7 6 adantr ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) )
8 1 numclwwlk7lem ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ) → 𝐾 ∈ ℕ0 )
9 3 7 8 syl2anc ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 RegUSGraph 𝐾 ) → 𝐾 ∈ ℕ0 )
10 2z ⊢ 2 ∈ ℤ
11 10 a1i ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 2 < 𝐾 ) → 2 ∈ ℤ )
12 nn0z ⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℤ )
13 12 adantr ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 2 < 𝐾 ) → 𝐾 ∈ ℤ )
14 peano2zm ⊢ ( 𝐾 ∈ ℤ → ( 𝐾 − 1 ) ∈ ℤ )
15 13 14 syl ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 2 < 𝐾 ) → ( 𝐾 − 1 ) ∈ ℤ )
16 zltlem1 ⊢ ( ( 2 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 2 < 𝐾 ↔ 2 ≤ ( 𝐾 − 1 ) ) )
17 10 12 16 sylancr ⊢ ( 𝐾 ∈ ℕ0 → ( 2 < 𝐾 ↔ 2 ≤ ( 𝐾 − 1 ) ) )
18 17 biimpa ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 2 < 𝐾 ) → 2 ≤ ( 𝐾 − 1 ) )
19 eluz2 ⊢ ( ( 𝐾 − 1 ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ ( 𝐾 − 1 ) ∈ ℤ ∧ 2 ≤ ( 𝐾 − 1 ) ) )
20 11 15 18 19 syl3anbrc ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 2 < 𝐾 ) → ( 𝐾 − 1 ) ∈ ( ℤ≥ ‘ 2 ) )
21 exprmfct ⊢ ( ( 𝐾 − 1 ) ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ ( 𝐾 − 1 ) )
22 20 21 syl ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 2 < 𝐾 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ ( 𝐾 − 1 ) )
23 5 anim1ci ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) )
24 1 finrusgrfusgr ⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) → 𝐺 ∈ FinUSGraph )
25 23 24 syl ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 RegUSGraph 𝐾 ) → 𝐺 ∈ FinUSGraph )
26 25 3ad2ant3 ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( 𝐾 − 1 ) ) ∧ ( 𝐾 ∈ ℕ0 ∧ 2 < 𝐾 ) ∧ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 RegUSGraph 𝐾 ) ) → 𝐺 ∈ FinUSGraph )
27 simp1l ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( 𝐾 − 1 ) ) ∧ ( 𝐾 ∈ ℕ0 ∧ 2 < 𝐾 ) ∧ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 RegUSGraph 𝐾 ) ) → 𝑝 ∈ ℙ )
28 numclwwlk8 ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑝 ∈ ℙ ) → ( ( ♯ ‘ ( 𝑝 ClWWalksN 𝐺 ) ) mod 𝑝 ) = 0 )
29 26 27 28 syl2anc ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( 𝐾 − 1 ) ) ∧ ( 𝐾 ∈ ℕ0 ∧ 2 < 𝐾 ) ∧ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 RegUSGraph 𝐾 ) ) → ( ( ♯ ‘ ( 𝑝 ClWWalksN 𝐺 ) ) mod 𝑝 ) = 0 )
30 3 3ad2ant3 ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( 𝐾 − 1 ) ) ∧ ( 𝐾 ∈ ℕ0 ∧ 2 < 𝐾 ) ∧ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 RegUSGraph 𝐾 ) ) → ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) )
31 pm3.22 ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) )
32 31 3adant1 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) )
33 32 adantr ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) )
34 33 3ad2ant3 ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( 𝐾 − 1 ) ) ∧ ( 𝐾 ∈ ℕ0 ∧ 2 < 𝐾 ) ∧ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 RegUSGraph 𝐾 ) ) → ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) )
35 simp1 ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( 𝐾 − 1 ) ) ∧ ( 𝐾 ∈ ℕ0 ∧ 2 < 𝐾 ) ∧ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 RegUSGraph 𝐾 ) ) → ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( 𝐾 − 1 ) ) )
36 1 numclwwlk7 ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( 𝐾 − 1 ) ) ) → ( ( ♯ ‘ ( 𝑝 ClWWalksN 𝐺 ) ) mod 𝑝 ) = 1 )
37 30 34 35 36 syl3anc ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( 𝐾 − 1 ) ) ∧ ( 𝐾 ∈ ℕ0 ∧ 2 < 𝐾 ) ∧ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 RegUSGraph 𝐾 ) ) → ( ( ♯ ‘ ( 𝑝 ClWWalksN 𝐺 ) ) mod 𝑝 ) = 1 )
38 eqeq1 ⊢ ( ( ( ♯ ‘ ( 𝑝 ClWWalksN 𝐺 ) ) mod 𝑝 ) = 0 → ( ( ( ♯ ‘ ( 𝑝 ClWWalksN 𝐺 ) ) mod 𝑝 ) = 1 ↔ 0 = 1 ) )
39 ax-1ne0 ⊢ 1 ≠ 0
40 39 nesymi ⊢ ¬ 0 = 1
41 40 pm2.21i ⊢ ( 0 = 1 → 𝐾 = 2 )
42 38 41 biimtrdi ⊢ ( ( ( ♯ ‘ ( 𝑝 ClWWalksN 𝐺 ) ) mod 𝑝 ) = 0 → ( ( ( ♯ ‘ ( 𝑝 ClWWalksN 𝐺 ) ) mod 𝑝 ) = 1 → 𝐾 = 2 ) )
43 29 37 42 sylc ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( 𝐾 − 1 ) ) ∧ ( 𝐾 ∈ ℕ0 ∧ 2 < 𝐾 ) ∧ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 RegUSGraph 𝐾 ) ) → 𝐾 = 2 )
44 43 a1d ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( 𝐾 − 1 ) ) ∧ ( 𝐾 ∈ ℕ0 ∧ 2 < 𝐾 ) ∧ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 RegUSGraph 𝐾 ) ) → ( 1 < 𝐾 → 𝐾 = 2 ) )
45 44 3exp ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( 𝐾 − 1 ) ) → ( ( 𝐾 ∈ ℕ0 ∧ 2 < 𝐾 ) → ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( 1 < 𝐾 → 𝐾 = 2 ) ) ) )
46 45 rexlimiva ⊢ ( ∃ 𝑝 ∈ ℙ 𝑝 ∥ ( 𝐾 − 1 ) → ( ( 𝐾 ∈ ℕ0 ∧ 2 < 𝐾 ) → ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( 1 < 𝐾 → 𝐾 = 2 ) ) ) )
47 22 46 mpcom ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 2 < 𝐾 ) → ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( 1 < 𝐾 → 𝐾 = 2 ) ) )
48 47 expcom ⊢ ( 2 < 𝐾 → ( 𝐾 ∈ ℕ0 → ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( 1 < 𝐾 → 𝐾 = 2 ) ) ) )
49 48 com23 ⊢ ( 2 < 𝐾 → ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝐾 ∈ ℕ0 → ( 1 < 𝐾 → 𝐾 = 2 ) ) ) )
50 1red ⊢ ( 𝐾 ∈ ℕ0 → 1 ∈ ℝ )
51 nn0re ⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℝ )
52 50 51 ltnled ⊢ ( 𝐾 ∈ ℕ0 → ( 1 < 𝐾 ↔ ¬ 𝐾 ≤ 1 ) )
53 1e2m1 ⊢ 1 = ( 2 − 1 )
54 53 a1i ⊢ ( 𝐾 ∈ ℕ0 → 1 = ( 2 − 1 ) )
55 54 breq2d ⊢ ( 𝐾 ∈ ℕ0 → ( 𝐾 ≤ 1 ↔ 𝐾 ≤ ( 2 − 1 ) ) )
56 55 notbid ⊢ ( 𝐾 ∈ ℕ0 → ( ¬ 𝐾 ≤ 1 ↔ ¬ 𝐾 ≤ ( 2 − 1 ) ) )
57 zltlem1 ⊢ ( ( 𝐾 ∈ ℤ ∧ 2 ∈ ℤ ) → ( 𝐾 < 2 ↔ 𝐾 ≤ ( 2 − 1 ) ) )
58 12 10 57 sylancl ⊢ ( 𝐾 ∈ ℕ0 → ( 𝐾 < 2 ↔ 𝐾 ≤ ( 2 − 1 ) ) )
59 58 bicomd ⊢ ( 𝐾 ∈ ℕ0 → ( 𝐾 ≤ ( 2 − 1 ) ↔ 𝐾 < 2 ) )
60 59 notbid ⊢ ( 𝐾 ∈ ℕ0 → ( ¬ 𝐾 ≤ ( 2 − 1 ) ↔ ¬ 𝐾 < 2 ) )
61 52 56 60 3bitrd ⊢ ( 𝐾 ∈ ℕ0 → ( 1 < 𝐾 ↔ ¬ 𝐾 < 2 ) )
62 2re ⊢ 2 ∈ ℝ
63 lttri3 ⊢ ( ( 𝐾 ∈ ℝ ∧ 2 ∈ ℝ ) → ( 𝐾 = 2 ↔ ( ¬ 𝐾 < 2 ∧ ¬ 2 < 𝐾 ) ) )
64 63 biimprd ⊢ ( ( 𝐾 ∈ ℝ ∧ 2 ∈ ℝ ) → ( ( ¬ 𝐾 < 2 ∧ ¬ 2 < 𝐾 ) → 𝐾 = 2 ) )
65 51 62 64 sylancl ⊢ ( 𝐾 ∈ ℕ0 → ( ( ¬ 𝐾 < 2 ∧ ¬ 2 < 𝐾 ) → 𝐾 = 2 ) )
66 65 expd ⊢ ( 𝐾 ∈ ℕ0 → ( ¬ 𝐾 < 2 → ( ¬ 2 < 𝐾 → 𝐾 = 2 ) ) )
67 61 66 sylbid ⊢ ( 𝐾 ∈ ℕ0 → ( 1 < 𝐾 → ( ¬ 2 < 𝐾 → 𝐾 = 2 ) ) )
68 67 com3r ⊢ ( ¬ 2 < 𝐾 → ( 𝐾 ∈ ℕ0 → ( 1 < 𝐾 → 𝐾 = 2 ) ) )
69 68 a1d ⊢ ( ¬ 2 < 𝐾 → ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝐾 ∈ ℕ0 → ( 1 < 𝐾 → 𝐾 = 2 ) ) ) )
70 49 69 pm2.61i ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝐾 ∈ ℕ0 → ( 1 < 𝐾 → 𝐾 = 2 ) ) )
71 9 70 mpd ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( 1 < 𝐾 → 𝐾 = 2 ) )
72 71 expimpd ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( ( 𝐺 RegUSGraph 𝐾 ∧ 1 < 𝐾 ) → 𝐾 = 2 ) )