Theorem numclwwlk8

Description: The size of the set of closed walks of length P , P prime, is divisible by P . This corresponds to statement 9 in Huneke p. 2: "It follows that, if p is a prime number, then the number of closed walks of length p is divisible by p", see also clwlksndivn . (Contributed by Alexander van der Vekens, 7-Oct-2018) (Revised by AV, 3-Jun-2021) (Proof shortened by AV, 2-Mar-2022)

	Ref	Expression
Assertion	numclwwlk8	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑃 ∈ ℙ ) → ( ( ♯ ‘ ( 𝑃 ClWWalksN 𝐺 ) ) mod 𝑃 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
2		clwwlkndivn	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑃 ∈ ℙ ) → 𝑃 ∥ ( ♯ ‘ ( 𝑃 ClWWalksN 𝐺 ) ) )
3		dvdsmod0	⊢ ( ( 𝑃 ∈ ℕ ∧ 𝑃 ∥ ( ♯ ‘ ( 𝑃 ClWWalksN 𝐺 ) ) ) → ( ( ♯ ‘ ( 𝑃 ClWWalksN 𝐺 ) ) mod 𝑃 ) = 0 )
4	1 2 3	syl2an2	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑃 ∈ ℙ ) → ( ( ♯ ‘ ( 𝑃 ClWWalksN 𝐺 ) ) mod 𝑃 ) = 0 )