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	|- Dioph = ( n e. NN0 |-> ran ( k e. ( ZZ>= ` n ) , p e. ( mzPoly ` ( 1 ... k ) ) |-> { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... n ) ) /\ ( p ` u ) = 0 ) } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdioph	|- Dioph
1		vn	|- n
2		cn0	|- NN0
3		vk	|- k
4		cuz	|- ZZ>=
5	1	cv	|- n
6	5 4	cfv	|- ( ZZ>= ` n )
7		vp	|- p
8		cmzp	|- mzPoly
9		c1	|- 1
10		cfz	|- ...
11	3	cv	|- k
12	9 11 10	co	|- ( 1 ... k )
13	12 8	cfv	|- ( mzPoly ` ( 1 ... k ) )
14		vt	|- t
15		vu	|- u
16		cmap	|- ^m
17	2 12 16	co	|- ( NN0 ^m ( 1 ... k ) )
18	14	cv	|- t
19	15	cv	|- u
20	9 5 10	co	|- ( 1 ... n )
21	19 20	cres	|- ( u |` ( 1 ... n ) )
22	18 21	wceq	|- t = ( u |` ( 1 ... n ) )
23	7	cv	|- p
24	19 23	cfv	|- ( p ` u )
25		cc0	|- 0
26	24 25	wceq	|- ( p ` u ) = 0
27	22 26	wa	|- ( t = ( u |` ( 1 ... n ) ) /\ ( p ` u ) = 0 )
28	27 15 17	wrex	|- E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... n ) ) /\ ( p ` u ) = 0 )
29	28 14	cab	|- { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... n ) ) /\ ( p ` u ) = 0 ) }
30	3 7 6 13 29	cmpo	|- ( k e. ( ZZ>= ` n ) , p e. ( mzPoly ` ( 1 ... k ) ) |-> { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... n ) ) /\ ( p ` u ) = 0 ) } )
31	30	crn	|- ran ( k e. ( ZZ>= ` n ) , p e. ( mzPoly ` ( 1 ... k ) ) |-> { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... n ) ) /\ ( p ` u ) = 0 ) } )
32	1 2 31	cmpt	|- ( n e. NN0 |-> ran ( k e. ( ZZ>= ` n ) , p e. ( mzPoly ` ( 1 ... k ) ) |-> { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... n ) ) /\ ( p ` u ) = 0 ) } ) )
33	0 32	wceq	|- Dioph = ( n e. NN0 |-> ran ( k e. ( ZZ>= ` n ) , p e. ( mzPoly ` ( 1 ... k ) ) |-> { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... n ) ) /\ ( p ` u ) = 0 ) } ) )