Theorem clwlksndivn

Description: The size of the set of closed walks of prime length N is divisible by N . 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". (Contributed by Alexander van der Vekens, 6-Jul-2018) (Revised by AV, 4-May-2021)

	Ref	Expression
Assertion	clwlksndivn	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ ) → 𝑁 ∥ ( ♯ ‘ { 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑐 ) ) = 𝑁 } ) )

Proof

Step	Hyp	Ref	Expression
1		clwwlkndivn	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ ) → 𝑁 ∥ ( ♯ ‘ ( 𝑁 ClWWalksN 𝐺 ) ) )
2		fusgrusgr	⊢ ( 𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph )
3		usgruspgr	⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ USPGraph )
4	2 3	syl	⊢ ( 𝐺 ∈ FinUSGraph → 𝐺 ∈ USPGraph )
5		prmnn	⊢ ( 𝑁 ∈ ℙ → 𝑁 ∈ ℕ )
6		clwlkssizeeq	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ ( 𝑁 ClWWalksN 𝐺 ) ) = ( ♯ ‘ { 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑐 ) ) = 𝑁 } ) )
7	4 5 6	syl2an	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ ) → ( ♯ ‘ ( 𝑁 ClWWalksN 𝐺 ) ) = ( ♯ ‘ { 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑐 ) ) = 𝑁 } ) )
8	1 7	breqtrd	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ ) → 𝑁 ∥ ( ♯ ‘ { 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑐 ) ) = 𝑁 } ) )