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 
|- V = ( Vtx ` G )
Assertion frgrreggt1 
|- ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) -> ( ( G RegUSGraph K /\ 1 < K ) -> K = 2 ) )

Proof

Step Hyp Ref Expression
1 frgrreggt1.v 
 |-  V = ( Vtx ` G )
2 simp1 
 |-  ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) -> G e. FriendGraph )
3 2 anim1ci 
 |-  ( ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ G RegUSGraph K ) -> ( G RegUSGraph K /\ G e. FriendGraph ) )
4 simp3 
 |-  ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) -> V =/= (/) )
5 simp2 
 |-  ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) -> V e. Fin )
6 4 5 jca 
 |-  ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) -> ( V =/= (/) /\ V e. Fin ) )
7 6 adantr 
 |-  ( ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ G RegUSGraph K ) -> ( V =/= (/) /\ V e. Fin ) )
8 1 numclwwlk7lem 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V =/= (/) /\ V e. Fin ) ) -> K e. NN0 )
9 3 7 8 syl2anc 
 |-  ( ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ G RegUSGraph K ) -> K e. NN0 )
10 2z 
 |-  2 e. ZZ
11 10 a1i 
 |-  ( ( K e. NN0 /\ 2 < K ) -> 2 e. ZZ )
12 nn0z 
 |-  ( K e. NN0 -> K e. ZZ )
13 12 adantr 
 |-  ( ( K e. NN0 /\ 2 < K ) -> K e. ZZ )
14 peano2zm 
 |-  ( K e. ZZ -> ( K - 1 ) e. ZZ )
15 13 14 syl 
 |-  ( ( K e. NN0 /\ 2 < K ) -> ( K - 1 ) e. ZZ )
16 zltlem1 
 |-  ( ( 2 e. ZZ /\ K e. ZZ ) -> ( 2 < K <-> 2 <_ ( K - 1 ) ) )
17 10 12 16 sylancr 
 |-  ( K e. NN0 -> ( 2 < K <-> 2 <_ ( K - 1 ) ) )
18 17 biimpa 
 |-  ( ( K e. NN0 /\ 2 < K ) -> 2 <_ ( K - 1 ) )
19 eluz2 
 |-  ( ( K - 1 ) e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ ( K - 1 ) e. ZZ /\ 2 <_ ( K - 1 ) ) )
20 11 15 18 19 syl3anbrc 
 |-  ( ( K e. NN0 /\ 2 < K ) -> ( K - 1 ) e. ( ZZ>= ` 2 ) )
21 exprmfct 
 |-  ( ( K - 1 ) e. ( ZZ>= ` 2 ) -> E. p e. Prime p || ( K - 1 ) )
22 20 21 syl 
 |-  ( ( K e. NN0 /\ 2 < K ) -> E. p e. Prime p || ( K - 1 ) )
23 5 anim1ci 
 |-  ( ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ G RegUSGraph K ) -> ( G RegUSGraph K /\ V e. Fin ) )
24 1 finrusgrfusgr 
 |-  ( ( G RegUSGraph K /\ V e. Fin ) -> G e. FinUSGraph )
25 23 24 syl 
 |-  ( ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ G RegUSGraph K ) -> G e. FinUSGraph )
26 25 3ad2ant3 
 |-  ( ( ( p e. Prime /\ p || ( K - 1 ) ) /\ ( K e. NN0 /\ 2 < K ) /\ ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ G RegUSGraph K ) ) -> G e. FinUSGraph )
27 simp1l 
 |-  ( ( ( p e. Prime /\ p || ( K - 1 ) ) /\ ( K e. NN0 /\ 2 < K ) /\ ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ G RegUSGraph K ) ) -> p e. Prime )
28 numclwwlk8 
 |-  ( ( G e. FinUSGraph /\ p e. Prime ) -> ( ( # ` ( p ClWWalksN G ) ) mod p ) = 0 )
29 26 27 28 syl2anc 
 |-  ( ( ( p e. Prime /\ p || ( K - 1 ) ) /\ ( K e. NN0 /\ 2 < K ) /\ ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ G RegUSGraph K ) ) -> ( ( # ` ( p ClWWalksN G ) ) mod p ) = 0 )
30 3 3ad2ant3 
 |-  ( ( ( p e. Prime /\ p || ( K - 1 ) ) /\ ( K e. NN0 /\ 2 < K ) /\ ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ G RegUSGraph K ) ) -> ( G RegUSGraph K /\ G e. FriendGraph ) )
31 pm3.22 
 |-  ( ( V e. Fin /\ V =/= (/) ) -> ( V =/= (/) /\ V e. Fin ) )
32 31 3adant1 
 |-  ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) -> ( V =/= (/) /\ V e. Fin ) )
33 32 adantr 
 |-  ( ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ G RegUSGraph K ) -> ( V =/= (/) /\ V e. Fin ) )
34 33 3ad2ant3 
 |-  ( ( ( p e. Prime /\ p || ( K - 1 ) ) /\ ( K e. NN0 /\ 2 < K ) /\ ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ G RegUSGraph K ) ) -> ( V =/= (/) /\ V e. Fin ) )
35 simp1 
 |-  ( ( ( p e. Prime /\ p || ( K - 1 ) ) /\ ( K e. NN0 /\ 2 < K ) /\ ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ G RegUSGraph K ) ) -> ( p e. Prime /\ p || ( K - 1 ) ) )
