numclwwlk7

Description: Statement 14 in Huneke p. 2: "The total number of closed walks of length p [in a friendship graph] is (k(k-1)+1)f(p)=1 (mod p)", since the number of vertices in a friendship graph is (k(k-1)+1), see frrusgrord0 or frrusgrord , and p divides (k-1), i.e., (k-1) mod p = 0 => k(k-1) mod p = 0 => k(k-1)+1 mod p = 1. Since the null graph is a friendship graph, see frgr0 , as well as k-regular (for any k), see 0vtxrgr , but has no closed walk, see 0clwlk0 , this theorem would be false for a null graph: ( ( #( P ClWWalksN G ) ) mod P ) = 0 =/= 1 , so this case must be excluded (by assuming V =/= (/) ). (Contributed by Alexander van der Vekens, 1-Sep-2018) (Revised by AV, 3-Jun-2021)

		Ref	Expression
	Hypothesis	numclwwlk6.v	$⊢ V = Vtx (G)$
	Assertion	numclwwlk7	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \neq \emptyset \land V \in Fin) \land (P \in ℙ \land P ∥ (K - 1))) \to \|P ClWWalksN G\| \mod P = 1$

Proof

Step	Hyp	Ref	Expression
1		numclwwlk6.v	$⊢ V = Vtx (G)$
2		simpll	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \neq \emptyset \land V \in Fin)) \to G RegUSGraph K$
3		simplr	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \neq \emptyset \land V \in Fin)) \to G \in FriendGraph$
4		simprr	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \neq \emptyset \land V \in Fin)) \to V \in Fin$
5	2 3 4	3jca	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \neq \emptyset \land V \in Fin)) \to (G RegUSGraph K \land G \in FriendGraph \land V \in Fin)$
6	1	numclwwlk6	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (P \in ℙ \land P ∥ (K - 1))) \to \|P ClWWalksN G\| \mod P = \|V\| \mod P$
7	5 6	stoic3	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \neq \emptyset \land V \in Fin) \land (P \in ℙ \land P ∥ (K - 1))) \to \|P ClWWalksN G\| \mod P = \|V\| \mod P$
8		simp2	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \neq \emptyset \land V \in Fin) \land (P \in ℙ \land P ∥ (K - 1))) \to (V \neq \emptyset \land V \in Fin)$
9	8	ancomd	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \neq \emptyset \land V \in Fin) \land (P \in ℙ \land P ∥ (K - 1))) \to (V \in Fin \land V \neq \emptyset)$
10		simp1	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \neq \emptyset \land V \in Fin) \land (P \in ℙ \land P ∥ (K - 1))) \to (G RegUSGraph K \land G \in FriendGraph)$
11	10	ancomd	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \neq \emptyset \land V \in Fin) \land (P \in ℙ \land P ∥ (K - 1))) \to (G \in FriendGraph \land G RegUSGraph K)$
12	1	frrusgrord	$⊢ (V \in Fin \land V \neq \emptyset) \to ((G \in FriendGraph \land G RegUSGraph K) \to \|V\| = K (K - 1) + 1)$
13	9 11 12	sylc	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \neq \emptyset \land V \in Fin) \land (P \in ℙ \land P ∥ (K - 1))) \to \|V\| = K (K - 1) + 1$
14	13	oveq1d	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \neq \emptyset \land V \in Fin) \land (P \in ℙ \land P ∥ (K - 1))) \to \|V\| \mod P = (K (K - 1) + 1) \mod P$
15	1	numclwwlk7lem	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \neq \emptyset \land V \in Fin)) \to K \in ℕ_{0}$
16		nn0cn	$⊢ K \in ℕ_{0} \to K \in ℂ$
17		peano2cnm	$⊢ K \in ℂ \to K - 1 \in ℂ$
18	16 17	syl	$⊢ K \in ℕ_{0} \to K - 1 \in ℂ$
19	16 18	mulcomd	$⊢ K \in ℕ_{0} \to K (K - 1) = (K - 1) K$
20	19	oveq1d	$⊢ K \in ℕ_{0} \to K (K - 1) \mod P = (K - 1) K \mod P$
21	20	adantr	$⊢ (K \in ℕ_{0} \land (P \in ℙ \land P ∥ (K - 1))) \to K (K - 1) \mod P = (K - 1) K \mod P$
22		prmnn	$⊢ P \in ℙ \to P \in ℕ$
23	22	ad2antrl	$⊢ (K \in ℕ_{0} \land (P \in ℙ \land P ∥ (K - 1))) \to P \in ℕ$
24		nn0z	$⊢ K \in ℕ_{0} \to K \in ℤ$
25		peano2zm	$⊢ K \in ℤ \to K - 1 \in ℤ$
26	24 25	syl	$⊢ K \in ℕ_{0} \to K - 1 \in ℤ$
27	26	adantr	$⊢ (K \in ℕ_{0} \land (P \in ℙ \land P ∥ (K - 1))) \to K - 1 \in ℤ$
28	24	adantr	$⊢ (K \in ℕ_{0} \land (P \in ℙ \land P ∥ (K - 1))) \to K \in ℤ$
29	23 27 28	3jca	$⊢ (K \in ℕ_{0} \land (P \in ℙ \land P ∥ (K - 1))) \to (P \in ℕ \land K - 1 \in ℤ \land K \in ℤ)$
30		simprr	$⊢ (K \in ℕ_{0} \land (P \in ℙ \land P ∥ (K - 1))) \to P ∥ (K - 1)$
31		mulmoddvds	$⊢ (P \in ℕ \land K - 1 \in ℤ \land K \in ℤ) \to (P ∥ (K - 1) \to (K - 1) K \mod P = 0)$
32	29 30 31	sylc	$⊢ (K \in ℕ_{0} \land (P \in ℙ \land P ∥ (K - 1))) \to (K - 1) K \mod P = 0$
33	21 32	eqtrd	$⊢ (K \in ℕ_{0} \land (P \in ℙ \land P ∥ (K - 1))) \to K (K - 1) \mod P = 0$
34	22	nnred	$⊢ P \in ℙ \to P \in ℝ$
35		prmgt1	$⊢ P \in ℙ \to 1 < P$
36	34 35	jca	$⊢ P \in ℙ \to (P \in ℝ \land 1 < P)$
37	36	ad2antrl	$⊢ (K \in ℕ_{0} \land (P \in ℙ \land P ∥ (K - 1))) \to (P \in ℝ \land 1 < P)$
38		1mod	$⊢ (P \in ℝ \land 1 < P) \to 1 \mod P = 1$
39	37 38	syl	$⊢ (K \in ℕ_{0} \land (P \in ℙ \land P ∥ (K - 1))) \to 1 \mod P = 1$
40	33 39	oveq12d	$⊢ (K \in ℕ_{0} \land (P \in ℙ \land P ∥ (K - 1))) \to (K (K - 1) \mod P) + (1 \mod P) = 0 + 1$
41	40	oveq1d	$⊢ (K \in ℕ_{0} \land (P \in ℙ \land P ∥ (K - 1))) \to ((K (K - 1) \mod P) + (1 \mod P)) \mod P = (0 + 1) \mod P$
42		nn0re	$⊢ K \in ℕ_{0} \to K \in ℝ$
43		peano2rem	$⊢ K \in ℝ \to K - 1 \in ℝ$
44	42 43	syl	$⊢ K \in ℕ_{0} \to K - 1 \in ℝ$
45	42 44	remulcld	$⊢ K \in ℕ_{0} \to K (K - 1) \in ℝ$
46	45	adantr	$⊢ (K \in ℕ_{0} \land (P \in ℙ \land P ∥ (K - 1))) \to K (K - 1) \in ℝ$
47		1red	$⊢ (K \in ℕ_{0} \land (P \in ℙ \land P ∥ (K - 1))) \to 1 \in ℝ$
48	22	nnrpd	$⊢ P \in ℙ \to P \in ℝ^{+}$
49	48	ad2antrl	$⊢ (K \in ℕ_{0} \land (P \in ℙ \land P ∥ (K - 1))) \to P \in ℝ^{+}$
50		modaddabs	$⊢ (K (K - 1) \in ℝ \land 1 \in ℝ \land P \in ℝ^{+}) \to ((K (K - 1) \mod P) + (1 \mod P)) \mod P = (K (K - 1) + 1) \mod P$
51	46 47 49 50	syl3anc	$⊢ (K \in ℕ_{0} \land (P \in ℙ \land P ∥ (K - 1))) \to ((K (K - 1) \mod P) + (1 \mod P)) \mod P = (K (K - 1) + 1) \mod P$
52		0p1e1	$⊢ 0 + 1 = 1$
53	52	oveq1i	$⊢ (0 + 1) \mod P = 1 \mod P$
54	34 35 38	syl2anc	$⊢ P \in ℙ \to 1 \mod P = 1$
55	54	ad2antrl	$⊢ (K \in ℕ_{0} \land (P \in ℙ \land P ∥ (K - 1))) \to 1 \mod P = 1$
56	53 55	eqtrid	$⊢ (K \in ℕ_{0} \land (P \in ℙ \land P ∥ (K - 1))) \to (0 + 1) \mod P = 1$
57	41 51 56	3eqtr3d	$⊢ (K \in ℕ_{0} \land (P \in ℙ \land P ∥ (K - 1))) \to (K (K - 1) + 1) \mod P = 1$
58	15 57	stoic3	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \neq \emptyset \land V \in Fin) \land (P \in ℙ \land P ∥ (K - 1))) \to (K (K - 1) + 1) \mod P = 1$
59	7 14 58	3eqtrd	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \neq \emptyset \land V \in Fin) \land (P \in ℙ \land P ∥ (K - 1))) \to \|P ClWWalksN G\| \mod P = 1$

Metamath Proof Explorer

Theorem numclwwlk7

Proof