Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  diophin Unicode version

Theorem diophin 26018
Description: If two sets are Diophantine, so is their intersection. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
Assertion
Ref Expression
diophin  |-  ( ( A  e.  (Dioph `  N )  /\  B  e.  (Dioph `  N )
)  ->  ( A  i^i  B )  e.  (Dioph `  N ) )

Proof of Theorem diophin
StepHypRef Expression
1 eldiophelnn0 26009 . . 3  |-  ( A  e.  (Dioph `  N
)  ->  N  e.  NN0 )
2 id1 22 . . . . . 6  |-  ( N  e.  NN0  ->  N  e. 
NN0 )
3 zex 9912 . . . . . . 7  |-  ZZ  e.  _V
4 difexg 4058 . . . . . . 7  |-  ( ZZ  e.  _V  ->  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) )  e.  _V )
53, 4mp1i 13 . . . . . 6  |-  ( N  e.  NN0  ->  ( ZZ 
\  ( ZZ>= `  ( N  +  1 ) ) )  e.  _V )
6 ominf 6960 . . . . . . 7  |-  -.  om  e.  Fin
7 nn0z 9925 . . . . . . . 8  |-  ( N  e.  NN0  ->  N  e.  ZZ )
8 lzenom 26015 . . . . . . . 8  |-  ( N  e.  ZZ  ->  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) )  ~~  om )
9 enfi 6964 . . . . . . . 8  |-  ( ( ZZ  \  ( ZZ>= `  ( N  +  1
) ) )  ~~  om 
->  ( ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) )  e.  Fin  <->  om  e.  Fin ) )
107, 8, 93syl 20 . . . . . . 7  |-  ( N  e.  NN0  ->  ( ( ZZ  \  ( ZZ>= `  ( N  +  1
) ) )  e. 
Fin 
<->  om  e.  Fin )
)
116, 10mtbiri 296 . . . . . 6  |-  ( N  e.  NN0  ->  -.  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) )  e.  Fin )
12 fz1eqin 26014 . . . . . . 7  |-  ( N  e.  NN0  ->  ( 1 ... N )  =  ( ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) )  i^i  NN ) )
13 inss1 3296 . . . . . . . 8  |-  ( ( ZZ  \  ( ZZ>= `  ( N  +  1
) ) )  i^i 
NN )  C_  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) )
1413a1i 12 . . . . . . 7  |-  ( N  e.  NN0  ->  ( ( ZZ  \  ( ZZ>= `  ( N  +  1
) ) )  i^i 
NN )  C_  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )
1512, 14eqsstrd 3133 . . . . . 6  |-  ( N  e.  NN0  ->  ( 1 ... N )  C_  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )
16 eldioph2b 26008 . . . . . 6  |-  ( ( ( N  e.  NN0  /\  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) )  e.  _V )  /\  ( -.  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) )  e.  Fin  /\  ( 1 ... N
)  C_  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )  -> 
( A  e.  (Dioph `  N )  <->  E. a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) A  =  { c  |  E. d  e.  ( NN0  ^m  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) ( c  =  ( d  |`  (
1 ... N ) )  /\  ( a `  d )  =  0 ) } ) )
172, 5, 11, 15, 16syl22anc 1188 . . . . 5  |-  ( N  e.  NN0  ->  ( A  e.  (Dioph `  N
)  <->  E. a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) A  =  {
c  |  E. d  e.  ( NN0  ^m  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) ( c  =  ( d  |`  ( 1 ... N
) )  /\  (
a `  d )  =  0 ) } ) )
18 nnex 9632 . . . . . . 7  |-  NN  e.  _V
1918a1i 12 . . . . . 6  |-  ( N  e.  NN0  ->  NN  e.  _V )
20 1z 9932 . . . . . . 7  |-  1  e.  ZZ
21 nnuz 10142 . . . . . . . 8  |-  NN  =  ( ZZ>= `  1 )
2221uzinf 10906 . . . . . . 7  |-  ( 1  e.  ZZ  ->  -.  NN  e.  Fin )
2320, 22mp1i 13 . . . . . 6  |-  ( N  e.  NN0  ->  -.  NN  e.  Fin )
24 elfznn 10697 . . . . . . . 8  |-  ( a  e.  ( 1 ... N )  ->  a  e.  NN )
2524ssriv 3105 . . . . . . 7  |-  ( 1 ... N )  C_  NN
2625a1i 12 . . . . . 6  |-  ( N  e.  NN0  ->  ( 1 ... N )  C_  NN )
27 eldioph2b 26008 . . . . . 6  |-  ( ( ( N  e.  NN0  /\  NN  e.  _V )  /\  ( -.  NN  e.  Fin  /\  ( 1 ... N )  C_  NN ) )  ->  ( B  e.  (Dioph `  N
)  <->  E. b  e.  (mzPoly `  NN ) B  =  { c  |  E. e  e.  ( NN0  ^m  NN ) ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) } ) )
282, 19, 23, 26, 27syl22anc 1188 . . . . 5  |-  ( N  e.  NN0  ->  ( B  e.  (Dioph `  N
)  <->  E. b  e.  (mzPoly `  NN ) B  =  { c  |  E. e  e.  ( NN0  ^m  NN ) ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) } ) )
2917, 28anbi12d 694 . . . 4  |-  ( N  e.  NN0  ->  ( ( A  e.  (Dioph `  N )  /\  B  e.  (Dioph `  N )
)  <->  ( E. a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) A  =  { c  |  E. d  e.  ( NN0  ^m  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) ( c  =  ( d  |`  (
1 ... N ) )  /\  ( a `  d )  =  0 ) }  /\  E. b  e.  (mzPoly `  NN ) B  =  {
c  |  E. e  e.  ( NN0  ^m  NN ) ( c  =  ( e  |`  (
1 ... N ) )  /\  ( b `  e )  =  0 ) } ) ) )
30 reeanv 2669 . . . . 5  |-  ( E. a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) E. b  e.  (mzPoly `  NN )
( A  =  {
c  |  E. d  e.  ( NN0  ^m  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) ( c  =  ( d  |`  ( 1 ... N
) )  /\  (
a `  d )  =  0 ) }  /\  B  =  {
c  |  E. e  e.  ( NN0  ^m  NN ) ( c  =  ( e  |`  (
1 ... N ) )  /\  ( b `  e )  =  0 ) } )  <->  ( E. a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) A  =  { c  |  E. d  e.  ( NN0  ^m  ( ZZ 
\  ( ZZ>= `  ( N  +  1 ) ) ) ) ( c  =  ( d  |`  ( 1 ... N
) )  /\  (
a `  d )  =  0 ) }  /\  E. b  e.  (mzPoly `  NN ) B  =  { c  |  E. e  e.  ( NN0  ^m  NN ) ( c  =  ( e  |`  ( 1 ... N ) )  /\  ( b `  e )  =  0 ) } ) )
31 inab 3343 . . . . . . . . 9  |-  ( { c  |  E. d  e.  ( NN0  ^m  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) ( c  =  ( d  |`  ( 1 ... N
) )  /\  (
a `  d )  =  0 ) }  i^i  { c  |  E. e  e.  ( NN0  ^m  NN ) ( c  =  ( e  |`  ( 1 ... N ) )  /\  ( b `  e )  =  0 ) } )  =  { c  |  ( E. d  e.  ( NN0  ^m  ( ZZ 
\  ( ZZ>= `  ( N  +  1 ) ) ) ) ( c  =  ( d  |`  ( 1 ... N
) )  /\  (
a `  d )  =  0 )  /\  E. e  e.  ( NN0 
^m  NN ) ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) ) }
32 reeanv 2669 . . . . . . . . . . 11  |-  ( E. d  e.  ( NN0 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) E. e  e.  ( NN0  ^m  NN ) ( ( c  =  ( d  |`  ( 1 ... N
) )  /\  (
a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N ) )  /\  ( b `  e )  =  0 ) )  <->  ( E. d  e.  ( NN0  ^m  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) ( c  =  ( d  |`  (
1 ... N ) )  /\  ( a `  d )  =  0 )  /\  E. e  e.  ( NN0  ^m  NN ) ( c  =  ( e  |`  (
1 ... N ) )  /\  ( b `  e )  =  0 ) ) )
33 simplrl 739 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  (
d  e.  ( NN0 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  /\  e  e.  ( NN0  ^m  NN ) ) )  /\  ( ( c  =  ( d  |`  (
1 ... N ) )  /\  ( a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) ) )  ->  d  e.  ( NN0  ^m  ( ZZ 
\  ( ZZ>= `  ( N  +  1 ) ) ) ) )
34 simplrr 740 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  (
d  e.  ( NN0 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  /\  e  e.  ( NN0  ^m  NN ) ) )  /\  ( ( c  =  ( d  |`  (
1 ... N ) )  /\  ( a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) ) )  ->  e  e.  ( NN0  ^m  NN ) )
3512eqcomd 2258 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  NN0  ->  ( ( ZZ  \  ( ZZ>= `  ( N  +  1
) ) )  i^i 
NN )  =  ( 1 ... N ) )
3635reseq2d 4862 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  NN0  ->  ( d  |`  ( ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) )  i^i  NN ) )  =  ( d  |`  ( 1 ... N
) ) )
3736ad3antrrr 713 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  (
d  e.  ( NN0 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  /\  e  e.  ( NN0  ^m  NN ) ) )  /\  ( ( c  =  ( d  |`  (
1 ... N ) )  /\  ( a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) ) )  ->  ( d  |`  ( ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) )  i^i  NN ) )  =  ( d  |`  ( 1 ... N
) ) )
3835reseq2d 4862 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  NN0  ->  ( e  |`  ( ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) )  i^i  NN ) )  =  ( e  |`  ( 1 ... N
) ) )
3938ad3antrrr 713 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  (
d  e.  ( NN0 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  /\  e  e.  ( NN0  ^m  NN ) ) )  /\  ( ( c  =  ( d  |`  (
1 ... N ) )  /\  ( a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) ) )  ->  ( e  |`  ( ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) )  i^i  NN ) )  =  ( e  |`  ( 1 ... N
) ) )
40 simprrl 743 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  (
d  e.  ( NN0 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  /\  e  e.  ( NN0  ^m  NN ) ) )  /\  ( ( c  =  ( d  |`  (
1 ... N ) )  /\  ( a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) ) )  ->  c  =  ( e  |`  (
1 ... N ) ) )
41 simprll 741 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  (
d  e.  ( NN0 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  /\  e  e.  ( NN0  ^m  NN ) ) )  /\  ( ( c  =  ( d  |`  (
1 ... N ) )  /\  ( a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) ) )  ->  c  =  ( d  |`  (
1 ... N ) ) )
4239, 40, 413eqtr2d 2291 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  (
d  e.  ( NN0 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  /\  e  e.  ( NN0  ^m  NN ) ) )  /\  ( ( c  =  ( d  |`  (
1 ... N ) )  /\  ( a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) ) )  ->  ( e  |`  ( ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) )  i^i  NN ) )  =  ( d  |`  ( 1 ... N
) ) )
4337, 42eqtr4d 2288 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  (
d  e.  ( NN0 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  /\  e  e.  ( NN0  ^m  NN ) ) )  /\  ( ( c  =  ( d  |`  (
1 ... N ) )  /\  ( a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) ) )  ->  ( d  |`  ( ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) )  i^i  NN ) )  =  ( e  |`  ( ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) )  i^i  NN ) ) )
44 elmapresaun 26016 . . . . . . . . . . . . . . . . . 18  |-  ( ( d  e.  ( NN0 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  /\  e  e.  ( NN0  ^m  NN )  /\  ( d  |`  ( ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) )  i^i  NN ) )  =  ( e  |`  ( ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) )  i^i  NN ) ) )  ->  (
d  u.  e )  e.  ( NN0  ^m  ( ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) )  u.  NN ) ) )
4533, 34, 43, 44syl3anc 1187 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  (
d  e.  ( NN0 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  /\  e  e.  ( NN0  ^m  NN ) ) )  /\  ( ( c  =  ( d  |`  (
1 ... N ) )  /\  ( a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) ) )  ->  ( d  u.  e )  e.  ( NN0  ^m  ( ( ZZ  \  ( ZZ>= `  ( N  +  1
) ) )  u.  NN ) ) )
4621uneq2i 3236 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ZZ  \  ( ZZ>= `  ( N  +  1
) ) )  u.  NN )  =  ( ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) )  u.  ( ZZ>= `  1
) )
4720a1i 12 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  NN0  ->  1  e.  ZZ )
48 nn0p1nn 9882 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( N  e.  NN0  ->  ( N  +  1 )  e.  NN )
4948nnge1d 9668 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  NN0  ->  1  <_ 
( N  +  1 ) )
50 lzunuz 26013 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( N  e.  ZZ  /\  1  e.  ZZ  /\  1  <_  ( N  +  1 ) )  ->  (
( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) )  u.  ( ZZ>= `  1
) )  =  ZZ )
517, 47, 49, 50syl3anc 1187 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  NN0  ->  ( ( ZZ  \  ( ZZ>= `  ( N  +  1
) ) )  u.  ( ZZ>= `  1 )
)  =  ZZ )
5246, 51syl5eq 2297 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  NN0  ->  ( ( ZZ  \  ( ZZ>= `  ( N  +  1
) ) )  u.  NN )  =  ZZ )
5352oveq2d 5726 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  NN0  ->  ( NN0 
^m  ( ( ZZ 
\  ( ZZ>= `  ( N  +  1 ) ) )  u.  NN ) )  =  ( NN0  ^m  ZZ ) )
5453ad3antrrr 713 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  (
d  e.  ( NN0 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  /\  e  e.  ( NN0  ^m  NN ) ) )  /\  ( ( c  =  ( d  |`  (
1 ... N ) )  /\  ( a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) ) )  ->  ( NN0  ^m  ( ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) )  u.  NN ) )  =  ( NN0 
^m  ZZ ) )
5545, 54eleqtrd 2329 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  (
d  e.  ( NN0 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  /\  e  e.  ( NN0  ^m  NN ) ) )  /\  ( ( c  =  ( d  |`  (
1 ... N ) )  /\  ( a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) ) )  ->  ( d  u.  e )  e.  ( NN0  ^m  ZZ ) )
56 unidm 3228 . . . . . . . . . . . . . . . . . . 19  |-  ( c  u.  c )  =  c
5741, 40uneq12d 3240 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  (
d  e.  ( NN0 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  /\  e  e.  ( NN0  ^m  NN ) ) )  /\  ( ( c  =  ( d  |`  (
1 ... N ) )  /\  ( a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) ) )  ->  ( c  u.  c )  =  ( ( d  |`  (
1 ... N ) )  u.  ( e  |`  ( 1 ... N
) ) ) )
5856, 57syl5eqr 2299 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  (
d  e.  ( NN0 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  /\  e  e.  ( NN0  ^m  NN ) ) )  /\  ( ( c  =  ( d  |`  (
1 ... N ) )  /\  ( a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) ) )  ->  c  =  ( ( d  |`  ( 1 ... N
) )  u.  (
e  |`  ( 1 ... N ) ) ) )
59 resundir 4877 . . . . . . . . . . . . . . . . . 18  |-  ( ( d  u.  e )  |`  ( 1 ... N
) )  =  ( ( d  |`  (
1 ... N ) )  u.  ( e  |`  ( 1 ... N
) ) )
6058, 59syl6eqr 2303 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  (
d  e.  ( NN0 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  /\  e  e.  ( NN0  ^m  NN ) ) )  /\  ( ( c  =  ( d  |`  (
1 ... N ) )  /\  ( a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) ) )  ->  c  =  ( ( d  u.  e )  |`  (
1 ... N ) ) )
61 uncom 3229 . . . . . . . . . . . . . . . . . . . . 21  |-  ( d  u.  e )  =  ( e  u.  d
)
6261reseq1i 4858 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( d  u.  e )  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  =  ( ( e  u.  d )  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )
63 incom 3269 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( NN 
i^i  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  =  ( ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) )  i^i  NN )
6463, 35syl5eq 2297 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( N  e.  NN0  ->  ( NN 
i^i  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  =  ( 1 ... N ) )
6564reseq2d 4862 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  NN0  ->  ( e  |`  ( NN  i^i  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )  =  ( e  |`  ( 1 ... N
) ) )
6665ad3antrrr 713 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  (
d  e.  ( NN0 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  /\  e  e.  ( NN0  ^m  NN ) ) )  /\  ( ( c  =  ( d  |`  (
1 ... N ) )  /\  ( a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) ) )  ->  ( e  |`  ( NN  i^i  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )  =  ( e  |`  ( 1 ... N
) ) )
6764reseq2d 4862 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( N  e.  NN0  ->  ( d  |`  ( NN  i^i  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )  =  ( d  |`  ( 1 ... N
) ) )
6867ad3antrrr 713 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  (
d  e.  ( NN0 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  /\  e  e.  ( NN0  ^m  NN ) ) )  /\  ( ( c  =  ( d  |`  (
1 ... N ) )  /\  ( a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) ) )  ->  ( d  |`  ( NN  i^i  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )  =  ( d  |`  ( 1 ... N
) ) )
6968, 41, 403eqtr2d 2291 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  (
d  e.  ( NN0 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  /\  e  e.  ( NN0  ^m  NN ) ) )  /\  ( ( c  =  ( d  |`  (
1 ... N ) )  /\  ( a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) ) )  ->  ( d  |`  ( NN  i^i  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )  =  ( e  |`  ( 1 ... N
) ) )
7066, 69eqtr4d 2288 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  (
d  e.  ( NN0 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  /\  e  e.  ( NN0  ^m  NN ) ) )  /\  ( ( c  =  ( d  |`  (
1 ... N ) )  /\  ( a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) ) )  ->  ( e  |`  ( NN  i^i  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )  =  ( d  |`  ( NN  i^i  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) ) )
71 elmapresaunres2 26017 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( e  e.  ( NN0 
^m  NN )  /\  d  e.  ( NN0  ^m  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  ( e  |`  ( NN  i^i  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )  =  ( d  |`  ( NN  i^i  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) ) )  ->  ( (
e  u.  d )  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  =  d )
7234, 33, 70, 71syl3anc 1187 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  (
d  e.  ( NN0 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  /\  e  e.  ( NN0  ^m  NN ) ) )  /\  ( ( c  =  ( d  |`  (
1 ... N ) )  /\  ( a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) ) )  ->  ( (
e  u.  d )  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  =  d )
7362, 72syl5eq 2297 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  (
d  e.  ( NN0 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  /\  e  e.  ( NN0  ^m  NN ) ) )  /\  ( ( c  =  ( d  |`  (
1 ... N ) )  /\  ( a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) ) )  ->  ( (
d  u.  e )  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  =  d )
7473fveq2d 5381 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  (
d  e.  ( NN0 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  /\  e  e.  ( NN0  ^m  NN ) ) )  /\  ( ( c  =  ( d  |`  (
1 ... N ) )  /\  ( a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) ) )  ->  ( a `  ( ( d  u.  e )  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )  =  ( a `  d ) )
75 simprlr 742 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  (
d  e.  ( NN0 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  /\  e  e.  ( NN0  ^m  NN ) ) )  /\  ( ( c  =  ( d  |`  (
1 ... N ) )  /\  ( a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) ) )  ->  ( a `  d )  =  0 )
7674, 75eqtrd 2285 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  (
d  e.  ( NN0 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  /\  e  e.  ( NN0  ^m  NN ) ) )  /\  ( ( c  =  ( d  |`  (
1 ... N ) )  /\  ( a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) ) )  ->  ( a `  ( ( d  u.  e )  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )  =  0 )
77 elmapresaunres2 26017 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( d  e.  ( NN0 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  /\  e  e.  ( NN0  ^m  NN )  /\  ( d  |`  ( ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) )  i^i  NN ) )  =  ( e  |`  ( ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) )  i^i  NN ) ) )  ->  (
( d  u.  e
)  |`  NN )  =  e )
7833, 34, 43, 77syl3anc 1187 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  (
d  e.  ( NN0 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  /\  e  e.  ( NN0  ^m  NN ) ) )  /\  ( ( c  =  ( d  |`  (
1 ... N ) )  /\  ( a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) ) )  ->  ( (
d  u.  e )  |`  NN )  =  e )
7978fveq2d 5381 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  (
d  e.  ( NN0 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  /\  e  e.  ( NN0  ^m  NN ) ) )  /\  ( ( c  =  ( d  |`  (
1 ... N ) )  /\  ( a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) ) )  ->  ( b `  ( ( d  u.  e )  |`  NN ) )  =  ( b `
 e ) )
80 simprrr 744 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  (
d  e.  ( NN0 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  /\  e  e.  ( NN0  ^m  NN ) ) )  /\  ( ( c  =  ( d  |`  (
1 ... N ) )  /\  ( a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) ) )  ->  ( b `  e )  =  0 )
8179, 80eqtrd 2285 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  (
d  e.  ( NN0 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  /\  e  e.  ( NN0  ^m  NN ) ) )  /\  ( ( c  =  ( d  |`  (
1 ... N ) )  /\  ( a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) ) )  ->  ( b `  ( ( d  u.  e )  |`  NN ) )  =  0 )
8260, 76, 81jca32 523 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  (
d  e.  ( NN0 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  /\  e  e.  ( NN0  ^m  NN ) ) )  /\  ( ( c  =  ( d  |`  (
1 ... N ) )  /\  ( a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) ) )  ->  ( c  =  ( ( d  u.  e )  |`  ( 1 ... N
) )  /\  (
( a `  (
( d  u.  e
)  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) )  =  0  /\  ( b `
 ( ( d  u.  e )  |`  NN ) )  =  0 ) ) )
83 reseq1 4856 . . . . . . . . . . . . . . . . . . 19  |-  ( f  =  ( d  u.  e )  ->  (
f  |`  ( 1 ... N ) )  =  ( ( d  u.  e )  |`  (
1 ... N ) ) )
8483eqeq2d 2264 . . . . . . . . . . . . . . . . . 18  |-  ( f  =  ( d  u.  e )  ->  (
c  =  ( f  |`  ( 1 ... N
) )  <->  c  =  ( ( d  u.  e )  |`  (
1 ... N ) ) ) )
85 reseq1 4856 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f  =  ( d  u.  e )  ->  (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  =  ( ( d  u.  e
)  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) )
8685fveq2d 5381 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  =  ( d  u.  e )  ->  (
a `  ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) )  =  ( a `  ( ( d  u.  e )  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) ) )
8786eqeq1d 2261 . . . . . . . . . . . . . . . . . . 19  |-  ( f  =  ( d  u.  e )  ->  (
( a `  (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) )  =  0  <->  ( a `  ( ( d  u.  e )  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )  =  0 ) )
88 reseq1 4856 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f  =  ( d  u.  e )  ->  (
f  |`  NN )  =  ( ( d  u.  e )  |`  NN ) )
8988fveq2d 5381 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  =  ( d  u.  e )  ->  (
b `  ( f  |`  NN ) )  =  ( b `  (
( d  u.  e
)  |`  NN ) ) )
9089eqeq1d 2261 . . . . . . . . . . . . . . . . . . 19  |-  ( f  =  ( d  u.  e )  ->  (
( b `  (
f  |`  NN ) )  =  0  <->  ( b `  ( ( d  u.  e )  |`  NN ) )  =  0 ) )
9187, 90anbi12d 694 . . . . . . . . . . . . . . . . . 18  |-  ( f  =  ( d  u.  e )  ->  (
( ( a `  ( f  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )  =  0  /\  (
b `  ( f  |`  NN ) )  =  0 )  <->  ( (
a `  ( (
d  u.  e )  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) )  =  0  /\  ( b `  ( ( d  u.  e )  |`  NN ) )  =  0 ) ) )
9284, 91anbi12d 694 . . . . . . . . . . . . . . . . 17  |-  ( f  =  ( d  u.  e )  ->  (
( c  =  ( f  |`  ( 1 ... N ) )  /\  ( ( a `
 ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) )  =  0  /\  ( b `  ( f  |`  NN ) )  =  0 ) )  <->  ( c  =  ( ( d  u.  e )  |`  (
1 ... N ) )  /\  ( ( a `
 ( ( d  u.  e )  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) )  =  0  /\  ( b `  ( ( d  u.  e )  |`  NN ) )  =  0 ) ) ) )
9392rcla4ev 2821 . . . . . . . . . . . . . . . 16  |-  ( ( ( d  u.  e
)  e.  ( NN0 
^m  ZZ )  /\  ( c  =  ( ( d  u.  e
)  |`  ( 1 ... N ) )  /\  ( ( a `  ( ( d  u.  e )  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )  =  0  /\  (
b `  ( (
d  u.  e )  |`  NN ) )  =  0 ) ) )  ->  E. f  e.  ( NN0  ^m  ZZ ) ( c  =  ( f  |`  ( 1 ... N ) )  /\  ( ( a `
 ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) )  =  0  /\  ( b `  ( f  |`  NN ) )  =  0 ) ) )
9455, 82, 93syl2anc 645 . . . . . . . . . . . . . . 15  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  (
d  e.  ( NN0 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  /\  e  e.  ( NN0  ^m  NN ) ) )  /\  ( ( c  =  ( d  |`  (
1 ... N ) )  /\  ( a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) ) )  ->  E. f  e.  ( NN0  ^m  ZZ ) ( c  =  ( f  |`  (
1 ... N ) )  /\  ( ( a `
 ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) )  =  0  /\  ( b `  ( f  |`  NN ) )  =  0 ) ) )
9594ex 425 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  (
d  e.  ( NN0 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  /\  e  e.  ( NN0  ^m  NN ) ) )  -> 
( ( ( c  =  ( d  |`  ( 1 ... N
) )  /\  (
a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N ) )  /\  ( b `  e )  =  0 ) )  ->  E. f  e.  ( NN0  ^m  ZZ ) ( c  =  ( f  |`  (
1 ... N ) )  /\  ( ( a `
 ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) )  =  0  /\  ( b `  ( f  |`  NN ) )  =  0 ) ) ) )
9695rexlimdvva 2636 . . . . . . . . . . . . 13  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  ( E. d  e.  ( NN0  ^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) E. e  e.  ( NN0  ^m  NN ) ( ( c  =  ( d  |`  ( 1 ... N
) )  /\  (
a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N ) )  /\  ( b `  e )  =  0 ) )  ->  E. f  e.  ( NN0  ^m  ZZ ) ( c  =  ( f  |`  (
1 ... N ) )  /\  ( ( a `
 ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) )  =  0  /\  ( b `  ( f  |`  NN ) )  =  0 ) ) ) )
97 simpr 449 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  f  e.  ( NN0  ^m  ZZ ) )  ->  f  e.  ( NN0  ^m  ZZ ) )
98 difss 3220 . . . . . . . . . . . . . . . . . 18  |-  ( ZZ 
\  ( ZZ>= `  ( N  +  1 ) ) )  C_  ZZ
99 elmapssres 25958 . . . . . . . . . . . . . . . . . 18  |-  ( ( f  e.  ( NN0 
^m  ZZ )  /\  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) 
C_  ZZ )  -> 
( f  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  e.  ( NN0  ^m  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )
10097, 98, 99sylancl 646 . . . . . . . . . . . . . . . . 17  |-  ( ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  f  e.  ( NN0  ^m  ZZ ) )  ->  (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  e.  ( NN0  ^m  ( ZZ 
\  ( ZZ>= `  ( N  +  1 ) ) ) ) )
101100adantr 453 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  f  e.  ( NN0  ^m  ZZ ) )  /\  (
c  =  ( f  |`  ( 1 ... N
) )  /\  (
( a `  (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) )  =  0  /\  ( b `
 ( f  |`  NN ) )  =  0 ) ) )  -> 
