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 ℕ₀ (to define the zero sets); the former could be avoided by considering coincidence sets of ℕ₀ 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 ℕ₀ 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...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0 ↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝‘𝑢) = 0)}))

Distinct variable group:   𝑘,𝑛,𝑝,𝑡,𝑢

Detailed syntax breakdown of Definition df-dioph

Step	Hyp	Ref	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 𝑝
6	2	cv 1542	. . . . . 6 class 𝑛
7		cuz 12438	. . . . . 6 class ℤ≥
8	6, 7	cfv 6380	. . . . 5 class (ℤ≥‘𝑛)
9		c1 10730	. . . . . . 7 class 1
10	4	cv 1542	. . . . . . 7 class 𝑘
11		cfz 13095	. . . . . . 7 class ...
12	9, 10, 11	co 7213	. . . . . 6 class (1...𝑘)
13		cmzp 40247	. . . . . 6 class mzPoly
14	12, 13	cfv 6380	. . . . 5 class (mzPoly‘(1...𝑘))
15		vt	. . . . . . . . . 10 setvar 𝑡
16	15	cv 1542	. . . . . . . . 9 class 𝑡
17		vu	. . . . . . . . . . 11 setvar 𝑢
18	17	cv 1542	. . . . . . . . . 10 class 𝑢
19	9, 6, 11	co 7213	. . . . . . . . . 10 class (1...𝑛)
20	18, 19	cres 5553	. . . . . . . . 9 class (𝑢 ↾ (1...𝑛))
21	16, 20	wceq 1543	. . . . . . . 8 wff 𝑡 = (𝑢 ↾ (1...𝑛))
22	5	cv 1542	. . . . . . . . . 10 class 𝑝
23	18, 22	cfv 6380	. . . . . . . . 9 class (𝑝‘𝑢)
24		cc0 10729	. . . . . . . . 9 class 0
25	23, 24	wceq 1543	. . . . . . . 8 wff (𝑝‘𝑢) = 0
26	21, 25	wa 399	. . . . . . 7 wff (𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝‘𝑢) = 0)
27		cmap 8508	. . . . . . . 8 class ↑m
28	3, 12, 27	co 7213	. . . . . . 7 class (ℕ0 ↑m (1...𝑘))
29	26, 17, 28	wrex 3062	. . . . . 6 wff ∃𝑢 ∈ (ℕ0 ↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝‘𝑢) = 0)
30	29, 15	cab 2714	. . . . 5 class {𝑡 ∣ ∃𝑢 ∈ (ℕ0 ↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝‘𝑢) = 0)}
31	4, 5, 8, 14, 30	cmpo 7215	. . . 4 class (𝑘 ∈ (ℤ≥‘𝑛), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0 ↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝‘𝑢) = 0)})
32	31	crn 5552	. . 3 class ran (𝑘 ∈ (ℤ≥‘𝑛), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0 ↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝‘𝑢) = 0)})
33	2, 3, 32	cmpt 5135	. 2 class (𝑛 ∈ ℕ0 ↦ ran (𝑘 ∈ (ℤ≥‘𝑛), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0 ↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝‘𝑢) = 0)}))
34	1, 33	wceq 1543	1 wff Dioph = (𝑛 ∈ ℕ0 ↦ ran (𝑘 ∈ (ℤ≥‘𝑛), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0 ↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝‘𝑢) = 0)}))

This definition is referenced by:  eldiophb  40282