This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. FinUSGraph /\ N e. Prime ) -> N || ( # ` { c e. ( ClWalks ` G ) | ( # ` ( 1st ` c ) ) = N } ) )

Proof

Step Hyp Ref Expression
1 clwwlkndivn 
 |-  ( ( G e. FinUSGraph /\ N e. Prime ) -> N || ( # ` ( N ClWWalksN G ) ) )
2 fusgrusgr 
 |-  ( G e. FinUSGraph -> G e. USGraph )
3 usgruspgr 
 |-  ( G e. USGraph -> G e. USPGraph )
4 2 3 syl 
 |-  ( G e. FinUSGraph -> G e. USPGraph )
5 prmnn 
 |-  ( N e. Prime -> N e. NN )
6 clwlkssizeeq 
 |-  ( ( G e. USPGraph /\ N e. NN ) -> ( # ` ( N ClWWalksN G ) ) = ( # ` { c e. ( ClWalks ` G ) | ( # ` ( 1st ` c ) ) = N } ) )
7 4 5 6 syl2an 
 |-  ( ( G e. FinUSGraph /\ N e. Prime ) -> ( # ` ( N ClWWalksN G ) ) = ( # ` { c e. ( ClWalks ` G ) | ( # ` ( 1st ` c ) ) = N } ) )
8 1 7 breqtrd 
 |-  ( ( G e. FinUSGraph /\ N e. Prime ) -> N || ( # ` { c e. ( ClWalks ` G ) | ( # ` ( 1st ` c ) ) = N } ) )