Definition df-eqp 31551

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

Step	Hyp	Ref	Expression
1		ceqp 31541	. 2 class ~Qp
2		vp	. . 3 setvar p
3		cprime 15385	. . 3 class Prime
4		vf	. . . . . . . 8 setvar f
5	4	cv 1482	. . . . . . 7 class f
6		vg	. . . . . . . 8 setvar g
7	6	cv 1482	. . . . . . 7 class g
8	5, 7	cpr 4179	. . . . . 6 class { f , g }
9		cz 11377	. . . . . . 7 class ZZ
10		cmap 7857	. . . . . . 7 class ^m
11	9, 9, 10	co 6650	. . . . . 6 class ( ZZ ^m ZZ )
12	8, 11	wss 3574	. . . . 5 wff { f , g } C_ ( ZZ ^m ZZ )
13		vn	. . . . . . . . . . 11 setvar n
14	13	cv 1482	. . . . . . . . . 10 class n
15	14	cneg 10267	. . . . . . . . 9 class -u n
16		cuz 11687	. . . . . . . . 9 class ZZ>=
17	15, 16	cfv 5888	. . . . . . . 8 class ( ZZ>= ` -u n )
18		vk	. . . . . . . . . . . . 13 setvar k
19	18	cv 1482	. . . . . . . . . . . 12 class k
20	19	cneg 10267	. . . . . . . . . . 11 class -u k
21	20, 5	cfv 5888	. . . . . . . . . 10 class ( f ` -u k )
22	20, 7	cfv 5888	. . . . . . . . . 10 class ( g ` -u k )
23		cmin 10266	. . . . . . . . . 10 class -
24	21, 22, 23	co 6650	. . . . . . . . 9 class ( ( f ` -u k ) - ( g ` -u k ) )
25	2	cv 1482	. . . . . . . . . 10 class p
26		c1 9937	. . . . . . . . . . . 12 class 1
27		caddc 9939	. . . . . . . . . . . 12 class +
28	14, 26, 27	co 6650	. . . . . . . . . . 11 class ( n + 1 )
29	19, 28, 27	co 6650	. . . . . . . . . 10 class ( k + ( n + 1 ) )
30		cexp 12860	. . . . . . . . . 10 class ^
31	25, 29, 30	co 6650	. . . . . . . . 9 class ( p ^ ( k + ( n + 1 ) ) )
32		cdiv 10684	. . . . . . . . 9 class /
33	24, 31, 32	co 6650	. . . . . . . 8 class ( ( ( f ` -u k ) - ( g ` -u k ) ) / ( p ^ ( k + ( n + 1 ) ) ) )
34	17, 33, 18	csu 14416	. . . . . . 7 class sum_ k e. ( ZZ>= ` -u n ) ( ( ( f ` -u k ) - ( g ` -u k ) ) / ( p ^ ( k + ( n + 1 ) ) ) )
35	34, 9	wcel 1990	. . . . . 6 wff sum_ k e. ( ZZ>= ` -u n ) ( ( ( f ` -u k ) - ( g ` -u k ) ) / ( p ^ ( k + ( n + 1 ) ) ) ) e. ZZ
36	35, 13, 9	wral 2912	. . . . 5 wff A. n e. ZZ sum_ k e. ( ZZ>= ` -u n ) ( ( ( f ` -u k ) - ( g ` -u k ) ) / ( p ^ ( k + ( n + 1 ) ) ) ) e. ZZ
37	12, 36	wa 384	. . . 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 )
38	37, 4, 6	copab 4712	. . 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 ) }
39	2, 3, 38	cmpt 4729	. 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 ) } )
40	1, 39	wceq 1483	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 ) } )

This definition is referenced by: (None)