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 34640
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 34631 . 2 class /Qp
2 vp . . 3 setvar 𝑝
3 cprime 16607 . . 3 class
4 ceqp 34630 . . . 4 class ~Qp
5 vy . . . . 5 setvar 𝑦
6 vf . . . . . . . . . . 11 setvar 𝑓
76cv 1540 . . . . . . . . . 10 class 𝑓
87ccnv 5675 . . . . . . . . 9 class 𝑓
9 cz 12557 . . . . . . . . . 10 class
10 cc0 11109 . . . . . . . . . . 11 class 0
1110csn 4628 . . . . . . . . . 10 class {0}
129, 11cdif 3945 . . . . . . . . 9 class (ℤ ∖ {0})
138, 12cima 5679 . . . . . . . 8 class (𝑓 “ (ℤ ∖ {0}))
14 vx . . . . . . . . 9 setvar 𝑥
1514cv 1540 . . . . . . . 8 class 𝑥
1613, 15wss 3948 . . . . . . 7 wff (𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥
17 cuz 12821 . . . . . . . 8 class
1817crn 5677 . . . . . . 7 class ran ℤ
1916, 14, 18wrex 3070 . . . . . 6 wff 𝑥 ∈ ran ℤ(𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥
20 cmap 8819 . . . . . . 7 class m
219, 9, 20co 7408 . . . . . 6 class (ℤ ↑m ℤ)
2219, 6, 21crab 3432 . . . . 5 class {𝑓 ∈ (ℤ ↑m ℤ) ∣ ∃𝑥 ∈ ran ℤ(𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥}
235cv 1540 . . . . . 6 class 𝑦
242cv 1540 . . . . . . . . . 10 class 𝑝
25 c1 11110 . . . . . . . . . 10 class 1
26 cmin 11443 . . . . . . . . . 10 class
2724, 25, 26co 7408 . . . . . . . . 9 class (𝑝 − 1)
28 cfz 13483 . . . . . . . . 9 class ...
2910, 27, 28co 7408 . . . . . . . 8 class (0...(𝑝 − 1))
309, 29, 20co 7408 . . . . . . 7 class (ℤ ↑m (0...(𝑝 − 1)))
3123, 30cin 3947 . . . . . 6 class (𝑦 ∩ (ℤ ↑m (0...(𝑝 − 1))))
3223, 31cxp 5674 . . . . 5 class (𝑦 × (𝑦 ∩ (ℤ ↑m (0...(𝑝 − 1)))))
335, 22, 32csb 3893 . . . 4 class {𝑓 ∈ (ℤ ↑m ℤ) ∣ ∃𝑥 ∈ ran ℤ(𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑦(𝑦 × (𝑦 ∩ (ℤ ↑m (0...(𝑝 − 1)))))
344, 33cin 3947 . . 3 class (~Qp ∩ {𝑓 ∈ (ℤ ↑m ℤ) ∣ ∃𝑥 ∈ ran ℤ(𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑦(𝑦 × (𝑦 ∩ (ℤ ↑m (0...(𝑝 − 1))))))
352, 3, 34cmpt 5231 . 2 class (𝑝 ∈ ℙ ↦ (~Qp ∩ {𝑓 ∈ (ℤ ↑m ℤ) ∣ ∃𝑥 ∈ ran ℤ(𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑦(𝑦 × (𝑦 ∩ (ℤ ↑m (0...(𝑝 − 1)))))))
361, 35wceq 1541 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