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 
|- J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
gpgusgralem.i 
|- I = ( 0 ..^ N )
Assertion gpgusgralem 
|- ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> { e e. ~P ( { 0 , 1 } X. I ) | E. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } C_ { p e. ~P ( { 0 , 1 } X. I ) | ( # ` p ) = 2 } )

Proof

Step Hyp Ref Expression
1 gpgusgralem.j 
 |-  J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
2 gpgusgralem.i 
 |-  I = ( 0 ..^ N )
3 uzuzle23 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ( ZZ>= ` 2 ) )
4 3 adantr 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> N e. ( ZZ>= ` 2 ) )
5 4 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ e e. ~P ( { 0 , 1 } X. I ) ) -> N e. ( ZZ>= ` 2 ) )
6 2 eleq2i 
 |-  ( x e. I <-> x e. ( 0 ..^ N ) )
7 6 biimpi 
 |-  ( x e. I -> x e. ( 0 ..^ N ) )
8 p1modne 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ x e. ( 0 ..^ N ) ) -> ( ( x + 1 ) mod N ) =/= x )
9 5 7 8 syl2an 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ e e. ~P ( { 0 , 1 } X. I ) ) /\ x e. I ) -> ( ( x + 1 ) mod N ) =/= x )
10 9 necomd 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ e e. ~P ( { 0 , 1 } X. I ) ) /\ x e. I ) -> x =/= ( ( x + 1 ) mod N ) )
11 10 olcd 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ e e. ~P ( { 0 , 1 } X. I ) ) /\ x e. I ) -> ( 0 =/= 0 \/ x =/= ( ( x + 1 ) mod N ) ) )
12 0z 
 |-  0 e. ZZ
13 vex 
 |-  x e. _V
14 opthneg 
 |-  ( ( 0 e. ZZ /\ x e. _V ) -> ( <. 0 , x >. =/= <. 0 , ( ( x + 1 ) mod N ) >. <-> ( 0 =/= 0 \/ x =/= ( ( x + 1 ) mod N ) ) ) )
15 12 13 14 mp2an 
 |-  ( <. 0 , x >. =/= <. 0 , ( ( x + 1 ) mod N ) >. <-> ( 0 =/= 0 \/ x =/= ( ( x + 1 ) mod N ) ) )
16 11 15 sylibr 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ e e. ~P ( { 0 , 1 } X. I ) ) /\ x e. I ) -> <. 0 , x >. =/= <. 0 , ( ( x + 1 ) mod N ) >. )
17 opex 
 |-  <. 0 , x >. e. _V
18 opex 
 |-  <. 0 , ( ( x + 1 ) mod N ) >. e. _V
19 hashprg 
 |-  ( ( <. 0 , x >. e. _V /\ <. 0 , ( ( x + 1 ) mod N ) >. e. _V ) -> ( <. 0 , x >. =/= <. 0 , ( ( x + 1 ) mod N ) >. <-> ( # ` { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } ) = 2 ) )
20 17 18 19 mp2an 
 |-  ( <. 0 , x >. =/= <. 0 , ( ( x + 1 ) mod N ) >. <-> ( # ` { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } ) = 2 )
21 16 20 sylib 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ e e. ~P ( { 0 , 1 } X. I ) ) /\ x e. I ) -> ( # ` { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } ) = 2 )
22 fveqeq2 
 |-  ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } -> ( ( # ` e ) = 2 <-> ( # ` { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } ) = 2 ) )
23 21 22 syl5ibrcom 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ e e. ~P ( { 0 , 1 } X. I ) ) /\ x e. I ) -> ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } -> ( # ` e ) = 2 ) )
24 0ne1 
 |-  0 =/= 1
25 24 a1i 
 |-  ( ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ e e. ~P ( { 0 , 1 } X. I ) ) /\ x e. I ) /\ e = { <. 0 , x >. , <. 1 , x >. } ) -> 0 =/= 1 )
26 25 orcd 
 |-  ( ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ e e. ~P ( { 0 , 1 } X. I ) ) /\ x e. I ) /\ e = { <. 0 , x >. , <. 1 , x >. } ) -> ( 0 =/= 1 \/ x =/= x ) )
27 opthneg 
 |-  ( ( 0 e. ZZ /\ x e. _V ) -> ( <. 0 , x >. =/= <. 1 , x >. <-> ( 0 =/= 1 \/ x =/= x ) ) )
