Metamath Proof Explorer

Theorem eldiophb

Description: Initial expression of Diophantine property of a set. (Contributed by Stefan O'Rear, 5-Oct-2014) (Revised by Mario Carneiro, 22-Sep-2015)

Ref Expression
Assertion eldiophb ( 𝐷 ∈ ( Dioph ‘ 𝑁 ) ↔ ( 𝑁 ∈ ℕ0 ∧ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ∃ 𝑝 ∈ ( mzPoly ‘ ( 1 ... 𝑘 ) ) 𝐷 = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) )

Proof

Step Hyp Ref Expression
1 df-dioph ⊢ Dioph = ( 𝑛 ∈ ℕ0 ↦ ran ( 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) , 𝑝 ∈ ( mzPoly ‘ ( 1 ... 𝑘 ) ) ↦ { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑛 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) )
2 1 dmmptss ⊢ dom Dioph ⊆ ℕ0
3 elfvdm ⊢ ( 𝐷 ∈ ( Dioph ‘ 𝑁 ) → 𝑁 ∈ dom Dioph )
4 2 3 sseldi ⊢ ( 𝐷 ∈ ( Dioph ‘ 𝑁 ) → 𝑁 ∈ ℕ0 )
5 fveq2 ⊢ ( 𝑛 = 𝑁 → ( ℤ≥ ‘ 𝑛 ) = ( ℤ≥ ‘ 𝑁 ) )
6 eqidd ⊢ ( 𝑛 = 𝑁 → ( mzPoly ‘ ( 1 ... 𝑘 ) ) = ( mzPoly ‘ ( 1 ... 𝑘 ) ) )
7 oveq2 ⊢ ( 𝑛 = 𝑁 → ( 1 ... 𝑛 ) = ( 1 ... 𝑁 ) )
8 7 reseq2d ⊢ ( 𝑛 = 𝑁 → ( 𝑢 ↾ ( 1 ... 𝑛 ) ) = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) )
9 8 eqeq2d ⊢ ( 𝑛 = 𝑁 → ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑛 ) ) ↔ 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ) )
10 9 anbi1d ⊢ ( 𝑛 = 𝑁 → ( ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑛 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) ↔ ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) ) )
11 10 rexbidv ⊢ ( 𝑛 = 𝑁 → ( ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑛 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) ↔ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) ) )
12 11 abbidv ⊢ ( 𝑛 = 𝑁 → { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑛 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } )
13 5 6 12 mpoeq123dv ⊢ ( 𝑛 = 𝑁 → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) , 𝑝 ∈ ( mzPoly ‘ ( 1 ... 𝑘 ) ) ↦ { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑛 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) = ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) , 𝑝 ∈ ( mzPoly ‘ ( 1 ... 𝑘 ) ) ↦ { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) )
14 13 rneqd ⊢ ( 𝑛 = 𝑁 → ran ( 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) , 𝑝 ∈ ( mzPoly ‘ ( 1 ... 𝑘 ) ) ↦ { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑛 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) = ran ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) , 𝑝 ∈ ( mzPoly ‘ ( 1 ... 𝑘 ) ) ↦ { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) )
15 ovex ⊢ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∈ V
16 15 pwex ⊢ 𝒫 ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∈ V
17 eqid ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) , 𝑝 ∈ ( mzPoly ‘ ( 1 ... 𝑘 ) ) ↦ { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) = ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) , 𝑝 ∈ ( mzPoly ‘ ( 1 ... 𝑘 ) ) ↦ { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } )
18 17 rnmpo ⊢ ran ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) , 𝑝 ∈ ( mzPoly ‘ ( 1 ... 𝑘 ) ) ↦ { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) = { 𝑑 ∣ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ∃ 𝑝 ∈ ( mzPoly ‘ ( 1 ... 𝑘 ) ) 𝑑 = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } }
19 elmapi ⊢ ( 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) → 𝑢 : ( 1 ... 𝑘 ) ⟶ ℕ0 )
20 fzss2 ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 1 ... 𝑁 ) ⊆ ( 1 ... 𝑘 ) )
21 fssres ⊢ ( ( 𝑢 : ( 1 ... 𝑘 ) ⟶ ℕ0 ∧ ( 1 ... 𝑁 ) ⊆ ( 1 ... 𝑘 ) ) → ( 𝑢 ↾ ( 1 ... 𝑁 ) ) : ( 1 ... 𝑁 ) ⟶ ℕ0 )
22 19 20 21 syl2anr ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ) → ( 𝑢 ↾ ( 1 ... 𝑁 ) ) : ( 1 ... 𝑁 ) ⟶ ℕ0 )
23 nn0ex ⊢ ℕ0 ∈ V
24 ovex ⊢ ( 1 ... 𝑁 ) ∈ V
25 23 24 elmap ⊢ ( ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ↔ ( 𝑢 ↾ ( 1 ... 𝑁 ) ) : ( 1 ... 𝑁 ) ⟶ ℕ0 )
26 22 25 sylibr ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ) → ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) )
27 eleq1 ⊢ ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) → ( 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ↔ ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) )
28 27 adantr ⊢ ( ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) → ( 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ↔ ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) )
29 26 28 syl5ibrcom ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ) → ( ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) → 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) )
30 29 rexlimdva ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) → ( ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) → 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) )
31 30 abssdv ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) → { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ⊆ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) )
32 15 elpw2 ⊢ ( { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ∈ 𝒫 ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ↔ { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ⊆ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) )
33 31 32 sylibr ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) → { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ∈ 𝒫 ( ℕ0 ↑m ( 1 ... 𝑁 ) ) )
34 eleq1 ⊢ ( 𝑑 = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } → ( 𝑑 ∈ 𝒫 ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ↔ { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ∈ 𝒫 ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) )
35 33 34 syl5ibrcom ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝑑 = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } → 𝑑 ∈ 𝒫 ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) )
36 35 rexlimdvw ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) → ( ∃ 𝑝 ∈ ( mzPoly ‘ ( 1 ... 𝑘 ) ) 𝑑 = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } → 𝑑 ∈ 𝒫 ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) )
37 36 rexlimiv ⊢ ( ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ∃ 𝑝 ∈ ( mzPoly ‘ ( 1 ... 𝑘 ) ) 𝑑 = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } → 𝑑 ∈ 𝒫 ( ℕ0 ↑m ( 1 ... 𝑁 ) ) )
38 37 abssi ⊢ { 𝑑 ∣ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ∃ 𝑝 ∈ ( mzPoly ‘ ( 1 ... 𝑘 ) ) 𝑑 = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } } ⊆ 𝒫 ( ℕ0 ↑m ( 1 ... 𝑁 ) )
39 18 38 eqsstri ⊢ ran ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) , 𝑝 ∈ ( mzPoly ‘ ( 1 ... 𝑘 ) ) ↦ { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) ⊆ 𝒫 ( ℕ0 ↑m ( 1 ... 𝑁 ) )
40 16 39 ssexi ⊢ ran ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) , 𝑝 ∈ ( mzPoly ‘ ( 1 ... 𝑘 ) ) ↦ { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) ∈ V
41 14 1 40 fvmpt ⊢ ( 𝑁 ∈ ℕ0 → ( Dioph ‘ 𝑁 ) = ran ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) , 𝑝 ∈ ( mzPoly ‘ ( 1 ... 𝑘 ) ) ↦ { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) )
42 41 eleq2d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐷 ∈ ( Dioph ‘ 𝑁 ) ↔ 𝐷 ∈ ran ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) , 𝑝 ∈ ( mzPoly ‘ ( 1 ... 𝑘 ) ) ↦ { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) ) )
43 ovex ⊢ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ∈ V
44 43 abrexex ⊢ { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) } ∈ V
45 simpl ⊢ ( ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) → 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) )
46 45 reximi ⊢ ( ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) → ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) )
47 46 ss2abi ⊢ { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ⊆ { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) }
48 44 47 ssexi ⊢ { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ∈ V
49 17 48 elrnmpo ⊢ ( 𝐷 ∈ ran ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) , 𝑝 ∈ ( mzPoly ‘ ( 1 ... 𝑘 ) ) ↦ { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) ↔ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ∃ 𝑝 ∈ ( mzPoly ‘ ( 1 ... 𝑘 ) ) 𝐷 = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } )
50 42 49 bitrdi ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐷 ∈ ( Dioph ‘ 𝑁 ) ↔ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ∃ 𝑝 ∈ ( mzPoly ‘ ( 1 ... 𝑘 ) ) 𝐷 = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) )
51 4 50 biadanii ⊢ ( 𝐷 ∈ ( Dioph ‘ 𝑁 ) ↔ ( 𝑁 ∈ ℕ0 ∧ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ∃ 𝑝 ∈ ( mzPoly ‘ ( 1 ... 𝑘 ) ) 𝐷 = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) )