Metamath Proof Explorer

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 ⊢ G ∈ FinUSGraph ∧ N ∈ ℙ → N ∥ c ∈ ClWalks ⁡ G | 1 st ⁡ c = N

Proof

Step Hyp Ref Expression
1 clwwlkndivn ⊢ G ∈ FinUSGraph ∧ N ∈ ℙ → N ∥ N ClWWalksN G
2 fusgrusgr ⊢ G ∈ FinUSGraph → G ∈ USGraph
3 usgruspgr ⊢ G ∈ USGraph → G ∈ USHGraph
4 2 3 syl ⊢ G ∈ FinUSGraph → G ∈ USHGraph
5 prmnn ⊢ N ∈ ℙ → N ∈ ℕ
6 clwlkssizeeq ⊢ G ∈ USHGraph ∧ N ∈ ℕ → N ClWWalksN G = c ∈ ClWalks ⁡ G | 1 st ⁡ c = N
7 4 5 6 syl2an ⊢ G ∈ FinUSGraph ∧ N ∈ ℙ → N ClWWalksN G = c ∈ ClWalks ⁡ G | 1 st ⁡ c = N
8 1 7 breqtrd ⊢ G ∈ FinUSGraph ∧ N ∈ ℙ → N ∥ c ∈ ClWalks ⁡ G | 1 st ⁡ c = N