Definition df-dioph 37319

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 15668 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 37326. (Contributed by Stefan O'Rear, 5-Oct-2014.)

Assertion

Ref	Expression
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 ) } ) )

Distinct variable group:   k, n, p, t, u

Detailed syntax breakdown of Definition df-dioph

Step	Hyp	Ref	Expression
1		cdioph 37318	. 2 class Dioph
2		vn	. . 3 setvar n
3		cn0 11292	. . 3 class NN0
4		vk	. . . . 5 setvar k
5		vp	. . . . 5 setvar p
6	2	cv 1482	. . . . . 6 class n
7		cuz 11687	. . . . . 6 class ZZ>=
8	6, 7	cfv 5888	. . . . 5 class ( ZZ>= ` n )
9		c1 9937	. . . . . . 7 class 1
10	4	cv 1482	. . . . . . 7 class k
11		cfz 12326	. . . . . . 7 class ...
12	9, 10, 11	co 6650	. . . . . 6 class ( 1 ... k )
13		cmzp 37285	. . . . . 6 class mzPoly
14	12, 13	cfv 5888	. . . . 5 class (mzPoly ` ( 1 ... k ) )
15		vt	. . . . . . . . . 10 setvar t
16	15	cv 1482	. . . . . . . . 9 class t
17		vu	. . . . . . . . . . 11 setvar u
18	17	cv 1482	. . . . . . . . . 10 class u
19	9, 6, 11	co 6650	. . . . . . . . . 10 class ( 1 ... n )
20	18, 19	cres 5116	. . . . . . . . 9 class ( u |` ( 1 ... n ) )
21	16, 20	wceq 1483	. . . . . . . 8 wff t = ( u |` ( 1 ... n ) )
22	5	cv 1482	. . . . . . . . . 10 class p
23	18, 22	cfv 5888	. . . . . . . . 9 class ( p ` u )
24		cc0 9936	. . . . . . . . 9 class 0
25	23, 24	wceq 1483	. . . . . . . 8 wff ( p ` u ) = 0
26	21, 25	wa 384	. . . . . . 7 wff ( t = ( u |` ( 1 ... n ) ) /\ ( p ` u ) = 0 )
27		cmap 7857	. . . . . . . 8 class ^m
28	3, 12, 27	co 6650	. . . . . . 7 class ( NN0 ^m ( 1 ... k ) )
29	26, 17, 28	wrex 2913	. . . . . 6 wff E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... n ) ) /\ ( p ` u ) = 0 )
30	29, 15	cab 2608	. . . . 5 class { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... n ) ) /\ ( p ` u ) = 0 ) }
31	4, 5, 8, 14, 30	cmpt2 6652	. . . 4 class ( 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	31	crn 5115	. . 3 class 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	2, 3, 32	cmpt 4729	. 2 class ( 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 ) } ) )
34	1, 33	wceq 1483	1 wff 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 ) } ) )

This definition is referenced by:  eldiophb  37320