gpgvtx0

Description: The outside vertices in a generalized Petersen graph G . (Contributed by AV, 30-Aug-2025)

	Ref	Expression
Hypotheses	gpgvtx0.j	$⊢ J = (1 ..^⌈\frac{N}{2}⌉)$
	gpgvtx0.g	No typesetting found for \|- G = ( N gPetersenGr K ) with typecode \|-
	gpgvtx0.v	$⊢ V = Vtx (G)$
Assertion	gpgvtx0	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land X \in V) \to (⟨0, (2^{nd} (X) + 1) \mod N⟩ \in V \land ⟨0, 2^{nd} (X)⟩ \in V \land ⟨0, (2^{nd} (X) - 1) \mod N⟩ \in V)$

Proof

Step	Hyp	Ref	Expression
1		gpgvtx0.j	$⊢ J = (1 ..^⌈\frac{N}{2}⌉)$
2		gpgvtx0.g	Could not format G = ( N gPetersenGr K ) : No typesetting found for \|- G = ( N gPetersenGr K ) with typecode \|-
3		gpgvtx0.v	$⊢ V = Vtx (G)$
4		eqid	$⊢ (0 ..^N) = (0 ..^N)$
5	4 1 2 3	gpgvtxel	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (X \in V \leftrightarrow \exists x \in \{0, 1\} \exists y \in (0 ..^N) X = ⟨x, y⟩)$
6	2	fveq2i	Could not format ( Vtx ` G ) = ( Vtx ` ( N gPetersenGr K ) ) : No typesetting found for \|- ( Vtx ` G ) = ( Vtx ` ( N gPetersenGr K ) ) with typecode \|-
7	3 6	eqtri	Could not format V = ( Vtx ` ( N gPetersenGr K ) ) : No typesetting found for \|- V = ( Vtx ` ( N gPetersenGr K ) ) with typecode \|-
8		eluz3nn	$⊢ N \in ℤ_{\geq 3} \to N \in ℕ$
9	1 4	gpgvtx	Could not format ( ( N e. NN /\ K e. J ) -> ( Vtx ` ( N gPetersenGr K ) ) = ( { 0 , 1 } X. ( 0 ..^ N ) ) ) : No typesetting found for \|- ( ( N e. NN /\ K e. J ) -> ( Vtx ` ( N gPetersenGr K ) ) = ( { 0 , 1 } X. ( 0 ..^ N ) ) ) with typecode \|-
10	8 9	sylan	Could not format ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( Vtx ` ( N gPetersenGr K ) ) = ( { 0 , 1 } X. ( 0 ..^ N ) ) ) : No typesetting found for \|- ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( Vtx ` ( N gPetersenGr K ) ) = ( { 0 , 1 } X. ( 0 ..^ N ) ) ) with typecode \|-
11	10	adantr	Could not format ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> ( Vtx ` ( N gPetersenGr K ) ) = ( { 0 , 1 } X. ( 0 ..^ N ) ) ) : No typesetting found for \|- ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( x e. { 0 , 1 } /\ y e. ( 0 ..^ N ) ) ) -> ( Vtx ` ( N gPetersenGr K ) ) = ( { 0 , 1 } X. ( 0 ..^ N ) ) ) with typecode \|-
12	7 11	eqtrid	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \to V = \{0, 1\} \times (0 ..^N)$
13		0elpr01	$⊢ 0 \in \{0, 1\}$
14	13	a1i	$⊢ (N \in ℤ_{\geq 3} \land y \in (0 ..^N)) \to 0 \in \{0, 1\}$
15		elfzoelz	$⊢ y \in (0 ..^N) \to y \in ℤ$
16	15	peano2zd	$⊢ y \in (0 ..^N) \to y + 1 \in ℤ$
17		zmodfzo	$⊢ (y + 1 \in ℤ \land N \in ℕ) \to (y + 1) \mod N \in (0 ..^N)$
18	16 8 17	syl2anr	$⊢ (N \in ℤ_{\geq 3} \land y \in (0 ..^N)) \to (y + 1) \mod N \in (0 ..^N)$
19	14 18	opelxpd	$⊢ (N \in ℤ_{\geq 3} \land y \in (0 ..^N)) \to ⟨0, (y + 1) \mod N⟩ \in (\{0, 1\} \times (0 ..^N))$
20		simpr	$⊢ (N \in ℤ_{\geq 3} \land y \in (0 ..^N)) \to y \in (0 ..^N)$
21	14 20	opelxpd	$⊢ (N \in ℤ_{\geq 3} \land y \in (0 ..^N)) \to ⟨0, y⟩ \in (\{0, 1\} \times (0 ..^N))$
22		1zzd	$⊢ y \in (0 ..^N) \to 1 \in ℤ$
23	15 22	zsubcld	$⊢ y \in (0 ..^N) \to y - 1 \in ℤ$
24		zmodfzo	$⊢ (y - 1 \in ℤ \land N \in ℕ) \to (y - 1) \mod N \in (0 ..^N)$
25	23 8 24	syl2anr	$⊢ (N \in ℤ_{\geq 3} \land y \in (0 ..^N)) \to (y - 1) \mod N \in (0 ..^N)$
26	14 25	opelxpd	$⊢ (N \in ℤ_{\geq 3} \land y \in (0 ..^N)) \to ⟨0, (y - 1) \mod N⟩ \in (\{0, 1\} \times (0 ..^N))$
27	19 21 26	3jca	$⊢ (N \in ℤ_{\geq 3} \land y \in (0 ..^N)) \to (⟨0, (y + 1) \mod N⟩ \in (\{0, 1\} \times (0 ..^N)) \land ⟨0, y⟩ \in (\{0, 1\} \times (0 ..^N)) \land ⟨0, (y - 1) \mod N⟩ \in (\{0, 1\} \times (0 ..^N)))$
28	27	ad2ant2rl	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \to (⟨0, (y + 1) \mod N⟩ \in (\{0, 1\} \times (0 ..^N)) \land ⟨0, y⟩ \in (\{0, 1\} \times (0 ..^N)) \land ⟨0, (y - 1) \mod N⟩ \in (\{0, 1\} \times (0 ..^N)))$
29	28	adantr	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \land V = \{0, 1\} \times (0 ..^N)) \to (⟨0, (y + 1) \mod N⟩ \in (\{0, 1\} \times (0 ..^N)) \land ⟨0, y⟩ \in (\{0, 1\} \times (0 ..^N)) \land ⟨0, (y - 1) \mod N⟩ \in (\{0, 1\} \times (0 ..^N)))$
30		eleq2	$⊢ V = \{0, 1\} \times (0 ..^N) \to (⟨0, (y + 1) \mod N⟩ \in V \leftrightarrow ⟨0, (y + 1) \mod N⟩ \in (\{0, 1\} \times (0 ..^N)))$
31		eleq2	$⊢ V = \{0, 1\} \times (0 ..^N) \to (⟨0, y⟩ \in V \leftrightarrow ⟨0, y⟩ \in (\{0, 1\} \times (0 ..^N)))$
32		eleq2	$⊢ V = \{0, 1\} \times (0 ..^N) \to (⟨0, (y - 1) \mod N⟩ \in V \leftrightarrow ⟨0, (y - 1) \mod N⟩ \in (\{0, 1\} \times (0 ..^N)))$
33	30 31 32	3anbi123d	$⊢ V = \{0, 1\} \times (0 ..^N) \to ((⟨0, (y + 1) \mod N⟩ \in V \land ⟨0, y⟩ \in V \land ⟨0, (y - 1) \mod N⟩ \in V) \leftrightarrow (⟨0, (y + 1) \mod N⟩ \in (\{0, 1\} \times (0 ..^N)) \land ⟨0, y⟩ \in (\{0, 1\} \times (0 ..^N)) \land ⟨0, (y - 1) \mod N⟩ \in (\{0, 1\} \times (0 ..^N))))$
34	33	adantl	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \land V = \{0, 1\} \times (0 ..^N)) \to ((⟨0, (y + 1) \mod N⟩ \in V \land ⟨0, y⟩ \in V \land ⟨0, (y - 1) \mod N⟩ \in V) \leftrightarrow (⟨0, (y + 1) \mod N⟩ \in (\{0, 1\} \times (0 ..^N)) \land ⟨0, y⟩ \in (\{0, 1\} \times (0 ..^N)) \land ⟨0, (y - 1) \mod N⟩ \in (\{0, 1\} \times (0 ..^N))))$
35	29 34	mpbird	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \land V = \{0, 1\} \times (0 ..^N)) \to (⟨0, (y + 1) \mod N⟩ \in V \land ⟨0, y⟩ \in V \land ⟨0, (y - 1) \mod N⟩ \in V)$
36	12 35	mpdan	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \to (⟨0, (y + 1) \mod N⟩ \in V \land ⟨0, y⟩ \in V \land ⟨0, (y - 1) \mod N⟩ \in V)$
37		vex	$⊢ x \in V$
38		vex	$⊢ y \in V$
39	37 38	op2ndd	$⊢ X = ⟨x, y⟩ \to 2^{nd} (X) = y$
40		oveq1	$⊢ 2^{nd} (X) = y \to 2^{nd} (X) + 1 = y + 1$
41	40	oveq1d	$⊢ 2^{nd} (X) = y \to (2^{nd} (X) + 1) \mod N = (y + 1) \mod N$
42	41	opeq2d	$⊢ 2^{nd} (X) = y \to ⟨0, (2^{nd} (X) + 1) \mod N⟩ = ⟨0, (y + 1) \mod N⟩$
43	42	eleq1d	$⊢ 2^{nd} (X) = y \to (⟨0, (2^{nd} (X) + 1) \mod N⟩ \in V \leftrightarrow ⟨0, (y + 1) \mod N⟩ \in V)$
44		opeq2	$⊢ 2^{nd} (X) = y \to ⟨0, 2^{nd} (X)⟩ = ⟨0, y⟩$
45	44	eleq1d	$⊢ 2^{nd} (X) = y \to (⟨0, 2^{nd} (X)⟩ \in V \leftrightarrow ⟨0, y⟩ \in V)$
46		oveq1	$⊢ 2^{nd} (X) = y \to 2^{nd} (X) - 1 = y - 1$
47	46	oveq1d	$⊢ 2^{nd} (X) = y \to (2^{nd} (X) - 1) \mod N = (y - 1) \mod N$
48	47	opeq2d	$⊢ 2^{nd} (X) = y \to ⟨0, (2^{nd} (X) - 1) \mod N⟩ = ⟨0, (y - 1) \mod N⟩$
49	48	eleq1d	$⊢ 2^{nd} (X) = y \to (⟨0, (2^{nd} (X) - 1) \mod N⟩ \in V \leftrightarrow ⟨0, (y - 1) \mod N⟩ \in V)$
50	43 45 49	3anbi123d	$⊢ 2^{nd} (X) = y \to ((⟨0, (2^{nd} (X) + 1) \mod N⟩ \in V \land ⟨0, 2^{nd} (X)⟩ \in V \land ⟨0, (2^{nd} (X) - 1) \mod N⟩ \in V) \leftrightarrow (⟨0, (y + 1) \mod N⟩ \in V \land ⟨0, y⟩ \in V \land ⟨0, (y - 1) \mod N⟩ \in V))$
51	39 50	syl	$⊢ X = ⟨x, y⟩ \to ((⟨0, (2^{nd} (X) + 1) \mod N⟩ \in V \land ⟨0, 2^{nd} (X)⟩ \in V \land ⟨0, (2^{nd} (X) - 1) \mod N⟩ \in V) \leftrightarrow (⟨0, (y + 1) \mod N⟩ \in V \land ⟨0, y⟩ \in V \land ⟨0, (y - 1) \mod N⟩ \in V))$
52	36 51	syl5ibrcom	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \to (X = ⟨x, y⟩ \to (⟨0, (2^{nd} (X) + 1) \mod N⟩ \in V \land ⟨0, 2^{nd} (X)⟩ \in V \land ⟨0, (2^{nd} (X) - 1) \mod N⟩ \in V))$
53	52	rexlimdvva	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (\exists x \in \{0, 1\} \exists y \in (0 ..^N) X = ⟨x, y⟩ \to (⟨0, (2^{nd} (X) + 1) \mod N⟩ \in V \land ⟨0, 2^{nd} (X)⟩ \in V \land ⟨0, (2^{nd} (X) - 1) \mod N⟩ \in V))$
54	5 53	sylbid	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (X \in V \to (⟨0, (2^{nd} (X) + 1) \mod N⟩ \in V \land ⟨0, 2^{nd} (X)⟩ \in V \land ⟨0, (2^{nd} (X) - 1) \mod N⟩ \in V))$
55	54	imp	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land X \in V) \to (⟨0, (2^{nd} (X) + 1) \mod N⟩ \in V \land ⟨0, 2^{nd} (X)⟩ \in V \land ⟨0, (2^{nd} (X) - 1) \mod N⟩ \in V)$

Metamath Proof Explorer

Theorem gpgvtx0

Proof