Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
2 |
1
|
fusgrvtxfi |
|- ( G e. FinUSGraph -> ( Vtx ` G ) e. Fin ) |
3 |
2
|
adantr |
|- ( ( G e. FinUSGraph /\ N e. Prime ) -> ( Vtx ` G ) e. Fin ) |
4 |
|
eqid |
|- ( N ClWWalksN G ) = ( N ClWWalksN G ) |
5 |
|
eqid |
|- { <. t , u >. | ( t e. ( N ClWWalksN G ) /\ u e. ( N ClWWalksN G ) /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) } = { <. t , u >. | ( t e. ( N ClWWalksN G ) /\ u e. ( N ClWWalksN G ) /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) } |
6 |
4 5
|
qerclwwlknfi |
|- ( ( Vtx ` G ) e. Fin -> ( ( N ClWWalksN G ) /. { <. t , u >. | ( t e. ( N ClWWalksN G ) /\ u e. ( N ClWWalksN G ) /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) } ) e. Fin ) |
7 |
|
hashcl |
|- ( ( ( N ClWWalksN G ) /. { <. t , u >. | ( t e. ( N ClWWalksN G ) /\ u e. ( N ClWWalksN G ) /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) } ) e. Fin -> ( # ` ( ( N ClWWalksN G ) /. { <. t , u >. | ( t e. ( N ClWWalksN G ) /\ u e. ( N ClWWalksN G ) /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) } ) ) e. NN0 ) |
8 |
3 6 7
|
3syl |
|- ( ( G e. FinUSGraph /\ N e. Prime ) -> ( # ` ( ( N ClWWalksN G ) /. { <. t , u >. | ( t e. ( N ClWWalksN G ) /\ u e. ( N ClWWalksN G ) /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) } ) ) e. NN0 ) |
9 |
8
|
nn0zd |
|- ( ( G e. FinUSGraph /\ N e. Prime ) -> ( # ` ( ( N ClWWalksN G ) /. { <. t , u >. | ( t e. ( N ClWWalksN G ) /\ u e. ( N ClWWalksN G ) /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) } ) ) e. ZZ ) |
10 |
|
prmz |
|- ( N e. Prime -> N e. ZZ ) |
11 |
10
|
adantl |
|- ( ( G e. FinUSGraph /\ N e. Prime ) -> N e. ZZ ) |
12 |
|
dvdsmul2 |
|- ( ( ( # ` ( ( N ClWWalksN G ) /. { <. t , u >. | ( t e. ( N ClWWalksN G ) /\ u e. ( N ClWWalksN G ) /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) } ) ) e. ZZ /\ N e. ZZ ) -> N || ( ( # ` ( ( N ClWWalksN G ) /. { <. t , u >. | ( t e. ( N ClWWalksN G ) /\ u e. ( N ClWWalksN G ) /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) } ) ) x. N ) ) |
13 |
9 11 12
|
syl2anc |
|- ( ( G e. FinUSGraph /\ N e. Prime ) -> N || ( ( # ` ( ( N ClWWalksN G ) /. { <. t , u >. | ( t e. ( N ClWWalksN G ) /\ u e. ( N ClWWalksN G ) /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) } ) ) x. N ) ) |
14 |
4 5
|
fusgrhashclwwlkn |
|- ( ( G e. FinUSGraph /\ N e. Prime ) -> ( # ` ( N ClWWalksN G ) ) = ( ( # ` ( ( N ClWWalksN G ) /. { <. t , u >. | ( t e. ( N ClWWalksN G ) /\ u e. ( N ClWWalksN G ) /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) } ) ) x. N ) ) |
15 |
13 14
|
breqtrrd |
|- ( ( G e. FinUSGraph /\ N e. Prime ) -> N || ( # ` ( N ClWWalksN G ) ) ) |