Users' Mathboxes 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 36136
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 15448 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 36143. (Contributed by Stefan O'Rear, 5-Oct-2014.)
Assertion
Ref Expression
df-dioph Dioph = (𝑛 ∈ ℕ0 ↦ ran (𝑘 ∈ (ℤ𝑛), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝𝑢) = 0)}))
Distinct variable group:   𝑘,𝑛,𝑝,𝑡,𝑢

Detailed syntax breakdown of Definition df-dioph
StepHypRef Expression
1 cdioph 36135 . 2 class Dioph
2 vn . . 3 setvar 𝑛
3 cn0 11135 . . 3 class 0
4 vk . . . . 5 setvar 𝑘
5 vp . . . . 5 setvar 𝑝
62cv 1473 . . . . . 6 class 𝑛
7 cuz 11515 . . . . . 6 class
86, 7cfv 5786 . . . . 5 class (ℤ𝑛)
9 c1 9789 . . . . . . 7 class 1
104cv 1473 . . . . . . 7 class 𝑘
11 cfz 12148 . . . . . . 7 class ...
129, 10, 11co 6523 . . . . . 6 class (1...𝑘)
13 cmzp 36102 . . . . . 6 class mzPoly
1412, 13cfv 5786 . . . . 5 class (mzPoly‘(1...𝑘))
15 vt . . . . . . . . . 10 setvar 𝑡
1615cv 1473 . . . . . . . . 9 class 𝑡
17 vu . . . . . . . . . . 11 setvar 𝑢
1817cv 1473 . . . . . . . . . 10 class 𝑢
199, 6, 11co 6523 . . . . . . . . . 10 class (1...𝑛)
2018, 19cres 5026 . . . . . . . . 9 class (𝑢 ↾ (1...𝑛))
2116, 20wceq 1474 . . . . . . . 8 wff 𝑡 = (𝑢 ↾ (1...𝑛))
225cv 1473 . . . . . . . . . 10 class 𝑝
2318, 22cfv 5786 . . . . . . . . 9 class (𝑝𝑢)
24 cc0 9788 . . . . . . . . 9 class 0
2523, 24wceq 1474 . . . . . . . 8 wff (𝑝𝑢) = 0
2621, 25wa 382 . . . . . . 7 wff (𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝𝑢) = 0)
27 cmap 7717 . . . . . . . 8 class 𝑚
283, 12, 27co 6523 . . . . . . 7 class (ℕ0𝑚 (1...𝑘))
2926, 17, 28wrex 2892 . . . . . 6 wff 𝑢 ∈ (ℕ0𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝𝑢) = 0)
3029, 15cab 2591 . . . . 5 class {𝑡 ∣ ∃𝑢 ∈ (ℕ0𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝𝑢) = 0)}
314, 5, 8, 14, 30cmpt2 6525 . . . 4 class (𝑘 ∈ (ℤ𝑛), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝𝑢) = 0)})
3231crn 5025 . . 3 class ran (𝑘 ∈ (ℤ𝑛), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝𝑢) = 0)})
332, 3, 32cmpt 4633 . 2 class (𝑛 ∈ ℕ0 ↦ ran (𝑘 ∈ (ℤ𝑛), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝𝑢) = 0)}))
341, 33wceq 1474 1 wff Dioph = (𝑛 ∈ ℕ0 ↦ ran (𝑘 ∈ (ℤ𝑛), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝𝑢) = 0)}))
Colors of variables: wff setvar class
This definition is referenced by:  eldiophb  36137
  Copyright terms: Public domain W3C validator