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 \in FinUSGraph \land N \in ℙ) \to N ∥ \|\{c \in ClWalks (G) \| \|1^{st} (c)\| = N\}\|$

Proof

Step	Hyp	Ref	Expression
1		clwwlkndivn	$⊢ (G \in FinUSGraph \land N \in ℙ) \to N ∥ \|N ClWWalksN G\|$
2		fusgrusgr	$⊢ G \in FinUSGraph \to G \in USGraph$
3		usgruspgr	$⊢ G \in USGraph \to G \in USHGraph$
4	2 3	syl	$⊢ G \in FinUSGraph \to G \in USHGraph$
5		prmnn	$⊢ N \in ℙ \to N \in ℕ$
6		clwlkssizeeq	$⊢ (G \in USHGraph \land N \in ℕ) \to \|N ClWWalksN G\| = \|\{c \in ClWalks (G) \| \|1^{st} (c)\| = N\}\|$
7	4 5 6	syl2an	$⊢ (G \in FinUSGraph \land N \in ℙ) \to \|N ClWWalksN G\| = \|\{c \in ClWalks (G) \| \|1^{st} (c)\| = N\}\|$
8	1 7	breqtrd	$⊢ (G \in FinUSGraph \land N \in ℙ) \to N ∥ \|\{c \in ClWalks (G) \| \|1^{st} (c)\| = N\}\|$

Metamath Proof Explorer

Theorem clwlksndivn

Proof