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 40281
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 16517 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 40288. (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 40280 . 2 class Dioph
2 vn . . 3 setvar 𝑛
3 cn0 12090 . . 3 class 0
4 vk . . . . 5 setvar 𝑘
5 vp . . . . 5 setvar 𝑝
62cv 1542 . . . . . 6 class 𝑛
7 cuz 12438 . . . . . 6 class
86, 7cfv 6380 . . . . 5 class (ℤ𝑛)
9 c1 10730 . . . . . . 7 class 1
104cv 1542 . . . . . . 7 class 𝑘
11 cfz 13095 . . . . . . 7 class ...
129, 10, 11co 7213 . . . . . 6 class (1...𝑘)
13 cmzp 40247 . . . . . 6 class mzPoly
1412, 13cfv 6380 . . . . 5 class (mzPoly‘(1...𝑘))
15 vt . . . . . . . . . 10 setvar 𝑡
1615cv 1542 . . . . . . . . 9 class 𝑡
17 vu . . . . . . . . . . 11 setvar 𝑢
1817cv 1542 . . . . . . . . . 10 class 𝑢
199, 6, 11co 7213 . . . . . . . . . 10 class (1...𝑛)
2018, 19cres 5553 . . . . . . . . 9 class (𝑢 ↾ (1...𝑛))
2116, 20wceq 1543 . . . . . . . 8 wff 𝑡 = (𝑢 ↾ (1...𝑛))
225cv 1542 . . . . . . . . . 10 class 𝑝
2318, 22cfv 6380 . . . . . . . . 9 class (𝑝𝑢)
24 cc0 10729 . . . . . . . . 9 class 0
2523, 24wceq 1543 . . . . . . . 8 wff (𝑝𝑢) = 0
2621, 25wa 399 . . . . . . 7 wff (𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝𝑢) = 0)
27 cmap 8508 . . . . . . . 8 class m
283, 12, 27co 7213 . . . . . . 7 class (ℕ0m (1...𝑘))
2926, 17, 28wrex 3062 . . . . . 6 wff 𝑢 ∈ (ℕ0m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝𝑢) = 0)
3029, 15cab 2714 . . . . 5 class {𝑡 ∣ ∃𝑢 ∈ (ℕ0m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝𝑢) = 0)}
314, 5, 8, 14, 30cmpo 7215 . . . 4 class (𝑘 ∈ (ℤ𝑛), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝𝑢) = 0)})
3231crn 5552 . . 3 class ran (𝑘 ∈ (ℤ𝑛), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝𝑢) = 0)})
332, 3, 32cmpt 5135 . 2 class (𝑛 ∈ ℕ0 ↦ ran (𝑘 ∈ (ℤ𝑛), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝𝑢) = 0)}))
341, 33wceq 1543 1 wff Dioph = (𝑛 ∈ ℕ0 ↦ ran (𝑘 ∈ (ℤ𝑛), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝𝑢) = 0)}))
Colors of variables: wff setvar class
This definition is referenced by:  eldiophb  40282
  Copyright terms: Public domain W3C validator