( f  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  e.  ( NN0  ^m  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )
102 nnssz 9922 . . . . . . . . . . . . . . . . . 18  |-  NN  C_  ZZ
103 elmapssres 25958 . . . . . . . . . . . . . . . . . 18  |-  ( ( f  e.  ( NN0 
^m  ZZ )  /\  NN  C_  ZZ )  -> 
( f  |`  NN )  e.  ( NN0  ^m  NN ) )
10497, 102, 103sylancl 646 . . . . . . . . . . . . . . . . 17  |-  ( ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  f  e.  ( NN0  ^m  ZZ ) )  ->  (
f  |`  NN )  e.  ( NN0  ^m  NN ) )
105104adantr 453 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  f  e.  ( NN0  ^m  ZZ ) )  /\  (
c  =  ( f  |`  ( 1 ... N
) )  /\  (
( a `  (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) )  =  0  /\  ( b `
 ( f  |`  NN ) )  =  0 ) ) )  -> 
( f  |`  NN )  e.  ( NN0  ^m  NN ) )
106 simprl 735 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  f  e.  ( NN0  ^m  ZZ ) )  /\  (
c  =  ( f  |`  ( 1 ... N
) )  /\  (
( a `  (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) )  =  0  /\  ( b `
 ( f  |`  NN ) )  =  0 ) ) )  -> 
c  =  ( f  |`  ( 1 ... N
) ) )
10715ad3antrrr 713 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  f  e.  ( NN0  ^m  ZZ ) )  /\  (
c  =  ( f  |`  ( 1 ... N
) )  /\  (
( a `  (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) )  =  0  /\  ( b `
 ( f  |`  NN ) )  =  0 ) ) )  -> 
