Metamath Proof Explorer

Theorem gpgiedgdmellem

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

Ref Expression
Hypotheses gpgvtxel.i ⊢ 𝐼 = ( 0 ..^ 𝑁 )
gpgvtxel.j ⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
Assertion gpgiedgdmellem ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) → ( ∃ 𝑥 ∈ 𝐼 ( 𝑌 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑌 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑌 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) → 𝑌 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ) )

Proof

Step Hyp Ref Expression
1 gpgvtxel.i ⊢ 𝐼 = ( 0 ..^ 𝑁 )
2 gpgvtxel.j ⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
3 prex ⊢ { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∈ V
4 3 a1i ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∈ V )
5 0elpr01 ⊢ 0 ∈ { 0 , 1 }
6 5 a1i ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → 0 ∈ { 0 , 1 } )
7 simpr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → 𝑥 ∈ 𝐼 )
8 6 7 opelxpd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → ⟨ 0 , 𝑥 ⟩ ∈ ( { 0 , 1 } × 𝐼 ) )
9 elfzoelz ⊢ ( 𝑥 ∈ ( 0 ..^ 𝑁 ) → 𝑥 ∈ ℤ )
10 9 1 eleq2s ⊢ ( 𝑥 ∈ 𝐼 → 𝑥 ∈ ℤ )
11 10 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → 𝑥 ∈ ℤ )
12 11 peano2zd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑥 + 1 ) ∈ ℤ )
13 simpll ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → 𝑁 ∈ ℕ )
14 zmodfzo ⊢ ( ( ( 𝑥 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑥 + 1 ) mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
15 12 13 14 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑥 + 1 ) mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
16 15 1 eleqtrrdi ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑥 + 1 ) mod 𝑁 ) ∈ 𝐼 )
17 6 16 opelxpd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × 𝐼 ) )
18 8 17 prssd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ⊆ ( { 0 , 1 } × 𝐼 ) )
19 4 18 elpwd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) )
20 eleq1 ⊢ ( 𝑌 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } → ( 𝑌 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ↔ { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ) )
21 19 20 syl5ibrcom ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑌 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } → 𝑌 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ) )
22 prex ⊢ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∈ V
23 22 a1i ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∈ V )
24 1elpr01 ⊢ 1 ∈ { 0 , 1 }
25 24 a1i ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → 1 ∈ { 0 , 1 } )
26 25 7 opelxpd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → ⟨ 1 , 𝑥 ⟩ ∈ ( { 0 , 1 } × 𝐼 ) )
27 8 26 prssd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ⊆ ( { 0 , 1 } × 𝐼 ) )
28 23 27 elpwd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) )
29 eleq1 ⊢ ( 𝑌 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } → ( 𝑌 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ↔ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ) )
30 28 29 syl5ibrcom ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑌 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } → 𝑌 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ) )
31 prex ⊢ { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ V
32 31 a1i ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ V )
33 elfzoelz ⊢ ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) → 𝐾 ∈ ℤ )
34 33 2 eleq2s ⊢ ( 𝐾 ∈ 𝐽 → 𝐾 ∈ ℤ )
35 34 ad2antlr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → 𝐾 ∈ ℤ )
36 11 35 zaddcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑥 + 𝐾 ) ∈ ℤ )
37 zmodfzo ⊢ ( ( ( 𝑥 + 𝐾 ) ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
38 36 13 37 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
39 38 1 eleqtrrdi ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ∈ 𝐼 )
40 25 39 opelxpd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × 𝐼 ) )
41 26 40 prssd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ⊆ ( { 0 , 1 } × 𝐼 ) )
42 32 41 elpwd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) )
43 eleq1 ⊢ ( 𝑌 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } → ( 𝑌 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ↔ { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ) )
44 42 43 syl5ibrcom ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑌 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } → 𝑌 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ) )
45 21 30 44 3jaod ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑌 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑌 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑌 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) → 𝑌 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ) )
46 45 rexlimdva ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) → ( ∃ 𝑥 ∈ 𝐼 ( 𝑌 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑌 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑌 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) → 𝑌 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ) )