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

Theorem diophin 30945
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
Dummy variables  a 
b  c  d  e  f  g are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eldiophelnn0 30936 . . 3  |-  ( A  e.  (Dioph `  N
)  ->  N  e.  NN0 )
2 id 22 . . . . . 6  |-  ( N  e.  NN0  ->  N  e. 
NN0 )
3 zex 10869 . . . . . . 7  |-  ZZ  e.  _V
4 difexg 4585 . . . . . . 7  |-  ( ZZ  e.  _V  ->  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) )  e.  _V )
53, 4mp1i 12 . . . . . 6  |-  ( N  e.  NN0  ->  ( ZZ 
\  ( ZZ>= `  ( N  +  1 ) ) )  e.  _V )
6 ominf 7725 . . . . . . 7  |-  -.  om  e.  Fin
7 nn0z 10883 . . . . . . . 8  |-  ( N  e.  NN0  ->  N  e.  ZZ )
8 lzenom 30942 . . . . . . . 8  |-  ( N  e.  ZZ  ->  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) )  ~~  om )
9 enfi 7729 . . . . . . . 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 301 . . . . . 6  |-  ( N  e.  NN0  ->  -.  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) )  e.  Fin )
12 fz1eqin 30941 . . . . . . 7  |-  ( N  e.  NN0  ->  ( 1 ... N )  =  ( ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) )  i^i  NN ) )
13 inss1 3704 . . . . . . 7  |-  ( ( ZZ  \  ( ZZ>= `  ( N  +  1
) ) )  i^i 
NN )  C_  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) )
1412, 13syl6eqss 3539 . . . . . 6  |-  ( N  e.  NN0  ->  ( 1 ... N )  C_  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )
15 eldioph2b 30935 . . . . . 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 ) } ) )
162, 5, 11, 14, 15syl22anc 1227 . . . . 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 ) } ) )
17 nnex 10537 . . . . . . 7  |-  NN  e.  _V
1817a1i 11 . . . . . 6  |-  ( N  e.  NN0  ->  NN  e.  _V )
19 1z 10890 . . . . . . 7  |-  1  e.  ZZ
20 nnuz 11117 . . . . . . . 8  |-  NN  =  ( ZZ>= `  1 )
2120uzinf 12058 . . . . . . 7  |-  ( 1  e.  ZZ  ->  -.  NN  e.  Fin )
2219, 21mp1i 12 . . . . . 6  |-  ( N  e.  NN0  ->  -.  NN  e.  Fin )
23 elfznn 11717 . . . . . . . 8  |-  ( a  e.  ( 1 ... N )  ->  a  e.  NN )
2423ssriv 3493 . . . . . . 7  |-  ( 1 ... N )  C_  NN
2524a1i 11 . . . . . 6  |-  ( N  e.  NN0  ->  ( 1 ... N )  C_  NN )
26 eldioph2b 30935 . . . . . 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 ) } ) )
272, 18, 22, 25, 26syl22anc 1227 . . . . 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 ) } ) )
2816, 27anbi12d 708 . . . 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 ) } ) ) )
29 reeanv 3022 . . . . 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 ) } ) )
30 inab 3763 . . . . . . . . 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 ) ) }
31 reeanv 3022 . . . . . . . . . . 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 ) ) )
32 simplrl 759 . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
33 simplrr 760 . . . . . . . . . . . . . . . . . 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 ) )
3412eqcomd 2462 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  NN0  ->  ( ( ZZ  \  ( ZZ>= `  ( N  +  1
) ) )  i^i 
NN )  =  ( 1 ... N ) )
3534reseq2d 5262 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  NN0  ->  ( d  |`  ( ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) )  i^i  NN ) )  =  ( d  |`  ( 1 ... N
) ) )
3635ad3antrrr 727 . . . . . . . . . . . . . . . . . . 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
) ) )
3734reseq2d 5262 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  NN0  ->  ( e  |`  ( ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) )  i^i  NN ) )  =  ( e  |`  ( 1 ... N
) ) )
3837ad3antrrr 727 . . . . . . . . . . . . . . . . . . . 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
) ) )
39 simprrl 763 . . . . . . . . . . . . . . . . . . . 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 ) ) )
40 simprll 761 . . . . . . . . . . . . . . . . . . . 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 ) ) )
4138, 39, 403eqtr2d 2501 . . . . . . . . . . . . . . . . . . 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
) ) )
4236, 41eqtr4d 2498 . . . . . . . . . . . . . . . . . 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 ) ) )
43 elmapresaun 30943 . . . . . . . . . . . . . . . . . 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 ) ) )
4432, 33, 42, 43syl3anc 1226 . . . . . . . . . . . . . . . . 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 ) ) )
4520uneq2i 3641 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ZZ  \  ( ZZ>= `  ( N  +  1
) ) )  u.  NN )  =  ( ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) )  u.  ( ZZ>= `  1
) )
4619a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  NN0  ->  1  e.  ZZ )
47 nn0p1nn 10831 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( N  e.  NN0  ->  ( N  +  1 )  e.  NN )
4847nnge1d 10574 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  NN0  ->  1  <_ 
( N  +  1 ) )
49 lzunuz 30940 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( N  e.  ZZ  /\  1  e.  ZZ  /\  1  <_  ( N  +  1 ) )  ->  (
( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) )  u.  ( ZZ>= `  1
) )  =  ZZ )
507, 46, 48, 49syl3anc 1226 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  NN0  ->  ( ( ZZ  \  ( ZZ>= `  ( N  +  1
) ) )  u.  ( ZZ>= `  1 )
)  =  ZZ )
5145, 50syl5eq 2507 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  NN0  ->  ( ( ZZ  \  ( ZZ>= `  ( N  +  1
) ) )  u.  NN )  =  ZZ )
5251oveq2d 6286 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  NN0  ->  ( NN0 
^m  ( ( ZZ 
\  ( ZZ>= `  ( N  +  1 ) ) )  u.  NN ) )  =  ( NN0  ^m  ZZ ) )
5352ad3antrrr 727 . . . . . . . . . . . . . . . . 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 ) )
5444, 53eleqtrd 2544 . . . . . . . . . . . . . . . 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 ) )
55 unidm 3633 . . . . . . . . . . . . . . . . . . 19  |-  ( c  u.  c )  =  c
5640, 39uneq12d 3645 . . . . . . . . . . . . . . . . . . 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
) ) ) )
5755, 56syl5eqr 2509 . . . . . . . . . . . . . . . . . 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 ) ) ) )
58 resundir 5276 . . . . . . . . . . . . . . . . . 18  |-  ( ( d  u.  e )  |`  ( 1 ... N
) )  =  ( ( d  |`  (
1 ... N ) )  u.  ( e  |`  ( 1 ... N
) ) )
5957, 58syl6eqr 2513 . . . . . . . . . . . . . . . . 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 ) ) )
60 uncom 3634 . . . . . . . . . . . . . . . . . . . . 21  |-  ( d  u.  e )  =  ( e  u.  d
)
6160reseq1i 5258 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( d  u.  e )  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  =  ( ( e  u.  d )  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )
62 incom 3677 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( NN 
i^i  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  =  ( ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) )  i^i  NN )
6362, 34syl5eq 2507 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( N  e.  NN0  ->  ( NN 
i^i  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  =  ( 1 ... N ) )
6463reseq2d 5262 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  NN0  ->  ( e  |`  ( NN  i^i  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )  =  ( e  |`  ( 1 ... N
) ) )
6564ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . 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
) ) )
6663reseq2d 5262 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( N  e.  NN0  ->  ( d  |`  ( NN  i^i  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )  =  ( d  |`  ( 1 ... N
) ) )
6766ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
6867, 40, 393eqtr2d 2501 . . . . . . . . . . . . . . . . . . . . . 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
) ) )
6965, 68eqtr4d 2498 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
70 elmapresaunres2 30944 . . . . . . . . . . . . . . . . . . . . 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 )
7133, 32, 69, 70syl3anc 1226 . . . . . . . . . . . . . . . . . . . 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 )
7261, 71syl5eq 2507 . . . . . . . . . . . . . . . . . . 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 )
7372fveq2d 5852 . . . . . . . . . . . . . . . . . 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 ) )
74 simprlr 762 . . . . . . . . . . . . . . . . . 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 )
7573, 74eqtrd 2495 . . . . . . . . . . . . . . . . 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 )
76 elmapresaunres2 30944 . . . . . . . . . . . . . . . . . . . 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 )
7732, 33, 42, 76syl3anc 1226 . . . . . . . . . . . . . . . . . . 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 )
7877fveq2d 5852 . . . . . . . . . . . . . . . . . 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 ) )
79 simprrr 764 . . . . . . . . . . . . . . . . . 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 )
8078, 79eqtrd 2495 . . . . . . . . . . . . . . . . 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 )
8159, 75, 80jca32 533 . . . . . . . . . . . . . . . 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 ) ) )
82 reseq1 5256 . . . . . . . . . . . . . . . . . . 19  |-  ( f  =  ( d  u.  e )  ->  (
f  |`  ( 1 ... N ) )  =  ( ( d  u.  e )  |`  (
1 ... N ) ) )
8382eqeq2d 2468 . . . . . . . . . . . . . . . . . 18  |-  ( f  =  ( d  u.  e )  ->  (
c  =  ( f  |`  ( 1 ... N
) )  <->  c  =  ( ( d  u.  e )  |`  (
1 ... N ) ) ) )
84 reseq1 5256 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f  =  ( d  u.  e )  ->  (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  =  ( ( d  u.  e
)  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) )
8584fveq2d 5852 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  =  ( d  u.  e )  ->  (
a `  ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) )  =  ( a `  ( ( d  u.  e )  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) ) )
8685eqeq1d 2456 . . . . . . . . . . . . . . . . . . 19  |-  ( f  =  ( d  u.  e )  ->  (
( a `  (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) )  =  0  <->  ( a `  ( ( d  u.  e )  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )  =  0 ) )
87 reseq1 5256 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f  =  ( d  u.  e )  ->  (
f  |`  NN )  =  ( ( d  u.  e )  |`  NN ) )
8887fveq2d 5852 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  =  ( d  u.  e )  ->  (
b `  ( f  |`  NN ) )  =  ( b `  (
( d  u.  e
)  |`  NN ) ) )
8988eqeq1d 2456 . . . . . . . . . . . . . . . . . . 19  |-  ( f  =  ( d  u.  e )  ->  (
( b `  (
f  |`  NN ) )  =  0  <->  ( b `  ( ( d  u.  e )  |`  NN ) )  =  0 ) )
9086, 89anbi12d 708 . . . . . . . . . . . . . . . . . 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 ) ) )
9183, 90anbi12d 708 . . . . . . . . . . . . . . . . 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 ) ) ) )
9291rspcev 3207 . . . . . . . . . . . . . . . 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 ) ) )
9354, 81, 92syl2anc 659 . . . . . . . . . . . . . . 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 ) ) )
9493ex 432 . . . . . . . . . . . . . 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 ) ) ) )
9594rexlimdvva 2953 . . . . . . . . . . . . 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 ) ) ) )
96 simpr 459 . . . . . . . . . . . . . . . . . 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 ) )
97 difss 3617 . . . . . . . . . . . . . . . . . 18  |-  ( ZZ 
\  ( ZZ>= `  ( N  +  1 ) ) )  C_  ZZ
98 elmapssres 7436 . . . . . . . . . . . . . . . . . 18  |-  ( ( f  e.  ( NN0 
^m  ZZ )  /\  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) 
C_  ZZ )  -> 
( f  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  e.  ( NN0  ^m  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )
9996, 97, 98sylancl 660 . . . . . . . . . . . . . . . . 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 ) ) ) ) )
10099adantr 463 . . . . . . . . . . . . . . . 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 ) ) ) ) )
101 nnssz 10880 . . . . . . . . . . . . . . . . . 18  |-  NN  C_  ZZ
102 elmapssres 7436 . . . . . . . . . . . . . . . . . 18  |-  ( ( f  e.  ( NN0 
^m  ZZ )  /\  NN  C_  ZZ )  -> 
( f  |`  NN )  e.  ( NN0  ^m  NN ) )
10396, 101, 102sylancl 660 . . . . . . . . . . . . . . . . 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 ) )
104103adantr 463 . . . . . . . . . . . . . . . 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 ) )
105 simprl 754 . . . . . . . . . . . . . . . . . . 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
) ) )
10614ad3antrrr 727 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
107106resabs1d 5291 . . . . . . . . . . . . . . . . . . 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
) ) )
108105, 107eqtr4d 2498 . . . . . . . . . . . . . . . . . 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 ) ) )
109 simprrl 763 . . . . . . . . . . . . . . . . . 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 )
110108, 109jca 530 . . . . . . . . . . . . . . . . 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 ) )
111 resabs1 5290 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1 ... N ) 
C_  NN  ->  ( ( f  |`  NN )  |`  ( 1 ... N
) )  =  ( f  |`  ( 1 ... N ) ) )
11224, 111mp1i 12 . . . . . . . . . . . . . . . . . 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
) ) )
113105, 112eqtr4d 2498 . . . . . . . . . . . . . . . . 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
) ) )
114 simprrr 764 . . . . . . . . . . . . . . . . 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 )
115110, 113, 114jca32 533 . . . . . . . . . . . . . . . 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 ) ) )
116 reseq1 5256 . . . . . . . . . . . . . . . . . . . 20  |-  ( d  =  ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  ->  ( d  |`  ( 1 ... N
) )  =  ( ( f  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  |`  ( 1 ... N
) ) )
117116eqeq2d 2468 . . . . . . . . . . . . . . . . . . 19  |-  ( d  =  ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  ->  ( c  =  ( d  |`  ( 1 ... N
) )  <->  c  =  ( ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  |`  ( 1 ... N ) ) ) )
118 fveq2 5848 . . . . . . . . . . . . . . . . . . . 20  |-  ( d  =  ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  ->  ( a `  d )  =  ( a `  ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) ) )
119118eqeq1d 2456 . . . . . . . . . . . . . . . . . . 19  |-  ( d  =  ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  ->  ( (
a `  d )  =  0  <->  ( a `  ( f  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )  =  0 ) )
120117, 119anbi12d 708 . . . . . . . . . . . . . . . . . 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 ) ) )
121120anbi1d 702 . . . . . . . . . . . . . . . . 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 ) ) ) )
122 reseq1 5256 . . . . . . . . . . . . . . . . . . . 20  |-  ( e  =  ( f  |`  NN )  ->  ( e  |`  ( 1 ... N
) )  =  ( ( f  |`  NN )  |`  ( 1 ... N
) ) )
123122eqeq2d 2468 . . . . . . . . . . . . . . . . . . 19  |-  ( e  =  ( f  |`  NN )  ->  ( c  =  ( e  |`  ( 1 ... N
) )  <->  c  =  ( ( f  |`  NN )  |`  ( 1 ... N ) ) ) )
124 fveq2 5848 . . . . . . . . . . . . . . . . . . . 20  |-  ( e  =  ( f  |`  NN )  ->  ( b `
 e )  =  ( b `  (
f  |`  NN ) ) )
125124eqeq1d 2456 . . . . . . . . . . . . . . . . . . 19  |-  ( e  =  ( f  |`  NN )  ->  ( ( b `  e )  =  0  <->  ( b `  ( f  |`  NN ) )  =  0 ) )
126123, 125anbi12d 708 . . . . . . . . . . . . . . . . . 18  |-  ( e  =  ( f  |`  NN )  ->  ( ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 )  <->  ( c  =  ( ( f  |`  NN )  |`  (
1 ... N ) )  /\  ( b `  ( f  |`  NN ) )  =  0 ) ) )
127126anbi2d 701 . . . . . . . . . . . . . . . . 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 ) ) ) )
128121, 127rspc2ev 3218 . . . . . . . . . . . . . . . 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 ) ) )
129100, 104, 115, 128syl3anc 1226 . . . . . . . . . . . . . . 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 ) ) )
130129ex 432 . . . . . . . . . . . . . 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 ) ) ) )
131130rexlimdva 2946 . . . . . . . . . . . . 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 ) ) ) )
13295, 131impbid 191 . . . . . . . . . . . 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 ) ) ) )
133 simplrl 759 . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
134 mzpf 30908 . . . . . . . . . . . . . . . . . . 19  |-  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  -> 
a : ( ZZ 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) --> ZZ )
135133, 134syl 16 . . . . . . . . . . . . . . . . . 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 )
136 nn0ssz 10881 . . . . . . . . . . . . . . . . . . . . . 22  |-  NN0  C_  ZZ
137 mapss 7454 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ZZ  e.  _V  /\  NN0  C_  ZZ )  ->  ( NN0  ^m  ZZ )  C_  ( ZZ  ^m  ZZ ) )
1383, 136, 137mp2an 670 . . . . . . . . . . . . . . . . . . . . 21  |-  ( NN0 
^m  ZZ )  C_  ( ZZ  ^m  ZZ )
139138sseli 3485 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  e.  ( NN0  ^m  ZZ )  ->  f  e.  ( ZZ  ^m  ZZ ) )
140 elmapssres 7436 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( f  e.  ( ZZ 
^m  ZZ )  /\  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) 
C_  ZZ )  -> 
( f  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  e.  ( ZZ  ^m  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )
141139, 97, 140sylancl 660 . . . . . . . . . . . . . . . . . . 19  |-  ( f  e.  ( NN0  ^m  ZZ )  ->  ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  e.  ( ZZ 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) )
142141adantl 464 . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
143135, 142ffvelrnd 6008 . . . . . . . . . . . . . . . . 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 )
144143zred 10965 . . . . . . . . . . . . . . . 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 )
145 simplrr 760 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  f  e.  ( NN0  ^m  ZZ ) )  ->  b  e.  (mzPoly `  NN )
)
146 mzpf 30908 . . . . . . . . . . . . . . . . . . 19  |-  ( b  e.  (mzPoly `  NN )  ->  b : ( ZZ  ^m  NN ) --> ZZ )
147145, 146syl 16 . . . . . . . . . . . . . . . . . 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 )
148 elmapssres 7436 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( f  e.  ( ZZ 
^m  ZZ )  /\  NN  C_  ZZ )  -> 
( f  |`  NN )  e.  ( ZZ  ^m  NN ) )
149139, 101, 148sylancl 660 . . . . . . . . . . . . . . . . . . 19  |-  ( f  e.  ( NN0  ^m  ZZ )  ->  ( f  |`  NN )  e.  ( ZZ  ^m  NN ) )
150149adantl 464 . . . . . . . . . . . . . . . . . 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 ) )
151147, 150ffvelrnd 6008 . . . . . . . . . . . . . . . . 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 )
152151zred 10965 . . . . . . . . . . . . . . . 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 )
153 sumsqeq0 12228 . . . . . . . . . . . . . . . 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 ) )
154144, 152, 153syl2anc 659 . . . . . . . . . . . . . . 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 ) )
155139adantl 464 . . . . . . . . . . . . . . . . 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 ) )
156 reseq1 5256 . . . . . . . . . . . . . . . . . . . . 21  |-  ( g  =  f  ->  (
g  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  =  ( f  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )
157156fveq2d 5852 . . . . . . . . . . . . . . . . . . . 20  |-  ( g  =  f  ->  (
a `  ( g  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) )  =  ( a `  ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) ) )
158157oveq1d 6285 . . . . . . . . . . . . . . . . . . 19  |-  ( g  =  f  ->  (
( a `  (
g  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) ) ^
2 )  =  ( ( a `  (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) ) ^
2 ) )
159 reseq1 5256 . . . . . . . . . . . . . . . . . . . . 21  |-  ( g  =  f  ->  (
g  |`  NN )  =  ( f  |`  NN ) )
160159fveq2d 5852 . . . . . . . . . . . . . . . . . . . 20  |-  ( g  =  f  ->  (
b `  ( g  |`  NN ) )  =  ( b `  (
f  |`  NN ) ) )
161160oveq1d 6285 . . . . . . . . . . . . . . . . . . 19  |-  ( g  =  f  ->  (
( b `  (
g  |`  NN ) ) ^ 2 )  =  ( ( b `  ( f  |`  NN ) ) ^ 2 ) )
162158, 161oveq12d 6288 . . . . . . . . . . . . . . . . . 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 ) ) )
163 eqid 2454 . . . . . . . . . . . . . . . . . 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 ) ) )
164 ovex 6298 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( a `  (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) ) ^
2 )  +  ( ( b `  (
f  |`  NN ) ) ^ 2 ) )  e.  _V
165162, 163, 164fvmpt 5931 . . . . . . . . . . . . . . . . 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 ) ) )
166155, 165syl 16 . . . . . . . . . . . . . . . 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 ) ) )
167166eqeq1d 2456 . . . . . . . . . . . . . . 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 ) )
168154, 167bitr4d 256 . . . . . . . . . . . . . 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 ) )
169168anbi2d 701 . . . . . . . . . . . . 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 ) ) )
170169rexbidva 2962 . . . . . . . . . . . 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 ) ) )
171132, 170bitrd 253 . . . . . . . . . . 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 ) ) )
17231, 171syl5bbr 259 . . . . . . . . . 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 ) ) )
173172abbidv 2590 . . . . . . . . 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 ) } )
17430, 173syl5eq 2507 . . . . . . . 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 ) } )
175 simpl 455 . . . . . . . . 9  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  N  e.  NN0 )
176 fzssuz 11728 . . . . . . . . . . . 12  |-  ( 1 ... N )  C_  ( ZZ>= `  1 )
177 uzssz 11101 . . . . . . . . . . . 12  |-  ( ZZ>= ` 
1 )  C_  ZZ
178176, 177sstri 3498 . . . . . . . . . . 11  |-  ( 1 ... N )  C_  ZZ
1793, 178pm3.2i 453 . . . . . . . . . 10  |-  ( ZZ  e.  _V  /\  (
1 ... N )  C_  ZZ )
180179a1i 11 . . . . . . . . 9  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  ( ZZ  e.  _V  /\  (
1 ... N )  C_  ZZ ) )
1813a1i 11 . . . . . . . . . . . 12  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  ZZ  e.  _V )
18297a1i 11 . . . . . . . . . . . 12  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) )  C_  ZZ )
183 simprl 754 . . . . . . . . . . . 12  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )
184 mzpresrename 30922 . . . . . . . . . . . 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 ) )
185181, 182, 183, 184syl3anc 1226 . . . . . . . . . . 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 )
)
186 2nn0 10808 . . . . . . . . . . 11  |-  2  e.  NN0
187 mzpexpmpt 30917 . . . . . . . . . . 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 ) )
188185, 186, 187sylancl 660 . . . . . . . . . 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 )
)
189101a1i 11 . . . . . . . . . . . 12  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  NN  C_  ZZ )
190 simprr 755 . . . . . . . . . . . 12  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  b  e.  (mzPoly `  NN )
)
191 mzpresrename 30922 . . . . . . . . . . . 12  |-  ( ( ZZ  e.  _V  /\  NN  C_  ZZ  /\  b  e.  (mzPoly `  NN )
)  ->  ( g  e.  ( ZZ  ^m  ZZ )  |->  ( b `  ( g  |`  NN ) ) )  e.  (mzPoly `  ZZ ) )
192181, 189, 190, 191syl3anc 1226 . . . . . . . . . . 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 ) )
193 mzpexpmpt 30917 . . . . . . . . . . 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 ) )
194192, 186, 193sylancl 660 . . . . . . . . . 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 ) )
195 mzpaddmpt 30913 . . . . . . . . . 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 ) )
196188, 194, 195syl2anc 659 . . . . . . . . 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 ) )
197 eldioph2 30934 . . . . . . . . 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
) )
198175, 180, 196, 197syl3anc 1226 . . . . . . . 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
) )
199174, 198eqeltrd 2542 . . . . . . 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 )
)
200 ineq12 3681 . . . . . . . 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 ) } ) )
201200eleq1d 2523 . . . . . . 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 )
) )
202199, 201syl5ibrcom 222 . . . . . 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 ) ) )
203202rexlimdvva 2953 . . . . 5  |-  ( N  e.  NN0  ->  ( 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 ) } )  -> 
( A  i^i  B
)  e.  (Dioph `  N ) ) )
20429, 203syl5bir 218 . . . 4  |-  ( N  e.  NN0  ->  ( ( 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 ) } )  -> 
( A  i^i  B
)  e.  (Dioph `  N ) ) )
20528, 204sylbid 215 . . 3  |-  ( N  e.  NN0  ->