( 1 ... N
)  C_  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )
108 resabs1 4891 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1 ... N ) 
C_  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) )  ->  ( (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  |`  (
1 ... N ) )  =  ( f  |`  ( 1 ... N
) ) )
109107, 108syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  f  e.  ( NN0  ^m  ZZ ) )  /\  (
c  =  ( f  |`  ( 1 ... N
) )  /\  (
( a `  (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) )  =  0  /\  ( b `
 ( f  |`  NN ) )  =  0 ) ) )  -> 
( ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  |`  ( 1 ... N ) )  =  ( f  |`  ( 1 ... N
) ) )
110106, 109eqtr4d 2288 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  f  e.  ( NN0  ^m  ZZ ) )  /\  (
c  =  ( f  |`  ( 1 ... N
) )  /\  (
( a `  (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) )  =  0  /\  ( b `
 ( f  |`  NN ) )  =  0 ) ) )  -> 
c  =  ( ( f  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  |`  (
1 ... N ) ) )
111 simprrl 743 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  f  e.  ( NN0  ^m  ZZ ) )  /\  (
c  =  ( f  |`  ( 1 ... N
) )  /\  (
( a `  (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) )  =  0  /\  ( b `
 ( f  |`  NN ) )  =  0 ) ) )  -> 
( a `  (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) )  =  0 )
112110, 111jca 520 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  f  e.  ( NN0  ^m  ZZ ) )  /\  (
c  =  ( f  |`  ( 1 ... N
) )  /\  (
( a `  (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) )  =  0  /\  ( b `
 ( f  |`  NN ) )  =  0 ) ) )  -> 
