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

Definition df-dioph 26835
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  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 13011 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 26842. (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
StepHypRef Expression
1 cdioph 26834 . 2  class Dioph
2 vn . . 3  set  n
3 cn0 9965 . . 3  class  NN0
4 vk . . . . 5  set  k
5 vp . . . . 5  set  p
62cv 1622 . . . . . 6  class  n
7 cuz 10230 . . . . . 6  class  ZZ>=
86, 7cfv 5255 . . . . 5  class  ( ZZ>= `  n )
9 c1 8738 . . . . . . 7  class  1
104cv 1622 . . . . . . 7  class  k
11 cfz 10782 . . . . . . 7  class  ...
129, 10, 11co 5858 . . . . . 6  class  ( 1 ... k )
13 cmzp 26800 . . . . . 6  class mzPoly
1412, 13cfv 5255 . . . . 5  class  (mzPoly `  ( 1 ... k
) )
15 vt . . . . . . . . . 10  set  t
1615cv 1622 . . . . . . . . 9  class  t
17 vu . . . . . . . . . . 11  set  u
1817cv 1622 . . . . . . . . . 10  class  u
199, 6, 11co 5858 . . . . . . . . . 10  class  ( 1 ... n )
2018, 19cres 4691 . . . . . . . . 9  class  ( u  |`  ( 1 ... n
) )
2116, 20wceq 1623 . . . . . . . 8  wff  t  =  ( u  |`  (
1 ... n ) )
225cv 1622 . . . . . . . . . 10  class  p
2318, 22cfv 5255 . . . . . . . . 9  class  ( p `
 u )
24 cc0 8737 . . . . . . . . 9  class  0
2523, 24wceq 1623 . . . . . . . 8  wff  ( p `
 u )  =  0
2621, 25wa 358 . . . . . . 7  wff  ( t  =  ( u  |`  ( 1 ... n
) )  /\  (
p `  u )  =  0 )
27 cmap 6772 . . . . . . . 8  class  ^m
283, 12, 27co 5858 . . . . . . 7  class  ( NN0 
^m  ( 1 ... k ) )
2926, 17, 28wrex 2544 . . . . . 6  wff  E. u  e.  ( NN0  ^m  (
1 ... k ) ) ( t  =  ( u  |`  ( 1 ... n ) )  /\  ( p `  u )  =  0 )
3029, 15cab 2269 . . . . 5  class  { t  |  E. u  e.  ( NN0  ^m  (
1 ... k ) ) ( t  =  ( u  |`  ( 1 ... n ) )  /\  ( p `  u )  =  0 ) }
314, 5, 8, 14, 30cmpt2 5860 . . . 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 ) } )
3231crn 4690 . . 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 ) } )
332, 3, 32cmpt 4077 . 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 ) } ) )
341, 33wceq 1623 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 ) } ) )
Colors of variables: wff set class
This definition is referenced by:  eldiophb  26836
  Copyright terms: Public domain W3C validator