Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-eqp Structured version   Visualization version   GIF version

Definition df-eqp 32962
 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
StepHypRef Expression
1 ceqp 32953 . 2 class ~Qp
2 vp . . 3 setvar 𝑝
3 cprime 16013 . . 3 class
4 vf . . . . . . . 8 setvar 𝑓
54cv 1537 . . . . . . 7 class 𝑓
6 vg . . . . . . . 8 setvar 𝑔
76cv 1537 . . . . . . 7 class 𝑔
85, 7cpr 4552 . . . . . 6 class {𝑓, 𝑔}
9 cz 11978 . . . . . . 7 class
10 cmap 8402 . . . . . . 7 class m
119, 9, 10co 7149 . . . . . 6 class (ℤ ↑m ℤ)
128, 11wss 3919 . . . . 5 wff {𝑓, 𝑔} ⊆ (ℤ ↑m ℤ)
13 vn . . . . . . . . . . 11 setvar 𝑛
1413cv 1537 . . . . . . . . . 10 class 𝑛
1514cneg 10869 . . . . . . . . 9 class -𝑛
16 cuz 12240 . . . . . . . . 9 class
1715, 16cfv 6343 . . . . . . . 8 class (ℤ‘-𝑛)
18 vk . . . . . . . . . . . . 13 setvar 𝑘
1918cv 1537 . . . . . . . . . . . 12 class 𝑘
2019cneg 10869 . . . . . . . . . . 11 class -𝑘
2120, 5cfv 6343 . . . . . . . . . 10 class (𝑓‘-𝑘)
2220, 7cfv 6343 . . . . . . . . . 10 class (𝑔‘-𝑘)
23 cmin 10868 . . . . . . . . . 10 class
2421, 22, 23co 7149 . . . . . . . . 9 class ((𝑓‘-𝑘) − (𝑔‘-𝑘))
252cv 1537 . . . . . . . . . 10 class 𝑝
26 c1 10536 . . . . . . . . . . . 12 class 1
27 caddc 10538 . . . . . . . . . . . 12 class +
2814, 26, 27co 7149 . . . . . . . . . . 11 class (𝑛 + 1)
2919, 28, 27co 7149 . . . . . . . . . 10 class (𝑘 + (𝑛 + 1))
30 cexp 13434 . . . . . . . . . 10 class
3125, 29, 30co 7149 . . . . . . . . 9 class (𝑝↑(𝑘 + (𝑛 + 1)))
32 cdiv 11295 . . . . . . . . 9 class /
3324, 31, 32co 7149 . . . . . . . 8 class (((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1))))
3417, 33, 18csu 15042 . . . . . . 7 class Σ𝑘 ∈ (ℤ‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1))))
3534, 9wcel 2115 . . . . . 6 wff Σ𝑘 ∈ (ℤ‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) ∈ ℤ
3635, 13, 9wral 3133 . . . . 5 wff 𝑛 ∈ ℤ Σ𝑘 ∈ (ℤ‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) ∈ ℤ
3712, 36wa 399 . . . 4 wff ({𝑓, 𝑔} ⊆ (ℤ ↑m ℤ) ∧ ∀𝑛 ∈ ℤ Σ𝑘 ∈ (ℤ‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) ∈ ℤ)
3837, 4, 6copab 5114 . . 3 class {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ (ℤ ↑m ℤ) ∧ ∀𝑛 ∈ ℤ Σ𝑘 ∈ (ℤ‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) ∈ ℤ)}
392, 3, 38cmpt 5132 . 2 class (𝑝 ∈ ℙ ↦ {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ (ℤ ↑m ℤ) ∧ ∀𝑛 ∈ ℤ Σ𝑘 ∈ (ℤ‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) ∈ ℤ)})
401, 39wceq 1538 1 wff ~Qp = (𝑝 ∈ ℙ ↦ {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ (ℤ ↑m ℤ) ∧ ∀𝑛 ∈ ℤ Σ𝑘 ∈ (ℤ‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) ∈ ℤ)})
 Colors of variables: wff setvar class This definition is referenced by: (None)
 Copyright terms: Public domain W3C validator