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 \land X \in V \land K \in ℕ_{0}) \to (2 ∥ (K - 1) \to \|X ClWWalksNOn (G) 2\| \mod 2 = 1)$

Proof

Step	Hyp	Ref	Expression
1		numclwwlk3.v	$⊢ V = Vtx (G)$
2	1	eleq2i	$⊢ X \in V \leftrightarrow X \in Vtx (G)$
3		clwwlknon2num	$⊢ (G RegUSGraph K \land X \in Vtx (G)) \to \|X ClWWalksNOn (G) 2\| = K$
4	2 3	sylan2b	$⊢ (G RegUSGraph K \land X \in V) \to \|X ClWWalksNOn (G) 2\| = K$
5	4	3adant3	$⊢ (G RegUSGraph K \land X \in V \land K \in ℕ_{0}) \to \|X ClWWalksNOn (G) 2\| = K$
6		oveq1	$⊢ \|X ClWWalksNOn (G) 2\| = K \to \|X ClWWalksNOn (G) 2\| \mod 2 = K \mod 2$
7	6	ad2antrr	$⊢ ((\|X ClWWalksNOn (G) 2\| = K \land (G RegUSGraph K \land X \in V \land K \in ℕ_{0})) \land 2 ∥ (K - 1)) \to \|X ClWWalksNOn (G) 2\| \mod 2 = K \mod 2$
8		2prm	$⊢ 2 \in ℙ$
9		nn0z	$⊢ K \in ℕ_{0} \to K \in ℤ$
10		modprm1div	$⊢ (2 \in ℙ \land K \in ℤ) \to (K \mod 2 = 1 \leftrightarrow 2 ∥ (K - 1))$
11	8 9 10	sylancr	$⊢ K \in ℕ_{0} \to (K \mod 2 = 1 \leftrightarrow 2 ∥ (K - 1))$
12	11	biimprd	$⊢ K \in ℕ_{0} \to (2 ∥ (K - 1) \to K \mod 2 = 1)$
13	12	3ad2ant3	$⊢ (G RegUSGraph K \land X \in V \land K \in ℕ_{0}) \to (2 ∥ (K - 1) \to K \mod 2 = 1)$
14	13	adantl	$⊢ (\|X ClWWalksNOn (G) 2\| = K \land (G RegUSGraph K \land X \in V \land K \in ℕ_{0})) \to (2 ∥ (K - 1) \to K \mod 2 = 1)$
15	14	imp	$⊢ ((\|X ClWWalksNOn (G) 2\| = K \land (G RegUSGraph K \land X \in V \land K \in ℕ_{0})) \land 2 ∥ (K - 1)) \to K \mod 2 = 1$
16	7 15	eqtrd	$⊢ ((\|X ClWWalksNOn (G) 2\| = K \land (G RegUSGraph K \land X \in V \land K \in ℕ_{0})) \land 2 ∥ (K - 1)) \to \|X ClWWalksNOn (G) 2\| \mod 2 = 1$
17	16	ex	$⊢ (\|X ClWWalksNOn (G) 2\| = K \land (G RegUSGraph K \land X \in V \land K \in ℕ_{0})) \to (2 ∥ (K - 1) \to \|X ClWWalksNOn (G) 2\| \mod 2 = 1)$
18	5 17	mpancom	$⊢ (G RegUSGraph K \land X \in V \land K \in ℕ_{0}) \to (2 ∥ (K - 1) \to \|X ClWWalksNOn (G) 2\| \mod 2 = 1)$