Metamath Proof Explorer

Theorem elnnrabdioph

Description: Diophantine set builder for positivity. (Contributed by Stefan O'Rear, 11-Oct-2014)

Ref Expression
Assertion elnnrabdioph ⊢ N ∈ ℕ 0 ∧ t ∈ ℤ 1 … N ⟼ A ∈ mzPoly ⁡ 1 … N → t ∈ ℕ 0 1 … N | A ∈ ℕ ∈ Dioph ⁡ N

Proof

Step Hyp Ref Expression
1 elnnuz ⊢ A ∈ ℕ ↔ A ∈ ℤ ≥ 1
2 1 rabbii ⊢ t ∈ ℕ 0 1 … N | A ∈ ℕ = t ∈ ℕ 0 1 … N | A ∈ ℤ ≥ 1
3 1z ⊢ 1 ∈ ℤ
4 eluzrabdioph ⊢ N ∈ ℕ 0 ∧ 1 ∈ ℤ ∧ t ∈ ℤ 1 … N ⟼ A ∈ mzPoly ⁡ 1 … N → t ∈ ℕ 0 1 … N | A ∈ ℤ ≥ 1 ∈ Dioph ⁡ N
5 3 4 mp3an2 ⊢ N ∈ ℕ 0 ∧ t ∈ ℤ 1 … N ⟼ A ∈ mzPoly ⁡ 1 … N → t ∈ ℕ 0 1 … N | A ∈ ℤ ≥ 1 ∈ Dioph ⁡ N
6 2 5 eqeltrid ⊢ N ∈ ℕ 0 ∧ t ∈ ℤ 1 … N ⟼ A ∈ mzPoly ⁡ 1 … N → t ∈ ℕ 0 1 … N | A ∈ ℕ ∈ Dioph ⁡ N