Definition df-rqp 30806

Description: There is a unique element of (ℤ ↑_𝑚 (0...(𝑝 − 1))) ~Qp -equivalent to any element of (ℤ ↑_𝑚 ℤ), 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 ∩ ⦋{𝑓 ∈ (ℤ ↑𝑚 ℤ) ∣ ∃𝑥 ∈ ran ℤ≥(◡𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑦⦌(𝑦 × (𝑦 ∩ (ℤ ↑𝑚 (0...(𝑝 − 1)))))))

Distinct variable group:   𝑓,𝑝,𝑥,𝑦

Detailed syntax breakdown of Definition df-rqp

Step	Hyp	Ref	Expression
1		crqp 30796	. 2 class /Qp
2		vp	. . 3 setvar 𝑝
3		cprime 15223	. . 3 class ℙ
4		ceqp 30795	. . . 4 class ~Qp
5		vy	. . . . 5 setvar 𝑦
6		vf	. . . . . . . . . . 11 setvar 𝑓
7	6	cv 1474	. . . . . . . . . 10 class 𝑓
8	7	ccnv 5037	. . . . . . . . 9 class ◡𝑓
9		cz 11254	. . . . . . . . . 10 class ℤ
10		cc0 9815	. . . . . . . . . . 11 class 0
11	10	csn 4125	. . . . . . . . . 10 class {0}
12	9, 11	cdif 3537	. . . . . . . . 9 class (ℤ ∖ {0})
13	8, 12	cima 5041	. . . . . . . 8 class (◡𝑓 “ (ℤ ∖ {0}))
14		vx	. . . . . . . . 9 setvar 𝑥
15	14	cv 1474	. . . . . . . 8 class 𝑥
16	13, 15	wss 3540	. . . . . . 7 wff (◡𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥
17		cuz 11563	. . . . . . . 8 class ℤ≥
18	17	crn 5039	. . . . . . 7 class ran ℤ≥
19	16, 14, 18	wrex 2897	. . . . . 6 wff ∃𝑥 ∈ ran ℤ≥(◡𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥
20		cmap 7744	. . . . . . 7 class ↑𝑚
21	9, 9, 20	co 6549	. . . . . 6 class (ℤ ↑𝑚 ℤ)
22	19, 6, 21	crab 2900	. . . . 5 class {𝑓 ∈ (ℤ ↑𝑚 ℤ) ∣ ∃𝑥 ∈ ran ℤ≥(◡𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥}
23	5	cv 1474	. . . . . 6 class 𝑦
24	2	cv 1474	. . . . . . . . . 10 class 𝑝
25		c1 9816	. . . . . . . . . 10 class 1
26		cmin 10145	. . . . . . . . . 10 class −
27	24, 25, 26	co 6549	. . . . . . . . 9 class (𝑝 − 1)
28		cfz 12197	. . . . . . . . 9 class ...
29	10, 27, 28	co 6549	. . . . . . . 8 class (0...(𝑝 − 1))
30	9, 29, 20	co 6549	. . . . . . 7 class (ℤ ↑𝑚 (0...(𝑝 − 1)))
31	23, 30	cin 3539	. . . . . 6 class (𝑦 ∩ (ℤ ↑𝑚 (0...(𝑝 − 1))))
32	23, 31	cxp 5036	. . . . 5 class (𝑦 × (𝑦 ∩ (ℤ ↑𝑚 (0...(𝑝 − 1)))))
33	5, 22, 32	csb 3499	. . . 4 class ⦋{𝑓 ∈ (ℤ ↑𝑚 ℤ) ∣ ∃𝑥 ∈ ran ℤ≥(◡𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑦⦌(𝑦 × (𝑦 ∩ (ℤ ↑𝑚 (0...(𝑝 − 1)))))
34	4, 33	cin 3539	. . 3 class (~Qp ∩ ⦋{𝑓 ∈ (ℤ ↑𝑚 ℤ) ∣ ∃𝑥 ∈ ran ℤ≥(◡𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑦⦌(𝑦 × (𝑦 ∩ (ℤ ↑𝑚 (0...(𝑝 − 1))))))
35	2, 3, 34	cmpt 4643	. 2 class (𝑝 ∈ ℙ ↦ (~Qp ∩ ⦋{𝑓 ∈ (ℤ ↑𝑚 ℤ) ∣ ∃𝑥 ∈ ran ℤ≥(◡𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑦⦌(𝑦 × (𝑦 ∩ (ℤ ↑𝑚 (0...(𝑝 − 1)))))))
36	1, 35	wceq 1475	1 wff /Qp = (𝑝 ∈ ℙ ↦ (~Qp ∩ ⦋{𝑓 ∈ (ℤ ↑𝑚 ℤ) ∣ ∃𝑥 ∈ ran ℤ≥(◡𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑦⦌(𝑦 × (𝑦 ∩ (ℤ ↑𝑚 (0...(𝑝 − 1)))))))

This definition is referenced by: (None)