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