Theorem 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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	numclwwlk5	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑃 ) ) mod 𝑃 ) = 1 )

Proof

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