( c  =  ( ( f  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  |`  ( 1 ... N
) )  /\  (
a `  ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) )  =  0 ) )
113 resabs1 4891 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1 ... N ) 
C_  NN  ->  ( ( f  |`  NN )  |`  ( 1 ... N
) )  =  ( f  |`  ( 1 ... N ) ) )
11425, 113mp1i 13 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  f  e.  ( NN0  ^m  ZZ ) )  /\  (
c  =  ( f  |`  ( 1 ... N
) )  /\  (
( a `  (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) )  =  0  /\  ( b `
 ( f  |`  NN ) )  =  0 ) ) )  -> 
( ( f  |`  NN )  |`  ( 1 ... N ) )  =  ( f  |`  ( 1 ... N
) ) )
115106, 114eqtr4d 2288 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  f  e.  ( NN0  ^m  ZZ ) )  /\  (
c  =  ( f  |`  ( 1 ... N
) )  /\  (
( a `  (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) )  =  0  /\  ( b `
 ( f  |`  NN ) )  =  0 ) ) )  -> 
c  =  ( ( f  |`  NN )  |`  ( 1 ... N
) ) )
116 simprrr 744 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  f  e.  ( NN0  ^m  ZZ ) )  /\  (
c  =  ( f  |`  ( 1 ... N
) )  /\  (
( a `  (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) )  =  0  /\  ( b `
 ( f  |`  NN ) )  =  0 ) ) )  -> 
