Definition df-rqp 34676

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

Step	Hyp	Ref	Expression
1		crqp 34667	. 2 class /Qp
2		vp	. . 3 setvar 𝑝
3		cprime 16608	. . 3 class ℙ
4		ceqp 34666	. . . 4 class ~Qp
5		vy	. . . . 5 setvar 𝑦
6		vf	. . . . . . . . . . 11 setvar 𝑓
7	6	cv 1541	. . . . . . . . . 10 class 𝑓
8	7	ccnv 5676	. . . . . . . . 9 class ◡𝑓
9		cz 12558	. . . . . . . . . 10 class ℤ
10		cc0 11110	. . . . . . . . . . 11 class 0
11	10	csn 4629	. . . . . . . . . 10 class {0}
12	9, 11	cdif 3946	. . . . . . . . 9 class (ℤ ∖ {0})
13	8, 12	cima 5680	. . . . . . . 8 class (◡𝑓 “ (ℤ ∖ {0}))
14		vx	. . . . . . . . 9 setvar 𝑥
15	14	cv 1541	. . . . . . . 8 class 𝑥
16	13, 15	wss 3949	. . . . . . 7 wff (◡𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥
17		cuz 12822	. . . . . . . 8 class ℤ≥
18	17	crn 5678	. . . . . . 7 class ran ℤ≥
19	16, 14, 18	wrex 3071	. . . . . 6 wff ∃𝑥 ∈ ran ℤ≥(◡𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥
20		cmap 8820	. . . . . . 7 class ↑m
21	9, 9, 20	co 7409	. . . . . 6 class (ℤ ↑m ℤ)
22	19, 6, 21	crab 3433	. . . . 5 class {𝑓 ∈ (ℤ ↑m ℤ) ∣ ∃𝑥 ∈ ran ℤ≥(◡𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥}
23	5	cv 1541	. . . . . 6 class 𝑦
24	2	cv 1541	. . . . . . . . . 10 class 𝑝
25		c1 11111	. . . . . . . . . 10 class 1
26		cmin 11444	. . . . . . . . . 10 class −
27	24, 25, 26	co 7409	. . . . . . . . 9 class (𝑝 − 1)
28		cfz 13484	. . . . . . . . 9 class ...
29	10, 27, 28	co 7409	. . . . . . . 8 class (0...(𝑝 − 1))
30	9, 29, 20	co 7409	. . . . . . 7 class (ℤ ↑m (0...(𝑝 − 1)))
31	23, 30	cin 3948	. . . . . 6 class (𝑦 ∩ (ℤ ↑m (0...(𝑝 − 1))))
32	23, 31	cxp 5675	. . . . 5 class (𝑦 × (𝑦 ∩ (ℤ ↑m (0...(𝑝 − 1)))))
33	5, 22, 32	csb 3894	. . . 4 class ⦋{𝑓 ∈ (ℤ ↑m ℤ) ∣ ∃𝑥 ∈ ran ℤ≥(◡𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑦⦌(𝑦 × (𝑦 ∩ (ℤ ↑m (0...(𝑝 − 1)))))
34	4, 33	cin 3948	. . 3 class (~Qp ∩ ⦋{𝑓 ∈ (ℤ ↑m ℤ) ∣ ∃𝑥 ∈ ran ℤ≥(◡𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑦⦌(𝑦 × (𝑦 ∩ (ℤ ↑m (0...(𝑝 − 1))))))
35	2, 3, 34	cmpt 5232	. 2 class (𝑝 ∈ ℙ ↦ (~Qp ∩ ⦋{𝑓 ∈ (ℤ ↑m ℤ) ∣ ∃𝑥 ∈ ran ℤ≥(◡𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑦⦌(𝑦 × (𝑦 ∩ (ℤ ↑m (0...(𝑝 − 1)))))))
36	1, 35	wceq 1542	1 wff /Qp = (𝑝 ∈ ℙ ↦ (~Qp ∩ ⦋{𝑓 ∈ (ℤ ↑m ℤ) ∣ ∃𝑥 ∈ ran ℤ≥(◡𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑦⦌(𝑦 × (𝑦 ∩ (ℤ ↑m (0...(𝑝 − 1)))))))

This definition is referenced by: (None)