Definition df-eqp 35598

Description: Define an equivalence relation on ℤ-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 Σ𝑘 ≤ 𝑛𝑓(𝑘)(𝑝↑𝑘) is a multiple of 𝑝↑(𝑛 + 1) for every 𝑛. (Contributed by Mario Carneiro, 2-Dec-2014.)

Assertion

Ref	Expression
df-eqp	⊢ ~Qp = (𝑝 ∈ ℙ ↦ {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ (ℤ ↑m ℤ) ∧ ∀𝑛 ∈ ℤ Σ𝑘 ∈ (ℤ≥‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) ∈ ℤ)})

Distinct variable group:   𝑓,𝑔,𝑘,𝑛,𝑝

Detailed syntax breakdown of Definition df-eqp

Step	Hyp	Ref	Expression
1		ceqp 35589	. 2 class ~Qp
2		vp	. . 3 setvar 𝑝
3		cprime 16689	. . 3 class ℙ
4		vf	. . . . . . . 8 setvar 𝑓
5	4	cv 1538	. . . . . . 7 class 𝑓
6		vg	. . . . . . . 8 setvar 𝑔
7	6	cv 1538	. . . . . . 7 class 𝑔
8	5, 7	cpr 4608	. . . . . 6 class {𝑓, 𝑔}
9		cz 12595	. . . . . . 7 class ℤ
10		cmap 8847	. . . . . . 7 class ↑m
11	9, 9, 10	co 7412	. . . . . 6 class (ℤ ↑m ℤ)
12	8, 11	wss 3931	. . . . 5 wff {𝑓, 𝑔} ⊆ (ℤ ↑m ℤ)
13		vn	. . . . . . . . . . 11 setvar 𝑛
14	13	cv 1538	. . . . . . . . . 10 class 𝑛
15	14	cneg 11474	. . . . . . . . 9 class -𝑛
16		cuz 12859	. . . . . . . . 9 class ℤ≥
17	15, 16	cfv 6540	. . . . . . . 8 class (ℤ≥‘-𝑛)
18		vk	. . . . . . . . . . . . 13 setvar 𝑘
19	18	cv 1538	. . . . . . . . . . . 12 class 𝑘
20	19	cneg 11474	. . . . . . . . . . 11 class -𝑘
21	20, 5	cfv 6540	. . . . . . . . . 10 class (𝑓‘-𝑘)
22	20, 7	cfv 6540	. . . . . . . . . 10 class (𝑔‘-𝑘)
23		cmin 11473	. . . . . . . . . 10 class −
24	21, 22, 23	co 7412	. . . . . . . . 9 class ((𝑓‘-𝑘) − (𝑔‘-𝑘))
25	2	cv 1538	. . . . . . . . . 10 class 𝑝
26		c1 11137	. . . . . . . . . . . 12 class 1
27		caddc 11139	. . . . . . . . . . . 12 class +
28	14, 26, 27	co 7412	. . . . . . . . . . 11 class (𝑛 + 1)
29	19, 28, 27	co 7412	. . . . . . . . . 10 class (𝑘 + (𝑛 + 1))
30		cexp 14083	. . . . . . . . . 10 class ↑
31	25, 29, 30	co 7412	. . . . . . . . 9 class (𝑝↑(𝑘 + (𝑛 + 1)))
32		cdiv 11901	. . . . . . . . 9 class /
33	24, 31, 32	co 7412	. . . . . . . 8 class (((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1))))
34	17, 33, 18	csu 15703	. . . . . . 7 class Σ𝑘 ∈ (ℤ≥‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1))))
35	34, 9	wcel 2107	. . . . . 6 wff Σ𝑘 ∈ (ℤ≥‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) ∈ ℤ
36	35, 13, 9	wral 3050	. . . . 5 wff ∀𝑛 ∈ ℤ Σ𝑘 ∈ (ℤ≥‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) ∈ ℤ
37	12, 36	wa 395	. . . 4 wff ({𝑓, 𝑔} ⊆ (ℤ ↑m ℤ) ∧ ∀𝑛 ∈ ℤ Σ𝑘 ∈ (ℤ≥‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) ∈ ℤ)
38	37, 4, 6	copab 5185	. . 3 class {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ (ℤ ↑m ℤ) ∧ ∀𝑛 ∈ ℤ Σ𝑘 ∈ (ℤ≥‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) ∈ ℤ)}
39	2, 3, 38	cmpt 5205	. 2 class (𝑝 ∈ ℙ ↦ {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ (ℤ ↑m ℤ) ∧ ∀𝑛 ∈ ℤ Σ𝑘 ∈ (ℤ≥‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) ∈ ℤ)})
40	1, 39	wceq 1539	1 wff ~Qp = (𝑝 ∈ ℙ ↦ {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ (ℤ ↑m ℤ) ∧ ∀𝑛 ∈ ℤ Σ𝑘 ∈ (ℤ≥‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) ∈ ℤ)})

This definition is referenced by: (None)