28 12 13 27 mp2an 
 |-  ( <. 0 , x >. =/= <. 1 , x >. <-> ( 0 =/= 1 \/ x =/= x ) )
29 26 28 sylibr 
 |-  ( ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ e e. ~P ( { 0 , 1 } X. I ) ) /\ x e. I ) /\ e = { <. 0 , x >. , <. 1 , x >. } ) -> <. 0 , x >. =/= <. 1 , x >. )
30 opex 
 |-  <. 1 , x >. e. _V
31 hashprg 
 |-  ( ( <. 0 , x >. e. _V /\ <. 1 , x >. e. _V ) -> ( <. 0 , x >. =/= <. 1 , x >. <-> ( # ` { <. 0 , x >. , <. 1 , x >. } ) = 2 ) )
32 17 30 31 mp2an 
 |-  ( <. 0 , x >. =/= <. 1 , x >. <-> ( # ` { <. 0 , x >. , <. 1 , x >. } ) = 2 )
33 29 32 sylib 
 |-  ( ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ e e. ~P ( { 0 , 1 } X. I ) ) /\ x e. I ) /\ e = { <. 0 , x >. , <. 1 , x >. } ) -> ( # ` { <. 0 , x >. , <. 1 , x >. } ) = 2 )
34 fveqeq2 
 |-  ( e = { <. 0 , x >. , <. 1 , x >. } -> ( ( # ` e ) = 2 <-> ( # ` { <. 0 , x >. , <. 1 , x >. } ) = 2 ) )
35 34 adantl 
 |-  ( ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ e e. ~P ( { 0 , 1 } X. I ) ) /\ x e. I ) /\ e = { <. 0 , x >. , <. 1 , x >. } ) -> ( ( # ` e ) = 2 <-> ( # ` { <. 0 , x >. , <. 1 , x >. } ) = 2 ) )
36 33 35 mpbird 
 |-  ( ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ e e. ~P ( { 0 , 1 } X. I ) ) /\ x e. I ) /\ e = { <. 0 , x >. , <. 1 , x >. } ) -> ( # ` e ) = 2 )
37 36 ex 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ e e. ~P ( { 0 , 1 } X. I ) ) /\ x e. I ) -> ( e = { <. 0 , x >. , <. 1 , x >. } -> ( # ` e ) = 2 ) )
38 eluzge3nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. NN )
39 38 ad3antrrr 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ e e. ~P ( { 0 , 1 } X. I ) ) /\ x e. I ) -> N e. NN )
40 elfzo0 
 |-  ( x e. ( 0 ..^ N ) <-> ( x e. NN0 /\ N e. NN /\ x < N ) )
41 6 40 bitri 
 |-  ( x e. I <-> ( x e. NN0 /\ N e. NN /\ x < N ) )
42 3simpb 
 |-  ( ( x e. NN0 /\ N e. NN /\ x < N ) -> ( x e. NN0 /\ x < N ) )
43 41 42 sylbi 
 |-  ( x e. I -> ( x e. NN0 /\ x < N ) )
44 43 adantl 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ e e. ~P ( { 0 , 1 } X. I ) ) /\ x e. I ) -> ( x e. NN0 /\ x < N ) )
45 1 eleq2i 
 |-  ( K e. J <-> K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) )
46 elfzo1 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) <-> ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ K < ( |^ ` ( N / 2 ) ) ) )
47 45 46 bitri 
 |-  ( K e. J <-> ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ K < ( |^ ` ( N / 2 ) ) ) )
48 simpl1 
 |-  ( ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ K < ( |^ ` ( N / 2 ) ) ) /\ N e. ( ZZ>= ` 3 ) ) -> K e. NN )
49 nnre 
 |-  ( K e. NN -> K e. RR )
50 nnre 
 |-  ( ( |^ ` ( N / 2 ) ) e. NN -> ( |^ ` ( N / 2 ) ) e. RR )
51 eluzelre 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. RR )
52 49 50 51 3anim123i 
 |-  ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ N e. ( ZZ>= ` 3 ) ) -> ( K e. RR /\ ( |^ ` ( N / 2 ) ) e. RR /\ N e. RR ) )
