Step |
Hyp |
Ref |
Expression |
1 |
|
clwwlkndivn |
⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ ) → 𝑁 ∥ ( ♯ ‘ ( 𝑁 ClWWalksN 𝐺 ) ) ) |
2 |
|
fusgrusgr |
⊢ ( 𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph ) |
3 |
|
usgruspgr |
⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ USPGraph ) |
4 |
2 3
|
syl |
⊢ ( 𝐺 ∈ FinUSGraph → 𝐺 ∈ USPGraph ) |
5 |
|
prmnn |
⊢ ( 𝑁 ∈ ℙ → 𝑁 ∈ ℕ ) |
6 |
|
clwlkssizeeq |
⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ ( 𝑁 ClWWalksN 𝐺 ) ) = ( ♯ ‘ { 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑐 ) ) = 𝑁 } ) ) |
7 |
4 5 6
|
syl2an |
⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ ) → ( ♯ ‘ ( 𝑁 ClWWalksN 𝐺 ) ) = ( ♯ ‘ { 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑐 ) ) = 𝑁 } ) ) |
8 |
1 7
|
breqtrd |
⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ ) → 𝑁 ∥ ( ♯ ‘ { 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑐 ) ) = 𝑁 } ) ) |