Metamath Proof Explorer


Theorem numclwwlk5lem

Description: Lemma for numclwwlk5 . (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 𝑉 = ( Vtx ‘ 𝐺 )
Assertion numclwwlk5lem ( ( 𝐺 RegUSGraph 𝐾𝑋𝑉𝐾 ∈ ℕ0 ) → ( 2 ∥ ( 𝐾 − 1 ) → ( ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ) mod 2 ) = 1 ) )

Proof

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 ) )