53 51 rehalfcld 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N / 2 ) e. RR )
54 53 adantl 
 |-  ( ( K e. NN /\ N e. ( ZZ>= ` 3 ) ) -> ( N / 2 ) e. RR )
55 eluzelz 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ZZ )
56 55 adantl 
 |-  ( ( K e. NN /\ N e. ( ZZ>= ` 3 ) ) -> N e. ZZ )
57 eluz2 
 |-  ( N e. ( ZZ>= ` 3 ) <-> ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) )
58 simp2 
 |-  ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> N e. ZZ )
59 0re 
 |-  0 e. RR
60 59 a1i 
 |-  ( ( N e. ZZ /\ 3 <_ N ) -> 0 e. RR )
61 3re 
 |-  3 e. RR
62 61 a1i 
 |-  ( ( N e. ZZ /\ 3 <_ N ) -> 3 e. RR )
63 zre 
 |-  ( N e. ZZ -> N e. RR )
64 63 adantr 
 |-  ( ( N e. ZZ /\ 3 <_ N ) -> N e. RR )
65 3pos 
 |-  0 < 3
66 59 61 65 ltleii 
 |-  0 <_ 3
67 66 a1i 
 |-  ( ( N e. ZZ /\ 3 <_ N ) -> 0 <_ 3 )
68 simpr 
 |-  ( ( N e. ZZ /\ 3 <_ N ) -> 3 <_ N )
69 60 62 64 67 68 letrd 
 |-  ( ( N e. ZZ /\ 3 <_ N ) -> 0 <_ N )
70 69 3adant1 
 |-  ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> 0 <_ N )
71 58 70 jca 
 |-  ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> ( N e. ZZ /\ 0 <_ N ) )
72 elnn0z 
 |-  ( N e. NN0 <-> ( N e. ZZ /\ 0 <_ N ) )
73 71 72 sylibr 
 |-  ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> N e. NN0 )
74 57 73 sylbi 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. NN0 )
75 2nn 
 |-  2 e. NN
76 75 a1i 
 |-  ( ( K e. NN /\ N e. ( ZZ>= ` 3 ) ) -> 2 e. NN )
77 nn0ledivnn 
 |-  ( ( N e. NN0 /\ 2 e. NN ) -> ( N / 2 ) <_ N )
78 74 76 77 syl2an2 
 |-  ( ( K e. NN /\ N e. ( ZZ>= ` 3 ) ) -> ( N / 2 ) <_ N )
79 54 56 78 3jca 
 |-  ( ( K e. NN /\ N e. ( ZZ>= ` 3 ) ) -> ( ( N / 2 ) e. RR /\ N e. ZZ /\ ( N / 2 ) <_ N ) )
80 79 3adant2 
 |-  ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ N e. ( ZZ>= ` 3 ) ) -> ( ( N / 2 ) e. RR /\ N e. ZZ /\ ( N / 2 ) <_ N ) )
81 ceille 
 |-  ( ( ( N / 2 ) e. RR /\ N e. ZZ /\ ( N / 2 ) <_ N ) -> ( |^ ` ( N / 2 ) ) <_ N )
82 80 81 syl 
 |-  ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ N e. ( ZZ>= ` 3 ) ) -> ( |^ ` ( N / 2 ) ) <_ N )
83 52 82 lelttrdi 
 |-  ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ N e. ( ZZ>= ` 3 ) ) -> ( K < ( |^ ` ( N / 2 ) ) -> K < N ) )
84 83 3exp 
 |-  ( K e. NN -> ( ( |^ ` ( N / 2 ) ) e. NN -> ( N e. ( ZZ>= ` 3 ) -> ( K < ( |^ ` ( N / 2 ) ) -> K < N ) ) ) )
85 84 com34 
 |-  ( K e. NN -> ( ( |^ ` ( N / 2 ) ) e. NN -> ( K < ( |^ ` ( N / 2 ) ) -> ( N e. ( ZZ>= ` 3 ) -> K < N ) ) ) )
86 85 3imp1 
 |-  ( ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ K < ( |^ ` ( N / 2 ) ) ) /\ N e. ( ZZ>= ` 3 ) ) -> K < N )
87 48 86 jca 
 |-  ( ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ K < ( |^ ` ( N / 2 ) ) ) /\ N e. ( ZZ>= ` 3 ) ) -> ( K e. NN /\ K < N ) )
88 87 ex 
 |-  ( ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ K < ( |^ ` ( N / 2 ) ) ) -> ( N e. ( ZZ>= ` 3 ) -> ( K e. NN /\ K < N ) ) )
