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		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		1elpr01	$⊢ 1 \in \{0, 1\}$
14	13	a1i	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \to 1 \in \{0, 1\}$
15		elfzoelz	$⊢ y \in (0 ..^N) \to y \in ℤ$
16	15	adantl	$⊢ (x \in \{0, 1\} \land y \in (0 ..^N)) \to y \in ℤ$
17	16	adantl	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \to y \in ℤ$
18		elfzoelz	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \to K \in ℤ$
19	18 1	eleq2s	$⊢ K \in J \to K \in ℤ$
20	19	adantl	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to K \in ℤ$
21	20	adantr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \to K \in ℤ$
22	17 21	zaddcld	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \to y + K \in ℤ$
23	8	adantr	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to N \in ℕ$
24	23	adantr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \to N \in ℕ$
25		zmodfzo	$⊢ (y + K \in ℤ \land N \in ℕ) \to (y + K) \mod N \in (0 ..^N)$
26	22 24 25	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)$
27	14 26	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))$
28		simprr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \to y \in (0 ..^N)$
29	14 28	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))$
30	17 21	zsubcld	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (x \in \{0, 1\} \land y \in (0 ..^N))) \to y - K \in ℤ$
31		zmodfzo	$⊢ (y - K \in ℤ \land N \in ℕ) \to (y - K) \mod N \in (0 ..^N)$
32	30 24 31	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)$
33	14 32	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))$
34	27 29 33	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)))$
35	34	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)))$
36		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)))$
37		eleq2	$⊢ V = \{0, 1\} \times (0 ..^N) \to (⟨1, y⟩ \in V \leftrightarrow ⟨1, y⟩ \in (\{0, 1\} \times (0 ..^N)))$
38		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)))$
39	36 37 38	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))))$
40	39	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))))$
41	35 40	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)$
42	12 41	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)$
43		vex	$⊢ x \in V$
44		vex	$⊢ y \in V$
45	43 44	op2ndd	$⊢ X = ⟨x, y⟩ \to 2^{nd} (X) = y$
46		oveq1	$⊢ 2^{nd} (X) = y \to 2^{nd} (X) + K = y + K$
47	46	oveq1d	$⊢ 2^{nd} (X) = y \to (2^{nd} (X) + K) \mod N = (y + K) \mod N$
48	47	opeq2d	$⊢ 2^{nd} (X) = y \to ⟨1, (2^{nd} (X) + K) \mod N⟩ = ⟨1, (y + K) \mod N⟩$
49	48	eleq1d	$⊢ 2^{nd} (X) = y \to (⟨1, (2^{nd} (X) + K) \mod N⟩ \in V \leftrightarrow ⟨1, (y + K) \mod N⟩ \in V)$
50		opeq2	$⊢ 2^{nd} (X) = y \to ⟨1, 2^{nd} (X)⟩ = ⟨1, y⟩$
51	50	eleq1d	$⊢ 2^{nd} (X) = y \to (⟨1, 2^{nd} (X)⟩ \in V \leftrightarrow ⟨1, y⟩ \in V)$
52		oveq1	$⊢ 2^{nd} (X) = y \to 2^{nd} (X) - K = y - K$
53	52	oveq1d	$⊢ 2^{nd} (X) = y \to (2^{nd} (X) - K) \mod N = (y - K) \mod N$
54	53	opeq2d	$⊢ 2^{nd} (X) = y \to ⟨1, (2^{nd} (X) - K) \mod N⟩ = ⟨1, (y - K) \mod N⟩$
55	54	eleq1d	$⊢ 2^{nd} (X) = y \to (⟨1, (2^{nd} (X) - K) \mod N⟩ \in V \leftrightarrow ⟨1, (y - K) \mod N⟩ \in V)$
56	49 51 55	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))$
57	45 56	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))$
58	42 57	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))$
59	58	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))$
60	5 59	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))$
61	60	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