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 = ( Vtx ` G )
Assertion numclwwlk5 
|- ( ( ( G RegUSGraph K /\ G e. FriendGraph /\ V e. Fin ) /\ ( X e. V /\ P e. Prime /\ P || ( K - 1 ) ) ) -> ( ( # ` ( X ( ClWWalksNOn ` G ) P ) ) mod P ) = 1 )

Proof

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