Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-rqp Structured version   Unicode version

Definition df-rqp 25091
Description: There is a unique element of  ( ZZ  ^m  ( 0 ... (
p  -  1 ) ) ) ~Qp -equivalent to any element of 
( ZZ  ^m  ZZ ), if the sequences are zero for sufficiently large negative values; this function selects that element. (Contributed by Mario Carneiro, 2-Dec-2014.)
Assertion
Ref Expression
df-rqp  |- /Qp  =  ( p  e.  Prime  |->  (~Qp  i^i  [_ { f  e.  ( ZZ  ^m  ZZ )  |  E. x  e. 
ran  ZZ>= ( `' f
" ( ZZ  \  { 0 } ) )  C_  x }  /  y ]_ (
y  X.  ( y  i^i  ( ZZ  ^m  ( 0 ... (
p  -  1 ) ) ) ) ) ) )
Distinct variable group:    f, p, x, y

Detailed syntax breakdown of Definition df-rqp
StepHypRef Expression
1 crqp 25082 . 2  class /Qp
2 vp . . 3  set  p
3 cprime 13079 . . 3  class  Prime
4 ceqp 25081 . . . 4  class ~Qp
5 vy . . . . 5  set  y
6 vf . . . . . . . . . . 11  set  f
76cv 1651 . . . . . . . . . 10  class  f
87ccnv 4877 . . . . . . . . 9  class  `' f
9 cz 10282 . . . . . . . . . 10  class  ZZ
10 cc0 8990 . . . . . . . . . . 11  class  0
1110csn 3814 . . . . . . . . . 10  class  { 0 }
129, 11cdif 3317 . . . . . . . . 9  class  ( ZZ 
\  { 0 } )
138, 12cima 4881 . . . . . . . 8  class  ( `' f " ( ZZ 
\  { 0 } ) )
14 vx . . . . . . . . 9  set  x
1514cv 1651 . . . . . . . 8  class  x
1613, 15wss 3320 . . . . . . 7  wff  ( `' f " ( ZZ 
\  { 0 } ) )  C_  x
17 cuz 10488 . . . . . . . 8  class  ZZ>=
1817crn 4879 . . . . . . 7  class  ran  ZZ>=
1916, 14, 18wrex 2706 . . . . . 6  wff  E. x  e.  ran  ZZ>= ( `' f
" ( ZZ  \  { 0 } ) )  C_  x
20 cmap 7018 . . . . . . 7  class  ^m
219, 9, 20co 6081 . . . . . 6  class  ( ZZ 
^m  ZZ )
2219, 6, 21crab 2709 . . . . 5  class  { f  e.  ( ZZ  ^m  ZZ )  |  E. x  e.  ran  ZZ>= ( `' f " ( ZZ 
\  { 0 } ) )  C_  x }
235cv 1651 . . . . . 6  class  y
242cv 1651 . . . . . . . . . 10  class  p
25 c1 8991 . . . . . . . . . 10  class  1
26 cmin 9291 . . . . . . . . . 10  class  -
2724, 25, 26co 6081 . . . . . . . . 9  class  ( p  -  1 )
28 cfz 11043 . . . . . . . . 9  class  ...
2910, 27, 28co 6081 . . . . . . . 8  class  ( 0 ... ( p  - 
1 ) )
309, 29, 20co 6081 . . . . . . 7  class  ( ZZ 
^m  ( 0 ... ( p  -  1 ) ) )
3123, 30cin 3319 . . . . . 6  class  ( y  i^i  ( ZZ  ^m  ( 0 ... (
p  -  1 ) ) ) )
3223, 31cxp 4876 . . . . 5  class  ( y  X.  ( y  i^i  ( ZZ  ^m  (
0 ... ( p  - 
1 ) ) ) ) )
335, 22, 32csb 3251 . . . 4  class  [_ {
f  e.  ( ZZ 
^m  ZZ )  |  E. x  e.  ran  ZZ>= ( `' f " ( ZZ  \  { 0 } ) )  C_  x }  /  y ]_ (
y  X.  ( y  i^i  ( ZZ  ^m  ( 0 ... (
p  -  1 ) ) ) ) )
344, 33cin 3319 . . 3  class  (~Qp  i^i  [_ { f  e.  ( ZZ  ^m  ZZ )  |  E. x  e. 
ran  ZZ>= ( `' f
" ( ZZ  \  { 0 } ) )  C_  x }  /  y ]_ (
y  X.  ( y  i^i  ( ZZ  ^m  ( 0 ... (
p  -  1 ) ) ) ) ) )
352, 3, 34cmpt 4266 . 2  class  ( p  e.  Prime  |->  (~Qp  i^i  [_ { f  e.  ( ZZ  ^m  ZZ )  |  E. x  e. 
ran  ZZ>= ( `' f
" ( ZZ  \  { 0 } ) )  C_  x }  /  y ]_ (
y  X.  ( y  i^i  ( ZZ  ^m  ( 0 ... (
p  -  1 ) ) ) ) ) ) )
361, 35wceq 1652 1  wff /Qp  =  ( p  e.  Prime  |->  (~Qp  i^i  [_ { f  e.  ( ZZ  ^m  ZZ )  |  E. x  e. 
ran  ZZ>= ( `' f
" ( ZZ  \  { 0 } ) )  C_  x }  /  y ]_ (
y  X.  ( y  i^i  ( ZZ  ^m  ( 0 ... (
p  -  1 ) ) ) ) ) ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator