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 = ( 𝑝 ∈ ℙ ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ ( ℤ ↑m ℤ ) ∧ ∀ 𝑛 ∈ ℤ Σ 𝑘 ∈ ( ℤ ‘ - 𝑛 ) ( ( ( 𝑓 ‘ - 𝑘 ) − ( 𝑔 ‘ - 𝑘 ) ) / ( 𝑝 ↑ ( 𝑘 + ( 𝑛 + 1 ) ) ) ) ∈ ℤ ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ceqp ~Qp
1 vp 𝑝
2 cprime
3 vf 𝑓
4 vg 𝑔
5 3 cv 𝑓
6 4 cv 𝑔
7 5 6 cpr { 𝑓 , 𝑔 }
8 cz
9 cmap m
10 8 8 9 co ( ℤ ↑m ℤ )
11 7 10 wss { 𝑓 , 𝑔 } ⊆ ( ℤ ↑m ℤ )
12 vn 𝑛
13 vk 𝑘
14 cuz
15 12 cv 𝑛
16 15 cneg - 𝑛
17 16 14 cfv ( ℤ ‘ - 𝑛 )
18 13 cv 𝑘
19 18 cneg - 𝑘
20 19 5 cfv ( 𝑓 ‘ - 𝑘 )
21 cmin
22 19 6 cfv ( 𝑔 ‘ - 𝑘 )
23 20 22 21 co ( ( 𝑓 ‘ - 𝑘 ) − ( 𝑔 ‘ - 𝑘 ) )
24 cdiv /
25 1 cv 𝑝
26 cexp
27 caddc +
28 c1 1
29 15 28 27 co ( 𝑛 + 1 )
30 18 29 27 co ( 𝑘 + ( 𝑛 + 1 ) )
31 25 30 26 co ( 𝑝 ↑ ( 𝑘 + ( 𝑛 + 1 ) ) )
32 23 31 24 co ( ( ( 𝑓 ‘ - 𝑘 ) − ( 𝑔 ‘ - 𝑘 ) ) / ( 𝑝 ↑ ( 𝑘 + ( 𝑛 + 1 ) ) ) )
33 17 32 13 csu Σ 𝑘 ∈ ( ℤ ‘ - 𝑛 ) ( ( ( 𝑓 ‘ - 𝑘 ) − ( 𝑔 ‘ - 𝑘 ) ) / ( 𝑝 ↑ ( 𝑘 + ( 𝑛 + 1 ) ) ) )
34 33 8 wcel Σ 𝑘 ∈ ( ℤ ‘ - 𝑛 ) ( ( ( 𝑓 ‘ - 𝑘 ) − ( 𝑔 ‘ - 𝑘 ) ) / ( 𝑝 ↑ ( 𝑘 + ( 𝑛 + 1 ) ) ) ) ∈ ℤ
35 34 12 8 wral 𝑛 ∈ ℤ Σ 𝑘 ∈ ( ℤ ‘ - 𝑛 ) ( ( ( 𝑓 ‘ - 𝑘 ) − ( 𝑔 ‘ - 𝑘 ) ) / ( 𝑝 ↑ ( 𝑘 + ( 𝑛 + 1 ) ) ) ) ∈ ℤ
36 11 35 wa ( { 𝑓 , 𝑔 } ⊆ ( ℤ ↑m ℤ ) ∧ ∀ 𝑛 ∈ ℤ Σ 𝑘 ∈ ( ℤ ‘ - 𝑛 ) ( ( ( 𝑓 ‘ - 𝑘 ) − ( 𝑔 ‘ - 𝑘 ) ) / ( 𝑝 ↑ ( 𝑘 + ( 𝑛 + 1 ) ) ) ) ∈ ℤ )
37 36 3 4 copab { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ ( ℤ ↑m ℤ ) ∧ ∀ 𝑛 ∈ ℤ Σ 𝑘 ∈ ( ℤ ‘ - 𝑛 ) ( ( ( 𝑓 ‘ - 𝑘 ) − ( 𝑔 ‘ - 𝑘 ) ) / ( 𝑝 ↑ ( 𝑘 + ( 𝑛 + 1 ) ) ) ) ∈ ℤ ) }
38 1 2 37 cmpt ( 𝑝 ∈ ℙ ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ ( ℤ ↑m ℤ ) ∧ ∀ 𝑛 ∈ ℤ Σ 𝑘 ∈ ( ℤ ‘ - 𝑛 ) ( ( ( 𝑓 ‘ - 𝑘 ) − ( 𝑔 ‘ - 𝑘 ) ) / ( 𝑝 ↑ ( 𝑘 + ( 𝑛 + 1 ) ) ) ) ∈ ℤ ) } )
39 0 38 wceq ~Qp = ( 𝑝 ∈ ℙ ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ ( ℤ ↑m ℤ ) ∧ ∀ 𝑛 ∈ ℤ Σ 𝑘 ∈ ( ℤ ‘ - 𝑛 ) ( ( ( 𝑓 ‘ - 𝑘 ) − ( 𝑔 ‘ - 𝑘 ) ) / ( 𝑝 ↑ ( 𝑘 + ( 𝑛 + 1 ) ) ) ) ∈ ℤ ) } )