Users' Mathboxes 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 33614
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 33605 . 2 class ~Qp
2 vp . . 3 setvar 𝑝
3 cprime 16374 . . 3 class
4 vf . . . . . . . 8 setvar 𝑓
54cv 1538 . . . . . . 7 class 𝑓
6 vg . . . . . . . 8 setvar 𝑔
76cv 1538 . . . . . . 7 class 𝑔
85, 7cpr 4565 . . . . . 6 class {𝑓, 𝑔}
9 cz 12317 . . . . . . 7 class
10 cmap 8613 . . . . . . 7 class m
119, 9, 10co 7277 . . . . . 6 class (ℤ ↑m ℤ)
128, 11wss 3888 . . . . 5 wff {𝑓, 𝑔} ⊆ (ℤ ↑m ℤ)
13 vn . . . . . . . . . . 11 setvar 𝑛
1413cv 1538 . . . . . . . . . 10 class 𝑛
1514cneg 11204 . . . . . . . . 9 class -𝑛
16 cuz 12580 . . . . . . . . 9 class
1715, 16cfv 6435 . . . . . . . 8 class (ℤ‘-𝑛)
18 vk . . . . . . . . . . . . 13 setvar 𝑘
1918cv 1538 . . . . . . . . . . . 12 class 𝑘
2019cneg 11204 . . . . . . . . . . 11 class -𝑘
2120, 5cfv 6435 . . . . . . . . . 10 class (𝑓‘-𝑘)
2220, 7cfv 6435 . . . . . . . . . 10 class (𝑔‘-𝑘)
23 cmin 11203 . . . . . . . . . 10 class
2421, 22, 23co 7277 . . . . . . . . 9 class ((𝑓‘-𝑘) − (𝑔‘-𝑘))
252cv 1538 . . . . . . . . . 10 class 𝑝
26 c1 10870 . . . . . . . . . . . 12 class 1
27 caddc 10872 . . . . . . . . . . . 12 class +
2814, 26, 27co 7277 . . . . . . . . . . 11 class (𝑛 + 1)
2919, 28, 27co 7277 . . . . . . . . . 10 class (𝑘 + (𝑛 + 1))
30 cexp 13780 . . . . . . . . . 10 class
3125, 29, 30co 7277 . . . . . . . . 9 class (𝑝↑(𝑘 + (𝑛 + 1)))
32 cdiv 11630 . . . . . . . . 9 class /
3324, 31, 32co 7277 . . . . . . . 8 class (((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1))))
3417, 33, 18csu 15395 . . . . . . 7 class Σ𝑘 ∈ (ℤ‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1))))
3534, 9wcel 2106 . . . . . 6 wff Σ𝑘 ∈ (ℤ‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) ∈ ℤ
3635, 13, 9wral 3064 . . . . 5 wff 𝑛 ∈ ℤ Σ𝑘 ∈ (ℤ‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) ∈ ℤ
3712, 36wa 396 . . . 4 wff ({𝑓, 𝑔} ⊆ (ℤ ↑m ℤ) ∧ ∀𝑛 ∈ ℤ Σ𝑘 ∈ (ℤ‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) ∈ ℤ)
3837, 4, 6copab 5138 . . 3 class {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ (ℤ ↑m ℤ) ∧ ∀𝑛 ∈ ℤ Σ𝑘 ∈ (ℤ‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) ∈ ℤ)}
392, 3, 38cmpt 5159 . 2 class (𝑝 ∈ ℙ ↦ {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ (ℤ ↑m ℤ) ∧ ∀𝑛 ∈ ℤ Σ𝑘 ∈ (ℤ‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) ∈ ℤ)})
401, 39wceq 1539 1 wff ~Qp = (𝑝 ∈ ℙ ↦ {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ (ℤ ↑m ℤ) ∧ ∀𝑛 ∈ ℤ Σ𝑘 ∈ (ℤ‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) ∈ ℤ)})
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator