df-rqp - Mathbox for Mario Carneiro

	Mathbox for Mario Carneiro		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-rqp		Structured version Visualization version Unicode version

Definition df-rqp 31552

Description: There is a unique element of

~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 $\$

**Detailed syntax breakdown of Definition df-rqp**
Step	Hyp	Ref	Expression
1		crqp 31542	. 2 /Qp
2		vp	. . 3
3		cprime 15385	. . 3
4		ceqp 31541	. . . 4 ~Qp
5		vy	. . . . 5
6		vf	. . . . . . . . . . 11
7	6	cv 1482	. . . . . . . . . 10
8	7	ccnv 5113	. . . . . . . . 9
9		cz 11377	. . . . . . . . . 10
10		cc0 9936	. . . . . . . . . . 11
11	10	csn 4177	. . . . . . . . . 10
12	9, 11	cdif 3571	. . . . . . . . 9 $\$
13	8, 12	cima 5117	. . . . . . . 8 $\$
14		vx	. . . . . . . . 9
15	14	cv 1482	. . . . . . . 8
16	13, 15	wss 3574	. . . . . . 7 $\$
17		cuz 11687	. . . . . . . 8
18	17	crn 5115	. . . . . . 7
19	16, 14, 18	wrex 2913	. . . . . 6 $\$
20		cmap 7857	. . . . . . 7
21	9, 9, 20	co 6650	. . . . . 6
22	19, 6, 21	crab 2916	. . . . 5 $\$
23	5	cv 1482	. . . . . 6
24	2	cv 1482	. . . . . . . . . 10
25		c1 9937	. . . . . . . . . 10
26		cmin 10266	. . . . . . . . . 10
27	24, 25, 26	co 6650	. . . . . . . . 9
28		cfz 12326	. . . . . . . . 9
29	10, 27, 28	co 6650	. . . . . . . 8
30	9, 29, 20	co 6650	. . . . . . 7
31	23, 30	cin 3573	. . . . . 6
32	23, 31	cxp 5112	. . . . 5
33	5, 22, 32	csb 3533	. . . 4 $\$
34	4, 33	cin 3573	. . 3 ~Qp $\$
35	2, 3, 34	cmpt 4729	. 2 ~Qp $\$
36	1, 35	wceq 1483	1 /Qp ~Qp $\$

Colors of variables: wff setvar class

This definition is referenced by: (None)