Metamath Proof Explorer

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 syl5eq ⊢ ( 𝑃 ∈ ℙ → ( ( 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 )