Metamath Proof Explorer

Theorem gpgusgralem

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

Ref Expression
Hypotheses gpgusgralem.j ⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
gpgusgralem.i ⊢ 𝐼 = ( 0 ..^ 𝑁 )
Assertion gpgusgralem ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → { 𝑒 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ∣ ∃ 𝑥 ∈ 𝐼 ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ⊆ { 𝑝 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ∣ ( ♯ ‘ 𝑝 ) = 2 } )

Proof

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