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 37138
 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 15649 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 37145. (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 37137 . 2 class Dioph
2 vn . . 3 setvar 𝑛
3 cn0 11277 . . 3 class 0
4 vk . . . . 5 setvar 𝑘
5 vp . . . . 5 setvar 𝑝
62cv 1480 . . . . . 6 class 𝑛
7 cuz 11672 . . . . . 6 class
86, 7cfv 5876 . . . . 5 class (ℤ𝑛)
9 c1 9922 . . . . . . 7 class 1
104cv 1480 . . . . . . 7 class 𝑘
11 cfz 12311 . . . . . . 7 class ...
129, 10, 11co 6635 . . . . . 6 class (1...𝑘)
13 cmzp 37104 . . . . . 6 class mzPoly
1412, 13cfv 5876 . . . . 5 class (mzPoly‘(1...𝑘))
15 vt . . . . . . . . . 10 setvar 𝑡
1615cv 1480 . . . . . . . . 9 class 𝑡
17 vu . . . . . . . . . . 11 setvar 𝑢
1817cv 1480 . . . . . . . . . 10 class 𝑢
199, 6, 11co 6635 . . . . . . . . . 10 class (1...𝑛)
2018, 19cres 5106 . . . . . . . . 9 class (𝑢 ↾ (1...𝑛))
2116, 20wceq 1481 . . . . . . . 8 wff 𝑡 = (𝑢 ↾ (1...𝑛))
225cv 1480 . . . . . . . . . 10 class 𝑝
2318, 22cfv 5876 . . . . . . . . 9 class (𝑝𝑢)
24 cc0 9921 . . . . . . . . 9 class 0
2523, 24wceq 1481 . . . . . . . 8 wff (𝑝𝑢) = 0
2621, 25wa 384 . . . . . . 7 wff (𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝𝑢) = 0)
27 cmap 7842 . . . . . . . 8 class 𝑚
283, 12, 27co 6635 . . . . . . 7 class (ℕ0𝑚 (1...𝑘))
2926, 17, 28wrex 2910 . . . . . 6 wff 𝑢 ∈ (ℕ0𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝𝑢) = 0)
3029, 15cab 2606 . . . . 5 class {𝑡 ∣ ∃𝑢 ∈ (ℕ0𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝𝑢) = 0)}
314, 5, 8, 14, 30cmpt2 6637 . . . 4 class (𝑘 ∈ (ℤ𝑛), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝𝑢) = 0)})
3231crn 5105 . . 3 class ran (𝑘 ∈ (ℤ𝑛), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝𝑢) = 0)})
332, 3, 32cmpt 4720 . 2 class (𝑛 ∈ ℕ0 ↦ ran (𝑘 ∈ (ℤ𝑛), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝𝑢) = 0)}))
341, 33wceq 1481 1 wff Dioph = (𝑛 ∈ ℕ0 ↦ ran (𝑘 ∈ (ℤ𝑛), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝𝑢) = 0)}))
 Colors of variables: wff setvar class This definition is referenced by:  eldiophb  37139
 Copyright terms: Public domain W3C validator