( b `  (
f  |`  NN ) )  =  0 )
117112, 115, 116jca32 523 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  f  e.  ( NN0  ^m  ZZ ) )  /\  (
c  =  ( f  |`  ( 1 ... N
) )  /\  (
( a `  (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) )  =  0  /\  ( b `
 ( f  |`  NN ) )  =  0 ) ) )  -> 
( ( c  =  ( ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  |`  ( 1 ... N ) )  /\  ( a `  ( f  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )  =  0 )  /\  ( c  =  ( ( f  |`  NN )  |`  ( 1 ... N
) )  /\  (
b `  ( f  |`  NN ) )  =  0 ) ) )
118 reseq1 4856 . . . . . . . . . . . . . . . . . . . 20  |-  ( d  =  ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  ->  ( d  |`  ( 1 ... N
) )  =  ( ( f  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  |`  ( 1 ... N
) ) )
119118eqeq2d 2264 . . . . . . . . . . . . . . . . . . 19  |-  ( d  =  ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  ->  ( c  =  ( d  |`  ( 1 ... N
) )  <->  c  =  ( ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  |`  ( 1 ... N ) ) ) )
120 fveq2 5377 . . . . . . . . . . . . . . . . . . . 20  |-  ( d  =  ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  ->  ( a `  d )  =  ( a `  ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) ) )
121120eqeq1d 2261 . . . . . . . . . . . . . . . . . . 19  |-  ( d  =  ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  ->  ( (
a `  d )  =  0  <->  ( a `  ( f  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )  =  0 ) )
122119, 121anbi12d 694 . . . . . . . . . . . . . . . . . 18  |-  ( d  =  ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  ->  ( (
c  =  ( d  |`  ( 1 ... N
) )  /\  (
a `  d )  =  0 )  <->  ( c  =  ( ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  |`  ( 1 ... N ) )  /\  ( a `  ( f  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )  =  0 ) ) )
123122anbi1d 688 . . . . . . . . . . . . . . . . 17  |-  ( d  =  ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  ->  ( (
( c  =  ( d  |`  ( 1 ... N ) )  /\  ( a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) )  <-> 
( ( c  =  ( ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  |`  ( 1 ... N ) )  /\  ( a `  ( f  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N ) )  /\  ( b `  e )  =  0 ) ) ) )
124 reseq1 4856 . . . . . . . . . . . . . . . . . . . 20  |-  ( e  =  ( f  |`  NN )  ->  ( e  |`  ( 1 ... N
) )  =  ( ( f  |`  NN )  |`  ( 1 ... N
) ) )
125124eqeq2d 2264 . . . . . . . . . . . . . . . . . . 19  |-  ( e  =  ( f  |`  NN )  ->  ( c  =  ( e  |`  ( 1 ... N
) )  <->  c  =  ( ( f  |`  NN )  |`  ( 1 ... N ) ) ) )
126 fveq2 5377 . . . . . . . . . . . . . . . . . . . 20  |-  ( e  =  ( f  |`  NN )  ->  ( b `
 e )  =  ( b `  (
f  |`  NN ) ) )
127126eqeq1d 2261 . . . . . . . . . . . . . . . . . . 19  |-  ( e  =  ( f  |`  NN )  ->  ( ( b `  e )  =  0  <->  ( b `  ( f  |`  NN ) )  =  0 ) )
128125, 127anbi12d 694 . . . . . . . . . . . . . . . . . 18  |-  ( e  =  ( f  |`  NN )  ->  ( ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 )  <->  ( c  =  ( ( f  |`  NN )  |`  (
1 ... N ) )  /\  ( b `  ( f  |`  NN ) )  =  0 ) ) )
129128anbi2d 687 . . . . . . . . . . . . . . . . 17  |-  ( e  =  ( f  |`  NN )  ->  ( ( ( c  =  ( ( f  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  |`  ( 1 ... N
) )  /\  (
a `  ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) )  <-> 
( ( c  =  ( ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  |`  ( 1 ... N ) )  /\  ( a `  ( f  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )  =  0 )  /\  ( c  =  ( ( f  |`  NN )  |`  ( 1 ... N
) )  /\  (
b `  ( f  |`  NN ) )  =  0 ) ) ) )
130123, 129rcla42ev 2829 . . . . . . . . . . . . . . . 16  |-  ( ( ( f  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  e.  ( NN0  ^m  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  ( f  |`  NN )  e.  ( NN0  ^m  NN )  /\  (
( c  =  ( ( f  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  |`  ( 1 ... N
) )  /\  (
a `  ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) )  =  0 )  /\  ( c  =  ( ( f  |`  NN )  |`  (
1 ... N ) )  /\  ( b `  ( f  |`  NN ) )  =  0 ) ) )  ->  E. d  e.  ( NN0  ^m  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) E. e  e.  ( NN0 
^m  NN ) ( ( c  =  ( d  |`  ( 1 ... N ) )  /\  ( a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) ) )
131101, 105, 117, 130syl3anc 1187 . . . . . . . . . . . . . . 15  |-  ( ( ( ( N  e. 
NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  f  e.  ( NN0  ^m  ZZ ) )  /\  (
c  =  ( f  |`  ( 1 ... N
) )  /\  (
( a `  (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) )  =  0  /\  ( b `
 ( f  |`  NN ) )  =  0 ) ) )  ->  E. d  e.  ( NN0  ^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) E. e  e.  ( NN0  ^m  NN ) ( ( c  =  ( d  |`  ( 1 ... N
) )  /\  (
a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N ) )  /\  ( b `  e )  =  0 ) ) )
132131ex 425 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  f  e.  ( NN0  ^m  ZZ ) )  ->  (
( c  =  ( f  |`  ( 1 ... N ) )  /\  ( ( a `
 ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) )  =  0  /\  ( b `  ( f  |`  NN ) )  =  0 ) )  ->  E. d  e.  ( NN0  ^m  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) E. e  e.  ( NN0 
^m  NN ) ( ( c  =  ( d  |`  ( 1 ... N ) )  /\  ( a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) ) ) )
133132rexlimdva 2629 . . . . . . . . . . . . 13  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  ( E. f  e.  ( NN0  ^m  ZZ ) ( c  =  ( f  |`  ( 1 ... N
) )  /\  (
( a `  (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) )  =  0  /\  ( b `
 ( f  |`  NN ) )  =  0 ) )  ->  E. d  e.  ( NN0  ^m  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) E. e  e.  ( NN0 
^m  NN ) ( ( c  =  ( d  |`  ( 1 ... N ) )  /\  ( a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) ) ) )
13496, 133impbid 185 . . . . . . . . . . . 12  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  ( E. d  e.  ( NN0  ^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) E. e  e.  ( NN0  ^m  NN ) ( ( c  =  ( d  |`  ( 1 ... N
) )  /\  (
a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N ) )  /\  ( b `  e )  =  0 ) )  <->  E. f  e.  ( NN0  ^m  ZZ ) ( c  =  ( f  |`  (
1 ... N ) )  /\  ( ( a `
 ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) )  =  0  /\  ( b `  ( f  |`  NN ) )  =  0 ) ) ) )
