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