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		0elpr01	$⊢ 0 \in \{0, 1\}$
6	5	a1i	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to 0 \in \{0, 1\}$
7		simpr	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to x \in I$
8	6 7	opelxpd	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to ⟨0, x⟩ \in (\{0, 1\} \times I)$
9		elfzoelz	$⊢ x \in (0 ..^N) \to x \in ℤ$
10	9 1	eleq2s	$⊢ x \in I \to x \in ℤ$
11	10	adantl	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to x \in ℤ$
12	11	peano2zd	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to x + 1 \in ℤ$
13		simpll	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to N \in ℕ$
14		zmodfzo	$⊢ (x + 1 \in ℤ \land N \in ℕ) \to (x + 1) \mod N \in (0 ..^N)$
15	12 13 14	syl2anc	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to (x + 1) \mod N \in (0 ..^N)$
16	15 1	eleqtrrdi	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to (x + 1) \mod N \in I$
17	6 16	opelxpd	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to ⟨0, (x + 1) \mod N⟩ \in (\{0, 1\} \times I)$
18	8 17	prssd	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \subseteq \{0, 1\} \times I$
19	4 18	elpwd	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \in 𝒫 (\{0, 1\} \times I)$
20		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))$
21	19 20	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))$
22		prex	$⊢ \{⟨0, x⟩, ⟨1, x⟩\} \in V$
23	22	a1i	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to \{⟨0, x⟩, ⟨1, x⟩\} \in V$
24		1elpr01	$⊢ 1 \in \{0, 1\}$
25	24	a1i	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to 1 \in \{0, 1\}$
26	25 7	opelxpd	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to ⟨1, x⟩ \in (\{0, 1\} \times I)$
27	8 26	prssd	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to \{⟨0, x⟩, ⟨1, x⟩\} \subseteq \{0, 1\} \times I$
28	23 27	elpwd	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to \{⟨0, x⟩, ⟨1, x⟩\} \in 𝒫 (\{0, 1\} \times I)$
29		eleq1	$⊢ Y = \{⟨0, x⟩, ⟨1, x⟩\} \to (Y \in 𝒫 (\{0, 1\} \times I) \leftrightarrow \{⟨0, x⟩, ⟨1, x⟩\} \in 𝒫 (\{0, 1\} \times I))$
30	28 29	syl5ibrcom	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to (Y = \{⟨0, x⟩, ⟨1, x⟩\} \to Y \in 𝒫 (\{0, 1\} \times I))$
31		prex	$⊢ \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\} \in V$
32	31	a1i	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\} \in V$
33		elfzoelz	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \to K \in ℤ$
34	33 2	eleq2s	$⊢ K \in J \to K \in ℤ$
35	34	ad2antlr	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to K \in ℤ$
36	11 35	zaddcld	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to x + K \in ℤ$
37		zmodfzo	$⊢ (x + K \in ℤ \land N \in ℕ) \to (x + K) \mod N \in (0 ..^N)$
38	36 13 37	syl2anc	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to (x + K) \mod N \in (0 ..^N)$
39	38 1	eleqtrrdi	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to (x + K) \mod N \in I$
40	25 39	opelxpd	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to ⟨1, (x + K) \mod N⟩ \in (\{0, 1\} \times I)$
41	26 40	prssd	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\} \subseteq \{0, 1\} \times I$
42	32 41	elpwd	$⊢ ((N \in ℕ \land K \in J) \land x \in I) \to \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\} \in 𝒫 (\{0, 1\} \times I)$
43		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))$
44	42 43	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))$
45	21 30 44	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))$
46	45	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