gpgvtx1

Description: The inside vertices in a generalized Petersen graph G . (Contributed by AV, 28-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	gpgvtx1	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land X \in V) \to (⟨1, (2^{nd} (X) + K) \mod N⟩ \in V \land ⟨1, 2^{nd} (X)⟩ \in V \land ⟨1, (2^{nd} (X) - K) \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		eluzge3nn	$⊢ 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		1ex	$⊢ 1 \in V$
14	13	prid2	$⊢ 1 \in \{0, 1\}$
15	14	a1i	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \to 1 \in \{0, 1\}$
16		elfzoelz	$⊢ y \in (0 ..^N) \to y \in ℤ$
17	16	adantl	$⊢ (x \in \{0, 1\} \land y \in (0 ..^N)) \to y \in ℤ$
18	17	adantl	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \to y \in ℤ$
19		elfzoelz	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \to K \in ℤ$
20	19 1	eleq2s	$⊢ K \in J \to K \in ℤ$
21	20	adantl	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to K \in ℤ$
22	21	adantr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \to K \in ℤ$
23	18 22	zaddcld	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \to y + K \in ℤ$
24	8	adantr	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to N \in ℕ$
25	24	adantr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \to N \in ℕ$
26		zmodfzo	$⊢ (y + K \in ℤ \land N \in ℕ) \to (y + K) \mod N \in (0 ..^N)$
27	23 25 26	syl2anc	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \to (y + K) \mod N \in (0 ..^N)$
28	15 27	opelxpd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \to ⟨1, (y + K) \mod N⟩ \in (\{0, 1\} \times (0 ..^N))$
29		simprr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \to y \in (0 ..^N)$
30	15 29	opelxpd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \to ⟨1, y⟩ \in (\{0, 1\} \times (0 ..^N))$
31	18 22	zsubcld	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \to y - K \in ℤ$
32		zmodfzo	$⊢ (y - K \in ℤ \land N \in ℕ) \to (y - K) \mod N \in (0 ..^N)$
33	31 25 32	syl2anc	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \to (y - K) \mod N \in (0 ..^N)$
34	15 33	opelxpd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \to ⟨1, (y - K) \mod N⟩ \in (\{0, 1\} \times (0 ..^N))$
35	28 30 34	3jca	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \to (⟨1, (y + K) \mod N⟩ \in (\{0, 1\} \times (0 ..^N)) \land ⟨1, y⟩ \in (\{0, 1\} \times (0 ..^N)) \land ⟨1, (y - K) \mod N⟩ \in (\{0, 1\} \times (0 ..^N)))$
36	35	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 (⟨1, (y + K) \mod N⟩ \in (\{0, 1\} \times (0 ..^N)) \land ⟨1, y⟩ \in (\{0, 1\} \times (0 ..^N)) \land ⟨1, (y - K) \mod N⟩ \in (\{0, 1\} \times (0 ..^N)))$
37		eleq2	$⊢ V = \{0, 1\} \times (0 ..^N) \to (⟨1, (y + K) \mod N⟩ \in V \leftrightarrow ⟨1, (y + K) \mod N⟩ \in (\{0, 1\} \times (0 ..^N)))$
38		eleq2	$⊢ V = \{0, 1\} \times (0 ..^N) \to (⟨1, y⟩ \in V \leftrightarrow ⟨1, y⟩ \in (\{0, 1\} \times (0 ..^N)))$
39		eleq2	$⊢ V = \{0, 1\} \times (0 ..^N) \to (⟨1, (y - K) \mod N⟩ \in V \leftrightarrow ⟨1, (y - K) \mod N⟩ \in (\{0, 1\} \times (0 ..^N)))$
40	37 38 39	3anbi123d	$⊢ V = \{0, 1\} \times (0 ..^N) \to ((⟨1, (y + K) \mod N⟩ \in V \land ⟨1, y⟩ \in V \land ⟨1, (y - K) \mod N⟩ \in V) \leftrightarrow (⟨1, (y + K) \mod N⟩ \in (\{0, 1\} \times (0 ..^N)) \land ⟨1, y⟩ \in (\{0, 1\} \times (0 ..^N)) \land ⟨1, (y - K) \mod N⟩ \in (\{0, 1\} \times (0 ..^N))))$
41	40	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 ((⟨1, (y + K) \mod N⟩ \in V \land ⟨1, y⟩ \in V \land ⟨1, (y - K) \mod N⟩ \in V) \leftrightarrow (⟨1, (y + K) \mod N⟩ \in (\{0, 1\} \times (0 ..^N)) \land ⟨1, y⟩ \in (\{0, 1\} \times (0 ..^N)) \land ⟨1, (y - K) \mod N⟩ \in (\{0, 1\} \times (0 ..^N))))$
42	36 41	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 (⟨1, (y + K) \mod N⟩ \in V \land ⟨1, y⟩ \in V \land ⟨1, (y - K) \mod N⟩ \in V)$
43	12 42	mpdan	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \to (⟨1, (y + K) \mod N⟩ \in V \land ⟨1, y⟩ \in V \land ⟨1, (y - K) \mod N⟩ \in V)$
44		vex	$⊢ x \in V$
45		vex	$⊢ y \in V$
46	44 45	op2ndd	$⊢ X = ⟨x, y⟩ \to 2^{nd} (X) = y$
47		oveq1	$⊢ 2^{nd} (X) = y \to 2^{nd} (X) + K = y + K$
48	47	oveq1d	$⊢ 2^{nd} (X) = y \to (2^{nd} (X) + K) \mod N = (y + K) \mod N$
49	48	opeq2d	$⊢ 2^{nd} (X) = y \to ⟨1, (2^{nd} (X) + K) \mod N⟩ = ⟨1, (y + K) \mod N⟩$
50	49	eleq1d	$⊢ 2^{nd} (X) = y \to (⟨1, (2^{nd} (X) + K) \mod N⟩ \in V \leftrightarrow ⟨1, (y + K) \mod N⟩ \in V)$
51		opeq2	$⊢ 2^{nd} (X) = y \to ⟨1, 2^{nd} (X)⟩ = ⟨1, y⟩$
52	51	eleq1d	$⊢ 2^{nd} (X) = y \to (⟨1, 2^{nd} (X)⟩ \in V \leftrightarrow ⟨1, y⟩ \in V)$
53		oveq1	$⊢ 2^{nd} (X) = y \to 2^{nd} (X) - K = y - K$
54	53	oveq1d	$⊢ 2^{nd} (X) = y \to (2^{nd} (X) - K) \mod N = (y - K) \mod N$
55	54	opeq2d	$⊢ 2^{nd} (X) = y \to ⟨1, (2^{nd} (X) - K) \mod N⟩ = ⟨1, (y - K) \mod N⟩$
56	55	eleq1d	$⊢ 2^{nd} (X) = y \to (⟨1, (2^{nd} (X) - K) \mod N⟩ \in V \leftrightarrow ⟨1, (y - K) \mod N⟩ \in V)$
57	50 52 56	3anbi123d	$⊢ 2^{nd} (X) = y \to ((⟨1, (2^{nd} (X) + K) \mod N⟩ \in V \land ⟨1, 2^{nd} (X)⟩ \in V \land ⟨1, (2^{nd} (X) - K) \mod N⟩ \in V) \leftrightarrow (⟨1, (y + K) \mod N⟩ \in V \land ⟨1, y⟩ \in V \land ⟨1, (y - K) \mod N⟩ \in V))$
58	46 57	syl	$⊢ X = ⟨x, y⟩ \to ((⟨1, (2^{nd} (X) + K) \mod N⟩ \in V \land ⟨1, 2^{nd} (X)⟩ \in V \land ⟨1, (2^{nd} (X) - K) \mod N⟩ \in V) \leftrightarrow (⟨1, (y + K) \mod N⟩ \in V \land ⟨1, y⟩ \in V \land ⟨1, (y - K) \mod N⟩ \in V))$
59	43 58	syl5ibrcom	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \to (X = ⟨x, y⟩ \to (⟨1, (2^{nd} (X) + K) \mod N⟩ \in V \land ⟨1, 2^{nd} (X)⟩ \in V \land ⟨1, (2^{nd} (X) - K) \mod N⟩ \in V))$
60	59	rexlimdvva	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (\exists x \in \{0, 1\} \exists y \in (0 ..^N) X = ⟨x, y⟩ \to (⟨1, (2^{nd} (X) + K) \mod N⟩ \in V \land ⟨1, 2^{nd} (X)⟩ \in V \land ⟨1, (2^{nd} (X) - K) \mod N⟩ \in V))$
61	5 60	sylbid	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (X \in V \to (⟨1, (2^{nd} (X) + K) \mod N⟩ \in V \land ⟨1, 2^{nd} (X)⟩ \in V \land ⟨1, (2^{nd} (X) - K) \mod N⟩ \in V))$
62	61	imp	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land X \in V) \to (⟨1, (2^{nd} (X) + K) \mod N⟩ \in V \land ⟨1, 2^{nd} (X)⟩ \in V \land ⟨1, (2^{nd} (X) - K) \mod N⟩ \in V)$

Metamath Proof Explorer

Theorem gpgvtx1

Proof