Theorem numclwwlk7

Description: Statement 14 in Huneke p. 2: "The total number of closed walks of length p [in a friendship graph] is (k(k-1)+1)f(p)=1 (mod p)", since the number of vertices in a friendship graph is (k(k-1)+1), see frrusgrord0 or frrusgrord , and p divides (k-1), i.e., (k-1) mod p = 0 => k(k-1) mod p = 0 => k(k-1)+1 mod p = 1. Since the null graph is a friendship graph, see frgr0 , as well as k-regular (for any k), see 0vtxrgr , but has no closed walk, see 0clwlk0 , this theorem would be false for a null graph: ( ( #( P ClWWalksN G ) ) mod P ) = 0 =/= 1 , so this case must be excluded (by assuming V =/= (/) ). (Contributed by Alexander van der Vekens, 1-Sep-2018) (Revised by AV, 3-Jun-2021)

	Ref	Expression
Hypothesis	numclwwlk6.v	|- V = ( Vtx ` G )
Assertion	numclwwlk7	|- ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V =/= (/) /\ V e. Fin ) /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( ( # ` ( P ClWWalksN G ) ) mod P ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		numclwwlk6.v	|- V = ( Vtx ` G )
2		simpll	|- ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V =/= (/) /\ V e. Fin ) ) -> G RegUSGraph K )
3		simplr	|- ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V =/= (/) /\ V e. Fin ) ) -> G e. FriendGraph )
4		simprr	|- ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V =/= (/) /\ V e. Fin ) ) -> V e. Fin )
5	2 3 4	3jca	|- ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V =/= (/) /\ V e. Fin ) ) -> ( G RegUSGraph K /\ G e. FriendGraph /\ V e. Fin ) )
6	1	numclwwlk6	|- ( ( ( G RegUSGraph K /\ G e. FriendGraph /\ V e. Fin ) /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( ( # ` ( P ClWWalksN G ) ) mod P ) = ( ( # ` V ) mod P ) )
7	5 6	stoic3	|- ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V =/= (/) /\ V e. Fin ) /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( ( # ` ( P ClWWalksN G ) ) mod P ) = ( ( # ` V ) mod P ) )
8		simp2	|- ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V =/= (/) /\ V e. Fin ) /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( V =/= (/) /\ V e. Fin ) )
9	8	ancomd	|- ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V =/= (/) /\ V e. Fin ) /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( V e. Fin /\ V =/= (/) ) )
10		simp1	|- ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V =/= (/) /\ V e. Fin ) /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( G RegUSGraph K /\ G e. FriendGraph ) )
11	10	ancomd	|- ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V =/= (/) /\ V e. Fin ) /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( G e. FriendGraph /\ G RegUSGraph K ) )
12	1	frrusgrord	|- ( ( V e. Fin /\ V =/= (/) ) -> ( ( G e. FriendGraph /\ G RegUSGraph K ) -> ( # ` V ) = ( ( K x. ( K - 1 ) ) + 1 ) ) )
13	9 11 12	sylc	|- ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V =/= (/) /\ V e. Fin ) /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( # ` V ) = ( ( K x. ( K - 1 ) ) + 1 ) )
14	13	oveq1d	|- ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V =/= (/) /\ V e. Fin ) /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( ( # ` V ) mod P ) = ( ( ( K x. ( K - 1 ) ) + 1 ) mod P ) )
15	1	numclwwlk7lem	|- ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V =/= (/) /\ V e. Fin ) ) -> K e. NN0 )
16		nn0cn	|- ( K e. NN0 -> K e. CC )
17		peano2cnm	|- ( K e. CC -> ( K - 1 ) e. CC )
18	16 17	syl	|- ( K e. NN0 -> ( K - 1 ) e. CC )
19	16 18	mulcomd	|- ( K e. NN0 -> ( K x. ( K - 1 ) ) = ( ( K - 1 ) x. K ) )
20	19	oveq1d	|- ( K e. NN0 -> ( ( K x. ( K - 1 ) ) mod P ) = ( ( ( K - 1 ) x. K ) mod P ) )
21	20	adantr	|- ( ( K e. NN0 /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( ( K x. ( K - 1 ) ) mod P ) = ( ( ( K - 1 ) x. K ) mod P ) )
22		prmnn	|- ( P e. Prime -> P e. NN )
23	22	ad2antrl	|- ( ( K e. NN0 /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> P e. NN )
24		nn0z	|- ( K e. NN0 -> K e. ZZ )
25		peano2zm	|- ( K e. ZZ -> ( K - 1 ) e. ZZ )
26	24 25	syl	|- ( K e. NN0 -> ( K - 1 ) e. ZZ )
27	26	adantr	|- ( ( K e. NN0 /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( K - 1 ) e. ZZ )
28	24	adantr	|- ( ( K e. NN0 /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> K e. ZZ )
29	23 27 28	3jca	|- ( ( K e. NN0 /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( P e. NN /\ ( K - 1 ) e. ZZ /\ K e. ZZ ) )
30		simprr	|- ( ( K e. NN0 /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> P || ( K - 1 ) )
31		mulmoddvds	|- ( ( P e. NN /\ ( K - 1 ) e. ZZ /\ K e. ZZ ) -> ( P || ( K - 1 ) -> ( ( ( K - 1 ) x. K ) mod P ) = 0 ) )
32	29 30 31	sylc	|- ( ( K e. NN0 /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( ( ( K - 1 ) x. K ) mod P ) = 0 )
33	21 32	eqtrd	|- ( ( K e. NN0 /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( ( K x. ( K - 1 ) ) mod P ) = 0 )
34	22	nnred	|- ( P e. Prime -> P e. RR )
35		prmgt1	|- ( P e. Prime -> 1 < P )
36	34 35	jca	|- ( P e. Prime -> ( P e. RR /\ 1 < P ) )
37	36	ad2antrl	|- ( ( K e. NN0 /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( P e. RR /\ 1 < P ) )
38		1mod	|- ( ( P e. RR /\ 1 < P ) -> ( 1 mod P ) = 1 )
39	37 38	syl	|- ( ( K e. NN0 /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( 1 mod P ) = 1 )
40	33 39	oveq12d	|- ( ( K e. NN0 /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( ( ( K x. ( K - 1 ) ) mod P ) + ( 1 mod P ) ) = ( 0 + 1 ) )
41	40	oveq1d	|- ( ( K e. NN0 /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( ( ( ( K x. ( K - 1 ) ) mod P ) + ( 1 mod P ) ) mod P ) = ( ( 0 + 1 ) mod P ) )
42		nn0re	|- ( K e. NN0 -> K e. RR )
43		peano2rem	|- ( K e. RR -> ( K - 1 ) e. RR )
44	42 43	syl	|- ( K e. NN0 -> ( K - 1 ) e. RR )
45	42 44	remulcld	|- ( K e. NN0 -> ( K x. ( K - 1 ) ) e. RR )
46	45	adantr	|- ( ( K e. NN0 /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( K x. ( K - 1 ) ) e. RR )
47		1red	|- ( ( K e. NN0 /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> 1 e. RR )
48	22	nnrpd	|- ( P e. Prime -> P e. RR+ )
49	48	ad2antrl	|- ( ( K e. NN0 /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> P e. RR+ )
50		modaddabs	|- ( ( ( K x. ( K - 1 ) ) e. RR /\ 1 e. RR /\ P e. RR+ ) -> ( ( ( ( K x. ( K - 1 ) ) mod P ) + ( 1 mod P ) ) mod P ) = ( ( ( K x. ( K - 1 ) ) + 1 ) mod P ) )
51	46 47 49 50	syl3anc	|- ( ( K e. NN0 /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( ( ( ( K x. ( K - 1 ) ) mod P ) + ( 1 mod P ) ) mod P ) = ( ( ( K x. ( K - 1 ) ) + 1 ) mod P ) )
52		0p1e1	|- ( 0 + 1 ) = 1
53	52	oveq1i	|- ( ( 0 + 1 ) mod P ) = ( 1 mod P )
54	34 35 38	syl2anc	|- ( P e. Prime -> ( 1 mod P ) = 1 )
55	54	ad2antrl	|- ( ( K e. NN0 /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( 1 mod P ) = 1 )
56	53 55	eqtrid	|- ( ( K e. NN0 /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( ( 0 + 1 ) mod P ) = 1 )
57	41 51 56	3eqtr3d	|- ( ( K e. NN0 /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( ( ( K x. ( K - 1 ) ) + 1 ) mod P ) = 1 )
58	15 57	stoic3	|- ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V =/= (/) /\ V e. Fin ) /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( ( ( K x. ( K - 1 ) ) + 1 ) mod P ) = 1 )
59	7 14 58	3eqtrd	|- ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V =/= (/) /\ V e. Fin ) /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( ( # ` ( P ClWWalksN G ) ) mod P ) = 1 )