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 e. FinUSGraph /\ P e. Prime ) -> ( ( # ` ( P ClWWalksN G ) ) mod P ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		prmnn	|- ( P e. Prime -> P e. NN )
2		clwwlkndivn	|- ( ( G e. FinUSGraph /\ P e. Prime ) -> P || ( # ` ( P ClWWalksN G ) ) )
3		dvdsmod0	|- ( ( P e. NN /\ P || ( # ` ( P ClWWalksN G ) ) ) -> ( ( # ` ( P ClWWalksN G ) ) mod P ) = 0 )
4	1 2 3	syl2an2	|- ( ( G e. FinUSGraph /\ P e. Prime ) -> ( ( # ` ( P ClWWalksN G ) ) mod P ) = 0 )