Metamath Proof Explorer

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 ⊢ G ∈ FinUSGraph ∧ P ∈ ℙ → P ClWWalksN G mod P = 0

Proof

Step Hyp Ref Expression
1 prmnn ⊢ P ∈ ℙ → P ∈ ℕ
2 clwwlkndivn ⊢ G ∈ FinUSGraph ∧ P ∈ ℙ → P ∥ P ClWWalksN G
3 dvdsmod0 ⊢ P ∈ ℕ ∧ P ∥ P ClWWalksN G → P ClWWalksN G mod P = 0
4 1 2 3 syl2an2 ⊢ G ∈ FinUSGraph ∧ P ∈ ℙ → P ClWWalksN G mod P = 0