Theorem gpgorder

Description: The order of the generalized Petersen graph GPG(N,K). (Contributed by AV, 29-Sep-2025)

	Ref	Expression
Hypothesis	gpgorder.j	$$⊢J=\left(1..^⌈\frac{N}{2}⌉\right)$$
Assertion	gpgorder	Could not format assertion : No typesetting found for |- ( ( N e. NN /\ K e. J ) -> ( # ` ( Vtx ` ( N gPetersenGr K ) ) ) = ( 2 x. N ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		gpgorder.j	$$⊢J=\left(1..^⌈\frac{N}{2}⌉\right)$$
2		eqid	$$⊢\left(0..^N\right)=\left(0..^N\right)$$
3	1 2	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 |-
4	3	fveq2d	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 |-
5		prfi	$$⊢\left\{0,1\right\}\in \mathrm{Fin}$$
6		fzofi	$$⊢\left(0..^N\right)\in \mathrm{Fin}$$
7	5 6	pm3.2i	$$⊢\left(\left\{0,1\right\}\in \mathrm{Fin}\wedge \left(0..^N\right)\in \mathrm{Fin}\right)$$
8		hashxp	$$⊢\left(\left\{0,1\right\}\in \mathrm{Fin}\wedge \left(0..^N\right)\in \mathrm{Fin}\right)\to \left|\left\{0,1\right\}\times \left(0..^N\right)\right|=\left|\left\{0,1\right\}\right|\left|\left(0..^N\right)\right|$$
9	7 8	mp1i	$$⊢\left(N\in \mathbb{N}\wedge K\in J\right)\to \left|\left\{0,1\right\}\times \left(0..^N\right)\right|=\left|\left\{0,1\right\}\right|\left|\left(0..^N\right)\right|$$
10		prhash2ex	$$⊢\left|\left\{0,1\right\}\right|=2$$
11	10	a1i	$$⊢\left(N\in \mathbb{N}\wedge K\in J\right)\to \left|\left\{0,1\right\}\right|=2$$
12		nnnn0	$$⊢N\in \mathbb{N}\to N\in {\mathbb{N}}_0$$
13		hashfzo0	$$⊢N\in {\mathbb{N}}_0\to \left|\left(0..^N\right)\right|=N$$
14	12 13	syl	$$⊢N\in \mathbb{N}\to \left|\left(0..^N\right)\right|=N$$
15	14	adantr	$$⊢\left(N\in \mathbb{N}\wedge K\in J\right)\to \left|\left(0..^N\right)\right|=N$$
16	11 15	oveq12d	$$⊢\left(N\in \mathbb{N}\wedge K\in J\right)\to \left|\left\{0,1\right\}\right|\left|\left(0..^N\right)\right|=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
17	4 9 16	3eqtrd	Could not format ( ( N e. NN /\ K e. J ) -> ( # ` ( Vtx ` ( N gPetersenGr K ) ) ) = ( 2 x. N ) ) : No typesetting found for |- ( ( N e. NN /\ K e. J ) -> ( # ` ( Vtx ` ( N gPetersenGr K ) ) ) = ( 2 x. N ) ) with typecode |-