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 ⊢ V = Vtx ⁡ G
Assertion numclwwlk5lem ⊢ G RegUSGraph K ∧ X ∈ V ∧ K ∈ ℕ 0 → 2 ∥ K − 1 → X ClWWalksNOn ⁡ G 2 mod 2 = 1

Proof

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