36 1 numclwwlk7 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V =/= (/) /\ V e. Fin ) /\ ( p e. Prime /\ p || ( K - 1 ) ) ) -> ( ( # ` ( p ClWWalksN G ) ) mod p ) = 1 )
37 30 34 35 36 syl3anc 
 |-  ( ( ( p e. Prime /\ p || ( K - 1 ) ) /\ ( K e. NN0 /\ 2 < K ) /\ ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ G RegUSGraph K ) ) -> ( ( # ` ( p ClWWalksN G ) ) mod p ) = 1 )
38 eqeq1 
 |-  ( ( ( # ` ( p ClWWalksN G ) ) mod p ) = 0 -> ( ( ( # ` ( p ClWWalksN G ) ) mod p ) = 1 <-> 0 = 1 ) )
39 ax-1ne0 
 |-  1 =/= 0
40 39 nesymi 
 |-  -. 0 = 1
41 40 pm2.21i 
 |-  ( 0 = 1 -> K = 2 )
42 38 41 syl6bi 
 |-  ( ( ( # ` ( p ClWWalksN G ) ) mod p ) = 0 -> ( ( ( # ` ( p ClWWalksN G ) ) mod p ) = 1 -> K = 2 ) )
43 29 37 42 sylc 
 |-  ( ( ( p e. Prime /\ p || ( K - 1 ) ) /\ ( K e. NN0 /\ 2 < K ) /\ ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ G RegUSGraph K ) ) -> K = 2 )
44 43 a1d 
 |-  ( ( ( p e. Prime /\ p || ( K - 1 ) ) /\ ( K e. NN0 /\ 2 < K ) /\ ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ G RegUSGraph K ) ) -> ( 1 < K -> K = 2 ) )
45 44 3exp 
 |-  ( ( p e. Prime /\ p || ( K - 1 ) ) -> ( ( K e. NN0 /\ 2 < K ) -> ( ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ G RegUSGraph K ) -> ( 1 < K -> K = 2 ) ) ) )
46 45 rexlimiva 
 |-  ( E. p e. Prime p || ( K - 1 ) -> ( ( K e. NN0 /\ 2 < K ) -> ( ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ G RegUSGraph K ) -> ( 1 < K -> K = 2 ) ) ) )
47 22 46 mpcom 
 |-  ( ( K e. NN0 /\ 2 < K ) -> ( ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ G RegUSGraph K ) -> ( 1 < K -> K = 2 ) ) )
48 47 expcom 
 |-  ( 2 < K -> ( K e. NN0 -> ( ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ G RegUSGraph K ) -> ( 1 < K -> K = 2 ) ) ) )
49 48 com23 
 |-  ( 2 < K -> ( ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ G RegUSGraph K ) -> ( K e. NN0 -> ( 1 < K -> K = 2 ) ) ) )
50 1red 
 |-  ( K e. NN0 -> 1 e. RR )
51 nn0re 
 |-  ( K e. NN0 -> K e. RR )
52 50 51 ltnled 
 |-  ( K e. NN0 -> ( 1 < K <-> -. K <_ 1 ) )
53 1e2m1 
 |-  1 = ( 2 - 1 )
54 53 a1i 
 |-  ( K e. NN0 -> 1 = ( 2 - 1 ) )
55 54 breq2d 
 |-  ( K e. NN0 -> ( K <_ 1 <-> K <_ ( 2 - 1 ) ) )
56 55 notbid 
 |-  ( K e. NN0 -> ( -. K <_ 1 <-> -. K <_ ( 2 - 1 ) ) )
57 zltlem1 
 |-  ( ( K e. ZZ /\ 2 e. ZZ ) -> ( K < 2 <-> K <_ ( 2 - 1 ) ) )
58 12 10 57 sylancl 
 |-  ( K e. NN0 -> ( K < 2 <-> K <_ ( 2 - 1 ) ) )
59 58 bicomd 
 |-  ( K e. NN0 -> ( K <_ ( 2 - 1 ) <-> K < 2 ) )
60 59 notbid 
 |-  ( K e. NN0 -> ( -. K <_ ( 2 - 1 ) <-> -. K < 2 ) )
61 52 56 60 3bitrd 
 |-  ( K e. NN0 -> ( 1 < K <-> -. K < 2 ) )
62 2re 
 |-  2 e. RR
63 lttri3 
 |-  ( ( K e. RR /\ 2 e. RR ) -> ( K = 2 <-> ( -. K < 2 /\ -. 2 < K ) ) )
64 63 biimprd 
 |-  ( ( K e. RR /\ 2 e. RR ) -> ( ( -. K < 2 /\ -. 2 < K ) -> K = 2 ) )
65 51 62 64 sylancl 
 |-  ( K e. NN0 -> ( ( -. K < 2 /\ -. 2 < K ) -> K = 2 ) )
66 65 expd 
 |-  ( K e. NN0 -> ( -. K < 2 -> ( -. 2 < K -> K = 2 ) ) )
67 61 66 sylbid 
 |-  ( K e. NN0 -> ( 1 < K -> ( -. 2 < K -> K = 2 ) ) )
68 67 com3r 
 |-  ( -. 2 < K -> ( K e. NN0 -> ( 1 < K -> K = 2 ) ) )
69 68 a1d 
 |-  ( -. 2 < K -> ( ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ G RegUSGraph K ) -> ( K e. NN0 -> ( 1 < K -> K = 2 ) ) ) )
70 49 69 pm2.61i 
 |-  ( ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ G RegUSGraph K ) -> ( K e. NN0 -> ( 1 < K -> K = 2 ) ) )
71 9 70 mpd 
 |-  ( ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ G RegUSGraph K ) -> ( 1 < K -> K = 2 ) )
72 71 expimpd 
 |-  ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) -> ( ( G RegUSGraph K /\ 1 < K ) -> K = 2 ) )