# 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 ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
Assertion numclwwlk5 ${⊢}\left(\left({G}\mathrm{RegUSGraph}{K}\wedge {G}\in \mathrm{FriendGraph}\wedge {V}\in \mathrm{Fin}\right)\wedge \left({X}\in {V}\wedge {P}\in ℙ\wedge {P}\parallel \left({K}-1\right)\right)\right)\to \left|{X}\mathrm{ClWWalksNOn}\left({G}\right){P}\right|\mathrm{mod}{P}=1$

### Proof

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