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

Definition df-eqp 23986
Description: Define an equivalence relation on  ZZ-indexed sequences of integers such that two sequences are equivalent iff the difference is equivalent to zero, and a sequence is equivalent to zero iff the sum  sum_ k  <_  n f ( k ) ( p ^
k ) is a multiple of  p ^ (
n  +  1 ) for every  n. (Contributed by Mario Carneiro, 2-Dec-2014.)
Assertion
Ref Expression
df-eqp  |- ~Qp  =  ( p  e.  Prime  |->  { <. f ,  g >.  |  ( { f ,  g }  C_  ( ZZ  ^m  ZZ )  /\  A. n  e.  ZZ  sum_ k  e.  ( ZZ>= `  -u n ) ( ( ( f `
 -u k )  -  ( g `  -u k
) )  /  (
p ^ ( k  +  ( n  + 
1 ) ) ) )  e.  ZZ ) } )
Distinct variable group:    f, g, k, n, p

Detailed syntax breakdown of Definition df-eqp
StepHypRef Expression
1 ceqp 23977 . 2  class ~Qp
2 vp . . 3  set  p
3 cprime 12758 . . 3  class  Prime
4 vf . . . . . . . 8  set  f
54cv 1622 . . . . . . 7  class  f
6 vg . . . . . . . 8  set  g
76cv 1622 . . . . . . 7  class  g
85, 7cpr 3641 . . . . . 6  class  { f ,  g }
9 cz 10024 . . . . . . 7  class  ZZ
10 cmap 6772 . . . . . . 7  class  ^m
119, 9, 10co 5858 . . . . . 6  class  ( ZZ 
^m  ZZ )
128, 11wss 3152 . . . . 5  wff  { f ,  g }  C_  ( ZZ  ^m  ZZ )
13 vn . . . . . . . . . . 11  set  n
1413cv 1622 . . . . . . . . . 10  class  n
1514cneg 9038 . . . . . . . . 9  class  -u n
16 cuz 10230 . . . . . . . . 9  class  ZZ>=
1715, 16cfv 5255 . . . . . . . 8  class  ( ZZ>= `  -u n )
18 vk . . . . . . . . . . . . 13  set  k
1918cv 1622 . . . . . . . . . . . 12  class  k
2019cneg 9038 . . . . . . . . . . 11  class  -u k
2120, 5cfv 5255 . . . . . . . . . 10  class  ( f `
 -u k )
2220, 7cfv 5255 . . . . . . . . . 10  class  ( g `
 -u k )
23 cmin 9037 . . . . . . . . . 10  class  -
2421, 22, 23co 5858 . . . . . . . . 9  class  ( ( f `  -u k
)  -  ( g `
 -u k ) )
252cv 1622 . . . . . . . . . 10  class  p
26 c1 8738 . . . . . . . . . . . 12  class  1
27 caddc 8740 . . . . . . . . . . . 12  class  +
2814, 26, 27co 5858 . . . . . . . . . . 11  class  ( n  +  1 )
2919, 28, 27co 5858 . . . . . . . . . 10  class  ( k  +  ( n  + 
1 ) )
30 cexp 11104 . . . . . . . . . 10  class  ^
3125, 29, 30co 5858 . . . . . . . . 9  class  ( p ^ ( k  +  ( n  +  1 ) ) )
32 cdiv 9423 . . . . . . . . 9  class  /
3324, 31, 32co 5858 . . . . . . . 8  class  ( ( ( f `  -u k
)  -  ( g `
 -u k ) )  /  ( p ^
( k  +  ( n  +  1 ) ) ) )
3417, 33, 18csu 12158 . . . . . . 7  class  sum_ k  e.  ( ZZ>= `  -u n ) ( ( ( f `
 -u k )  -  ( g `  -u k
) )  /  (
p ^ ( k  +  ( n  + 
1 ) ) ) )
3534, 9wcel 1684 . . . . . 6  wff  sum_ k  e.  ( ZZ>= `  -u n ) ( ( ( f `
 -u k )  -  ( g `  -u k
) )  /  (
p ^ ( k  +  ( n  + 
1 ) ) ) )  e.  ZZ
3635, 13, 9wral 2543 . . . . 5  wff  A. n  e.  ZZ  sum_ k  e.  (
ZZ>= `  -u n ) ( ( ( f `  -u k )  -  (
g `  -u k ) )  /  ( p ^ ( k  +  ( n  +  1 ) ) ) )  e.  ZZ
3712, 36wa 358 . . . 4  wff  ( { f ,  g } 
C_  ( ZZ  ^m  ZZ )  /\  A. n  e.  ZZ  sum_ k  e.  (
ZZ>= `  -u n ) ( ( ( f `  -u k )  -  (
g `  -u k ) )  /  ( p ^ ( k  +  ( n  +  1 ) ) ) )  e.  ZZ )
3837, 4, 6copab 4076 . . 3  class  { <. f ,  g >.  |  ( { f ,  g }  C_  ( ZZ  ^m  ZZ )  /\  A. n  e.  ZZ  sum_ k  e.  ( ZZ>= `  -u n ) ( ( ( f `
 -u k )  -  ( g `  -u k
) )  /  (
p ^ ( k  +  ( n  + 
1 ) ) ) )  e.  ZZ ) }
392, 3, 38cmpt 4077 . 2  class  ( p  e.  Prime  |->  { <. f ,  g >.  |  ( { f ,  g }  C_  ( ZZ  ^m  ZZ )  /\  A. n  e.  ZZ  sum_ k  e.  ( ZZ>= `  -u n ) ( ( ( f `
 -u k )  -  ( g `  -u k
) )  /  (
p ^ ( k  +  ( n  + 
1 ) ) ) )  e.  ZZ ) } )
401, 39wceq 1623 1  wff ~Qp  =  ( p  e.  Prime  |->  { <. f ,  g >.  |  ( { f ,  g }  C_  ( ZZ  ^m  ZZ )  /\  A. n  e.  ZZ  sum_ k  e.  ( ZZ>= `  -u n ) ( ( ( f `
 -u k )  -  ( g `  -u k
) )  /  (
p ^ ( k  +  ( n  + 
1 ) ) ) )  e.  ZZ ) } )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator