Definition df-dioph

Description: A Diophantine set is a set of positive integers which is a projection of the zero set of some polynomial. This definition somewhat awkwardly mixes ZZ (via mzPoly ) and NN0 (to define the zero sets); the former could be avoided by considering coincidence sets of NN0 polynomials at the cost of requiring two, and the second is driven by consistency with our mu-recursive functions and the requirements of the Davis-Putnam-Robinson-Matiyasevich proof. Both are avoidable at a complexity cost. In particular, it is a consequence of 4sq that implicitly restricting variables to NN0 adds no expressive power over allowing them to range over ZZ . While this definition stipulates a specific index set for the polynomials, there is actually flexibility here, see eldioph2b . (Contributed by Stefan O'Rear, 5-Oct-2014)

	Ref	Expression
Assertion	df-dioph	$$⊢\mathrm{Dioph}=\left(n\in {\mathbb{N}}_0⟼\mathrm{ran}\left(k\in {\mathbb{Z}}_{\ge n},p\in \mathrm{mzPoly}\left(\left(1\dots k\right)\right)⟼\left\{t|\exists u\in \left({{\mathbb{N}}_0}^{\left(1\dots k\right)}\right)\left(t={u\upharpoonright }_{\left(1\dots n\right)}\wedge p\left(u\right)=0\right)\right\}\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdioph	$$class\mathrm{Dioph}$$
1		vn	$$setvarn$$
2		cn0	$$class{\mathbb{N}}_0$$
3		vk	$$setvark$$
4		cuz	$$class{\mathbb{Z}}_{\ge }$$
5	1	cv	$$setvarn$$
6	5 4	cfv	$$class{\mathbb{Z}}_{\ge n}$$
7		vp	$$setvarp$$
8		cmzp	$$class\mathrm{mzPoly}$$
9		c1	$$class1$$
10		cfz	$$class\dots$$
11	3	cv	$$setvark$$
12	9 11 10	co	$$class\left(1\dots k\right)$$
13	12 8	cfv	$$class\mathrm{mzPoly}\left(\left(1\dots k\right)\right)$$
14		vt	$$setvart$$
15		vu	$$setvaru$$
16		cmap	$$class{\uparrow }_{𝑚}$$
17	2 12 16	co	$$class\left({{\mathbb{N}}_0}^{\left(1\dots k\right)}\right)$$
18	14	cv	$$setvart$$
19	15	cv	$$setvaru$$
20	9 5 10	co	$$class\left(1\dots n\right)$$
21	19 20	cres	$$class\left({u\upharpoonright }_{\left(1\dots n\right)}\right)$$
22	18 21	wceq	$$wfft={u\upharpoonright }_{\left(1\dots n\right)}$$
23	7	cv	$$setvarp$$
24	19 23	cfv	$$classp\left(u\right)$$
25		cc0	$$class0$$
26	24 25	wceq	$$wffp\left(u\right)=0$$
27	22 26	wa	$$wff\left(t={u\upharpoonright }_{\left(1\dots n\right)}\wedge p\left(u\right)=0\right)$$
28	27 15 17	wrex	$$wff\exists u\in \left({{\mathbb{N}}_0}^{\left(1\dots k\right)}\right)\left(t={u\upharpoonright }_{\left(1\dots n\right)}\wedge p\left(u\right)=0\right)$$
29	28 14	cab	$$class\left\{t|\exists u\in \left({{\mathbb{N}}_0}^{\left(1\dots k\right)}\right)\left(t={u\upharpoonright }_{\left(1\dots n\right)}\wedge p\left(u\right)=0\right)\right\}$$
30	3 7 6 13 29	cmpo	$$class\left(k\in {\mathbb{Z}}_{\ge n},p\in \mathrm{mzPoly}\left(\left(1\dots k\right)\right)⟼\left\{t|\exists u\in \left({{\mathbb{N}}_0}^{\left(1\dots k\right)}\right)\left(t={u\upharpoonright }_{\left(1\dots n\right)}\wedge p\left(u\right)=0\right)\right\}\right)$$
31	30	crn	$$class\mathrm{ran}\left(k\in {\mathbb{Z}}_{\ge n},p\in \mathrm{mzPoly}\left(\left(1\dots k\right)\right)⟼\left\{t|\exists u\in \left({{\mathbb{N}}_0}^{\left(1\dots k\right)}\right)\left(t={u\upharpoonright }_{\left(1\dots n\right)}\wedge p\left(u\right)=0\right)\right\}\right)$$
32	1 2 31	cmpt	$$class\left(n\in {\mathbb{N}}_0⟼\mathrm{ran}\left(k\in {\mathbb{Z}}_{\ge n},p\in \mathrm{mzPoly}\left(\left(1\dots k\right)\right)⟼\left\{t|\exists u\in \left({{\mathbb{N}}_0}^{\left(1\dots k\right)}\right)\left(t={u\upharpoonright }_{\left(1\dots n\right)}\wedge p\left(u\right)=0\right)\right\}\right)\right)$$
33	0 32	wceq	$$wff\mathrm{Dioph}=\left(n\in {\mathbb{N}}_0⟼\mathrm{ran}\left(k\in {\mathbb{Z}}_{\ge n},p\in \mathrm{mzPoly}\left(\left(1\dots k\right)\right)⟼\left\{t|\exists u\in \left({{\mathbb{N}}_0}^{\left(1\dots k\right)}\right)\left(t={u\upharpoonright }_{\left(1\dots n\right)}\wedge p\left(u\right)=0\right)\right\}\right)\right)$$