Theorem gpgvtxdg3

Description: Every vertex in a generalized Petersen graph has degree 3. (Contributed by AV, 4-Sep-2025)

	Ref	Expression
Hypotheses	gpgvtxdg3.j	$$⊢J=\left(1..^⌈\frac{N}{2}⌉\right)$$
	gpgvtxdg3.g	No typesetting found for |- G = ( N gPetersenGr K ) with typecode |-
	gpgvtxdg3.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
Assertion	gpgvtxdg3	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge K\in J\wedge X\in V\right)\to \mathrm{VtxDeg}\left(G\right)\left(X\right)=3$$

Proof

Step	Hyp	Ref	Expression
1		gpgvtxdg3.j	$$⊢J=\left(1..^⌈\frac{N}{2}⌉\right)$$
2		gpgvtxdg3.g	Could not format G = ( N gPetersenGr K ) : No typesetting found for |- G = ( N gPetersenGr K ) with typecode |-
3		gpgvtxdg3.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
4	1	eleq2i	$$⊢K\in J\leftrightarrow K\in \left(1..^⌈\frac{N}{2}⌉\right)$$
5	4	biimpi	$$⊢K\in J\to K\in \left(1..^⌈\frac{N}{2}⌉\right)$$
6	5	anim2i	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge K\in J\right)\to \left(N\in {\mathbb{Z}}_{\ge 3}\wedge K\in \left(1..^⌈\frac{N}{2}⌉\right)\right)$$
7	6	3adant3	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge K\in J\wedge X\in V\right)\to \left(N\in {\mathbb{Z}}_{\ge 3}\wedge K\in \left(1..^⌈\frac{N}{2}⌉\right)\right)$$
8		gpgusgra	Could not format ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( N gPetersenGr K ) e. USGraph ) : No typesetting found for |- ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( N gPetersenGr K ) e. USGraph ) with typecode |-
9	7 8	syl	Could not format ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. V ) -> ( N gPetersenGr K ) e. USGraph ) : No typesetting found for |- ( ( N e. ( ZZ>= ` 3 ) /\ K e. J /\ X e. V ) -> ( N gPetersenGr K ) e. USGraph ) with typecode |-
10	2 9	eqeltrid	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge K\in J\wedge X\in V\right)\to G\in \mathrm{USGraph}$$
11		simp3	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge K\in J\wedge X\in V\right)\to X\in V$$
12	3	hashnbusgrvd	$$⊢\left(G\in \mathrm{USGraph}\wedge X\in V\right)\to \left|G\mathrm{NeighbVtx}X\right|=\mathrm{VtxDeg}\left(G\right)\left(X\right)$$
13	12	eqcomd	$$⊢\left(G\in \mathrm{USGraph}\wedge X\in V\right)\to \mathrm{VtxDeg}\left(G\right)\left(X\right)=\left|G\mathrm{NeighbVtx}X\right|$$
14	10 11 13	syl2anc	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge K\in J\wedge X\in V\right)\to \mathrm{VtxDeg}\left(G\right)\left(X\right)=\left|G\mathrm{NeighbVtx}X\right|$$
15		eqid	$$⊢G\mathrm{NeighbVtx}X=G\mathrm{NeighbVtx}X$$
16	1 2 3 15	gpgcubic	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge K\in J\wedge X\in V\right)\to \left|G\mathrm{NeighbVtx}X\right|=3$$
17	14 16	eqtrd	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge K\in J\wedge X\in V\right)\to \mathrm{VtxDeg}\left(G\right)\left(X\right)=3$$