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