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 e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A e. NN0 } e. ( Dioph ` N ) )

Proof

Step Hyp Ref Expression
1 risset 
 |-  ( A e. NN0 <-> E. b e. NN0 b = A )
2 1 rabbii 
 |-  { t e. ( NN0 ^m ( 1 ... N ) ) | A e. NN0 } = { t e. ( NN0 ^m ( 1 ... N ) ) | E. b e. NN0 b = A }
3 2 a1i 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A e. NN0 } = { t e. ( NN0 ^m ( 1 ... N ) ) | E. b e. NN0 b = A } )
4 nfcv 
 |-  F/_ t ( NN0 ^m ( 1 ... N ) )
5 nfcv 
 |-  F/_ a ( NN0 ^m ( 1 ... N ) )
6 nfv 
 |-  F/ a E. b e. NN0 b = A
7 nfcv 
 |-  F/_ t NN0
8 nfcsb1v 
 |-  F/_ t [_ a / t ]_ A
9 8 nfeq2 
 |-  F/ t b = [_ a / t ]_ A
10 7 9 nfrex 
 |-  F/ t E. b e. NN0 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 -> ( E. b e. NN0 b = A <-> E. b e. NN0 b = [_ a / t ]_ A ) )
14 4 5 6 10 13 cbvrabw 
 |-  { t e. ( NN0 ^m ( 1 ... N ) ) | E. b e. NN0 b = A } = { a e. ( NN0 ^m ( 1 ... N ) ) | E. b e. NN0 b = [_ a / t ]_ A }
15 3 14 eqtrdi 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A e. NN0 } = { a e. ( NN0 ^m ( 1 ... N ) ) | E. b e. NN0 b = [_ a / t ]_ A } )
16 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
17 16 adantr 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> ( N + 1 ) e. NN0 )
18 ovex 
 |-  ( 1 ... ( N + 1 ) ) e. _V
19 nn0p1nn 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN )
20 elfz1end 
 |-  ( ( N + 1 ) e. NN <-> ( N + 1 ) e. ( 1 ... ( N + 1 ) ) )
21 19 20 sylib 
 |-  ( N e. NN0 -> ( N + 1 ) e. ( 1 ... ( N + 1 ) ) )
22 21 adantr 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> ( N + 1 ) e. ( 1 ... ( N + 1 ) ) )
23 mzpproj 
 |-  ( ( ( 1 ... ( N + 1 ) ) e. _V /\ ( N + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> ( c e. ( ZZ ^m ( 1 ... ( N + 1 ) ) ) |-> ( c ` ( N + 1 ) ) ) e. ( mzPoly ` ( 1 ... ( N + 1 ) ) ) )
24 18 22 23 sylancr 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> ( c e. ( ZZ ^m ( 1 ... ( N + 1 ) ) ) |-> ( c ` ( N + 1 ) ) ) e. ( mzPoly ` ( 1 ... ( N + 1 ) ) ) )
25 eqid 
 |-  ( N + 1 ) = ( N + 1 )
26 25 rabdiophlem2 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> ( c e. ( ZZ ^m ( 1 ... ( N + 1 ) ) ) |-> [_ ( c |` ( 1 ... N ) ) / t ]_ A ) e. ( mzPoly ` ( 1 ... ( N + 1 ) ) ) )
27 eqrabdioph 
 |-  ( ( ( N + 1 ) e. NN0 /\ ( c e. ( ZZ ^m ( 1 ... ( N + 1 ) ) ) |-> ( c ` ( N + 1 ) ) ) e. ( mzPoly ` ( 1 ... ( N + 1 ) ) ) /\ ( c e. ( ZZ ^m ( 1 ... ( N + 1 ) ) ) |-> [_ ( c |` ( 1 ... N ) ) / t ]_ A ) e. ( mzPoly ` ( 1 ... ( N + 1 ) ) ) ) -> { c e. ( NN0 ^m ( 1 ... ( N + 1 ) ) ) | ( c ` ( N + 1 ) ) = [_ ( c |` ( 1 ... N ) ) / t ]_ A } e. ( Dioph ` ( N + 1 ) ) )
28 17 24 26 27 syl3anc 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { c e. ( NN0 ^m ( 1 ... ( N + 1 ) ) ) | ( c ` ( N + 1 ) ) = [_ ( c |` ( 1 ... N ) ) / t ]_ A } e. ( 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 e. NN0 /\ { c e. ( NN0 ^m ( 1 ... ( N + 1 ) ) ) | ( c ` ( N + 1 ) ) = [_ ( c |` ( 1 ... N ) ) / t ]_ A } e. ( Dioph ` ( N + 1 ) ) ) -> { a e. ( NN0 ^m ( 1 ... N ) ) | E. b e. NN0 b = [_ a / t ]_ A } e. ( Dioph ` N ) )
33 28 32 syldan 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { a e. ( NN0 ^m ( 1 ... N ) ) | E. b e. NN0 b = [_ a / t ]_ A } e. ( Dioph ` N ) )
34 15 33 eqeltrd 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A e. NN0 } e. ( Dioph ` N ) )