Metamath Proof Explorer

Definition df-eqp

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)

Ref Expression
Assertion 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 ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ceqp 
 |-  ~Qp
1 vp 
 |-  p
2 cprime 
 |-  Prime
3 vf 
 |-  f
4 vg 
 |-  g
5 3 cv 
 |-  f
6 4 cv 
 |-  g
7 5 6 cpr 
 |-  { f , g }
8 cz 
 |-  ZZ
9 cmap 
 |-  ^m
10 8 8 9 co 
 |-  ( ZZ ^m ZZ )
11 7 10 wss 
 |-  { f , g } C_ ( ZZ ^m ZZ )
12 vn 
 |-  n
13 vk 
 |-  k
14 cuz 
 |-  ZZ>=
15 12 cv 
 |-  n
16 15 cneg 
 |-  -u n
17 16 14 cfv 
 |-  ( ZZ>= ` -u n )
18 13 cv 
 |-  k
19 18 cneg 
 |-  -u k
20 19 5 cfv 
 |-  ( f ` -u k )
21 cmin 
 |-  -
22 19 6 cfv 
 |-  ( g ` -u k )
23 20 22 21 co 
 |-  ( ( f ` -u k ) - ( g ` -u k ) )
24 cdiv 
 |-  /
25 1 cv 
 |-  p
26 cexp 
 |-  ^
27 caddc 
 |-  +
28 c1 
 |-  1
29 15 28 27 co 
 |-  ( n + 1 )
30 18 29 27 co 
 |-  ( k + ( n + 1 ) )
31 25 30 26 co 
 |-  ( p ^ ( k + ( n + 1 ) ) )
32 23 31 24 co 
 |-  ( ( ( f ` -u k ) - ( g ` -u k ) ) / ( p ^ ( k + ( n + 1 ) ) ) )
33 17 32 13 csu 
 |-  sum_ k e. ( ZZ>= ` -u n ) ( ( ( f ` -u k ) - ( g ` -u k ) ) / ( p ^ ( k + ( n + 1 ) ) ) )
34 33 8 wcel 
 |-  sum_ k e. ( ZZ>= ` -u n ) ( ( ( f ` -u k ) - ( g ` -u k ) ) / ( p ^ ( k + ( n + 1 ) ) ) ) e. ZZ
35 34 12 8 wral 
 |-  A. n e. ZZ sum_ k e. ( ZZ>= ` -u n ) ( ( ( f ` -u k ) - ( g ` -u k ) ) / ( p ^ ( k + ( n + 1 ) ) ) ) e. ZZ
36 11 35 wa 
 |-  ( { 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 )
37 36 3 4 copab 
 |-  { <. 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 ) }
38 1 2 37 cmpt 
 |-  ( 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 ) } )
39 0 38 wceq 
 |-  ~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 ) } )