Metamath Proof Explorer

Theorem eldioph3b

Description: Define Diophantine sets in terms of polynomials with variables indexed by NN . This avoids a quantifier over the number of witness variables and will be easier to use than eldiophb in most cases. (Contributed by Stefan O'Rear, 10-Oct-2014)

Ref Expression
Assertion eldioph3b ⊢ A ∈ Dioph ⁡ N ↔ N ∈ ℕ 0 ∧ ∃ p ∈ mzPoly ⁡ ℕ A = t | ∃ u ∈ ℕ 0 ℕ t = u ↾ 1 … N ∧ p ⁡ u = 0

Proof

Step Hyp Ref Expression
1 eldiophelnn0 ⊢ A ∈ Dioph ⁡ N → N ∈ ℕ 0
2 nnex ⊢ ℕ ∈ V
3 1z ⊢ 1 ∈ ℤ
4 nnuz ⊢ ℕ = ℤ ≥ 1
5 4 uzinf ⊢ 1 ∈ ℤ → ¬ ℕ ∈ Fin
6 3 5 ax-mp ⊢ ¬ ℕ ∈ Fin
7 elfznn ⊢ p ∈ 1 … N → p ∈ ℕ
8 7 ssriv ⊢ 1 … N ⊆ ℕ
9 eldioph2b ⊢ N ∈ ℕ 0 ∧ ℕ ∈ V ∧ ¬ ℕ ∈ Fin ∧ 1 … N ⊆ ℕ → A ∈ Dioph ⁡ N ↔ ∃ p ∈ mzPoly ⁡ ℕ A = t | ∃ u ∈ ℕ 0 ℕ t = u ↾ 1 … N ∧ p ⁡ u = 0
10 6 8 9 mpanr12 ⊢ N ∈ ℕ 0 ∧ ℕ ∈ V → A ∈ Dioph ⁡ N ↔ ∃ p ∈ mzPoly ⁡ ℕ A = t | ∃ u ∈ ℕ 0 ℕ t = u ↾ 1 … N ∧ p ⁡ u = 0
11 2 10 mpan2 ⊢ N ∈ ℕ 0 → A ∈ Dioph ⁡ N ↔ ∃ p ∈ mzPoly ⁡ ℕ A = t | ∃ u ∈ ℕ 0 ℕ t = u ↾ 1 … N ∧ p ⁡ u = 0
12 1 11 biadanii ⊢ A ∈ Dioph ⁡ N ↔ N ∈ ℕ 0 ∧ ∃ p ∈ mzPoly ⁡ ℕ A = t | ∃ u ∈ ℕ 0 ℕ t = u ↾ 1 … N ∧ p ⁡ u = 0