89 47 88 sylbi 
 |-  ( K e. J -> ( N e. ( ZZ>= ` 3 ) -> ( K e. NN /\ K < N ) ) )
90 89 impcom 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( K e. NN /\ K < N ) )
91 90 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ e e. ~P ( { 0 , 1 } X. I ) ) -> ( K e. NN /\ K < N ) )
92 91 adantr 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ e e. ~P ( { 0 , 1 } X. I ) ) /\ x e. I ) -> ( K e. NN /\ K < N ) )
93 addmodne 
 |-  ( ( N e. NN /\ ( x e. NN0 /\ x < N ) /\ ( K e. NN /\ K < N ) ) -> ( ( x + K ) mod N ) =/= x )
94 39 44 92 93 syl3anc 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ e e. ~P ( { 0 , 1 } X. I ) ) /\ x e. I ) -> ( ( x + K ) mod N ) =/= x )
95 94 necomd 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ e e. ~P ( { 0 , 1 } X. I ) ) /\ x e. I ) -> x =/= ( ( x + K ) mod N ) )
96 95 olcd 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ e e. ~P ( { 0 , 1 } X. I ) ) /\ x e. I ) -> ( 1 =/= 1 \/ x =/= ( ( x + K ) mod N ) ) )
97 1z 
 |-  1 e. ZZ
98 opthneg 
 |-  ( ( 1 e. ZZ /\ x e. _V ) -> ( <. 1 , x >. =/= <. 1 , ( ( x + K ) mod N ) >. <-> ( 1 =/= 1 \/ x =/= ( ( x + K ) mod N ) ) ) )
99 97 13 98 mp2an 
 |-  ( <. 1 , x >. =/= <. 1 , ( ( x + K ) mod N ) >. <-> ( 1 =/= 1 \/ x =/= ( ( x + K ) mod N ) ) )
100 96 99 sylibr 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ e e. ~P ( { 0 , 1 } X. I ) ) /\ x e. I ) -> <. 1 , x >. =/= <. 1 , ( ( x + K ) mod N ) >. )
101 opex 
 |-  <. 1 , ( ( x + K ) mod N ) >. e. _V
102 hashprg 
 |-  ( ( <. 1 , x >. e. _V /\ <. 1 , ( ( x + K ) mod N ) >. e. _V ) -> ( <. 1 , x >. =/= <. 1 , ( ( x + K ) mod N ) >. <-> ( # ` { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) = 2 ) )
103 30 101 102 mp2an 
 |-  ( <. 1 , x >. =/= <. 1 , ( ( x + K ) mod N ) >. <-> ( # ` { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) = 2 )
104 100 103 sylib 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ e e. ~P ( { 0 , 1 } X. I ) ) /\ x e. I ) -> ( # ` { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) = 2 )
105 fveqeq2 
 |-  ( e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } -> ( ( # ` e ) = 2 <-> ( # ` { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) = 2 ) )
106 104 105 syl5ibrcom 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ e e. ~P ( { 0 , 1 } X. I ) ) /\ x e. I ) -> ( e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } -> ( # ` e ) = 2 ) )
107 23 37 106 3jaod 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ e e. ~P ( { 0 , 1 } X. I ) ) /\ x e. I ) -> ( ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) -> ( # ` e ) = 2 ) )
108 107 rexlimdva 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ e e. ~P ( { 0 , 1 } X. I ) ) -> ( E. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) -> ( # ` e ) = 2 ) )
109 108 ss2rabdv 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> { e e. ~P ( { 0 , 1 } X. I ) | E. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } C_ { e e. ~P ( { 0 , 1 } X. I ) | ( # ` e ) = 2 } )
110 fveqeq2 
 |-  ( p = e -> ( ( # ` p ) = 2 <-> ( # ` e ) = 2 ) )
111 110 cbvrabv 
 |-  { p e. ~P ( { 0 , 1 } X. I ) | ( # ` p ) = 2 } = { e e. ~P ( { 0 , 1 } X. I ) | ( # ` e ) = 2 }
112 109 111 sseqtrrdi 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> { e e. ~P ( { 0 , 1 } X. I ) | E. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } C_ { p e. ~P ( { 0 , 1 } X. I ) | ( # ` p ) = 2 } )