Step |
Hyp |
Ref |
Expression |
1 |
|
clwwlkndivn |
|- ( ( G e. FinUSGraph /\ N e. Prime ) -> N || ( # ` ( N ClWWalksN G ) ) ) |
2 |
|
fusgrusgr |
|- ( G e. FinUSGraph -> G e. USGraph ) |
3 |
|
usgruspgr |
|- ( G e. USGraph -> G e. USPGraph ) |
4 |
2 3
|
syl |
|- ( G e. FinUSGraph -> G e. USPGraph ) |
5 |
|
prmnn |
|- ( N e. Prime -> N e. NN ) |
6 |
|
clwlkssizeeq |
|- ( ( G e. USPGraph /\ N e. NN ) -> ( # ` ( N ClWWalksN G ) ) = ( # ` { c e. ( ClWalks ` G ) | ( # ` ( 1st ` c ) ) = N } ) ) |
7 |
4 5 6
|
syl2an |
|- ( ( G e. FinUSGraph /\ N e. Prime ) -> ( # ` ( N ClWWalksN G ) ) = ( # ` { c e. ( ClWalks ` G ) | ( # ` ( 1st ` c ) ) = N } ) ) |
8 |
1 7
|
breqtrd |
|- ( ( G e. FinUSGraph /\ N e. Prime ) -> N || ( # ` { c e. ( ClWalks ` G ) | ( # ` ( 1st ` c ) ) = N } ) ) |