Theorem gpgprismgriedgdmss

Description: A subset of the index of edges of the generalized Petersen graph GPG(N,1). (Contributed by AV, 2-Nov-2025)

	Ref	Expression
Assertion	gpgprismgriedgdmss	Could not format assertion : No typesetting found for |- ( N e. ( ZZ>= ` 3 ) -> ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } u. { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } ) C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		eluz3nn	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N\in \mathbb{N}$$
2		lbfzo0	$$⊢0\in \left(0..^N\right)\leftrightarrow N\in \mathbb{N}$$
3	1 2	sylibr	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 0\in \left(0..^N\right)$$
4		opeq2	$$⊢x=0\to ⟨0,x⟩=⟨0,0⟩$$
5		oveq1	$$⊢x=0\to x+1=0+1$$
6		0p1e1	$$⊢0+1=1$$
7	5 6	eqtrdi	$$⊢x=0\to x+1=1$$
8	7	oveq1d	$$⊢x=0\to \left(x+1\right)\mathrm{mod}N=1\mathrm{mod}N$$
9	8	opeq2d	$$⊢x=0\to ⟨0,\left(x+1\right)\mathrm{mod}N⟩=⟨0,1\mathrm{mod}N⟩$$
10	4 9	preq12d	$$⊢x=0\to \left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}=\left\{⟨0,0⟩,⟨0,1\mathrm{mod}N⟩\right\}$$
11	10	eqeq2d	$$⊢x=0\to \left(\left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,0⟩,⟨0,1\mathrm{mod}N⟩\right\}\right)$$
12	11	adantl	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge x=0\right)\to \left(\left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,0⟩,⟨0,1\mathrm{mod}N⟩\right\}\right)$$
13		uzuzle23	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N\in {\mathbb{Z}}_{\ge 2}$$
14		eluz2b1	$$⊢N\in {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(N\in \mathbb{Z}\wedge 1<N\right)$$
15		zre	$$⊢N\in \mathbb{Z}\to N\in ℝ$$
16	15	anim1i	$$⊢\left(N\in \mathbb{Z}\wedge 1<N\right)\to \left(N\in ℝ\wedge 1<N\right)$$
17	14 16	sylbi	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(N\in ℝ\wedge 1<N\right)$$
18		1mod	$$⊢\left(N\in ℝ\wedge 1<N\right)\to 1\mathrm{mod}N=1$$
19	13 17 18	3syl	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1\mathrm{mod}N=1$$
20	19	eqcomd	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1=1\mathrm{mod}N$$
21	20	opeq2d	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to ⟨0,1⟩=⟨0,1\mathrm{mod}N⟩$$
22	21	preq2d	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,0⟩,⟨0,1\mathrm{mod}N⟩\right\}$$
23	3 12 22	rspcedvd	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \exists x\in \left(0..^N\right)\left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}$$
24	23	3mix1d	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(\exists x\in \left(0..^N\right)\left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \exists x\in \left(0..^N\right)\left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \exists x\in \left(0..^N\right)\left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
25		3r19.43	$$⊢\exists x\in \left(0..^N\right)\left(\left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\leftrightarrow \left(\exists x\in \left(0..^N\right)\left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \exists x\in \left(0..^N\right)\left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \exists x\in \left(0..^N\right)\left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
26	24 25	sylibr	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \exists x\in \left(0..^N\right)\left(\left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
27		eqid	$$⊢\left(0..^N\right)=\left(0..^N\right)$$
28		eqid	Could not format ( N gPetersenGr 1 ) = ( N gPetersenGr 1 ) : No typesetting found for |- ( N gPetersenGr 1 ) = ( N gPetersenGr 1 ) with typecode |-
29	27 28	gpgprismgriedgdmel	Could not format ( N e. ( ZZ>= ` 3 ) -> ( { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) <-> E. x e. ( 0 ..^ N ) ( { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) ) : No typesetting found for |- ( N e. ( ZZ>= ` 3 ) -> ( { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) <-> E. x e. ( 0 ..^ N ) ( { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) ) with typecode |-
30	26 29	mpbird	Could not format ( N e. ( ZZ>= ` 3 ) -> { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) ) : No typesetting found for |- ( N e. ( ZZ>= ` 3 ) -> { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) ) with typecode |-
31		opeq2	$$⊢x=0\to ⟨1,x⟩=⟨1,0⟩$$
32	4 31	preq12d	$$⊢x=0\to \left\{⟨0,x⟩,⟨1,x⟩\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}$$
33	32	eqeq2d	$$⊢x=0\to \left(\left\{⟨0,0⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\leftrightarrow \left\{⟨0,0⟩,⟨1,0⟩\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}\right)$$
34	33	adantl	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge x=0\right)\to \left(\left\{⟨0,0⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\leftrightarrow \left\{⟨0,0⟩,⟨1,0⟩\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}\right)$$
35		eqid	$$⊢\left\{⟨0,0⟩,⟨1,0⟩\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}$$
36	35	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left\{⟨0,0⟩,⟨1,0⟩\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}$$
37	3 34 36	rspcedvd	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \exists x\in \left(0..^N\right)\left\{⟨0,0⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}$$
38	37	3mix2d	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(\exists x\in \left(0..^N\right)\left\{⟨0,0⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \exists x\in \left(0..^N\right)\left\{⟨0,0⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \exists x\in \left(0..^N\right)\left\{⟨0,0⟩,⟨1,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
39		3r19.43	$$⊢\exists x\in \left(0..^N\right)\left(\left\{⟨0,0⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨0,0⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨0,0⟩,⟨1,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\leftrightarrow \left(\exists x\in \left(0..^N\right)\left\{⟨0,0⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \exists x\in \left(0..^N\right)\left\{⟨0,0⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \exists x\in \left(0..^N\right)\left\{⟨0,0⟩,⟨1,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
40	38 39	sylibr	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \exists x\in \left(0..^N\right)\left(\left\{⟨0,0⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨0,0⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨0,0⟩,⟨1,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
41	27 28	gpgprismgriedgdmel	Could not format ( N e. ( ZZ>= ` 3 ) -> ( { <. 0 , 0 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) <-> E. x e. ( 0 ..^ N ) ( { <. 0 , 0 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , 0 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , 0 >. , <. 1 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) ) : No typesetting found for |- ( N e. ( ZZ>= ` 3 ) -> ( { <. 0 , 0 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) <-> E. x e. ( 0 ..^ N ) ( { <. 0 , 0 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , 0 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , 0 >. , <. 1 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) ) with typecode |-
42	40 41	mpbird	Could not format ( N e. ( ZZ>= ` 3 ) -> { <. 0 , 0 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) ) : No typesetting found for |- ( N e. ( ZZ>= ` 3 ) -> { <. 0 , 0 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) ) with typecode |-
43	30 42	prssd	Could not format ( N e. ( ZZ>= ` 3 ) -> { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) ) : No typesetting found for |- ( N e. ( ZZ>= ` 3 ) -> { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) ) with typecode |-
44		1nn0	$$⊢1\in {\mathbb{N}}_0$$
45	44	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1\in {\mathbb{N}}_0$$
46		eluz2gt1	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 1<N$$
47	13 46	syl	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1<N$$
48		elfzo0	$$⊢1\in \left(0..^N\right)\leftrightarrow \left(1\in {\mathbb{N}}_0\wedge N\in \mathbb{N}\wedge 1<N\right)$$
49	45 1 47 48	syl3anbrc	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1\in \left(0..^N\right)$$
50		opeq2	$$⊢x=1\to ⟨0,x⟩=⟨0,1⟩$$
51		opeq2	$$⊢x=1\to ⟨1,x⟩=⟨1,1⟩$$
52	50 51	preq12d	$$⊢x=1\to \left\{⟨0,x⟩,⟨1,x⟩\right\}=\left\{⟨0,1⟩,⟨1,1⟩\right\}$$
53	52	eqeq2d	$$⊢x=1\to \left(\left\{⟨1,1⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\leftrightarrow \left\{⟨1,1⟩,⟨0,1⟩\right\}=\left\{⟨0,1⟩,⟨1,1⟩\right\}\right)$$
54	53	adantl	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge x=1\right)\to \left(\left\{⟨1,1⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\leftrightarrow \left\{⟨1,1⟩,⟨0,1⟩\right\}=\left\{⟨0,1⟩,⟨1,1⟩\right\}\right)$$
55		prcom	$$⊢\left\{⟨1,1⟩,⟨0,1⟩\right\}=\left\{⟨0,1⟩,⟨1,1⟩\right\}$$
56	55	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left\{⟨1,1⟩,⟨0,1⟩\right\}=\left\{⟨0,1⟩,⟨1,1⟩\right\}$$
57	49 54 56	rspcedvd	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \exists x\in \left(0..^N\right)\left\{⟨1,1⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}$$
58	57	3mix2d	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(\exists x\in \left(0..^N\right)\left\{⟨1,1⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \exists x\in \left(0..^N\right)\left\{⟨1,1⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \exists x\in \left(0..^N\right)\left\{⟨1,1⟩,⟨0,1⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
59		3r19.43	$$⊢\exists x\in \left(0..^N\right)\left(\left\{⟨1,1⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨1,1⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨1,1⟩,⟨0,1⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\leftrightarrow \left(\exists x\in \left(0..^N\right)\left\{⟨1,1⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \exists x\in \left(0..^N\right)\left\{⟨1,1⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \exists x\in \left(0..^N\right)\left\{⟨1,1⟩,⟨0,1⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
60	58 59	sylibr	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \exists x\in \left(0..^N\right)\left(\left\{⟨1,1⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨1,1⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨1,1⟩,⟨0,1⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
61	27 28	gpgprismgriedgdmel	Could not format ( N e. ( ZZ>= ` 3 ) -> ( { <. 1 , 1 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) <-> E. x e. ( 0 ..^ N ) ( { <. 1 , 1 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , 1 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 1 >. , <. 0 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) ) : No typesetting found for |- ( N e. ( ZZ>= ` 3 ) -> ( { <. 1 , 1 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) <-> E. x e. ( 0 ..^ N ) ( { <. 1 , 1 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , 1 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 1 >. , <. 0 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) ) with typecode |-
62	60 61	mpbird	Could not format ( N e. ( ZZ>= ` 3 ) -> { <. 1 , 1 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) ) : No typesetting found for |- ( N e. ( ZZ>= ` 3 ) -> { <. 1 , 1 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) ) with typecode |-
63	8	opeq2d	$$⊢x=0\to ⟨1,\left(x+1\right)\mathrm{mod}N⟩=⟨1,1\mathrm{mod}N⟩$$
64	31 63	preq12d	$$⊢x=0\to \left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}=\left\{⟨1,0⟩,⟨1,1\mathrm{mod}N⟩\right\}$$
65	64	eqeq2d	$$⊢x=0\to \left(\left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨1,0⟩,⟨1,1\mathrm{mod}N⟩\right\}\right)$$
66	65	adantl	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge x=0\right)\to \left(\left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨1,0⟩,⟨1,1\mathrm{mod}N⟩\right\}\right)$$
67		prcom	$$⊢\left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨1,0⟩,⟨1,1⟩\right\}$$
68	20	opeq2d	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to ⟨1,1⟩=⟨1,1\mathrm{mod}N⟩$$
69	68	preq2d	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left\{⟨1,0⟩,⟨1,1⟩\right\}=\left\{⟨1,0⟩,⟨1,1\mathrm{mod}N⟩\right\}$$
70	67 69	eqtrid	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨1,0⟩,⟨1,1\mathrm{mod}N⟩\right\}$$
71	3 66 70	rspcedvd	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \exists x\in \left(0..^N\right)\left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}$$
72	71	3mix3d	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(\exists x\in \left(0..^N\right)\left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \exists x\in \left(0..^N\right)\left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \exists x\in \left(0..^N\right)\left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
73		3r19.43	$$⊢\exists x\in \left(0..^N\right)\left(\left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\leftrightarrow \left(\exists x\in \left(0..^N\right)\left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \exists x\in \left(0..^N\right)\left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \exists x\in \left(0..^N\right)\left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
74	72 73	sylibr	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \exists x\in \left(0..^N\right)\left(\left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
75	27 28	gpgprismgriedgdmel	Could not format ( N e. ( ZZ>= ` 3 ) -> ( { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) <-> E. x e. ( 0 ..^ N ) ( { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) ) : No typesetting found for |- ( N e. ( ZZ>= ` 3 ) -> ( { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) <-> E. x e. ( 0 ..^ N ) ( { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) ) with typecode |-
76	74 75	mpbird	Could not format ( N e. ( ZZ>= ` 3 ) -> { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) ) : No typesetting found for |- ( N e. ( ZZ>= ` 3 ) -> { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) ) with typecode |-
77	62 76	prssd	Could not format ( N e. ( ZZ>= ` 3 ) -> { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) ) : No typesetting found for |- ( N e. ( ZZ>= ` 3 ) -> { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) ) with typecode |-
78	43 77	unssd	Could not format ( N e. ( ZZ>= ` 3 ) -> ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } u. { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } ) C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) ) : No typesetting found for |- ( N e. ( ZZ>= ` 3 ) -> ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } u. { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } ) C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) ) with typecode |-