gpgusgralem

Description: Lemma for gpgusgra . (Contributed by AV, 27-Aug-2025) (Proof shortened by AV, 6-Sep-2025)

	Ref	Expression
Hypotheses	gpgusgralem.j	$⊢ J = (1 ..^⌈\frac{N}{2}⌉)$
	gpgusgralem.i	$⊢ I = (0 ..^N)$
Assertion	gpgusgralem	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to \{e \in 𝒫 (\{0, 1\} \times I) \| \exists x \in I (e = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor e = \{⟨0, x⟩, ⟨1, x⟩\} \lor e = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})\} \subseteq \{p \in 𝒫 (\{0, 1\} \times I) \| \|p\| = 2\}$

Proof

Step	Hyp	Ref	Expression
1		gpgusgralem.j	$⊢ J = (1 ..^⌈\frac{N}{2}⌉)$
2		gpgusgralem.i	$⊢ I = (0 ..^N)$
3		uzuzle23	$⊢ N \in ℤ_{\geq 3} \to N \in ℤ_{\geq 2}$
4	3	adantr	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to N \in ℤ_{\geq 2}$
5	4	adantr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land e \in 𝒫 (\{0, 1\} \times I)) \to N \in ℤ_{\geq 2}$
6	2	eleq2i	$⊢ x \in I \leftrightarrow x \in (0 ..^N)$
7	6	biimpi	$⊢ x \in I \to x \in (0 ..^N)$
8		p1modne	$⊢ (N \in ℤ_{\geq 2} \land x \in (0 ..^N)) \to (x + 1) \mod N \neq x$
9	5 7 8	syl2an	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land e \in 𝒫 (\{0, 1\} \times I)) \land x \in I) \to (x + 1) \mod N \neq x$
10	9	necomd	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land e \in 𝒫 (\{0, 1\} \times I)) \land x \in I) \to x \neq (x + 1) \mod N$
11	10	olcd	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land e \in 𝒫 (\{0, 1\} \times I)) \land x \in I) \to (0 \neq 0 \lor x \neq (x + 1) \mod N)$
12		0z	$⊢ 0 \in ℤ$
13		vex	$⊢ x \in V$
14		opthneg	$⊢ (0 \in ℤ \land x \in V) \to (⟨0, x⟩ \neq ⟨0, (x + 1) \mod N⟩ \leftrightarrow (0 \neq 0 \lor x \neq (x + 1) \mod N))$
15	12 13 14	mp2an	$⊢ ⟨0, x⟩ \neq ⟨0, (x + 1) \mod N⟩ \leftrightarrow (0 \neq 0 \lor x \neq (x + 1) \mod N)$
16	11 15	sylibr	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land e \in 𝒫 (\{0, 1\} \times I)) \land x \in I) \to ⟨0, x⟩ \neq ⟨0, (x + 1) \mod N⟩$
17		opex	$⊢ ⟨0, x⟩ \in V$
18		opex	$⊢ ⟨0, (x + 1) \mod N⟩ \in V$
19		hashprg	$⊢ (⟨0, x⟩ \in V \land ⟨0, (x + 1) \mod N⟩ \in V) \to (⟨0, x⟩ \neq ⟨0, (x + 1) \mod N⟩ \leftrightarrow \|\{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\}\| = 2)$
20	17 18 19	mp2an	$⊢ ⟨0, x⟩ \neq ⟨0, (x + 1) \mod N⟩ \leftrightarrow \|\{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\}\| = 2$
21	16 20	sylib	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land e \in 𝒫 (\{0, 1\} \times I)) \land x \in I) \to \|\{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\}\| = 2$
22		fveqeq2	$⊢ e = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \to (\|e\| = 2 \leftrightarrow \|\{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\}\| = 2)$
23	21 22	syl5ibrcom	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land e \in 𝒫 (\{0, 1\} \times I)) \land x \in I) \to (e = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \to \|e\| = 2)$
24		0ne1	$⊢ 0 \neq 1$
25	24	a1i	$⊢ ((((N \in ℤ_{\geq 3} \land K \in J) \land e \in 𝒫 (\{0, 1\} \times I)) \land x \in I) \land e = \{⟨0, x⟩, ⟨1, x⟩\}) \to 0 \neq 1$
26	25	orcd	$⊢ ((((N \in ℤ_{\geq 3} \land K \in J) \land e \in 𝒫 (\{0, 1\} \times I)) \land x \in I) \land e = \{⟨0, x⟩, ⟨1, x⟩\}) \to (0 \neq 1 \lor x \neq x)$
27		opthneg	$⊢ (0 \in ℤ \land x \in V) \to (⟨0, x⟩ \neq ⟨1, x⟩ \leftrightarrow (0 \neq 1 \lor x \neq x))$
28	12 13 27	mp2an	$⊢ ⟨0, x⟩ \neq ⟨1, x⟩ \leftrightarrow (0 \neq 1 \lor x \neq x)$
29	26 28	sylibr	$⊢ ((((N \in ℤ_{\geq 3} \land K \in J) \land e \in 𝒫 (\{0, 1\} \times I)) \land x \in I) \land e = \{⟨0, x⟩, ⟨1, x⟩\}) \to ⟨0, x⟩ \neq ⟨1, x⟩$
30		opex	$⊢ ⟨1, x⟩ \in V$
31		hashprg	$⊢ (⟨0, x⟩ \in V \land ⟨1, x⟩ \in V) \to (⟨0, x⟩ \neq ⟨1, x⟩ \leftrightarrow \|\{⟨0, x⟩, ⟨1, x⟩\}\| = 2)$
32	17 30 31	mp2an	$⊢ ⟨0, x⟩ \neq ⟨1, x⟩ \leftrightarrow \|\{⟨0, x⟩, ⟨1, x⟩\}\| = 2$
33	29 32	sylib	$⊢ ((((N \in ℤ_{\geq 3} \land K \in J) \land e \in 𝒫 (\{0, 1\} \times I)) \land x \in I) \land e = \{⟨0, x⟩, ⟨1, x⟩\}) \to \|\{⟨0, x⟩, ⟨1, x⟩\}\| = 2$
34		fveqeq2	$⊢ e = \{⟨0, x⟩, ⟨1, x⟩\} \to (\|e\| = 2 \leftrightarrow \|\{⟨0, x⟩, ⟨1, x⟩\}\| = 2)$
35	34	adantl	$⊢ ((((N \in ℤ_{\geq 3} \land K \in J) \land e \in 𝒫 (\{0, 1\} \times I)) \land x \in I) \land e = \{⟨0, x⟩, ⟨1, x⟩\}) \to (\|e\| = 2 \leftrightarrow \|\{⟨0, x⟩, ⟨1, x⟩\}\| = 2)$
36	33 35	mpbird	$⊢ ((((N \in ℤ_{\geq 3} \land K \in J) \land e \in 𝒫 (\{0, 1\} \times I)) \land x \in I) \land e = \{⟨0, x⟩, ⟨1, x⟩\}) \to \|e\| = 2$
37	36	ex	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land e \in 𝒫 (\{0, 1\} \times I)) \land x \in I) \to (e = \{⟨0, x⟩, ⟨1, x⟩\} \to \|e\| = 2)$
38		eluzge3nn	$⊢ N \in ℤ_{\geq 3} \to N \in ℕ$
39	38	ad3antrrr	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land e \in 𝒫 (\{0, 1\} \times I)) \land x \in I) \to N \in ℕ$
40		elfzo0	$⊢ x \in (0 ..^N) \leftrightarrow (x \in ℕ_{0} \land N \in ℕ \land x < N)$
41	6 40	bitri	$⊢ x \in I \leftrightarrow (x \in ℕ_{0} \land N \in ℕ \land x < N)$
42		3simpb	$⊢ (x \in ℕ_{0} \land N \in ℕ \land x < N) \to (x \in ℕ_{0} \land x < N)$
43	41 42	sylbi	$⊢ x \in I \to (x \in ℕ_{0} \land x < N)$
44	43	adantl	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land e \in 𝒫 (\{0, 1\} \times I)) \land x \in I) \to (x \in ℕ_{0} \land x < N)$
45	1	eleq2i	$⊢ K \in J \leftrightarrow K \in (1 ..^⌈\frac{N}{2}⌉)$
46		elfzo1	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \leftrightarrow (K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land K < ⌈\frac{N}{2}⌉)$
47	45 46	bitri	$⊢ K \in J \leftrightarrow (K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land K < ⌈\frac{N}{2}⌉)$
48		simpl1	$⊢ ((K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land K < ⌈\frac{N}{2}⌉) \land N \in ℤ_{\geq 3}) \to K \in ℕ$
49		nnre	$⊢ K \in ℕ \to K \in ℝ$
50		nnre	$⊢ ⌈\frac{N}{2}⌉ \in ℕ \to ⌈\frac{N}{2}⌉ \in ℝ$
51		eluzelre	$⊢ N \in ℤ_{\geq 3} \to N \in ℝ$
52	49 50 51	3anim123i	$⊢ (K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land N \in ℤ_{\geq 3}) \to (K \in ℝ \land ⌈\frac{N}{2}⌉ \in ℝ \land N \in ℝ)$
53	51	rehalfcld	$⊢ N \in ℤ_{\geq 3} \to \frac{N}{2} \in ℝ$
54	53	adantl	$⊢ (K \in ℕ \land N \in ℤ_{\geq 3}) \to \frac{N}{2} \in ℝ$
55		eluzelz	$⊢ N \in ℤ_{\geq 3} \to N \in ℤ$
56	55	adantl	$⊢ (K \in ℕ \land N \in ℤ_{\geq 3}) \to N \in ℤ$
57		eluz2	$⊢ N \in ℤ_{\geq 3} \leftrightarrow (3 \in ℤ \land N \in ℤ \land 3 \leq N)$
58		simp2	$⊢ (3 \in ℤ \land N \in ℤ \land 3 \leq N) \to N \in ℤ$
59		0re	$⊢ 0 \in ℝ$
60	59	a1i	$⊢ (N \in ℤ \land 3 \leq N) \to 0 \in ℝ$
61		3re	$⊢ 3 \in ℝ$
62	61	a1i	$⊢ (N \in ℤ \land 3 \leq N) \to 3 \in ℝ$
63		zre	$⊢ N \in ℤ \to N \in ℝ$
64	63	adantr	$⊢ (N \in ℤ \land 3 \leq N) \to N \in ℝ$
65		3pos	$⊢ 0 < 3$
66	59 61 65	ltleii	$⊢ 0 \leq 3$
67	66	a1i	$⊢ (N \in ℤ \land 3 \leq N) \to 0 \leq 3$
68		simpr	$⊢ (N \in ℤ \land 3 \leq N) \to 3 \leq N$
69	60 62 64 67 68	letrd	$⊢ (N \in ℤ \land 3 \leq N) \to 0 \leq N$
70	69	3adant1	$⊢ (3 \in ℤ \land N \in ℤ \land 3 \leq N) \to 0 \leq N$
71	58 70	jca	$⊢ (3 \in ℤ \land N \in ℤ \land 3 \leq N) \to (N \in ℤ \land 0 \leq N)$
72		elnn0z	$⊢ N \in ℕ_{0} \leftrightarrow (N \in ℤ \land 0 \leq N)$
73	71 72	sylibr	$⊢ (3 \in ℤ \land N \in ℤ \land 3 \leq N) \to N \in ℕ_{0}$
74	57 73	sylbi	$⊢ N \in ℤ_{\geq 3} \to N \in ℕ_{0}$
75		2nn	$⊢ 2 \in ℕ$
76	75	a1i	$⊢ (K \in ℕ \land N \in ℤ_{\geq 3}) \to 2 \in ℕ$
77		nn0ledivnn	$⊢ (N \in ℕ_{0} \land 2 \in ℕ) \to \frac{N}{2} \leq N$
78	74 76 77	syl2an2	$⊢ (K \in ℕ \land N \in ℤ_{\geq 3}) \to \frac{N}{2} \leq N$
79	54 56 78	3jca	$⊢ (K \in ℕ \land N \in ℤ_{\geq 3}) \to (\frac{N}{2} \in ℝ \land N \in ℤ \land \frac{N}{2} \leq N)$
80	79	3adant2	$⊢ (K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land N \in ℤ_{\geq 3}) \to (\frac{N}{2} \in ℝ \land N \in ℤ \land \frac{N}{2} \leq N)$
81		ceille	$⊢ (\frac{N}{2} \in ℝ \land N \in ℤ \land \frac{N}{2} \leq N) \to ⌈\frac{N}{2}⌉ \leq N$
82	80 81	syl	$⊢ (K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land N \in ℤ_{\geq 3}) \to ⌈\frac{N}{2}⌉ \leq N$
83	52 82	lelttrdi	$⊢ (K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land N \in ℤ_{\geq 3}) \to (K < ⌈\frac{N}{2}⌉ \to K < N)$
84	83	3exp	$⊢ K \in ℕ \to (⌈\frac{N}{2}⌉ \in ℕ \to (N \in ℤ_{\geq 3} \to (K < ⌈\frac{N}{2}⌉ \to K < N)))$
85	84	com34	$⊢ K \in ℕ \to (⌈\frac{N}{2}⌉ \in ℕ \to (K < ⌈\frac{N}{2}⌉ \to (N \in ℤ_{\geq 3} \to K < N)))$
86	85	3imp1	$⊢ ((K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land K < ⌈\frac{N}{2}⌉) \land N \in ℤ_{\geq 3}) \to K < N$
87	48 86	jca	$⊢ ((K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land K < ⌈\frac{N}{2}⌉) \land N \in ℤ_{\geq 3}) \to (K \in ℕ \land K < N)$
88	87	ex	$⊢ (K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land K < ⌈\frac{N}{2}⌉) \to (N \in ℤ_{\geq 3} \to (K \in ℕ \land K < N))$
89	47 88	sylbi	$⊢ K \in J \to (N \in ℤ_{\geq 3} \to (K \in ℕ \land K < N))$
90	89	impcom	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to (K \in ℕ \land K < N)$
91	90	adantr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land e \in 𝒫 (\{0, 1\} \times I)) \to (K \in ℕ \land K < N)$
92	91	adantr	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land e \in 𝒫 (\{0, 1\} \times I)) \land x \in I) \to (K \in ℕ \land K < N)$
93		addmodne	$⊢ (N \in ℕ \land (x \in ℕ_{0} \land x < N) \land (K \in ℕ \land K < N)) \to (x + K) \mod N \neq x$
94	39 44 92 93	syl3anc	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land e \in 𝒫 (\{0, 1\} \times I)) \land x \in I) \to (x + K) \mod N \neq x$
95	94	necomd	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land e \in 𝒫 (\{0, 1\} \times I)) \land x \in I) \to x \neq (x + K) \mod N$
96	95	olcd	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land e \in 𝒫 (\{0, 1\} \times I)) \land x \in I) \to (1 \neq 1 \lor x \neq (x + K) \mod N)$
97		1z	$⊢ 1 \in ℤ$
98		opthneg	$⊢ (1 \in ℤ \land x \in V) \to (⟨1, x⟩ \neq ⟨1, (x + K) \mod N⟩ \leftrightarrow (1 \neq 1 \lor x \neq (x + K) \mod N))$
99	97 13 98	mp2an	$⊢ ⟨1, x⟩ \neq ⟨1, (x + K) \mod N⟩ \leftrightarrow (1 \neq 1 \lor x \neq (x + K) \mod N)$
100	96 99	sylibr	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land e \in 𝒫 (\{0, 1\} \times I)) \land x \in I) \to ⟨1, x⟩ \neq ⟨1, (x + K) \mod N⟩$
101		opex	$⊢ ⟨1, (x + K) \mod N⟩ \in V$
102		hashprg	$⊢ (⟨1, x⟩ \in V \land ⟨1, (x + K) \mod N⟩ \in V) \to (⟨1, x⟩ \neq ⟨1, (x + K) \mod N⟩ \leftrightarrow \|\{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}\| = 2)$
103	30 101 102	mp2an	$⊢ ⟨1, x⟩ \neq ⟨1, (x + K) \mod N⟩ \leftrightarrow \|\{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}\| = 2$
104	100 103	sylib	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land e \in 𝒫 (\{0, 1\} \times I)) \land x \in I) \to \|\{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}\| = 2$
105		fveqeq2	$⊢ e = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\} \to (\|e\| = 2 \leftrightarrow \|\{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}\| = 2)$
106	104 105	syl5ibrcom	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land e \in 𝒫 (\{0, 1\} \times I)) \land x \in I) \to (e = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\} \to \|e\| = 2)$
107	23 37 106	3jaod	$⊢ (((N \in ℤ_{\geq 3} \land K \in J) \land e \in 𝒫 (\{0, 1\} \times I)) \land x \in I) \to ((e = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor e = \{⟨0, x⟩, ⟨1, x⟩\} \lor e = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \to \|e\| = 2)$
108	107	rexlimdva	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land e \in 𝒫 (\{0, 1\} \times I)) \to (\exists x \in I (e = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor e = \{⟨0, x⟩, ⟨1, x⟩\} \lor e = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \to \|e\| = 2)$
109	108	ss2rabdv	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to \{e \in 𝒫 (\{0, 1\} \times I) \| \exists x \in I (e = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor e = \{⟨0, x⟩, ⟨1, x⟩\} \lor e = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})\} \subseteq \{e \in 𝒫 (\{0, 1\} \times I) \| \|e\| = 2\}$
110		fveqeq2	$⊢ p = e \to (\|p\| = 2 \leftrightarrow \|e\| = 2)$
111	110	cbvrabv	$⊢ \{p \in 𝒫 (\{0, 1\} \times I) \| \|p\| = 2\} = \{e \in 𝒫 (\{0, 1\} \times I) \| \|e\| = 2\}$
112	109 111	sseqtrrdi	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to \{e \in 𝒫 (\{0, 1\} \times I) \| \exists x \in I (e = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor e = \{⟨0, x⟩, ⟨1, x⟩\} \lor e = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})\} \subseteq \{p \in 𝒫 (\{0, 1\} \times I) \| \|p\| = 2\}$

Metamath Proof Explorer

Theorem gpgusgralem

Proof