135 simplrl 739 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  f  e.  ( NN0  ^m  ZZ ) )  ->  a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )
136 mzpf 25980 . . . . . . . . . . . . . . . . . . 19  |-  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  -> 
a : ( ZZ 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) --> ZZ )
137135, 136syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  f  e.  ( NN0  ^m  ZZ ) )  ->  a : ( ZZ  ^m  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) --> ZZ )
138 nn0ssz 9923 . . . . . . . . . . . . . . . . . . . . . 22  |-  NN0  C_  ZZ
139 mapss 6696 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ZZ  e.  _V  /\  NN0  C_  ZZ )  ->  ( NN0  ^m  ZZ )  C_  ( ZZ  ^m  ZZ ) )
1403, 138, 139mp2an 656 . . . . . . . . . . . . . . . . . . . . 21  |-  ( NN0 
^m  ZZ )  C_  ( ZZ  ^m  ZZ )
141140sseli 3099 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  e.  ( NN0  ^m  ZZ )  ->  f  e.  ( ZZ  ^m  ZZ ) )
142 elmapssres 25958 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( f  e.  ( ZZ 
^m  ZZ )  /\  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) 
C_  ZZ )  -> 
( f  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  e.  ( ZZ  ^m  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )
143141, 98, 142sylancl 646 . . . . . . . . . . . . . . . . . . 19  |-  ( f  e.  ( NN0  ^m  ZZ )  ->  ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  e.  ( ZZ 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) )
144143adantl 454 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  f  e.  ( NN0  ^m  ZZ ) )  ->  (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  e.  ( ZZ  ^m  ( ZZ 
\  ( ZZ>= `  ( N  +  1 ) ) ) ) )
145 ffvelrn 5515 . . . . . . . . . . . . . . . . . 18  |-  ( ( a : ( ZZ 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) --> ZZ  /\  ( f  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  e.  ( ZZ  ^m  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )  ->  ( a `  ( f  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )  e.  ZZ )
146137, 144, 145syl2anc 645 . . . . . . . . . . . . . . . . 17  |-  ( ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  f  e.  ( NN0  ^m  ZZ ) )  ->  (
a `  ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) )  e.  ZZ )
147146zred 9996 . . . . . . . . . . . . . . . 16  |-  ( ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  f  e.  ( NN0  ^m  ZZ ) )  ->  (
a `  ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) )  e.  RR )
148 simplrr 740 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  f  e.  ( NN0  ^m  ZZ ) )  ->  b  e.  (mzPoly `  NN )
)
149 mzpf 25980 . . . . . . . . . . . . . . . . . . 19  |-  ( b  e.  (mzPoly `  NN )  ->  b : ( ZZ  ^m  NN ) --> ZZ )
150148, 149syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  f  e.  ( NN0  ^m  ZZ ) )  ->  b : ( ZZ  ^m  NN ) --> ZZ )
151 elmapssres 25958 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( f  e.  ( ZZ 
^m  ZZ )  /\  NN  C_  ZZ )  -> 
( f  |`  NN )  e.  ( ZZ  ^m  NN ) )
152141, 102, 151sylancl 646 . . . . . . . . . . . . . . . . . . 19  |-  ( f  e.  ( NN0  ^m  ZZ )  ->  ( f  |`  NN )  e.  ( ZZ  ^m  NN ) )
153152adantl 454 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  f  e.  ( NN0  ^m  ZZ ) )  ->  (
f  |`  NN )  e.  ( ZZ  ^m  NN ) )
154 ffvelrn 5515 . . . . . . . . . . . . . . . . . 18  |-  ( ( b : ( ZZ 
^m  NN ) --> ZZ 
/\  ( f  |`  NN )  e.  ( ZZ  ^m  NN ) )  ->  ( b `  ( f  |`  NN ) )  e.  ZZ )
155150, 153, 154syl2anc 645 . . . . . . . . . . . . . . . . 17  |-  ( ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  f  e.  ( NN0  ^m  ZZ ) )  ->  (
b `  ( f  |`  NN ) )  e.  ZZ )
156155zred 9996 . . . . . . . . . . . . . . . 16  |-  ( ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  f  e.  ( NN0  ^m  ZZ ) )  ->  (
b `  ( f  |`  NN ) )  e.  RR )
157 sumsqeq0 11060 . . . . . . . . . . . . . . . 16  |-  ( ( ( a `  (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) )  e.  RR  /\  ( b `
 ( f  |`  NN ) )  e.  RR )  ->  ( ( ( a `  ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) )  =  0  /\  ( b `  ( f  |`  NN ) )  =  0 )  <-> 
