numclwwlk5

Description: Statement 13 in Huneke p. 2: "Let p be a prime divisor of k-1; then f(p) = 1 (mod p) [for each vertex v]". (Contributed by Alexander van der Vekens, 7-Oct-2018) (Revised by AV, 2-Jun-2021) (Revised by AV, 7-Mar-2022)

		Ref	Expression
	Hypothesis	numclwwlk3.v	$⊢ V = Vtx (G)$
	Assertion	numclwwlk5	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1))) \to \|X ClWWalksNOn (G) P\| \mod P = 1$

Proof

Step	Hyp	Ref	Expression
1		numclwwlk3.v	$⊢ V = Vtx (G)$
2		simpl1	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land 2 \in ℙ \land 2 ∥ (K - 1))) \to G RegUSGraph K$
3		simpr1	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land 2 \in ℙ \land 2 ∥ (K - 1))) \to X \in V$
4	1	finrusgrfusgr	$⊢ (G RegUSGraph K \land V \in Fin) \to G \in FinUSGraph$
5	4	3adant2	$⊢ (G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \to G \in FinUSGraph$
6	5	adantl	$⊢ (X \in V \land (G RegUSGraph K \land G \in FriendGraph \land V \in Fin)) \to G \in FinUSGraph$
7		simpr1	$⊢ (X \in V \land (G RegUSGraph K \land G \in FriendGraph \land V \in Fin)) \to G RegUSGraph K$
8		ne0i	$⊢ X \in V \to V \neq \emptyset$
9	8	adantr	$⊢ (X \in V \land (G RegUSGraph K \land G \in FriendGraph \land V \in Fin)) \to V \neq \emptyset$
10	1	frusgrnn0	$⊢ (G \in FinUSGraph \land G RegUSGraph K \land V \neq \emptyset) \to K \in ℕ_{0}$
11	6 7 9 10	syl3anc	$⊢ (X \in V \land (G RegUSGraph K \land G \in FriendGraph \land V \in Fin)) \to K \in ℕ_{0}$
12	11	ex	$⊢ X \in V \to ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \to K \in ℕ_{0})$
13	12	3ad2ant1	$⊢ (X \in V \land 2 \in ℙ \land 2 ∥ (K - 1)) \to ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \to K \in ℕ_{0})$
14	13	impcom	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land 2 \in ℙ \land 2 ∥ (K - 1))) \to K \in ℕ_{0}$
15	2 3 14	3jca	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land 2 \in ℙ \land 2 ∥ (K - 1))) \to (G RegUSGraph K \land X \in V \land K \in ℕ_{0})$
16		simpr3	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land 2 \in ℙ \land 2 ∥ (K - 1))) \to 2 ∥ (K - 1)$
17	1	numclwwlk5lem	$⊢ (G RegUSGraph K \land X \in V \land K \in ℕ_{0}) \to (2 ∥ (K - 1) \to \|X ClWWalksNOn (G) 2\| \mod 2 = 1)$
18	15 16 17	sylc	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land 2 \in ℙ \land 2 ∥ (K - 1))) \to \|X ClWWalksNOn (G) 2\| \mod 2 = 1$
19	18	a1i	$⊢ P = 2 \to (((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land 2 \in ℙ \land 2 ∥ (K - 1))) \to \|X ClWWalksNOn (G) 2\| \mod 2 = 1)$
20		eleq1	$⊢ P = 2 \to (P \in ℙ \leftrightarrow 2 \in ℙ)$
21		breq1	$⊢ P = 2 \to (P ∥ (K - 1) \leftrightarrow 2 ∥ (K - 1))$
22	20 21	3anbi23d	$⊢ P = 2 \to ((X \in V \land P \in ℙ \land P ∥ (K - 1)) \leftrightarrow (X \in V \land 2 \in ℙ \land 2 ∥ (K - 1)))$
23	22	anbi2d	$⊢ P = 2 \to (((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1))) \leftrightarrow ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land 2 \in ℙ \land 2 ∥ (K - 1))))$
24		oveq2	$⊢ P = 2 \to X ClWWalksNOn (G) P = X ClWWalksNOn (G) 2$
25	24	fveq2d	$⊢ P = 2 \to \|X ClWWalksNOn (G) P\| = \|X ClWWalksNOn (G) 2\|$
26		id	$⊢ P = 2 \to P = 2$
27	25 26	oveq12d	$⊢ P = 2 \to \|X ClWWalksNOn (G) P\| \mod P = \|X ClWWalksNOn (G) 2\| \mod 2$
28	27	eqeq1d	$⊢ P = 2 \to (\|X ClWWalksNOn (G) P\| \mod P = 1 \leftrightarrow \|X ClWWalksNOn (G) 2\| \mod 2 = 1)$
29	19 23 28	3imtr4d	$⊢ P = 2 \to (((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1))) \to \|X ClWWalksNOn (G) P\| \mod P = 1)$
30		3simpa	$⊢ (G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \to (G RegUSGraph K \land G \in FriendGraph)$
31	30	adantr	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1))) \to (G RegUSGraph K \land G \in FriendGraph)$
32	31	adantl	$⊢ (P \neq 2 \land ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1)))) \to (G RegUSGraph K \land G \in FriendGraph)$
33		simprl3	$⊢ (P \neq 2 \land ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1)))) \to V \in Fin$
34		simprr1	$⊢ (P \neq 2 \land ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1)))) \to X \in V$
35		eldifsn	$⊢ P \in (ℙ ∖ \{2\}) \leftrightarrow (P \in ℙ \land P \neq 2)$
36		oddprmge3	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℤ_{\geq 3}$
37	35 36	sylbir	$⊢ (P \in ℙ \land P \neq 2) \to P \in ℤ_{\geq 3}$
38	37	ex	$⊢ P \in ℙ \to (P \neq 2 \to P \in ℤ_{\geq 3})$
39	38	3ad2ant2	$⊢ (X \in V \land P \in ℙ \land P ∥ (K - 1)) \to (P \neq 2 \to P \in ℤ_{\geq 3})$
40	39	adantl	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1))) \to (P \neq 2 \to P \in ℤ_{\geq 3})$
41	40	impcom	$⊢ (P \neq 2 \land ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1)))) \to P \in ℤ_{\geq 3}$
42	1	numclwwlk3	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \in Fin \land X \in V \land P \in ℤ_{\geq 3})) \to \|X ClWWalksNOn (G) P\| = (K - 1) \|X ClWWalksNOn (G) (P - 2)\| + K^{P - 2}$
43	32 33 34 41 42	syl13anc	$⊢ (P \neq 2 \land ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1)))) \to \|X ClWWalksNOn (G) P\| = (K - 1) \|X ClWWalksNOn (G) (P - 2)\| + K^{P - 2}$
44	43	oveq1d	$⊢ (P \neq 2 \land ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1)))) \to \|X ClWWalksNOn (G) P\| \mod P = ((K - 1) \|X ClWWalksNOn (G) (P - 2)\| + K^{P - 2}) \mod P$
45	12	3ad2ant1	$⊢ (X \in V \land P \in ℙ \land P ∥ (K - 1)) \to ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \to K \in ℕ_{0})$
46	45	impcom	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1))) \to K \in ℕ_{0}$
47	46	nn0zd	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1))) \to K \in ℤ$
48		peano2zm	$⊢ K \in ℤ \to K - 1 \in ℤ$
49		zre	$⊢ K - 1 \in ℤ \to K - 1 \in ℝ$
50	47 48 49	3syl	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1))) \to K - 1 \in ℝ$
51		simpl3	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1))) \to V \in Fin$
52	1	clwwlknonfin	$⊢ V \in Fin \to X ClWWalksNOn (G) (P - 2) \in Fin$
53		hashcl	$⊢ X ClWWalksNOn (G) (P - 2) \in Fin \to \|X ClWWalksNOn (G) (P - 2)\| \in ℕ_{0}$
54	51 52 53	3syl	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1))) \to \|X ClWWalksNOn (G) (P - 2)\| \in ℕ_{0}$
55	54	nn0red	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1))) \to \|X ClWWalksNOn (G) (P - 2)\| \in ℝ$
56	50 55	remulcld	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1))) \to (K - 1) \|X ClWWalksNOn (G) (P - 2)\| \in ℝ$
57	46	nn0red	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1))) \to K \in ℝ$
58		prmm2nn0	$⊢ P \in ℙ \to P - 2 \in ℕ_{0}$
59	58	3ad2ant2	$⊢ (X \in V \land P \in ℙ \land P ∥ (K - 1)) \to P - 2 \in ℕ_{0}$
60	59	adantl	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1))) \to P - 2 \in ℕ_{0}$
61	57 60	reexpcld	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1))) \to K^{P - 2} \in ℝ$
62		prmnn	$⊢ P \in ℙ \to P \in ℕ$
63	62	nnrpd	$⊢ P \in ℙ \to P \in ℝ^{+}$
64	63	3ad2ant2	$⊢ (X \in V \land P \in ℙ \land P ∥ (K - 1)) \to P \in ℝ^{+}$
65	64	adantl	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1))) \to P \in ℝ^{+}$
66	56 61 65	3jca	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1))) \to ((K - 1) \|X ClWWalksNOn (G) (P - 2)\| \in ℝ \land K^{P - 2} \in ℝ \land P \in ℝ^{+})$
67	66	adantl	$⊢ (P \neq 2 \land ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1)))) \to ((K - 1) \|X ClWWalksNOn (G) (P - 2)\| \in ℝ \land K^{P - 2} \in ℝ \land P \in ℝ^{+})$
68		modaddabs	$⊢ ((K - 1) \|X ClWWalksNOn (G) (P - 2)\| \in ℝ \land K^{P - 2} \in ℝ \land P \in ℝ^{+}) \to (((K - 1) \|X ClWWalksNOn (G) (P - 2)\| \mod P) + (K^{P - 2} \mod P)) \mod P = ((K - 1) \|X ClWWalksNOn (G) (P - 2)\| + K^{P - 2}) \mod P$
69	68	eqcomd	$⊢ ((K - 1) \|X ClWWalksNOn (G) (P - 2)\| \in ℝ \land K^{P - 2} \in ℝ \land P \in ℝ^{+}) \to ((K - 1) \|X ClWWalksNOn (G) (P - 2)\| + K^{P - 2}) \mod P = (((K - 1) \|X ClWWalksNOn (G) (P - 2)\| \mod P) + (K^{P - 2} \mod P)) \mod P$
70	67 69	syl	$⊢ (P \neq 2 \land ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1)))) \to ((K - 1) \|X ClWWalksNOn (G) (P - 2)\| + K^{P - 2}) \mod P = (((K - 1) \|X ClWWalksNOn (G) (P - 2)\| \mod P) + (K^{P - 2} \mod P)) \mod P$
71	62	3ad2ant2	$⊢ (X \in V \land P \in ℙ \land P ∥ (K - 1)) \to P \in ℕ$
72	71	adantl	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1))) \to P \in ℕ$
73		nn0z	$⊢ K \in ℕ_{0} \to K \in ℤ$
74	46 73 48	3syl	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1))) \to K - 1 \in ℤ$
75	54	nn0zd	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1))) \to \|X ClWWalksNOn (G) (P - 2)\| \in ℤ$
76	72 74 75	3jca	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1))) \to (P \in ℕ \land K - 1 \in ℤ \land \|X ClWWalksNOn (G) (P - 2)\| \in ℤ)$
77		simpr3	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1))) \to P ∥ (K - 1)$
78		mulmoddvds	$⊢ (P \in ℕ \land K - 1 \in ℤ \land \|X ClWWalksNOn (G) (P - 2)\| \in ℤ) \to (P ∥ (K - 1) \to (K - 1) \|X ClWWalksNOn (G) (P - 2)\| \mod P = 0)$
79	76 77 78	sylc	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1))) \to (K - 1) \|X ClWWalksNOn (G) (P - 2)\| \mod P = 0$
80		simpr2	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1))) \to P \in ℙ$
81	80 47	jca	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1))) \to (P \in ℙ \land K \in ℤ)$
82		powm2modprm	$⊢ (P \in ℙ \land K \in ℤ) \to (P ∥ (K - 1) \to K^{P - 2} \mod P = 1)$
83	81 77 82	sylc	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1))) \to K^{P - 2} \mod P = 1$
84	79 83	oveq12d	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1))) \to ((K - 1) \|X ClWWalksNOn (G) (P - 2)\| \mod P) + (K^{P - 2} \mod P) = 0 + 1$
85	84	oveq1d	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1))) \to (((K - 1) \|X ClWWalksNOn (G) (P - 2)\| \mod P) + (K^{P - 2} \mod P)) \mod P = (0 + 1) \mod P$
86		0p1e1	$⊢ 0 + 1 = 1$
87	86	oveq1i	$⊢ (0 + 1) \mod P = 1 \mod P$
88	62	nnred	$⊢ P \in ℙ \to P \in ℝ$
89		prmgt1	$⊢ P \in ℙ \to 1 < P$
90		1mod	$⊢ (P \in ℝ \land 1 < P) \to 1 \mod P = 1$
91	88 89 90	syl2anc	$⊢ P \in ℙ \to 1 \mod P = 1$
92	87 91	eqtrid	$⊢ P \in ℙ \to (0 + 1) \mod P = 1$
93	92	3ad2ant2	$⊢ (X \in V \land P \in ℙ \land P ∥ (K - 1)) \to (0 + 1) \mod P = 1$
94	93	adantl	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1))) \to (0 + 1) \mod P = 1$
95	85 94	eqtrd	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1))) \to (((K - 1) \|X ClWWalksNOn (G) (P - 2)\| \mod P) + (K^{P - 2} \mod P)) \mod P = 1$
96	95	adantl	$⊢ (P \neq 2 \land ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1)))) \to (((K - 1) \|X ClWWalksNOn (G) (P - 2)\| \mod P) + (K^{P - 2} \mod P)) \mod P = 1$
97	44 70 96	3eqtrd	$⊢ (P \neq 2 \land ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1)))) \to \|X ClWWalksNOn (G) P\| \mod P = 1$
98	97	ex	$⊢ P \neq 2 \to (((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1))) \to \|X ClWWalksNOn (G) P\| \mod P = 1)$
99	29 98	pm2.61ine	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (X \in V \land P \in ℙ \land P ∥ (K - 1))) \to \|X ClWWalksNOn (G) P\| \mod P = 1$

Metamath Proof Explorer

Theorem numclwwlk5

Proof