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 32963
 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 32954 . 2 class /Qp
2 vp . . 3 setvar 𝑝
3 cprime 16013 . . 3 class
4 ceqp 32953 . . . 4 class ~Qp
5 vy . . . . 5 setvar 𝑦
6 vf . . . . . . . . . . 11 setvar 𝑓
76cv 1537 . . . . . . . . . 10 class 𝑓
87ccnv 5541 . . . . . . . . 9 class 𝑓
9 cz 11978 . . . . . . . . . 10 class
10 cc0 10535 . . . . . . . . . . 11 class 0
1110csn 4550 . . . . . . . . . 10 class {0}
129, 11cdif 3916 . . . . . . . . 9 class (ℤ ∖ {0})
138, 12cima 5545 . . . . . . . 8 class (𝑓 “ (ℤ ∖ {0}))
14 vx . . . . . . . . 9 setvar 𝑥
1514cv 1537 . . . . . . . 8 class 𝑥
1613, 15wss 3919 . . . . . . 7 wff (𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥
17 cuz 12240 . . . . . . . 8 class
1817crn 5543 . . . . . . 7 class ran ℤ
1916, 14, 18wrex 3134 . . . . . 6 wff 𝑥 ∈ ran ℤ(𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥
20 cmap 8402 . . . . . . 7 class m
219, 9, 20co 7149 . . . . . 6 class (ℤ ↑m ℤ)
2219, 6, 21crab 3137 . . . . 5 class {𝑓 ∈ (ℤ ↑m ℤ) ∣ ∃𝑥 ∈ ran ℤ(𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥}
235cv 1537 . . . . . 6 class 𝑦
242cv 1537 . . . . . . . . . 10 class 𝑝
25 c1 10536 . . . . . . . . . 10 class 1
26 cmin 10868 . . . . . . . . . 10 class
2724, 25, 26co 7149 . . . . . . . . 9 class (𝑝 − 1)
28 cfz 12894 . . . . . . . . 9 class ...
2910, 27, 28co 7149 . . . . . . . 8 class (0...(𝑝 − 1))
309, 29, 20co 7149 . . . . . . 7 class (ℤ ↑m (0...(𝑝 − 1)))
3123, 30cin 3918 . . . . . 6 class (𝑦 ∩ (ℤ ↑m (0...(𝑝 − 1))))
3223, 31cxp 5540 . . . . 5 class (𝑦 × (𝑦 ∩ (ℤ ↑m (0...(𝑝 − 1)))))
335, 22, 32csb 3866 . . . 4 class {𝑓 ∈ (ℤ ↑m ℤ) ∣ ∃𝑥 ∈ ran ℤ(𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑦(𝑦 × (𝑦 ∩ (ℤ ↑m (0...(𝑝 − 1)))))
344, 33cin 3918 . . 3 class (~Qp ∩ {𝑓 ∈ (ℤ ↑m ℤ) ∣ ∃𝑥 ∈ ran ℤ(𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑦(𝑦 × (𝑦 ∩ (ℤ ↑m (0...(𝑝 − 1))))))
352, 3, 34cmpt 5132 . 2 class (𝑝 ∈ ℙ ↦ (~Qp ∩ {𝑓 ∈ (ℤ ↑m ℤ) ∣ ∃𝑥 ∈ ran ℤ(𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑦(𝑦 × (𝑦 ∩ (ℤ ↑m (0...(𝑝 − 1)))))))
361, 35wceq 1538 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