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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	numclwwlk7	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ( ♯ ‘ ( 𝑃 ClWWalksN 𝐺 ) ) mod 𝑃 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		numclwwlk6.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		simpll	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ) → 𝐺 RegUSGraph 𝐾 )
3		simplr	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ) → 𝐺 ∈ FriendGraph )
4		simprr	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ) → 𝑉 ∈ Fin )
5	2 3 4	3jca	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ) → ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) )
6	1	numclwwlk6	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ( ♯ ‘ ( 𝑃 ClWWalksN 𝐺 ) ) mod 𝑃 ) = ( ( ♯ ‘ 𝑉 ) mod 𝑃 ) )
7	5 6	stoic3	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ( ♯ ‘ ( 𝑃 ClWWalksN 𝐺 ) ) mod 𝑃 ) = ( ( ♯ ‘ 𝑉 ) mod 𝑃 ) )
8		simp2	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) )
9	8	ancomd	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) )
10		simp1	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) )
11	10	ancomd	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) )
12	1	frrusgrord	⊢ ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) → ( ♯ ‘ 𝑉 ) = ( ( 𝐾 · ( 𝐾 − 1 ) ) + 1 ) ) )
13	9 11 12	sylc	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ♯ ‘ 𝑉 ) = ( ( 𝐾 · ( 𝐾 − 1 ) ) + 1 ) )
14	13	oveq1d	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ( ♯ ‘ 𝑉 ) mod 𝑃 ) = ( ( ( 𝐾 · ( 𝐾 − 1 ) ) + 1 ) mod 𝑃 ) )
15	1	numclwwlk7lem	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ) → 𝐾 ∈ ℕ0 )
16		nn0cn	⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℂ )
17		peano2cnm	⊢ ( 𝐾 ∈ ℂ → ( 𝐾 − 1 ) ∈ ℂ )
18	16 17	syl	⊢ ( 𝐾 ∈ ℕ0 → ( 𝐾 − 1 ) ∈ ℂ )
19	16 18	mulcomd	⊢ ( 𝐾 ∈ ℕ0 → ( 𝐾 · ( 𝐾 − 1 ) ) = ( ( 𝐾 − 1 ) · 𝐾 ) )
20	19	oveq1d	⊢ ( 𝐾 ∈ ℕ0 → ( ( 𝐾 · ( 𝐾 − 1 ) ) mod 𝑃 ) = ( ( ( 𝐾 − 1 ) · 𝐾 ) mod 𝑃 ) )
21	20	adantr	⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ( 𝐾 · ( 𝐾 − 1 ) ) mod 𝑃 ) = ( ( ( 𝐾 − 1 ) · 𝐾 ) mod 𝑃 ) )
22		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
23	22	ad2antrl	⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → 𝑃 ∈ ℕ )
24		nn0z	⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℤ )
25		peano2zm	⊢ ( 𝐾 ∈ ℤ → ( 𝐾 − 1 ) ∈ ℤ )
26	24 25	syl	⊢ ( 𝐾 ∈ ℕ0 → ( 𝐾 − 1 ) ∈ ℤ )
27	26	adantr	⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( 𝐾 − 1 ) ∈ ℤ )
28	24	adantr	⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → 𝐾 ∈ ℤ )
29	23 27 28	3jca	⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( 𝑃 ∈ ℕ ∧ ( 𝐾 − 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) )
30		simprr	⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → 𝑃 ∥ ( 𝐾 − 1 ) )
31		mulmoddvds	⊢ ( ( 𝑃 ∈ ℕ ∧ ( 𝐾 − 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑃 ∥ ( 𝐾 − 1 ) → ( ( ( 𝐾 − 1 ) · 𝐾 ) mod 𝑃 ) = 0 ) )
32	29 30 31	sylc	⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ( ( 𝐾 − 1 ) · 𝐾 ) mod 𝑃 ) = 0 )
33	21 32	eqtrd	⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ( 𝐾 · ( 𝐾 − 1 ) ) mod 𝑃 ) = 0 )
34	22	nnred	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℝ )
35		prmgt1	⊢ ( 𝑃 ∈ ℙ → 1 < 𝑃 )
36	34 35	jca	⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ∈ ℝ ∧ 1 < 𝑃 ) )
37	36	ad2antrl	⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( 𝑃 ∈ ℝ ∧ 1 < 𝑃 ) )
38		1mod	⊢ ( ( 𝑃 ∈ ℝ ∧ 1 < 𝑃 ) → ( 1 mod 𝑃 ) = 1 )
39	37 38	syl	⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( 1 mod 𝑃 ) = 1 )
40	33 39	oveq12d	⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ( ( 𝐾 · ( 𝐾 − 1 ) ) mod 𝑃 ) + ( 1 mod 𝑃 ) ) = ( 0 + 1 ) )
41	40	oveq1d	⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ( ( ( 𝐾 · ( 𝐾 − 1 ) ) mod 𝑃 ) + ( 1 mod 𝑃 ) ) mod 𝑃 ) = ( ( 0 + 1 ) mod 𝑃 ) )
42		nn0re	⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℝ )
43		peano2rem	⊢ ( 𝐾 ∈ ℝ → ( 𝐾 − 1 ) ∈ ℝ )
44	42 43	syl	⊢ ( 𝐾 ∈ ℕ0 → ( 𝐾 − 1 ) ∈ ℝ )
45	42 44	remulcld	⊢ ( 𝐾 ∈ ℕ0 → ( 𝐾 · ( 𝐾 − 1 ) ) ∈ ℝ )
46	45	adantr	⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( 𝐾 · ( 𝐾 − 1 ) ) ∈ ℝ )
47		1red	⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → 1 ∈ ℝ )
48	22	nnrpd	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℝ+ )
49	48	ad2antrl	⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → 𝑃 ∈ ℝ+ )
50		modaddabs	⊢ ( ( ( 𝐾 · ( 𝐾 − 1 ) ) ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) → ( ( ( ( 𝐾 · ( 𝐾 − 1 ) ) mod 𝑃 ) + ( 1 mod 𝑃 ) ) mod 𝑃 ) = ( ( ( 𝐾 · ( 𝐾 − 1 ) ) + 1 ) mod 𝑃 ) )
51	46 47 49 50	syl3anc	⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ( ( ( 𝐾 · ( 𝐾 − 1 ) ) mod 𝑃 ) + ( 1 mod 𝑃 ) ) mod 𝑃 ) = ( ( ( 𝐾 · ( 𝐾 − 1 ) ) + 1 ) mod 𝑃 ) )
52		0p1e1	⊢ ( 0 + 1 ) = 1
53	52	oveq1i	⊢ ( ( 0 + 1 ) mod 𝑃 ) = ( 1 mod 𝑃 )
54	34 35 38	syl2anc	⊢ ( 𝑃 ∈ ℙ → ( 1 mod 𝑃 ) = 1 )
55	54	ad2antrl	⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( 1 mod 𝑃 ) = 1 )
56	53 55	eqtrid	⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ( 0 + 1 ) mod 𝑃 ) = 1 )
57	41 51 56	3eqtr3d	⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ( ( 𝐾 · ( 𝐾 − 1 ) ) + 1 ) mod 𝑃 ) = 1 )
58	15 57	stoic3	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ( ( 𝐾 · ( 𝐾 − 1 ) ) + 1 ) mod 𝑃 ) = 1 )
59	7 14 58	3eqtrd	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ( ♯ ‘ ( 𝑃 ClWWalksN 𝐺 ) ) mod 𝑃 ) = 1 )