Theorem gpgprismgr4cycllem3

Description: Lemma 3 for gpgprismgr4cycl0 . (Contributed by AV, 5-Nov-2025)

	Ref	Expression
Hypothesis	gpgprismgr4cycllem1.f	$$⊢F=⟨“\left\{⟨0,0⟩,⟨0,1⟩\right\}\left\{⟨0,1⟩,⟨1,1⟩\right\}\left\{⟨1,1⟩,⟨1,0⟩\right\}\left\{⟨1,0⟩,⟨0,0⟩\right\}”⟩$$
Assertion	gpgprismgr4cycllem3	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge X\in \left(0..^4\right)\right)\to \left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		gpgprismgr4cycllem1.f	$$⊢F=⟨“\left\{⟨0,0⟩,⟨0,1⟩\right\}\left\{⟨0,1⟩,⟨1,1⟩\right\}\left\{⟨1,1⟩,⟨1,0⟩\right\}\left\{⟨1,0⟩,⟨0,0⟩\right\}”⟩$$
2		fzo0to42pr	$$⊢\left(0..^4\right)=\left\{0,1\right\}\cup \left\{2,3\right\}$$
3	2	eleq2i	$$⊢X\in \left(0..^4\right)\leftrightarrow X\in \left(\left\{0,1\right\}\cup \left\{2,3\right\}\right)$$
4		elun	$$⊢X\in \left(\left\{0,1\right\}\cup \left\{2,3\right\}\right)\leftrightarrow \left(X\in \left\{0,1\right\}\vee X\in \left\{2,3\right\}\right)$$
5	3 4	bitri	$$⊢X\in \left(0..^4\right)\leftrightarrow \left(X\in \left\{0,1\right\}\vee X\in \left\{2,3\right\}\right)$$
6		elpri	$$⊢X\in \left\{0,1\right\}\to \left(X=0\vee X=1\right)$$
7		0elpr01	$$⊢0\in \left\{0,1\right\}$$
8	7	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 0\in \left\{0,1\right\}$$
9		eluz3nn	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N\in \mathbb{N}$$
10		lbfzo0	$$⊢0\in \left(0..^N\right)\leftrightarrow N\in \mathbb{N}$$
11	9 10	sylibr	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 0\in \left(0..^N\right)$$
12	8 11	opelxpd	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to ⟨0,0⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)$$
13		1nn0	$$⊢1\in {\mathbb{N}}_0$$
14	13	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1\in {\mathbb{N}}_0$$
15		uzuzle23	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N\in {\mathbb{Z}}_{\ge 2}$$
16		eluz2gt1	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 1<N$$
17	15 16	syl	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1<N$$
18		elfzo0	$$⊢1\in \left(0..^N\right)\leftrightarrow \left(1\in {\mathbb{N}}_0\wedge N\in \mathbb{N}\wedge 1<N\right)$$
19	14 9 17 18	syl3anbrc	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1\in \left(0..^N\right)$$
20	8 19	opelxpd	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to ⟨0,1⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)$$
21		prelpwi	$$⊢\left(⟨0,0⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge ⟨0,1⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)\right)\to \left\{⟨0,0⟩,⟨0,1⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)$$
22	12 20 21	syl2anc	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left\{⟨0,0⟩,⟨0,1⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)$$
23		opeq2	$$⊢x=0\to ⟨0,x⟩=⟨0,0⟩$$
24		oveq1	$$⊢x=0\to x+1=0+1$$
25	24	oveq1d	$$⊢x=0\to \left(x+1\right)\mathrm{mod}N=\left(0+1\right)\mathrm{mod}N$$
26	25	opeq2d	$$⊢x=0\to ⟨0,\left(x+1\right)\mathrm{mod}N⟩=⟨0,\left(0+1\right)\mathrm{mod}N⟩$$
27	23 26	preq12d	$$⊢x=0\to \left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}=\left\{⟨0,0⟩,⟨0,\left(0+1\right)\mathrm{mod}N⟩\right\}$$
28	27	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,\left(0+1\right)\mathrm{mod}N⟩\right\}\right)$$
29		opeq2	$$⊢x=0\to ⟨1,x⟩=⟨1,0⟩$$
30	23 29	preq12d	$$⊢x=0\to \left\{⟨0,x⟩,⟨1,x⟩\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}$$
31	30	eqeq2d	$$⊢x=0\to \left(\left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\leftrightarrow \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}\right)$$
32	25	opeq2d	$$⊢x=0\to ⟨1,\left(x+1\right)\mathrm{mod}N⟩=⟨1,\left(0+1\right)\mathrm{mod}N⟩$$
33	29 32	preq12d	$$⊢x=0\to \left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}=\left\{⟨1,0⟩,⟨1,\left(0+1\right)\mathrm{mod}N⟩\right\}$$
34	33	eqeq2d	$$⊢x=0\to \left(\left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨1,0⟩,⟨1,\left(0+1\right)\mathrm{mod}N⟩\right\}\right)$$
35	28 31 34	3orbi123d	$$⊢x=0\to \left(\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(\left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,0⟩,⟨0,\left(0+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}\vee \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨1,0⟩,⟨1,\left(0+1\right)\mathrm{mod}N⟩\right\}\right)\right)$$
36		eluzelre	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N\in ℝ$$
37		1mod	$$⊢\left(N\in ℝ\wedge 1<N\right)\to 1\mathrm{mod}N=1$$
38	36 17 37	syl2anc	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1\mathrm{mod}N=1$$
39		1e0p1	$$⊢1=0+1$$
40	39	oveq1i	$$⊢1\mathrm{mod}N=\left(0+1\right)\mathrm{mod}N$$
41	38 40	eqtr3di	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1=\left(0+1\right)\mathrm{mod}N$$
42	41	opeq2d	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to ⟨0,1⟩=⟨0,\left(0+1\right)\mathrm{mod}N⟩$$
43	42	preq2d	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,0⟩,⟨0,\left(0+1\right)\mathrm{mod}N⟩\right\}$$
44	43	3mix1d	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(\left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,0⟩,⟨0,\left(0+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}\vee \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨1,0⟩,⟨1,\left(0+1\right)\mathrm{mod}N⟩\right\}\right)$$
45	35 11 44	rspcedvdw	$$⊢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)$$
46	22 45	jca	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(\left\{⟨0,0⟩,⟨0,1⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \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)\right)$$
47		fveq2	$$⊢X=0\to F\left(X\right)=F\left(0\right)$$
48	1	fveq1i	$$⊢F\left(0\right)=⟨“\left\{⟨0,0⟩,⟨0,1⟩\right\}\left\{⟨0,1⟩,⟨1,1⟩\right\}\left\{⟨1,1⟩,⟨1,0⟩\right\}\left\{⟨1,0⟩,⟨0,0⟩\right\}”⟩\left(0\right)$$
49		prex	$$⊢\left\{⟨0,0⟩,⟨0,1⟩\right\}\in \mathrm{V}$$
50		s4fv0	$$⊢\left\{⟨0,0⟩,⟨0,1⟩\right\}\in \mathrm{V}\to ⟨“\left\{⟨0,0⟩,⟨0,1⟩\right\}\left\{⟨0,1⟩,⟨1,1⟩\right\}\left\{⟨1,1⟩,⟨1,0⟩\right\}\left\{⟨1,0⟩,⟨0,0⟩\right\}”⟩\left(0\right)=\left\{⟨0,0⟩,⟨0,1⟩\right\}$$
51	49 50	ax-mp	$$⊢⟨“\left\{⟨0,0⟩,⟨0,1⟩\right\}\left\{⟨0,1⟩,⟨1,1⟩\right\}\left\{⟨1,1⟩,⟨1,0⟩\right\}\left\{⟨1,0⟩,⟨0,0⟩\right\}”⟩\left(0\right)=\left\{⟨0,0⟩,⟨0,1⟩\right\}$$
52	48 51	eqtri	$$⊢F\left(0\right)=\left\{⟨0,0⟩,⟨0,1⟩\right\}$$
53	47 52	eqtrdi	$$⊢X=0\to F\left(X\right)=\left\{⟨0,0⟩,⟨0,1⟩\right\}$$
54	53	eleq1d	$$⊢X=0\to \left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\leftrightarrow \left\{⟨0,0⟩,⟨0,1⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\right)$$
55	53	eqeq1d	$$⊢X=0\to \left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
56	53	eqeq1d	$$⊢X=0\to \left(F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\leftrightarrow \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\right)$$
57	53	eqeq1d	$$⊢X=0\to \left(F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow \left\{⟨0,0⟩,⟨0,1⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
58	55 56 57	3orbi123d	$$⊢X=0\to \left(\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\leftrightarrow \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)\right)$$
59	58	rexbidv	$$⊢X=0\to \left(\exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\leftrightarrow \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)\right)$$
60	54 59	anbi12d	$$⊢X=0\to \left(\left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\leftrightarrow \left(\left\{⟨0,0⟩,⟨0,1⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \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)\right)\right)$$
61	46 60	imbitrrid	$$⊢X=0\to \left(N\in {\mathbb{Z}}_{\ge 3}\to \left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\right)$$
62		1elpr01	$$⊢1\in \left\{0,1\right\}$$
63	62	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1\in \left\{0,1\right\}$$
64	63 19	opelxpd	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to ⟨1,1⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)$$
65		prelpwi	$$⊢\left(⟨0,1⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge ⟨1,1⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)\right)\to \left\{⟨0,1⟩,⟨1,1⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)$$
66	20 64 65	syl2anc	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left\{⟨0,1⟩,⟨1,1⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)$$
67		opeq2	$$⊢x=1\to ⟨0,x⟩=⟨0,1⟩$$
68		oveq1	$$⊢x=1\to x+1=1+1$$
69	68	oveq1d	$$⊢x=1\to \left(x+1\right)\mathrm{mod}N=\left(1+1\right)\mathrm{mod}N$$
70	69	opeq2d	$$⊢x=1\to ⟨0,\left(x+1\right)\mathrm{mod}N⟩=⟨0,\left(1+1\right)\mathrm{mod}N⟩$$
71	67 70	preq12d	$$⊢x=1\to \left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}=\left\{⟨0,1⟩,⟨0,\left(1+1\right)\mathrm{mod}N⟩\right\}$$
72	71	eqeq2d	$$⊢x=1\to \left(\left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,1⟩,⟨0,\left(1+1\right)\mathrm{mod}N⟩\right\}\right)$$
73		opeq2	$$⊢x=1\to ⟨1,x⟩=⟨1,1⟩$$
74	67 73	preq12d	$$⊢x=1\to \left\{⟨0,x⟩,⟨1,x⟩\right\}=\left\{⟨0,1⟩,⟨1,1⟩\right\}$$
75	74	eqeq2d	$$⊢x=1\to \left(\left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\leftrightarrow \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,1⟩,⟨1,1⟩\right\}\right)$$
76	69	opeq2d	$$⊢x=1\to ⟨1,\left(x+1\right)\mathrm{mod}N⟩=⟨1,\left(1+1\right)\mathrm{mod}N⟩$$
77	73 76	preq12d	$$⊢x=1\to \left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}=\left\{⟨1,1⟩,⟨1,\left(1+1\right)\mathrm{mod}N⟩\right\}$$
78	77	eqeq2d	$$⊢x=1\to \left(\left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨1,1⟩,⟨1,\left(1+1\right)\mathrm{mod}N⟩\right\}\right)$$
79	72 75 78	3orbi123d	$$⊢x=1\to \left(\left(\left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\leftrightarrow \left(\left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,1⟩,⟨0,\left(1+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,1⟩,⟨1,1⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨1,1⟩,⟨1,\left(1+1\right)\mathrm{mod}N⟩\right\}\right)\right)$$
80		eqid	$$⊢\left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,1⟩,⟨1,1⟩\right\}$$
81	80	3mix2i	$$⊢\left(\left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,1⟩,⟨0,\left(1+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,1⟩,⟨1,1⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨1,1⟩,⟨1,\left(1+1\right)\mathrm{mod}N⟩\right\}\right)$$
82	81	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(\left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,1⟩,⟨0,\left(1+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,1⟩,⟨1,1⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨1,1⟩,⟨1,\left(1+1\right)\mathrm{mod}N⟩\right\}\right)$$
83	79 19 82	rspcedvdw	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \exists x\in \left(0..^N\right)\left(\left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
84	66 83	jca	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(\left\{⟨0,1⟩,⟨1,1⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(\left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)$$
85		fveq2	$$⊢X=1\to F\left(X\right)=F\left(1\right)$$
86	1	fveq1i	$$⊢F\left(1\right)=⟨“\left\{⟨0,0⟩,⟨0,1⟩\right\}\left\{⟨0,1⟩,⟨1,1⟩\right\}\left\{⟨1,1⟩,⟨1,0⟩\right\}\left\{⟨1,0⟩,⟨0,0⟩\right\}”⟩\left(1\right)$$
87		prex	$$⊢\left\{⟨0,1⟩,⟨1,1⟩\right\}\in \mathrm{V}$$
88		s4fv1	$$⊢\left\{⟨0,1⟩,⟨1,1⟩\right\}\in \mathrm{V}\to ⟨“\left\{⟨0,0⟩,⟨0,1⟩\right\}\left\{⟨0,1⟩,⟨1,1⟩\right\}\left\{⟨1,1⟩,⟨1,0⟩\right\}\left\{⟨1,0⟩,⟨0,0⟩\right\}”⟩\left(1\right)=\left\{⟨0,1⟩,⟨1,1⟩\right\}$$
89	87 88	ax-mp	$$⊢⟨“\left\{⟨0,0⟩,⟨0,1⟩\right\}\left\{⟨0,1⟩,⟨1,1⟩\right\}\left\{⟨1,1⟩,⟨1,0⟩\right\}\left\{⟨1,0⟩,⟨0,0⟩\right\}”⟩\left(1\right)=\left\{⟨0,1⟩,⟨1,1⟩\right\}$$
90	86 89	eqtri	$$⊢F\left(1\right)=\left\{⟨0,1⟩,⟨1,1⟩\right\}$$
91	85 90	eqtrdi	$$⊢X=1\to F\left(X\right)=\left\{⟨0,1⟩,⟨1,1⟩\right\}$$
92	91	eleq1d	$$⊢X=1\to \left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\leftrightarrow \left\{⟨0,1⟩,⟨1,1⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\right)$$
93	91	eqeq1d	$$⊢X=1\to \left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
94	91	eqeq1d	$$⊢X=1\to \left(F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\leftrightarrow \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\right)$$
95	91	eqeq1d	$$⊢X=1\to \left(F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
96	93 94 95	3orbi123d	$$⊢X=1\to \left(\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\leftrightarrow \left(\left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)$$
97	96	rexbidv	$$⊢X=1\to \left(\exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\leftrightarrow \exists x\in \left(0..^N\right)\left(\left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)$$
98	92 97	anbi12d	$$⊢X=1\to \left(\left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\leftrightarrow \left(\left\{⟨0,1⟩,⟨1,1⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(\left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨0,1⟩,⟨1,1⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\right)$$
99	84 98	imbitrrid	$$⊢X=1\to \left(N\in {\mathbb{Z}}_{\ge 3}\to \left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\right)$$
100	61 99	jaoi	$$⊢\left(X=0\vee X=1\right)\to \left(N\in {\mathbb{Z}}_{\ge 3}\to \left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\right)$$
101	6 100	syl	$$⊢X\in \left\{0,1\right\}\to \left(N\in {\mathbb{Z}}_{\ge 3}\to \left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\right)$$
102		elpri	$$⊢X\in \left\{2,3\right\}\to \left(X=2\vee X=3\right)$$
103	63 11	opelxpd	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to ⟨1,0⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)$$
104	64 103	jca	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(⟨1,1⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge ⟨1,0⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)\right)$$
105	104	adantr	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge X=2\right)\to \left(⟨1,1⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge ⟨1,0⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)\right)$$
106		prelpwi	$$⊢\left(⟨1,1⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge ⟨1,0⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)\right)\to \left\{⟨1,1⟩,⟨1,0⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)$$
107	105 106	syl	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge X=2\right)\to \left\{⟨1,1⟩,⟨1,0⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)$$
108	27	eqeq2d	$$⊢x=0\to \left(\left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,0⟩,⟨0,\left(0+1\right)\mathrm{mod}N⟩\right\}\right)$$
109	30	eqeq2d	$$⊢x=0\to \left(\left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\leftrightarrow \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}\right)$$
110	33	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,\left(0+1\right)\mathrm{mod}N⟩\right\}\right)$$
111	108 109 110	3orbi123d	$$⊢x=0\to \left(\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(\left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,0⟩,⟨0,\left(0+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}\vee \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨1,0⟩,⟨1,\left(0+1\right)\mathrm{mod}N⟩\right\}\right)\right)$$
112		prcom	$$⊢\left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨1,0⟩,⟨1,1⟩\right\}$$
113	41	opeq2d	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to ⟨1,1⟩=⟨1,\left(0+1\right)\mathrm{mod}N⟩$$
114	113	preq2d	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left\{⟨1,0⟩,⟨1,1⟩\right\}=\left\{⟨1,0⟩,⟨1,\left(0+1\right)\mathrm{mod}N⟩\right\}$$
115	112 114	eqtrid	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨1,0⟩,⟨1,\left(0+1\right)\mathrm{mod}N⟩\right\}$$
116	115	3mix3d	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(\left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,0⟩,⟨0,\left(0+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}\vee \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨1,0⟩,⟨1,\left(0+1\right)\mathrm{mod}N⟩\right\}\right)$$
117	111 11 116	rspcedvdw	$$⊢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)$$
118	117	adantr	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge X=2\right)\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)$$
119	107 118	jca	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge X=2\right)\to \left(\left\{⟨1,1⟩,⟨1,0⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \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)\right)$$
120		fveq2	$$⊢X=2\to F\left(X\right)=F\left(2\right)$$
121	1	fveq1i	$$⊢F\left(2\right)=⟨“\left\{⟨0,0⟩,⟨0,1⟩\right\}\left\{⟨0,1⟩,⟨1,1⟩\right\}\left\{⟨1,1⟩,⟨1,0⟩\right\}\left\{⟨1,0⟩,⟨0,0⟩\right\}”⟩\left(2\right)$$
122		prex	$$⊢\left\{⟨1,1⟩,⟨1,0⟩\right\}\in \mathrm{V}$$
123		s4fv2	$$⊢\left\{⟨1,1⟩,⟨1,0⟩\right\}\in \mathrm{V}\to ⟨“\left\{⟨0,0⟩,⟨0,1⟩\right\}\left\{⟨0,1⟩,⟨1,1⟩\right\}\left\{⟨1,1⟩,⟨1,0⟩\right\}\left\{⟨1,0⟩,⟨0,0⟩\right\}”⟩\left(2\right)=\left\{⟨1,1⟩,⟨1,0⟩\right\}$$
124	122 123	ax-mp	$$⊢⟨“\left\{⟨0,0⟩,⟨0,1⟩\right\}\left\{⟨0,1⟩,⟨1,1⟩\right\}\left\{⟨1,1⟩,⟨1,0⟩\right\}\left\{⟨1,0⟩,⟨0,0⟩\right\}”⟩\left(2\right)=\left\{⟨1,1⟩,⟨1,0⟩\right\}$$
125	121 124	eqtri	$$⊢F\left(2\right)=\left\{⟨1,1⟩,⟨1,0⟩\right\}$$
126	120 125	eqtrdi	$$⊢X=2\to F\left(X\right)=\left\{⟨1,1⟩,⟨1,0⟩\right\}$$
127	126	eleq1d	$$⊢X=2\to \left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\leftrightarrow \left\{⟨1,1⟩,⟨1,0⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\right)$$
128	126	eqeq1d	$$⊢X=2\to \left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
129	126	eqeq1d	$$⊢X=2\to \left(F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\leftrightarrow \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\right)$$
130	126	eqeq1d	$$⊢X=2\to \left(F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow \left\{⟨1,1⟩,⟨1,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
131	128 129 130	3orbi123d	$$⊢X=2\to \left(\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\leftrightarrow \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)\right)$$
132	131	rexbidv	$$⊢X=2\to \left(\exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\leftrightarrow \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)\right)$$
133	127 132	anbi12d	$$⊢X=2\to \left(\left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\leftrightarrow \left(\left\{⟨1,1⟩,⟨1,0⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \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)\right)\right)$$
134	133	adantl	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge X=2\right)\to \left(\left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\leftrightarrow \left(\left\{⟨1,1⟩,⟨1,0⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \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)\right)\right)$$
135	119 134	mpbird	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge X=2\right)\to \left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)$$
136	135	expcom	$$⊢X=2\to \left(N\in {\mathbb{Z}}_{\ge 3}\to \left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\right)$$
137		prelpwi	$$⊢\left(⟨1,0⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge ⟨0,0⟩\in \left(\left\{0,1\right\}\times \left(0..^N\right)\right)\right)\to \left\{⟨1,0⟩,⟨0,0⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)$$
138	103 12 137	syl2anc	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left\{⟨1,0⟩,⟨0,0⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)$$
139	27	eqeq2d	$$⊢x=0\to \left(\left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,0⟩,⟨0,\left(0+1\right)\mathrm{mod}N⟩\right\}\right)$$
140	30	eqeq2d	$$⊢x=0\to \left(\left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\leftrightarrow \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}\right)$$
141	33	eqeq2d	$$⊢x=0\to \left(\left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨1,0⟩,⟨1,\left(0+1\right)\mathrm{mod}N⟩\right\}\right)$$
142	139 140 141	3orbi123d	$$⊢x=0\to \left(\left(\left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\leftrightarrow \left(\left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,0⟩,⟨0,\left(0+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨1,0⟩,⟨1,\left(0+1\right)\mathrm{mod}N⟩\right\}\right)\right)$$
143		prcom	$$⊢\left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}$$
144	143	3mix2i	$$⊢\left(\left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,0⟩,⟨0,\left(0+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨1,0⟩,⟨1,\left(0+1\right)\mathrm{mod}N⟩\right\}\right)$$
145	144	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(\left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,0⟩,⟨0,\left(0+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨1,0⟩,⟨1,\left(0+1\right)\mathrm{mod}N⟩\right\}\right)$$
146	142 11 145	rspcedvdw	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \exists x\in \left(0..^N\right)\left(\left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
147	138 146	jca	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(\left\{⟨1,0⟩,⟨0,0⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(\left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)$$
148		fveq2	$$⊢X=3\to F\left(X\right)=F\left(3\right)$$
149	1	fveq1i	$$⊢F\left(3\right)=⟨“\left\{⟨0,0⟩,⟨0,1⟩\right\}\left\{⟨0,1⟩,⟨1,1⟩\right\}\left\{⟨1,1⟩,⟨1,0⟩\right\}\left\{⟨1,0⟩,⟨0,0⟩\right\}”⟩\left(3\right)$$
150		prex	$$⊢\left\{⟨1,0⟩,⟨0,0⟩\right\}\in \mathrm{V}$$
151		s4fv3	$$⊢\left\{⟨1,0⟩,⟨0,0⟩\right\}\in \mathrm{V}\to ⟨“\left\{⟨0,0⟩,⟨0,1⟩\right\}\left\{⟨0,1⟩,⟨1,1⟩\right\}\left\{⟨1,1⟩,⟨1,0⟩\right\}\left\{⟨1,0⟩,⟨0,0⟩\right\}”⟩\left(3\right)=\left\{⟨1,0⟩,⟨0,0⟩\right\}$$
152	150 151	ax-mp	$$⊢⟨“\left\{⟨0,0⟩,⟨0,1⟩\right\}\left\{⟨0,1⟩,⟨1,1⟩\right\}\left\{⟨1,1⟩,⟨1,0⟩\right\}\left\{⟨1,0⟩,⟨0,0⟩\right\}”⟩\left(3\right)=\left\{⟨1,0⟩,⟨0,0⟩\right\}$$
153	149 152	eqtri	$$⊢F\left(3\right)=\left\{⟨1,0⟩,⟨0,0⟩\right\}$$
154	148 153	eqtrdi	$$⊢X=3\to F\left(X\right)=\left\{⟨1,0⟩,⟨0,0⟩\right\}$$
155	154	eleq1d	$$⊢X=3\to \left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\leftrightarrow \left\{⟨1,0⟩,⟨0,0⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\right)$$
156	154	eqeq1d	$$⊢X=3\to \left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
157	154	eqeq1d	$$⊢X=3\to \left(F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\leftrightarrow \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\right)$$
158	154	eqeq1d	$$⊢X=3\to \left(F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\leftrightarrow \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)$$
159	156 157 158	3orbi123d	$$⊢X=3\to \left(\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\leftrightarrow \left(\left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)$$
160	159	rexbidv	$$⊢X=3\to \left(\exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\leftrightarrow \exists x\in \left(0..^N\right)\left(\left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)$$
161	155 160	anbi12d	$$⊢X=3\to \left(\left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\leftrightarrow \left(\left\{⟨1,0⟩,⟨0,0⟩\right\}\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(\left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee \left\{⟨1,0⟩,⟨0,0⟩\right\}=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\right)$$
162	147 161	imbitrrid	$$⊢X=3\to \left(N\in {\mathbb{Z}}_{\ge 3}\to \left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\right)$$
163	136 162	jaoi	$$⊢\left(X=2\vee X=3\right)\to \left(N\in {\mathbb{Z}}_{\ge 3}\to \left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\right)$$
164	102 163	syl	$$⊢X\in \left\{2,3\right\}\to \left(N\in {\mathbb{Z}}_{\ge 3}\to \left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\right)$$
165	101 164	jaoi	$$⊢\left(X\in \left\{0,1\right\}\vee X\in \left\{2,3\right\}\right)\to \left(N\in {\mathbb{Z}}_{\ge 3}\to \left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\right)$$
166	5 165	sylbi	$$⊢X\in \left(0..^4\right)\to \left(N\in {\mathbb{Z}}_{\ge 3}\to \left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)\right)$$
167	166	impcom	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge X\in \left(0..^4\right)\right)\to \left(F\left(X\right)\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)\wedge \exists x\in \left(0..^N\right)\left(F\left(X\right)=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee F\left(X\right)=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee F\left(X\right)=\left\{⟨1,x⟩,⟨1,\left(x+1\right)\mathrm{mod}N⟩\right\}\right)\right)$$