Definition df-eqp 31551

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

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

Detailed syntax breakdown of Definition df-eqp

Step	Hyp	Ref	Expression
1		ceqp 31541	. 2 class ~Qp
2		vp	. . 3 setvar 𝑝
3		cprime 15385	. . 3 class ℙ
4		vf	. . . . . . . 8 setvar 𝑓
5	4	cv 1482	. . . . . . 7 class 𝑓
6		vg	. . . . . . . 8 setvar 𝑔
7	6	cv 1482	. . . . . . 7 class 𝑔
8	5, 7	cpr 4179	. . . . . 6 class {𝑓, 𝑔}
9		cz 11377	. . . . . . 7 class ℤ
10		cmap 7857	. . . . . . 7 class ↑𝑚
11	9, 9, 10	co 6650	. . . . . 6 class (ℤ ↑𝑚 ℤ)
12	8, 11	wss 3574	. . . . 5 wff {𝑓, 𝑔} ⊆ (ℤ ↑𝑚 ℤ)
13		vn	. . . . . . . . . . 11 setvar 𝑛
14	13	cv 1482	. . . . . . . . . 10 class 𝑛
15	14	cneg 10267	. . . . . . . . 9 class -𝑛
16		cuz 11687	. . . . . . . . 9 class ℤ≥
17	15, 16	cfv 5888	. . . . . . . 8 class (ℤ≥‘-𝑛)
18		vk	. . . . . . . . . . . . 13 setvar 𝑘
19	18	cv 1482	. . . . . . . . . . . 12 class 𝑘
20	19	cneg 10267	. . . . . . . . . . 11 class -𝑘
21	20, 5	cfv 5888	. . . . . . . . . 10 class (𝑓‘-𝑘)
22	20, 7	cfv 5888	. . . . . . . . . 10 class (𝑔‘-𝑘)
23		cmin 10266	. . . . . . . . . 10 class −
24	21, 22, 23	co 6650	. . . . . . . . 9 class ((𝑓‘-𝑘) − (𝑔‘-𝑘))
25	2	cv 1482	. . . . . . . . . 10 class 𝑝
26		c1 9937	. . . . . . . . . . . 12 class 1
27		caddc 9939	. . . . . . . . . . . 12 class +
28	14, 26, 27	co 6650	. . . . . . . . . . 11 class (𝑛 + 1)
29	19, 28, 27	co 6650	. . . . . . . . . 10 class (𝑘 + (𝑛 + 1))
30		cexp 12860	. . . . . . . . . 10 class ↑
31	25, 29, 30	co 6650	. . . . . . . . 9 class (𝑝↑(𝑘 + (𝑛 + 1)))
32		cdiv 10684	. . . . . . . . 9 class /
33	24, 31, 32	co 6650	. . . . . . . 8 class (((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1))))
34	17, 33, 18	csu 14416	. . . . . . 7 class Σ𝑘 ∈ (ℤ≥‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1))))
35	34, 9	wcel 1990	. . . . . 6 wff Σ𝑘 ∈ (ℤ≥‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) ∈ ℤ
36	35, 13, 9	wral 2912	. . . . 5 wff ∀𝑛 ∈ ℤ Σ𝑘 ∈ (ℤ≥‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) ∈ ℤ
37	12, 36	wa 384	. . . 4 wff ({𝑓, 𝑔} ⊆ (ℤ ↑𝑚 ℤ) ∧ ∀𝑛 ∈ ℤ Σ𝑘 ∈ (ℤ≥‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) ∈ ℤ)
38	37, 4, 6	copab 4712	. . 3 class {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ (ℤ ↑𝑚 ℤ) ∧ ∀𝑛 ∈ ℤ Σ𝑘 ∈ (ℤ≥‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) ∈ ℤ)}
39	2, 3, 38	cmpt 4729	. 2 class (𝑝 ∈ ℙ ↦ {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ (ℤ ↑𝑚 ℤ) ∧ ∀𝑛 ∈ ℤ Σ𝑘 ∈ (ℤ≥‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) ∈ ℤ)})
40	1, 39	wceq 1483	1 wff ~Qp = (𝑝 ∈ ℙ ↦ {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ (ℤ ↑𝑚 ℤ) ∧ ∀𝑛 ∈ ℤ Σ𝑘 ∈ (ℤ≥‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) ∈ ℤ)})

This definition is referenced by: (None)