Step |
Hyp |
Ref |
Expression |
1 |
|
numclwwlk3.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
1
|
eleq2i |
⊢ ( 𝑋 ∈ 𝑉 ↔ 𝑋 ∈ ( Vtx ‘ 𝐺 ) ) |
3 |
|
clwwlknon2num |
⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ ( Vtx ‘ 𝐺 ) ) → ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ) = 𝐾 ) |
4 |
2 3
|
sylan2b |
⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ) = 𝐾 ) |
5 |
4
|
3adant3 |
⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ) = 𝐾 ) |
6 |
|
oveq1 |
⊢ ( ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ) = 𝐾 → ( ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ) mod 2 ) = ( 𝐾 mod 2 ) ) |
7 |
6
|
ad2antrr |
⊢ ( ( ( ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ) = 𝐾 ∧ ( 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ ℕ0 ) ) ∧ 2 ∥ ( 𝐾 − 1 ) ) → ( ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ) mod 2 ) = ( 𝐾 mod 2 ) ) |
8 |
|
2prm |
⊢ 2 ∈ ℙ |
9 |
|
nn0z |
⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℤ ) |
10 |
|
modprm1div |
⊢ ( ( 2 ∈ ℙ ∧ 𝐾 ∈ ℤ ) → ( ( 𝐾 mod 2 ) = 1 ↔ 2 ∥ ( 𝐾 − 1 ) ) ) |
11 |
8 9 10
|
sylancr |
⊢ ( 𝐾 ∈ ℕ0 → ( ( 𝐾 mod 2 ) = 1 ↔ 2 ∥ ( 𝐾 − 1 ) ) ) |
12 |
11
|
biimprd |
⊢ ( 𝐾 ∈ ℕ0 → ( 2 ∥ ( 𝐾 − 1 ) → ( 𝐾 mod 2 ) = 1 ) ) |
13 |
12
|
3ad2ant3 |
⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( 2 ∥ ( 𝐾 − 1 ) → ( 𝐾 mod 2 ) = 1 ) ) |
14 |
13
|
adantl |
⊢ ( ( ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ) = 𝐾 ∧ ( 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ ℕ0 ) ) → ( 2 ∥ ( 𝐾 − 1 ) → ( 𝐾 mod 2 ) = 1 ) ) |
15 |
14
|
imp |
⊢ ( ( ( ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ) = 𝐾 ∧ ( 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ ℕ0 ) ) ∧ 2 ∥ ( 𝐾 − 1 ) ) → ( 𝐾 mod 2 ) = 1 ) |
16 |
7 15
|
eqtrd |
⊢ ( ( ( ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ) = 𝐾 ∧ ( 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ ℕ0 ) ) ∧ 2 ∥ ( 𝐾 − 1 ) ) → ( ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ) mod 2 ) = 1 ) |
17 |
16
|
ex |
⊢ ( ( ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ) = 𝐾 ∧ ( 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ ℕ0 ) ) → ( 2 ∥ ( 𝐾 − 1 ) → ( ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ) mod 2 ) = 1 ) ) |
18 |
5 17
|
mpancom |
⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( 2 ∥ ( 𝐾 − 1 ) → ( ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ) mod 2 ) = 1 ) ) |