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

Definition df-rqp 23987
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 23978 . 2  class /Qp
2 vp . . 3  set  p
3 cprime 12758 . . 3  class  Prime
4 ceqp 23977 . . . 4  class ~Qp
5 vy . . . . 5  set  y
6 vf . . . . . . . . . . 11  set  f
76cv 1622 . . . . . . . . . 10  class  f
87ccnv 4688 . . . . . . . . 9  class  `' f
9 cz 10024 . . . . . . . . . 10  class  ZZ
10 cc0 8737 . . . . . . . . . . 11  class  0
1110csn 3640 . . . . . . . . . 10  class  { 0 }
129, 11cdif 3149 . . . . . . . . 9  class  ( ZZ 
\  { 0 } )
138, 12cima 4692 . . . . . . . 8  class  ( `' f " ( ZZ 
\  { 0 } ) )
14 vx . . . . . . . . 9  set  x
1514cv 1622 . . . . . . . 8  class  x
1613, 15wss 3152 . . . . . . 7  wff  ( `' f " ( ZZ 
\  { 0 } ) )  C_  x
17 cuz 10230 . . . . . . . 8  class  ZZ>=
1817crn 4690 . . . . . . 7  class  ran  ZZ>=
1916, 14, 18wrex 2544 . . . . . 6  wff  E. x  e.  ran  ZZ>= ( `' f
" ( ZZ  \  { 0 } ) )  C_  x
20 cmap 6772 . . . . . . 7  class  ^m
219, 9, 20co 5858 . . . . . 6  class  ( ZZ 
^m  ZZ )
2219, 6, 21crab 2547 . . . . 5  class  { f  e.  ( ZZ  ^m  ZZ )  |  E. x  e.  ran  ZZ>= ( `' f " ( ZZ 
\  { 0 } ) )  C_  x }
235cv 1622 . . . . . 6  class  y
242cv 1622 . . . . . . . . . 10  class  p
25 c1 8738 . . . . . . . . . 10  class  1
26 cmin 9037 . . . . . . . . . 10  class  -
2724, 25, 26co 5858 . . . . . . . . 9  class  ( p  -  1 )
28 cfz 10782 . . . . . . . . 9  class  ...
2910, 27, 28co 5858 . . . . . . . 8  class  ( 0 ... ( p  - 
1 ) )
309, 29, 20co 5858 . . . . . . 7  class  ( ZZ 
^m  ( 0 ... ( p  -  1 ) ) )
3123, 30cin 3151 . . . . . 6  class  ( y  i^i  ( ZZ  ^m  ( 0 ... (
p  -  1 ) ) ) )
3223, 31cxp 4687 . . . . 5  class  ( y  X.  ( y  i^i  ( ZZ  ^m  (
0 ... ( p  - 
1 ) ) ) ) )
335, 22, 32csb 3081 . . . 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 3151 . . 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 4077 . 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 1623 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