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

Definition df-rqp 33614
Description: There is a unique element of (ℤ ↑m (0...(𝑝 − 1))) ~Qp -equivalent to any element of (ℤ ↑m ℤ), if the sequences are zero for sufficiently large negative values; this function selects that element. (Contributed by Mario Carneiro, 2-Dec-2014.)
Assertion
Ref Expression
df-rqp /Qp = (𝑝 ∈ ℙ ↦ (~Qp ∩ {𝑓 ∈ (ℤ ↑m ℤ) ∣ ∃𝑥 ∈ ran ℤ(𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑦(𝑦 × (𝑦 ∩ (ℤ ↑m (0...(𝑝 − 1)))))))
Distinct variable group:   𝑓,𝑝,𝑥,𝑦

Detailed syntax breakdown of Definition df-rqp
StepHypRef Expression
1 crqp 33605 . 2 class /Qp
2 vp . . 3 setvar 𝑝
3 cprime 16374 . . 3 class
4 ceqp 33604 . . . 4 class ~Qp
5 vy . . . . 5 setvar 𝑦
6 vf . . . . . . . . . . 11 setvar 𝑓
76cv 1541 . . . . . . . . . 10 class 𝑓
87ccnv 5589 . . . . . . . . 9 class 𝑓
9 cz 12319 . . . . . . . . . 10 class
10 cc0 10872 . . . . . . . . . . 11 class 0
1110csn 4567 . . . . . . . . . 10 class {0}
129, 11cdif 3889 . . . . . . . . 9 class (ℤ ∖ {0})
138, 12cima 5593 . . . . . . . 8 class (𝑓 “ (ℤ ∖ {0}))
14 vx . . . . . . . . 9 setvar 𝑥
1514cv 1541 . . . . . . . 8 class 𝑥
1613, 15wss 3892 . . . . . . 7 wff (𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥
17 cuz 12581 . . . . . . . 8 class
1817crn 5591 . . . . . . 7 class ran ℤ
1916, 14, 18wrex 3067 . . . . . 6 wff 𝑥 ∈ ran ℤ(𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥
20 cmap 8598 . . . . . . 7 class m
219, 9, 20co 7271 . . . . . 6 class (ℤ ↑m ℤ)
2219, 6, 21crab 3070 . . . . 5 class {𝑓 ∈ (ℤ ↑m ℤ) ∣ ∃𝑥 ∈ ran ℤ(𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥}
235cv 1541 . . . . . 6 class 𝑦
242cv 1541 . . . . . . . . . 10 class 𝑝
25 c1 10873 . . . . . . . . . 10 class 1
26 cmin 11205 . . . . . . . . . 10 class
2724, 25, 26co 7271 . . . . . . . . 9 class (𝑝 − 1)
28 cfz 13238 . . . . . . . . 9 class ...
2910, 27, 28co 7271 . . . . . . . 8 class (0...(𝑝 − 1))
309, 29, 20co 7271 . . . . . . 7 class (ℤ ↑m (0...(𝑝 − 1)))
3123, 30cin 3891 . . . . . 6 class (𝑦 ∩ (ℤ ↑m (0...(𝑝 − 1))))
3223, 31cxp 5588 . . . . 5 class (𝑦 × (𝑦 ∩ (ℤ ↑m (0...(𝑝 − 1)))))
335, 22, 32csb 3837 . . . 4 class {𝑓 ∈ (ℤ ↑m ℤ) ∣ ∃𝑥 ∈ ran ℤ(𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑦(𝑦 × (𝑦 ∩ (ℤ ↑m (0...(𝑝 − 1)))))
344, 33cin 3891 . . 3 class (~Qp ∩ {𝑓 ∈ (ℤ ↑m ℤ) ∣ ∃𝑥 ∈ ran ℤ(𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑦(𝑦 × (𝑦 ∩ (ℤ ↑m (0...(𝑝 − 1))))))
352, 3, 34cmpt 5162 . 2 class (𝑝 ∈ ℙ ↦ (~Qp ∩ {𝑓 ∈ (ℤ ↑m ℤ) ∣ ∃𝑥 ∈ ran ℤ(𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑦(𝑦 × (𝑦 ∩ (ℤ ↑m (0...(𝑝 − 1)))))))
361, 35wceq 1542 1 wff /Qp = (𝑝 ∈ ℙ ↦ (~Qp ∩ {𝑓 ∈ (ℤ ↑m ℤ) ∣ ∃𝑥 ∈ ran ℤ(𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑦(𝑦 × (𝑦 ∩ (ℤ ↑m (0...(𝑝 − 1)))))))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator