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∈ℕ01…N|A∈ℕ0∈Dioph⁡N

Proof

Step Hyp Ref Expression
1 risset ⊢A∈ℕ0↔∃b∈ℕ0b=A
2 1 rabbii ⊢t∈ℕ01…N|A∈ℕ0=t∈ℕ01…N|∃b∈ℕ0b=A
3 2 a1i ⊢N∈ℕ0∧t∈ℤ1…N⟼A∈mzPoly⁡1…N→t∈ℕ01…N|A∈ℕ0=t∈ℕ01…N|∃b∈ℕ0b=A
4 nfcv ⊢Ⅎ_tℕ01…N
5 nfcv ⊢Ⅎ_aℕ01…N
6 nfv ⊢Ⅎa∃b∈ℕ0b=A
7 nfcv ⊢Ⅎ_tℕ0
8 nfcsb1v ⊢Ⅎ_t⦋a/t⦌A
9 8 nfeq2 ⊢Ⅎtb=⦋a/t⦌A
10 7 9 nfrexw ⊢Ⅎt∃b∈ℕ0b=⦋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∈ℕ0b=A↔∃b∈ℕ0b=⦋a/t⦌A
14 4 5 6 10 13 cbvrabw ⊢t∈ℕ01…N|∃b∈ℕ0b=A=a∈ℕ01…N|∃b∈ℕ0b=⦋a/t⦌A
15 3 14 eqtrdi ⊢N∈ℕ0∧t∈ℤ1…N⟼A∈mzPoly⁡1…N→t∈ℕ01…N|A∈ℕ0=a∈ℕ01…N|∃b∈ℕ0b=⦋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∈ℕ01…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∈ℕ01…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∈ℕ01…N+1|c⁡N+1=⦋c↾1…N/t⦌A∈Dioph⁡N+1→a∈ℕ01…N|∃b∈ℕ0b=⦋a/t⦌A∈Dioph⁡N
33 28 32 syldan ⊢N∈ℕ0∧t∈ℤ1…N⟼A∈mzPoly⁡1…N→a∈ℕ01…N|∃b∈ℕ0b=⦋a/t⦌A∈Dioph⁡N
34 15 33 eqeltrd ⊢N∈ℕ0∧t∈ℤ1…N⟼A∈mzPoly⁡1…N→t∈ℕ01…N|A∈ℕ0∈Dioph⁡N