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	$$⊢{~}_{{\mathbb{Q}}_p}=\left(p\in \mathbb{P}⟼\left\{⟨f,g⟩|\left(\left\{f,g\right\}\subseteq {\mathbb{Z}}^{\mathbb{Z}}\wedge \forall n\in \mathbb{Z}\sum _{k\in {\mathbb{Z}}_{\ge \left(-n\right)}}\left(\frac{f\left(-k\right)-g\left(-k\right)}{p^{k+n+1}}\right)\in \mathbb{Z}\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ceqp	$$class{~}_{{\mathbb{Q}}_p}$$
1		vp	$$setvarp$$
2		cprime	$$class\mathbb{P}$$
3		vf	$$setvarf$$
4		vg	$$setvarg$$
5	3	cv	$$setvarf$$
6	4	cv	$$setvarg$$
7	5 6	cpr	$$class\left\{f,g\right\}$$
8		cz	$$class\mathbb{Z}$$
9		cmap	$$class{\uparrow }_{𝑚}$$
10	8 8 9	co	$$class\left({\mathbb{Z}}^{\mathbb{Z}}\right)$$
11	7 10	wss	$$wff\left\{f,g\right\}\subseteq {\mathbb{Z}}^{\mathbb{Z}}$$
12		vn	$$setvarn$$
13		vk	$$setvark$$
14		cuz	$$class{\mathbb{Z}}_{\ge }$$
15	12	cv	$$setvarn$$
16	15	cneg	$$class\left(-n\right)$$
17	16 14	cfv	$$class{\mathbb{Z}}_{\ge \left(-n\right)}$$
18	13	cv	$$setvark$$
19	18	cneg	$$class\left(-k\right)$$
20	19 5	cfv	$$classf\left(-k\right)$$
21		cmin	$$class-$$
22	19 6	cfv	$$classg\left(-k\right)$$
23	20 22 21	co	$$class\left(f\left(-k\right)-g\left(-k\right)\right)$$
24		cdiv	$$class÷$$
25	1	cv	$$setvarp$$
26		cexp	$$class^$$
27		caddc	$$class+$$
28		c1	$$class1$$
29	15 28 27	co	$$class\left(n+1\right)$$
30	18 29 27	co	$$class\left(k+n+1\right)$$
31	25 30 26	co	$$class{p}^{k+n+1}$$
32	23 31 24	co	$$class\left(\frac{f\left(-k\right)-g\left(-k\right)}{p^{k+n+1}}\right)$$
33	17 32 13	csu	$$class\sum _{k\in {\mathbb{Z}}_{\ge \left(-n\right)}}\left(\frac{f\left(-k\right)-g\left(-k\right)}{p^{k+n+1}}\right)$$
34	33 8	wcel	$$wff\sum _{k\in {\mathbb{Z}}_{\ge \left(-n\right)}}\left(\frac{f\left(-k\right)-g\left(-k\right)}{p^{k+n+1}}\right)\in \mathbb{Z}$$
35	34 12 8	wral	$$wff\forall n\in \mathbb{Z}\sum _{k\in {\mathbb{Z}}_{\ge \left(-n\right)}}\left(\frac{f\left(-k\right)-g\left(-k\right)}{p^{k+n+1}}\right)\in \mathbb{Z}$$
36	11 35	wa	$$wff\left(\left\{f,g\right\}\subseteq {\mathbb{Z}}^{\mathbb{Z}}\wedge \forall n\in \mathbb{Z}\sum _{k\in {\mathbb{Z}}_{\ge \left(-n\right)}}\left(\frac{f\left(-k\right)-g\left(-k\right)}{p^{k+n+1}}\right)\in \mathbb{Z}\right)$$
37	36 3 4	copab	$$class\left\{⟨f,g⟩|\left(\left\{f,g\right\}\subseteq {\mathbb{Z}}^{\mathbb{Z}}\wedge \forall n\in \mathbb{Z}\sum _{k\in {\mathbb{Z}}_{\ge \left(-n\right)}}\left(\frac{f\left(-k\right)-g\left(-k\right)}{p^{k+n+1}}\right)\in \mathbb{Z}\right)\right\}$$
38	1 2 37	cmpt	$$class\left(p\in \mathbb{P}⟼\left\{⟨f,g⟩|\left(\left\{f,g\right\}\subseteq {\mathbb{Z}}^{\mathbb{Z}}\wedge \forall n\in \mathbb{Z}\sum _{k\in {\mathbb{Z}}_{\ge \left(-n\right)}}\left(\frac{f\left(-k\right)-g\left(-k\right)}{p^{k+n+1}}\right)\in \mathbb{Z}\right)\right\}\right)$$
39	0 38	wceq	$$wff{~}_{{\mathbb{Q}}_p}=\left(p\in \mathbb{P}⟼\left\{⟨f,g⟩|\left(\left\{f,g\right\}\subseteq {\mathbb{Z}}^{\mathbb{Z}}\wedge \forall n\in \mathbb{Z}\sum _{k\in {\mathbb{Z}}_{\ge \left(-n\right)}}\left(\frac{f\left(-k\right)-g\left(-k\right)}{p^{k+n+1}}\right)\in \mathbb{Z}\right)\right\}\right)$$