Definition df-dioph

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 ZZ (via mzPoly ) and NN0 (to define the zero sets); the former could be avoided by considering coincidence sets of NN0 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 that implicitly restricting variables to NN0 adds no expressive power over allowing them to range over ZZ . While this definition stipulates a specific index set for the polynomials, there is actually flexibility here, see eldioph2b . (Contributed by Stefan O'Rear, 5-Oct-2014)

	Ref	Expression
Assertion	df-dioph	⊢ Dioph = ( 𝑛 ∈ ℕ0 ↦ ran ( 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) , 𝑝 ∈ ( mzPoly ‘ ( 1 ... 𝑘 ) ) ↦ { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑛 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdioph	⊢ Dioph
1		vn	⊢ 𝑛
2		cn0	⊢ ℕ0
3		vk	⊢ 𝑘
4		cuz	⊢ ℤ≥
5	1	cv	⊢ 𝑛
6	5 4	cfv	⊢ ( ℤ≥ ‘ 𝑛 )
7		vp	⊢ 𝑝
8		cmzp	⊢ mzPoly
9		c1	⊢ 1
10		cfz	⊢ ...
11	3	cv	⊢ 𝑘
12	9 11 10	co	⊢ ( 1 ... 𝑘 )
13	12 8	cfv	⊢ ( mzPoly ‘ ( 1 ... 𝑘 ) )
14		vt	⊢ 𝑡
15		vu	⊢ 𝑢
16		cmap	⊢ ↑m
17	2 12 16	co	⊢ ( ℕ0 ↑m ( 1 ... 𝑘 ) )
18	14	cv	⊢ 𝑡
19	15	cv	⊢ 𝑢
20	9 5 10	co	⊢ ( 1 ... 𝑛 )
21	19 20	cres	⊢ ( 𝑢 ↾ ( 1 ... 𝑛 ) )
22	18 21	wceq	⊢ 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑛 ) )
23	7	cv	⊢ 𝑝
24	19 23	cfv	⊢ ( 𝑝 ‘ 𝑢 )
25		cc0	⊢ 0
26	24 25	wceq	⊢ ( 𝑝 ‘ 𝑢 ) = 0
27	22 26	wa	⊢ ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑛 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 )
28	27 15 17	wrex	⊢ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑛 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 )
29	28 14	cab	⊢ { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑛 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) }
30	3 7 6 13 29	cmpo	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) , 𝑝 ∈ ( mzPoly ‘ ( 1 ... 𝑘 ) ) ↦ { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑛 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } )
31	30	crn	⊢ ran ( 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) , 𝑝 ∈ ( mzPoly ‘ ( 1 ... 𝑘 ) ) ↦ { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑛 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } )
32	1 2 31	cmpt	⊢ ( 𝑛 ∈ ℕ0 ↦ ran ( 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) , 𝑝 ∈ ( mzPoly ‘ ( 1 ... 𝑘 ) ) ↦ { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑛 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) )
33	0 32	wceq	⊢ Dioph = ( 𝑛 ∈ ℕ0 ↦ ran ( 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) , 𝑝 ∈ ( mzPoly ‘ ( 1 ... 𝑘 ) ) ↦ { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑛 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) )