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 syl6bi ( ( ( ♯ ‘ ( 𝑝 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 ) )