( ( ( a `
 ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) ) ^ 2 )  +  ( ( b `  ( f  |`  NN ) ) ^
2 ) )  =  0 ) )
158147, 156, 157syl2anc 645 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  f  e.  ( NN0  ^m  ZZ ) )  ->  (
( ( a `  ( f  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )  =  0  /\  (
b `  ( f  |`  NN ) )  =  0 )  <->  ( (
( a `  (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) ) ^
2 )  +  ( ( b `  (
f  |`  NN ) ) ^ 2 ) )  =  0 ) )
159141adantl 454 . . . . . . . . . . . . . . . . 17  |-  ( ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  f  e.  ( NN0  ^m  ZZ ) )  ->  f  e.  ( ZZ  ^m  ZZ ) )
160 reseq1 4856 . . . . . . . . . . . . . . . . . . . . 21  |-  ( g  =  f  ->  (
g  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  =  ( f  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )
161160fveq2d 5381 . . . . . . . . . . . . . . . . . . . 20  |-  ( g  =  f  ->  (
a `  ( g  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) )  =  ( a `  ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) ) )
162161oveq1d 5725 . . . . . . . . . . . . . . . . . . 19  |-  ( g  =  f  ->  (
( a `  (
g  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) ) ^
2 )  =  ( ( a `  (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) ) ^
2 ) )
163 reseq1 4856 . . . . . . . . . . . . . . . . . . . . 21  |-  ( g  =  f  ->  (
g  |`  NN )  =  ( f  |`  NN ) )
164163fveq2d 5381 . . . . . . . . . . . . . . . . . . . 20  |-  ( g  =  f  ->  (
b `  ( g  |`  NN ) )  =  ( b `  (
f  |`  NN ) ) )
165164oveq1d 5725 . . . . . . . . . . . . . . . . . . 19  |-  ( g  =  f  ->  (
( b `  (
g  |`  NN ) ) ^ 2 )  =  ( ( b `  ( f  |`  NN ) ) ^ 2 ) )
166162, 165oveq12d 5728 . . . . . . . . . . . . . . . . . 18  |-  ( g  =  f  ->  (
( ( a `  ( g  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) ) ^ 2 )  +  ( ( b `  ( g  |`  NN ) ) ^ 2 ) )  =  ( ( ( a `  (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) ) ^
2 )  +  ( ( b `  (
f  |`  NN ) ) ^ 2 ) ) )
167 eqid 2253 . . . . . . . . . . . . . . . . . 18  |-  ( g  e.  ( ZZ  ^m  ZZ )  |->  ( ( ( a `  (
g  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) ) ^
2 )  +  ( ( b `  (
g  |`  NN ) ) ^ 2 ) ) )  =  ( g  e.  ( ZZ  ^m  ZZ )  |->  ( ( ( a `  (
g  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) ) ^
2 )  +  ( ( b `  (
g  |`  NN ) ) ^ 2 ) ) )
168 ovex 5735 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( a `  (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) ) ^
2 )  +  ( ( b `  (
f  |`  NN ) ) ^ 2 ) )  e.  _V
169166, 167, 168fvmpt 5454 . . . . . . . . . . . . . . . . 17  |-  ( f  e.  ( ZZ  ^m  ZZ )  ->  ( ( g  e.  ( ZZ 
^m  ZZ )  |->  ( ( ( a `  ( g  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) ) ^ 2 )  +  ( ( b `  ( g  |`  NN ) ) ^ 2 ) ) ) `  f
)  =  ( ( ( a `  (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) ) ^
2 )  +  ( ( b `  (
f  |`  NN ) ) ^ 2 ) ) )
170159, 169syl 17 . . . . . . . . . . . . . . . 16  |-  ( ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  f  e.  ( NN0  ^m  ZZ ) )  ->  (
( g  e.  ( ZZ  ^m  ZZ ) 
|->  ( ( ( a `
 ( g  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) ) ^ 2 )  +  ( ( b `  ( g  |`  NN ) ) ^
2 ) ) ) `
 f )  =  ( ( ( a `
 ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) ) ^ 2 )  +  ( ( b `  ( f  |`  NN ) ) ^
2 ) ) )
171170eqeq1d 2261 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  f  e.  ( NN0  ^m  ZZ ) )  ->  (
( ( g  e.  ( ZZ  ^m  ZZ )  |->  ( ( ( a `  ( g  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) ) ^ 2 )  +  ( ( b `  ( g  |`  NN ) ) ^
2 ) ) ) `
 f )  =  0  <->  ( ( ( a `  ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) ) ^ 2 )  +  ( ( b `  ( f  |`  NN ) ) ^
2 ) )  =  0 ) )
172158, 171bitr4d 249 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  f  e.  ( NN0  ^m  ZZ ) )  ->  (
( ( a `  ( f  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )  =  0  /\  (
b `  ( f  |`  NN ) )  =  0 )  <->  ( (
g  e.  ( ZZ 
^m  ZZ )  |->  ( ( ( a `  ( g  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) ) ^ 2 )  +  ( ( b `  ( g  |`  NN ) ) ^ 2 ) ) ) `  f
)  =  0 ) )
173172anbi2d 687 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  f  e.  ( NN0  ^m  ZZ ) )  ->  (
( c  =  ( f  |`  ( 1 ... N ) )  /\  ( ( a `
 ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) )  =  0  /\  ( b `  ( f  |`  NN ) )  =  0 ) )  <->  ( c  =  ( f  |`  (
1 ... N ) )  /\  ( ( g  e.  ( ZZ  ^m  ZZ )  |->  ( ( ( a `  (
g  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) ) ^
2 )  +  ( ( b `  (
g  |`  NN ) ) ^ 2 ) ) ) `  f )  =  0 ) ) )
174173rexbidva 2524 . . . . . . . . . . . 12  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  ( E. f  e.  ( NN0  ^m  ZZ ) ( c  =  ( f  |`  ( 1 ... N
) )  /\  (
( a `  (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) )  =  0  /\  ( b `
 ( f  |`  NN ) )  =  0 ) )  <->  E. f  e.  ( NN0  ^m  ZZ ) ( c  =  ( f  |`  (
1 ... N ) )  /\  ( ( g  e.  ( ZZ  ^m  ZZ )  |->  ( ( ( a `  (
g  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) ) ^
2 )  +  ( ( b `  (
g  |`  NN ) ) ^ 2 ) ) ) `  f )  =  0 ) ) )
175134, 174bitrd 246 . . . . . . . . . . 11  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  ( E. d  e.  ( NN0  ^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) E. e  e.  ( NN0  ^m  NN ) ( ( c  =  ( d  |`  ( 1 ... N
) )  /\  (
a `  d )  =  0 )  /\  ( c  =  ( e  |`  ( 1 ... N ) )  /\  ( b `  e )  =  0 ) )  <->  E. f  e.  ( NN0  ^m  ZZ ) ( c  =  ( f  |`  (
1 ... N ) )  /\  ( ( g  e.  ( ZZ  ^m  ZZ )  |->  ( ( ( a `  (
g  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) ) ^
2 )  +  ( ( b `  (
g  |`  NN ) ) ^ 2 ) ) ) `  f )  =  0 ) ) )
17632, 175syl5bbr 252 . . . . . . . . . 10  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  (
( E. d  e.  ( NN0  ^m  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) ( c  =  ( d  |`  ( 1 ... N
) )  /\  (
a `  d )  =  0 )  /\  E. e  e.  ( NN0 
^m  NN ) ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) )  <->  E. f  e.  ( NN0  ^m  ZZ ) ( c  =  ( f  |`  ( 1 ... N
) )  /\  (
( g  e.  ( ZZ  ^m  ZZ ) 
|->  ( ( ( a `
 ( g  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) ) ^ 2 )  +  ( ( b `  ( g  |`  NN ) ) ^
2 ) ) ) `
 f )  =  0 ) ) )
177176abbidv 2363 . . . . . . . . 9  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  { c  |  ( E. d  e.  ( NN0  ^m  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) ( c  =  ( d  |`  ( 1 ... N
) )  /\  (
a `  d )  =  0 )  /\  E. e  e.  ( NN0 
^m  NN ) ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 ) ) }  =  { c  |  E. f  e.  ( NN0  ^m  ZZ ) ( c  =  ( f  |`  (
1 ... N ) )  /\  ( ( g  e.  ( ZZ  ^m  ZZ )  |->  ( ( ( a `  (
g  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) ) ^
2 )  +  ( ( b `  (
g  |`  NN ) ) ^ 2 ) ) ) `  f )  =  0 ) } )
17831, 177syl5eq 2297 . . . . . . . 8  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  ( { c  |  E. d  e.  ( NN0  ^m  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) ( c  =  ( d  |`  (
1 ... N ) )  /\  ( a `  d )  =  0 ) }  i^i  {
c  |  E. e  e.  ( NN0  ^m  NN ) ( c  =  ( e  |`  (
1 ... N ) )  /\  ( b `  e )  =  0 ) } )  =  { c  |  E. f  e.  ( NN0  ^m  ZZ ) ( c  =  ( f  |`  ( 1 ... N
) )  /\  (
( g  e.  ( ZZ  ^m  ZZ ) 
|->  ( ( ( a `
 ( g  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) ) ^ 2 )  +  ( ( b `  ( g  |`  NN ) ) ^
2 ) ) ) `
 f )  =  0 ) } )
179 simpl 445 . . . . . . . . 9  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  N  e.  NN0 )
180 fzssuz 10710 . . . . . . . . . . . 12  |-  ( 1 ... N )  C_  ( ZZ>= `  1 )
181 uzssz 10126 . . . . . . . . . . . 12  |-  ( ZZ>= ` 
1 )  C_  ZZ
182180, 181sstri 3109 . . . . . . . . . . 11  |-  ( 1 ... N )  C_  ZZ
1833, 182pm3.2i 443 . . . . . . . . . 10  |-  ( ZZ  e.  _V  /\  (
1 ... N )  C_  ZZ )
184183a1i 12 . . . . . . . . 9  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  ( ZZ  e.  _V  /\  (
1 ... N )  C_  ZZ ) )
1853a1i 12 . . . . . . . . . . . 12  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  ZZ  e.  _V )
18698a1i 12 . . . . . . . . . . . 12  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) )  C_  ZZ )
187 simprl 735 . . . . . . . . . . . 12  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )
188 mzpresrename 25994 . . . . . . . . . . . 12  |-  ( ( ZZ  e.  _V  /\  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) 
C_  ZZ  /\  a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )  -> 
( g  e.  ( ZZ  ^m  ZZ ) 
|->  ( a `  (
g  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) ) )  e.  (mzPoly `  ZZ ) )
189185, 186, 187, 188syl3anc 1187 . . . . . . . . . . 11  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  (
g  e.  ( ZZ 
^m  ZZ )  |->  ( a `  ( g  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) ) )  e.  (mzPoly `  ZZ )
)
190 2nn0 9861 . . . . . . . . . . 11  |-  2  e.  NN0
191 mzpexpmpt 25989 . . . . . . . . . . 11  |-  ( ( ( g  e.  ( ZZ  ^m  ZZ ) 
|->  ( a `  (
g  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) ) )  e.  (mzPoly `  ZZ )  /\  2  e.  NN0 )  ->  ( g  e.  ( ZZ  ^m  ZZ )  |->  ( ( a `
 ( g  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) ) ^ 2 ) )  e.  (mzPoly `  ZZ ) )
192189, 190, 191sylancl 646 . . . . . . . . . 10  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  (
g  e.  ( ZZ 
^m  ZZ )  |->  ( ( a `  (
g  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) ) ^
2 ) )  e.  (mzPoly `  ZZ )
)
193102a1i 12 . . . . . . . . . . . 12  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  NN  C_  ZZ )
194 simprr 736 . . . . . . . . . . . 12  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  b  e.  (mzPoly `  NN )
)
195 mzpresrename 25994 . . . . . . . . . . . 12  |-  ( ( ZZ  e.  _V  /\  NN  C_  ZZ  /\  b  e.  (mzPoly `  NN )
)  ->  ( g  e.  ( ZZ  ^m  ZZ )  |->  ( b `  ( g  |`  NN ) ) )  e.  (mzPoly `  ZZ ) )
196185, 193, 194, 195syl3anc 1187 . . . . . . . . . . 11  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  (
g  e.  ( ZZ 
^m  ZZ )  |->  ( b `  ( g  |`  NN ) ) )  e.  (mzPoly `  ZZ ) )
197 mzpexpmpt 25989 . . . . . . . . . . 11  |-  ( ( ( g  e.  ( ZZ  ^m  ZZ ) 
|->  ( b `  (
g  |`  NN ) ) )  e.  (mzPoly `  ZZ )  /\  2  e.  NN0 )  ->  (
g  e.  ( ZZ 
^m  ZZ )  |->  ( ( b `  (
g  |`  NN ) ) ^ 2 ) )  e.  (mzPoly `  ZZ ) )
198196, 190, 197sylancl 646 . . . . . . . . . 10  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  (
g  e.  ( ZZ 
^m  ZZ )  |->  ( ( b `  (
g  |`  NN ) ) ^ 2 ) )  e.  (mzPoly `  ZZ ) )
199 mzpaddmpt 25985 . . . . . . . . . 10  |-  ( ( ( g  e.  ( ZZ  ^m  ZZ ) 
|->  ( ( a `  ( g  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) ) ^ 2 ) )  e.  (mzPoly `  ZZ )  /\  ( g  e.  ( ZZ  ^m  ZZ )  |->  ( ( b `
 ( g  |`  NN ) ) ^ 2 ) )  e.  (mzPoly `  ZZ ) )  -> 
( g  e.  ( ZZ  ^m  ZZ ) 
|->  ( ( ( a `
 ( g  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) ) ^ 2 )  +  ( ( b `  ( g  |`  NN ) ) ^
2 ) ) )  e.  (mzPoly `  ZZ ) )
200192, 198, 199syl2anc 645 . . . . . . . . 9  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  (
g  e.  ( ZZ 
^m  ZZ )  |->  ( ( ( a `  ( g  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) ) ^ 2 )  +  ( ( b `  ( g  |`  NN ) ) ^ 2 ) ) )  e.  (mzPoly `  ZZ ) )
201 eldioph2 26007 . . . . . . . . 9  |-  ( ( N  e.  NN0  /\  ( ZZ  e.  _V  /\  ( 1 ... N
)  C_  ZZ )  /\  ( g  e.  ( ZZ  ^m  ZZ ) 
|->  ( ( ( a `
 ( g  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) ) ^ 2 )  +  ( ( b `  ( g  |`  NN ) ) ^
2 ) ) )  e.  (mzPoly `  ZZ ) )  ->  { c  |  E. f  e.  ( NN0  ^m  ZZ ) ( c  =  ( f  |`  (
1 ... N ) )  /\  ( ( g  e.  ( ZZ  ^m  ZZ )  |->  ( ( ( a `  (
g  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) ) ^
2 )  +  ( ( b `  (
g  |`  NN ) ) ^ 2 ) ) ) `  f )  =  0 ) }  e.  (Dioph `  N
) )
202179, 184, 200, 201syl3anc 1187 . . . . . . . 8  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  { c  |  E. f  e.  ( NN0  ^m  ZZ ) ( c  =  ( f  |`  (
1 ... N ) )  /\  ( ( g  e.  ( ZZ  ^m  ZZ )  |->  ( ( ( a `  (
g  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) ) ^
2 )  +  ( ( b `  (
g  |`  NN ) ) ^ 2 ) ) ) `  f )  =  0 ) }  e.  (Dioph `  N
) )
203178, 202eqeltrd 2327 . . . . . . 7  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  ( { c  |  E. d  e.  ( NN0  ^m  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) ( c  =  ( d  |`  (
1 ... N ) )  /\  ( a `  d )  =  0 ) }  i^i  {
c  |  E. e  e.  ( NN0  ^m  NN ) ( c  =  ( e  |`  (
1 ... N ) )  /\  ( b `  e )  =  0 ) } )  e.  (Dioph `  N )
)
204 ineq12 3273 . . . . . . . 8  |-  ( ( A  =  { c  |  E. d  e.  ( NN0  ^m  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) ( c  =  ( d  |`  ( 1 ... N
) )  /\  (
a `  d )  =  0 ) }  /\  B  =  {
c  |  E. e  e.  ( NN0  ^m  NN ) ( c  =  ( e  |`  (
1 ... N ) )  /\  ( b `  e )  =  0 ) } )  -> 
( A  i^i  B
)  =  ( { c  |  E. d  e.  ( NN0  ^m  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) ( c  =  ( d  |`  ( 1 ... N
) )  /\  (
a `  d )  =  0 ) }  i^i  { c  |  E. e  e.  ( NN0  ^m  NN ) ( c  =  ( e  |`  ( 1 ... N ) )  /\  ( b `  e )  =  0 ) } ) )
205204eleq1d 2319 . . . . . . 7  |-  ( ( A  =  { c  |  E. d  e.  ( NN0  ^m  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) ( c  =  ( d  |`  ( 1 ... N
) )  /\  (
a `  d )  =  0 ) }  /\  B  =  {
c  |  E. e  e.  ( NN0  ^m  NN ) ( c  =  ( e  |`  (
1 ... N ) )  /\  ( b `  e )  =  0 ) } )  -> 
( ( A  i^i  B )  e.  (Dioph `  N )  <->  ( {
c  |  E. d  e.  ( NN0  ^m  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) ( c  =  ( d  |`  ( 1 ... N
) )  /\  (
a `  d )  =  0 ) }  i^i  { c  |  E. e  e.  ( NN0  ^m  NN ) ( c  =  ( e  |`  ( 1 ... N ) )  /\  ( b `  e )  =  0 ) } )  e.  (Dioph `  N )
) )
206203, 205syl5ibrcom 215 . . . . . 6  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  (
( A  =  {
c  |  E. d  e.  ( NN0  ^m  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) ( c  =  ( d  |`  ( 1 ... N
) )  /\  (
a `  d )  =  0 ) }  /\  B  =  {
c  |  E. e  e.  ( NN0  ^m  NN ) ( c  =  ( e  |`  (
1 ... N ) )  /\  ( b `  e )  =  0 ) } )  -> 
( A  i^i  B
)  e.  (Dioph `  N ) ) )
207206rexlimdvva 2636 . . . . 5  |-  ( N  e.  NN0  ->  ( E. a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N