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

Definition df-dioph 39868
 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 ℤ (via mzPoly) and ℕ0 (to define the zero sets); the former could be avoided by considering coincidence sets of ℕ0 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 16310 that implicitly restricting variables to ℕ0 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 39875. (Contributed by Stefan O'Rear, 5-Oct-2014.)
Assertion
Ref Expression
df-dioph Dioph = (𝑛 ∈ ℕ0 ↦ ran (𝑘 ∈ (ℤ𝑛), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝𝑢) = 0)}))
Distinct variable group:   𝑘,𝑛,𝑝,𝑡,𝑢

Detailed syntax breakdown of Definition df-dioph
StepHypRef Expression
1 cdioph 39867 . 2 class Dioph
2 vn . . 3 setvar 𝑛
3 cn0 11903 . . 3 class 0
4 vk . . . . 5 setvar 𝑘
5 vp . . . . 5 setvar 𝑝
62cv 1537 . . . . . 6 class 𝑛
7 cuz 12251 . . . . . 6 class
86, 7cfv 6332 . . . . 5 class (ℤ𝑛)
9 c1 10545 . . . . . . 7 class 1
104cv 1537 . . . . . . 7 class 𝑘
11 cfz 12905 . . . . . . 7 class ...
129, 10, 11co 7145 . . . . . 6 class (1...𝑘)
13 cmzp 39834 . . . . . 6 class mzPoly
1412, 13cfv 6332 . . . . 5 class (mzPoly‘(1...𝑘))
15 vt . . . . . . . . . 10 setvar 𝑡
1615cv 1537 . . . . . . . . 9 class 𝑡
17 vu . . . . . . . . . . 11 setvar 𝑢
1817cv 1537 . . . . . . . . . 10 class 𝑢
199, 6, 11co 7145 . . . . . . . . . 10 class (1...𝑛)
2018, 19cres 5525 . . . . . . . . 9 class (𝑢 ↾ (1...𝑛))
2116, 20wceq 1538 . . . . . . . 8 wff 𝑡 = (𝑢 ↾ (1...𝑛))
225cv 1537 . . . . . . . . . 10 class 𝑝
2318, 22cfv 6332 . . . . . . . . 9 class (𝑝𝑢)
24 cc0 10544 . . . . . . . . 9 class 0
2523, 24wceq 1538 . . . . . . . 8 wff (𝑝𝑢) = 0
2621, 25wa 399 . . . . . . 7 wff (𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝𝑢) = 0)
27 cmap 8407 . . . . . . . 8 class m
283, 12, 27co 7145 . . . . . . 7 class (ℕ0m (1...𝑘))
2926, 17, 28wrex 3107 . . . . . 6 wff 𝑢 ∈ (ℕ0m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝𝑢) = 0)
3029, 15cab 2776 . . . . 5 class {𝑡 ∣ ∃𝑢 ∈ (ℕ0m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝𝑢) = 0)}
314, 5, 8, 14, 30cmpo 7147 . . . 4 class (𝑘 ∈ (ℤ𝑛), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝𝑢) = 0)})
3231crn 5524 . . 3 class ran (𝑘 ∈ (ℤ𝑛), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝𝑢) = 0)})
332, 3, 32cmpt 5114 . 2 class (𝑛 ∈ ℕ0 ↦ ran (𝑘 ∈ (ℤ𝑛), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝𝑢) = 0)}))
341, 33wceq 1538 1 wff Dioph = (𝑛 ∈ ℕ0 ↦ ran (𝑘 ∈ (ℤ𝑛), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝𝑢) = 0)}))
 Colors of variables: wff setvar class This definition is referenced by:  eldiophb  39869
 Copyright terms: Public domain W3C validator