Mathbox for Stefan O'Rear < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-dioph Structured version   Unicode version

Definition df-dioph 26814
 Description: A Diophantine set is a set of natural numbers which is a projection of the zero set of some polynomial. This definition somewhat awkwardly mixes (via mzPoly) and (to define the zero sets); the former could be avoided by considering coincidence sets of 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 13332 that implicitly restricting variables to adds no expressive power over allowing them to range over . While this definition stipulates a specific index set for the polynomials, there is actually flexibility here, see eldioph2b 26821. (Contributed by Stefan O'Rear, 5-Oct-2014.)
Assertion
Ref Expression
df-dioph Dioph mzPoly
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-dioph
StepHypRef Expression
1 cdioph 26813 . 2 Dioph
2 vn . . 3
3 cn0 10221 . . 3
4 vk . . . . 5
5 vp . . . . 5
62cv 1651 . . . . . 6
7 cuz 10488 . . . . . 6
86, 7cfv 5454 . . . . 5
9 c1 8991 . . . . . . 7
104cv 1651 . . . . . . 7
11 cfz 11043 . . . . . . 7
129, 10, 11co 6081 . . . . . 6
13 cmzp 26779 . . . . . 6 mzPoly
1412, 13cfv 5454 . . . . 5 mzPoly
15 vt . . . . . . . . . 10
1615cv 1651 . . . . . . . . 9
17 vu . . . . . . . . . . 11
1817cv 1651 . . . . . . . . . 10
199, 6, 11co 6081 . . . . . . . . . 10
2018, 19cres 4880 . . . . . . . . 9
2116, 20wceq 1652 . . . . . . . 8
225cv 1651 . . . . . . . . . 10
2318, 22cfv 5454 . . . . . . . . 9
24 cc0 8990 . . . . . . . . 9
2523, 24wceq 1652 . . . . . . . 8
2621, 25wa 359 . . . . . . 7
27 cmap 7018 . . . . . . . 8
283, 12, 27co 6081 . . . . . . 7
2926, 17, 28wrex 2706 . . . . . 6
3029, 15cab 2422 . . . . 5
314, 5, 8, 14, 30cmpt2 6083 . . . 4 mzPoly
3231crn 4879 . . 3 mzPoly
332, 3, 32cmpt 4266 . 2 mzPoly
341, 33wceq 1652 1 Dioph mzPoly
 Colors of variables: wff set class This definition is referenced by:  eldiophb  26815
 Copyright terms: Public domain W3C validator