Definition df-rqp 32898

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 32889	. 2 class /Qp
2		vp	. . 3 setvar 𝑝
3		cprime 16009	. . 3 class ℙ
4		ceqp 32888	. . . 4 class ~Qp
5		vy	. . . . 5 setvar 𝑦
6		vf	. . . . . . . . . . 11 setvar 𝑓
7	6	cv 1532	. . . . . . . . . 10 class 𝑓
8	7	ccnv 5549	. . . . . . . . 9 class ◡𝑓
9		cz 11975	. . . . . . . . . 10 class ℤ
10		cc0 10531	. . . . . . . . . . 11 class 0
11	10	csn 4561	. . . . . . . . . 10 class {0}
12	9, 11	cdif 3933	. . . . . . . . 9 class (ℤ ∖ {0})
13	8, 12	cima 5553	. . . . . . . 8 class (◡𝑓 “ (ℤ ∖ {0}))
14		vx	. . . . . . . . 9 setvar 𝑥
15	14	cv 1532	. . . . . . . 8 class 𝑥
16	13, 15	wss 3936	. . . . . . 7 wff (◡𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥
17		cuz 12237	. . . . . . . 8 class ℤ≥
18	17	crn 5551	. . . . . . 7 class ran ℤ≥
19	16, 14, 18	wrex 3139	. . . . . 6 wff ∃𝑥 ∈ ran ℤ≥(◡𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥
20		cmap 8400	. . . . . . 7 class ↑m
21	9, 9, 20	co 7150	. . . . . 6 class (ℤ ↑m ℤ)
22	19, 6, 21	crab 3142	. . . . 5 class {𝑓 ∈ (ℤ ↑m ℤ) ∣ ∃𝑥 ∈ ran ℤ≥(◡𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥}
23	5	cv 1532	. . . . . 6 class 𝑦
24	2	cv 1532	. . . . . . . . . 10 class 𝑝
25		c1 10532	. . . . . . . . . 10 class 1
26		cmin 10864	. . . . . . . . . 10 class −
27	24, 25, 26	co 7150	. . . . . . . . 9 class (𝑝 − 1)
28		cfz 12886	. . . . . . . . 9 class ...
29	10, 27, 28	co 7150	. . . . . . . 8 class (0...(𝑝 − 1))
30	9, 29, 20	co 7150	. . . . . . 7 class (ℤ ↑m (0...(𝑝 − 1)))
31	23, 30	cin 3935	. . . . . 6 class (𝑦 ∩ (ℤ ↑m (0...(𝑝 − 1))))
32	23, 31	cxp 5548	. . . . 5 class (𝑦 × (𝑦 ∩ (ℤ ↑m (0...(𝑝 − 1)))))
33	5, 22, 32	csb 3883	. . . 4 class ⦋{𝑓 ∈ (ℤ ↑m ℤ) ∣ ∃𝑥 ∈ ran ℤ≥(◡𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑦⦌(𝑦 × (𝑦 ∩ (ℤ ↑m (0...(𝑝 − 1)))))
34	4, 33	cin 3935	. . 3 class (~Qp ∩ ⦋{𝑓 ∈ (ℤ ↑m ℤ) ∣ ∃𝑥 ∈ ran ℤ≥(◡𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑦⦌(𝑦 × (𝑦 ∩ (ℤ ↑m (0...(𝑝 − 1))))))
35	2, 3, 34	cmpt 5139	. 2 class (𝑝 ∈ ℙ ↦ (~Qp ∩ ⦋{𝑓 ∈ (ℤ ↑m ℤ) ∣ ∃𝑥 ∈ ran ℤ≥(◡𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑦⦌(𝑦 × (𝑦 ∩ (ℤ ↑m (0...(𝑝 − 1)))))))
36	1, 35	wceq 1533	1 wff /Qp = (𝑝 ∈ ℙ ↦ (~Qp ∩ ⦋{𝑓 ∈ (ℤ ↑m ℤ) ∣ ∃𝑥 ∈ ran ℤ≥(◡𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑦⦌(𝑦 × (𝑦 ∩ (ℤ ↑m (0...(𝑝 − 1)))))))

This definition is referenced by: (None)