Metamath Proof Explorer

Theorem elnn0rabdioph

Description: Diophantine set builder for nonnegativity constraints. The first builder which uses a witness variable internally; an expression is nonnegative if there is a nonnegative integer equal to it. (Contributed by Stefan O'Rear, 11-Oct-2014)

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

Proof

Step Hyp Ref Expression
1 risset ⊢ A ∈ ℕ 0 ↔ ∃ b ∈ ℕ 0 b = A
2 1 rabbii ⊢ t ∈ ℕ 0 1 … N | A ∈ ℕ 0 = t ∈ ℕ 0 1 … N | ∃ b ∈ ℕ 0 b = A
3 2 a1i ⊢ N ∈ ℕ 0 ∧ t ∈ ℤ 1 … N ⟼ A ∈ mzPoly ⁡ 1 … N → t ∈ ℕ 0 1 … N | A ∈ ℕ 0 = t ∈ ℕ 0 1 … N | ∃ b ∈ ℕ 0 b = A
4 nfcv ⊢ Ⅎ _ t ℕ 0 1 … N
5 nfcv ⊢ Ⅎ _ a ℕ 0 1 … N
6 nfv ⊢ Ⅎ a ∃ b ∈ ℕ 0 b = A
7 nfcv ⊢ Ⅎ _ t ℕ 0
8 nfcsb1v ⊢ Ⅎ _ t ⦋ a / t⦌ A
9 8 nfeq2 ⊢ Ⅎ t b = ⦋ a / t⦌ A
10 7 9 nfrex ⊢ Ⅎ t ∃ b ∈ ℕ 0 b = ⦋ a / t⦌ A
11 csbeq1a ⊢ t = a → A = ⦋ a / t⦌ A
12 11 eqeq2d ⊢ t = a → b = A ↔ b = ⦋ a / t⦌ A
13 12 rexbidv ⊢ t = a → ∃ b ∈ ℕ 0 b = A ↔ ∃ b ∈ ℕ 0 b = ⦋ a / t⦌ A
14 4 5 6 10 13 cbvrabw ⊢ t ∈ ℕ 0 1 … N | ∃ b ∈ ℕ 0 b = A = a ∈ ℕ 0 1 … N | ∃ b ∈ ℕ 0 b = ⦋ a / t⦌ A
15 3 14 eqtrdi ⊢ N ∈ ℕ 0 ∧ t ∈ ℤ 1 … N ⟼ A ∈ mzPoly ⁡ 1 … N → t ∈ ℕ 0 1 … N | A ∈ ℕ 0 = a ∈ ℕ 0 1 … N | ∃ b ∈ ℕ 0 b = ⦋ a / t⦌ A
16 peano2nn0 ⊢ N ∈ ℕ 0 → N + 1 ∈ ℕ 0
17 16 adantr ⊢ N ∈ ℕ 0 ∧ t ∈ ℤ 1 … N ⟼ A ∈ mzPoly ⁡ 1 … N → N + 1 ∈ ℕ 0
18 ovex ⊢ 1 … N + 1 ∈ V
19 nn0p1nn ⊢ N ∈ ℕ 0 → N + 1 ∈ ℕ
20 elfz1end ⊢ N + 1 ∈ ℕ ↔ N + 1 ∈ 1 … N + 1
21 19 20 sylib ⊢ N ∈ ℕ 0 → N + 1 ∈ 1 … N + 1
22 21 adantr ⊢ N ∈ ℕ 0 ∧ t ∈ ℤ 1 … N ⟼ A ∈ mzPoly ⁡ 1 … N → N + 1 ∈ 1 … N + 1
23 mzpproj ⊢ 1 … N + 1 ∈ V ∧ N + 1 ∈ 1 … N + 1 → c ∈ ℤ 1 … N + 1 ⟼ c ⁡ N + 1 ∈ mzPoly ⁡ 1 … N + 1
24 18 22 23 sylancr ⊢ N ∈ ℕ 0 ∧ t ∈ ℤ 1 … N ⟼ A ∈ mzPoly ⁡ 1 … N → c ∈ ℤ 1 … N + 1 ⟼ c ⁡ N + 1 ∈ mzPoly ⁡ 1 … N + 1
25 eqid ⊢ N + 1 = N + 1
26 25 rabdiophlem2 ⊢ N ∈ ℕ 0 ∧ t ∈ ℤ 1 … N ⟼ A ∈ mzPoly ⁡ 1 … N → c ∈ ℤ 1 … N + 1 ⟼ ⦋ c ↾ 1 … N / t⦌ A ∈ mzPoly ⁡ 1 … N + 1
27 eqrabdioph ⊢ N + 1 ∈ ℕ 0 ∧ c ∈ ℤ 1 … N + 1 ⟼ c ⁡ N + 1 ∈ mzPoly ⁡ 1 … N + 1 ∧ c ∈ ℤ 1 … N + 1 ⟼ ⦋ c ↾ 1 … N / t⦌ A ∈ mzPoly ⁡ 1 … N + 1 → c ∈ ℕ 0 1 … N + 1 | c ⁡ N + 1 = ⦋ c ↾ 1 … N / t⦌ A ∈ Dioph ⁡ N + 1
28 17 24 26 27 syl3anc ⊢ N ∈ ℕ 0 ∧ t ∈ ℤ 1 … N ⟼ A ∈ mzPoly ⁡ 1 … N → c ∈ ℕ 0 1 … N + 1 | c ⁡ N + 1 = ⦋ c ↾ 1 … N / t⦌ A ∈ Dioph ⁡ N + 1
29 eqeq1 ⊢ b = c ⁡ N + 1 → b = ⦋ a / t⦌ A ↔ c ⁡ N + 1 = ⦋ a / t⦌ A
30 csbeq1 ⊢ a = c ↾ 1 … N → ⦋ a / t⦌ A = ⦋ c ↾ 1 … N / t⦌ A
31 30 eqeq2d ⊢ a = c ↾ 1 … N → c ⁡ N + 1 = ⦋ a / t⦌ A ↔ c ⁡ N + 1 = ⦋ c ↾ 1 … N / t⦌ A
32 25 29 31 rexrabdioph ⊢ N ∈ ℕ 0 ∧ c ∈ ℕ 0 1 … N + 1 | c ⁡ N + 1 = ⦋ c ↾ 1 … N / t⦌ A ∈ Dioph ⁡ N + 1 → a ∈ ℕ 0 1 … N | ∃ b ∈ ℕ 0 b = ⦋ a / t⦌ A ∈ Dioph ⁡ N
33 28 32 syldan ⊢ N ∈ ℕ 0 ∧ t ∈ ℤ 1 … N ⟼ A ∈ mzPoly ⁡ 1 … N → a ∈ ℕ 0 1 … N | ∃ b ∈ ℕ 0 b = ⦋ a / t⦌ A ∈ Dioph ⁡ N
34 15 33 eqeltrd ⊢ N ∈ ℕ 0 ∧ t ∈ ℤ 1 … N ⟼ A ∈ mzPoly ⁡ 1 … N → t ∈ ℕ 0 1 … N | A ∈ ℕ 0 ∈ Dioph ⁡ N