Metamath Proof Explorer

Theorem elnnrabdioph

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

Ref Expression
Assertion elnnrabdioph 
|- ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A e. NN } e. ( Dioph ` N ) )

Proof

Step Hyp Ref Expression
1 elnnuz 
 |-  ( A e. NN <-> A e. ( ZZ>= ` 1 ) )
2 1 rabbii 
 |-  { t e. ( NN0 ^m ( 1 ... N ) ) | A e. NN } = { t e. ( NN0 ^m ( 1 ... N ) ) | A e. ( ZZ>= ` 1 ) }
3 1z 
 |-  1 e. ZZ
4 eluzrabdioph 
 |-  ( ( N e. NN0 /\ 1 e. ZZ /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A e. ( ZZ>= ` 1 ) } e. ( Dioph ` N ) )
5 3 4 mp3an2 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A e. ( ZZ>= ` 1 ) } e. ( Dioph ` N ) )
6 2 5 eqeltrid 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A e. NN } e. ( Dioph ` N ) )