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 ~p = p f g | f g n k n f k g k p k + n + 1

Detailed syntax breakdown

Step Hyp Ref Expression
0 ceqp class ~p
1 vp setvar p
2 cprime class
3 vf setvar f
4 vg setvar g
5 3 cv setvar f
6 4 cv setvar g
7 5 6 cpr class f g
8 cz class
9 cmap class 𝑚
10 8 8 9 co class
11 7 10 wss wff f g
12 vn setvar n
13 vk setvar k
14 cuz class
15 12 cv setvar n
16 15 cneg class n
17 16 14 cfv class n
18 13 cv setvar k
19 18 cneg class k
20 19 5 cfv class f k
21 cmin class
22 19 6 cfv class g k
23 20 22 21 co class f k g k
24 cdiv class ÷
25 1 cv setvar p
26 cexp class ^
27 caddc class +
28 c1 class 1
29 15 28 27 co class n + 1
30 18 29 27 co class k + n + 1
31 25 30 26 co class p k + n + 1
32 23 31 24 co class f k g k p k + n + 1
33 17 32 13 csu class k n f k g k p k + n + 1
34 33 8 wcel wff k n f k g k p k + n + 1
35 34 12 8 wral wff n k n f k g k p k + n + 1
36 11 35 wa wff f g n k n f k g k p k + n + 1
37 36 3 4 copab class f g | f g n k n f k g k p k + n + 1
38 1 2 37 cmpt class p f g | f g n k n f k g k p k + n + 1
39 0 38 wceq wff ~p = p f g | f g n k n f k g k p k + n + 1