gpgiedgdmellem

Description: Lemma for gpgiedgdmel and gpgedgel . (Contributed by AV, 2-Nov-2025)

	Ref	Expression
Hypotheses	gpgvtxel.i	$⊢ I = (0 ..^N)$
	gpgvtxel.j	$⊢ J = (1 ..^⌈\frac{N}{2}⌉)$
Assertion	gpgiedgdmellem	$⊢ (N \in ℕ \land K \in J) \to (\exists x \in I (Y = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor Y = \{⟨0, x⟩, ⟨1, x⟩\} \lor Y = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \to Y \in 𝒫 (\{0, 1\} \times I))$

Proof

Step	Hyp	Ref	Expression
1		gpgvtxel.i	$⊢ I = (0 ..^N)$
2		gpgvtxel.j	$⊢ J = (1 ..^⌈\frac{N}{2}⌉)$
3		prex	$⊢ \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \in V$
4	3	a1i	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \in V$
5		c0ex	$⊢ 0 \in V$
6	5	prid1	$⊢ 0 \in \{0, 1\}$
7	6	a1i	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to 0 \in \{0, 1\}$
8		simpr	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to x \in I$
9	7 8	opelxpd	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to ⟨0, x⟩ \in (\{0, 1\} \times I)$
10		elfzoelz	$⊢ x \in (0 ..^N) \to x \in ℤ$
11	10 1	eleq2s	$⊢ x \in I \to x \in ℤ$
12	11	adantl	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to x \in ℤ$
13	12	peano2zd	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to x + 1 \in ℤ$
14		simpll	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to N \in ℕ$
15		zmodfzo	$⊢ (x + 1 \in ℤ \land N \in ℕ) \to (x + 1) \mod N \in (0 ..^N)$
16	13 14 15	syl2anc	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to (x + 1) \mod N \in (0 ..^N)$
17	16 1	eleqtrrdi	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to (x + 1) \mod N \in I$
18	7 17	opelxpd	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to ⟨0, (x + 1) \mod N⟩ \in (\{0, 1\} \times I)$
19	9 18	prssd	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \subseteq \{0, 1\} \times I$
20	4 19	elpwd	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \in 𝒫 (\{0, 1\} \times I)$
21		eleq1	$⊢ Y = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \to (Y \in 𝒫 (\{0, 1\} \times I) \leftrightarrow \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \in 𝒫 (\{0, 1\} \times I))$
22	20 21	syl5ibrcom	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to (Y = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \to Y \in 𝒫 (\{0, 1\} \times I))$
23		prex	$⊢ \{⟨0, x⟩, ⟨1, x⟩\} \in V$
24	23	a1i	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to \{⟨0, x⟩, ⟨1, x⟩\} \in V$
25		1ex	$⊢ 1 \in V$
26	25	prid2	$⊢ 1 \in \{0, 1\}$
27	26	a1i	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to 1 \in \{0, 1\}$
28	27 8	opelxpd	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to ⟨1, x⟩ \in (\{0, 1\} \times I)$
29	9 28	prssd	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to \{⟨0, x⟩, ⟨1, x⟩\} \subseteq \{0, 1\} \times I$
30	24 29	elpwd	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to \{⟨0, x⟩, ⟨1, x⟩\} \in 𝒫 (\{0, 1\} \times I)$
31		eleq1	$⊢ Y = \{⟨0, x⟩, ⟨1, x⟩\} \to (Y \in 𝒫 (\{0, 1\} \times I) \leftrightarrow \{⟨0, x⟩, ⟨1, x⟩\} \in 𝒫 (\{0, 1\} \times I))$
32	30 31	syl5ibrcom	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to (Y = \{⟨0, x⟩, ⟨1, x⟩\} \to Y \in 𝒫 (\{0, 1\} \times I))$
33		prex	$⊢ \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\} \in V$
34	33	a1i	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\} \in V$
35		elfzoelz	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \to K \in ℤ$
36	35 2	eleq2s	$⊢ K \in J \to K \in ℤ$
37	36	ad2antlr	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to K \in ℤ$
38	12 37	zaddcld	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to x + K \in ℤ$
39		zmodfzo	$⊢ (x + K \in ℤ \land N \in ℕ) \to (x + K) \mod N \in (0 ..^N)$
40	38 14 39	syl2anc	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to (x + K) \mod N \in (0 ..^N)$
41	40 1	eleqtrrdi	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to (x + K) \mod N \in I$
42	27 41	opelxpd	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to ⟨1, (x + K) \mod N⟩ \in (\{0, 1\} \times I)$
43	28 42	prssd	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\} \subseteq \{0, 1\} \times I$
44	34 43	elpwd	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\} \in 𝒫 (\{0, 1\} \times I)$
45		eleq1	$⊢ Y = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\} \to (Y \in 𝒫 (\{0, 1\} \times I) \leftrightarrow \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\} \in 𝒫 (\{0, 1\} \times I))$
46	44 45	syl5ibrcom	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to (Y = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\} \to Y \in 𝒫 (\{0, 1\} \times I))$
47	22 32 46	3jaod	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to ((Y = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor Y = \{⟨0, x⟩, ⟨1, x⟩\} \lor Y = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \to Y \in 𝒫 (\{0, 1\} \times I))$
48	47	rexlimdva	$⊢ (N \in ℕ \land K \in J) \to (\exists x \in I (Y = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor Y = \{⟨0, x⟩, ⟨1, x⟩\} \lor Y = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \to Y \in 𝒫 (\{0, 1\} \times I))$

Metamath Proof Explorer

Theorem gpgiedgdmellem

Proof