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 e. ( Dioph ` N ) <-> ( N e. NN0 /\ E. p e. ( mzPoly ` NN ) A = { t | E. u e. ( NN0 ^m NN ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) )

Proof

Step Hyp Ref Expression
1 eldiophelnn0 
 |-  ( A e. ( Dioph ` N ) -> N e. NN0 )
2 nnex 
 |-  NN e. _V
3 1z 
 |-  1 e. ZZ
4 nnuz 
 |-  NN = ( ZZ>= ` 1 )
5 4 uzinf 
 |-  ( 1 e. ZZ -> -. NN e. Fin )
6 3 5 ax-mp 
 |-  -. NN e. Fin
7 elfznn 
 |-  ( p e. ( 1 ... N ) -> p e. NN )
8 7 ssriv 
 |-  ( 1 ... N ) C_ NN
9 eldioph2b 
 |-  ( ( ( N e. NN0 /\ NN e. _V ) /\ ( -. NN e. Fin /\ ( 1 ... N ) C_ NN ) ) -> ( A e. ( Dioph ` N ) <-> E. p e. ( mzPoly ` NN ) A = { t | E. u e. ( NN0 ^m NN ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) )
10 6 8 9 mpanr12 
 |-  ( ( N e. NN0 /\ NN e. _V ) -> ( A e. ( Dioph ` N ) <-> E. p e. ( mzPoly ` NN ) A = { t | E. u e. ( NN0 ^m NN ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) )
11 2 10 mpan2 
 |-  ( N e. NN0 -> ( A e. ( Dioph ` N ) <-> E. p e. ( mzPoly ` NN ) A = { t | E. u e. ( NN0 ^m NN ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) )
12 1 11 biadanii 
 |-  ( A e. ( Dioph ` N ) <-> ( N e. NN0 /\ E. p e. ( mzPoly ` NN ) A = { t | E. u e. ( NN0 ^m NN ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) )