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

Theorem diophin 26763
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 26754 . . 3  |-  ( A  e.  (Dioph `  N
)  ->  N  e.  NN0 )
2 id 20 . . . . . 6  |-  ( N  e.  NN0  ->  N  e. 
NN0 )
3 zex 10275 . . . . . . 7  |-  ZZ  e.  _V
4 difexg 4338 . . . . . . 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 7307 . . . . . . 7  |-  -.  om  e.  Fin
7 nn0z 10288 . . . . . . . 8  |-  ( N  e.  NN0  ->  N  e.  ZZ )
8 lzenom 26760 . . . . . . . 8  |-  ( N  e.  ZZ  ->  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) )  ~~  om )
9 enfi 7311 . . . . . . . 8  |-  ( ( ZZ  \  ( ZZ>= `  ( N  +  1
) ) )  ~~  om 
->  ( ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) )  e.  Fin  <->  om  e.  Fin ) )
107, 8, 93syl 19 . . . . . . 7  |-  ( N  e.  NN0  ->  ( ( ZZ  \  ( ZZ>= `  ( N  +  1
) ) )  e. 
Fin 
<->  om  e.  Fin )
)
116, 10mtbiri 295 . . . . . 6  |-  ( N  e.  NN0  ->  -.  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) )  e.  Fin )
12 fz1eqin 26759 . . . . . . 7  |-  ( N  e.  NN0  ->  ( 1 ... N )  =  ( ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) )  i^i  NN ) )
13 inss1 3548 . . . . . . 7  |-  ( ( ZZ  \  ( ZZ>= `  ( N  +  1
) ) )  i^i 
NN )  C_  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) )
1412, 13syl6eqss 3385 . . . . . 6  |-  ( N  e.  NN0  ->  ( 1 ... N )  C_  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )
15 eldioph2b 26753 . . . . . 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 1185 . . . . 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 9990 . . . . . . 7  |-  NN  e.  _V
1817a1i 11 . . . . . 6  |-  ( N  e.  NN0  ->  NN  e.  _V )
19 1z 10295 . . . . . . 7  |-  1  e.  ZZ
20 nnuz 10505 . . . . . . . 8  |-  NN  =  ( ZZ>= `  1 )
2120uzinf 11288 . . . . . . 7  |-  ( 1  e.  ZZ  ->  -.  NN  e.  Fin )
2219, 21mp1i 12 . . . . . 6  |-  ( N  e.  NN0  ->  -.  NN  e.  Fin )
23 elfznn 11064 . . . . . . . 8  |-  ( a  e.  ( 1 ... N )  ->  a  e.  NN )
2423ssriv 3339 . . . . . . 7  |-  ( 1 ... N )  C_  NN
2524a1i 11 . . . . . 6  |-  ( N  e.  NN0  ->  ( 1 ... N )  C_  NN )
26 eldioph2b 26753 . . . . . 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 1185 . . . . 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 692 . . . 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 2862 . . . . 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 3596 . . . . . . . . 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 2862 . . . . . . . . . . 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 737 . . . . . . . . . . . . . . . . . 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 738 . . . . . . . . . . . . . . . . . 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 2435 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  NN0  ->  ( ( ZZ  \  ( ZZ>= `  ( N  +  1
) ) )  i^i 
NN )  =  ( 1 ... N ) )
3534reseq2d 5132 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  NN0  ->  ( d  |`  ( ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) )  i^i  NN ) )  =  ( d  |`  ( 1 ... N
) ) )
3635ad3antrrr 711 . . . . . . . . . . . . . . . . . . 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 5132 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  NN0  ->  ( e  |`  ( ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) )  i^i  NN ) )  =  ( e  |`  ( 1 ... N
) ) )
3837ad3antrrr 711 . . . . . . . . . . . . . . . . . . . 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 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  =  ( e  |`  (
1 ... N ) ) )
40 simprll 739 . . . . . . . . . . . . . . . . . . . 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 2468 . . . . . . . . . . . . . . . . . . 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 2465 . . . . . . . . . . . . . . . . . 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 26761 . . . . . . . . . . . . . . . . . 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 1184 . . . . . . . . . . . . . . . . 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 3485 . . . . . . . . . . . . . . . . . . . 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 10243 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( N  e.  NN0  ->  ( N  +  1 )  e.  NN )
4847nnge1d 10026 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  NN0  ->  1  <_ 
( N  +  1 ) )
49 lzunuz 26758 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( N  e.  ZZ  /\  1  e.  ZZ  /\  1  <_  ( N  +  1 ) )  ->  (
( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) )  u.  ( ZZ>= `  1
) )  =  ZZ )
507, 46, 48, 49syl3anc 1184 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  NN0  ->  ( ( ZZ  \  ( ZZ>= `  ( N  +  1
) ) )  u.  ( ZZ>= `  1 )
)  =  ZZ )
5145, 50syl5eq 2474 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  NN0  ->  ( ( ZZ  \  ( ZZ>= `  ( N  +  1
) ) )  u.  NN )  =  ZZ )
5251oveq2d 6083 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  NN0  ->  ( NN0 
^m  ( ( ZZ 
\  ( ZZ>= `  ( N  +  1 ) ) )  u.  NN ) )  =  ( NN0  ^m  ZZ ) )
5352ad3antrrr 711 . . . . . . . . . . . . . . . . 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 2506 . . . . . . . . . . . . . . . 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 3477 . . . . . . . . . . . . . . . . . . 19  |-  ( c  u.  c )  =  c
5640, 39uneq12d 3489 . . . . . . . . . . . . . . . . . . 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 2476 . . . . . . . . . . . . . . . . . 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 5147 . . . . . . . . . . . . . . . . . 18  |-  ( ( d  u.  e )  |`  ( 1 ... N
) )  =  ( ( d  |`  (
1 ... N ) )  u.  ( e  |`  ( 1 ... N
) ) )
5957, 58syl6eqr 2480 . . . . . . . . . . . . . . . . 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 3478 . . . . . . . . . . . . . . . . . . . . 21  |-  ( d  u.  e )  =  ( e  u.  d
)
6160reseq1i 5128 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( d  u.  e )  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  =  ( ( e  u.  d )  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )
62 incom 3520 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( NN 
i^i  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  =  ( ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) )  i^i  NN )
6362, 34syl5eq 2474 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( N  e.  NN0  ->  ( NN 
i^i  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  =  ( 1 ... N ) )
6463reseq2d 5132 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  NN0  ->  ( e  |`  ( NN  i^i  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )  =  ( e  |`  ( 1 ... N
) ) )
6564ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . 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 5132 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( N  e.  NN0  ->  ( d  |`  ( NN  i^i  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )  =  ( d  |`  ( 1 ... N
) ) )
6766ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . . 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 2468 . . . . . . . . . . . . . . . . . . . . . 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 2465 . . . . . . . . . . . . . . . . . . . . 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 26762 . . . . . . . . . . . . . . . . . . . . 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 1184 . . . . . . . . . . . . . . . . . . . 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 2474 . . . . . . . . . . . . . . . . . . 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 5718 . . . . . . . . . . . . . . . . . 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 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 ) ) )  ->  ( a `  d )  =  0 )
7573, 74eqtrd 2462 . . . . . . . . . . . . . . . . 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 26762 . . . . . . . . . . . . . . . . . . . 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 1184 . . . . . . . . . . . . . . . . . . 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 5718 . . . . . . . . . . . . . . . . . 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 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 ) ) )  ->  ( b `  e )  =  0 )
8078, 79eqtrd 2462 . . . . . . . . . . . . . . . . 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 522 . . . . . . . . . . . . . . . 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 5126 . . . . . . . . . . . . . . . . . . 19  |-  ( f  =  ( d  u.  e )  ->  (
f  |`  ( 1 ... N ) )  =  ( ( d  u.  e )  |`  (
1 ... N ) ) )
8382eqeq2d 2441 . . . . . . . . . . . . . . . . . 18  |-  ( f  =  ( d  u.  e )  ->  (
c  =  ( f  |`  ( 1 ... N
) )  <->  c  =  ( ( d  u.  e )  |`  (
1 ... N ) ) ) )
84 reseq1 5126 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f  =  ( d  u.  e )  ->  (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  =  ( ( d  u.  e
)  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) )
8584fveq2d 5718 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  =  ( d  u.  e )  ->  (
a `  ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) )  =  ( a `  ( ( d  u.  e )  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) ) )
8685eqeq1d 2438 . . . . . . . . . . . . . . . . . . 19  |-  ( f  =  ( d  u.  e )  ->  (
( a `  (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) )  =  0  <->  ( a `  ( ( d  u.  e )  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )  =  0 ) )
87 reseq1 5126 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f  =  ( d  u.  e )  ->  (
f  |`  NN )  =  ( ( d  u.  e )  |`  NN ) )
8887fveq2d 5718 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  =  ( d  u.  e )  ->  (
b `  ( f  |`  NN ) )  =  ( b `  (
( d  u.  e
)  |`  NN ) ) )
8988eqeq1d 2438 . . . . . . . . . . . . . . . . . . 19  |-  ( f  =  ( d  u.  e )  ->  (
( b `  (
f  |`  NN ) )  =  0  <->  ( b `  ( ( d  u.  e )  |`  NN ) )  =  0 ) )
9086, 89anbi12d 692 . . . . . . . . . . . . . . . . . 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 692 . . . . . . . . . . . . . . . . 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 3039 . . . . . . . . . . . . . . . 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 643 . . . . . . . . . . . . . . 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 424 . . . . . . . . . . . . . 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 2824 . . . . . . . . . . . . 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 448 . . . . . . . . . . . . . . . . . 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 3461 . . . . . . . . . . . . . . . . . 18  |-  ( ZZ 
\  ( ZZ>= `  ( N  +  1 ) ) )  C_  ZZ
98 elmapssres 26703 . . . . . . . . . . . . . . . . . 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 644 . . . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . . . 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 10285 . . . . . . . . . . . . . . . . . 18  |-  NN  C_  ZZ
102 elmapssres 26703 . . . . . . . . . . . . . . . . . 18  |-  ( ( f  e.  ( NN0 
^m  ZZ )  /\  NN  C_  ZZ )  -> 
( f  |`  NN )  e.  ( NN0  ^m  NN ) )
10396, 101, 102sylancl 644 . . . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . . . . . . 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 711 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
107 resabs1 5161 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1 ... N ) 
C_  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) )  ->  ( (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  |`  (
1 ... N ) )  =  ( f  |`  ( 1 ... N
) ) )
108106, 107syl 16 . . . . . . . . . . . . . . . . . . 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
) ) )
109105, 108eqtr4d 2465 . . . . . . . . . . . . . . . . . 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 ) ) )
110 simprrl 741 . . . . . . . . . . . . . . . . . 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 )
111109, 110jca 519 . . . . . . . . . . . . . . . . 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 ) )
112 resabs1 5161 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1 ... N ) 
C_  NN  ->  ( ( f  |`  NN )  |`  ( 1 ... N
) )  =  ( f  |`  ( 1 ... N ) ) )
11324, 112mp1i 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
) ) )
114105, 113eqtr4d 2465 . . . . . . . . . . . . . . . . 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
) ) )
115 simprrr 742 . . . . . . . . . . . . . . . . 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 )
116111, 114, 115jca32 522 . . . . . . . . . . . . . . . 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 ) ) )
117 reseq1 5126 . . . . . . . . . . . . . . . . . . . 20  |-  ( d  =  ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  ->  ( d  |`  ( 1 ... N
) )  =  ( ( f  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  |`  ( 1 ... N
) ) )
118117eqeq2d 2441 . . . . . . . . . . . . . . . . . . 19  |-  ( d  =  ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  ->  ( c  =  ( d  |`  ( 1 ... N
) )  <->  c  =  ( ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  |`  ( 1 ... N ) ) ) )
119 fveq2 5714 . . . . . . . . . . . . . . . . . . . 20  |-  ( d  =  ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  ->  ( a `  d )  =  ( a `  ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) ) )
120119eqeq1d 2438 . . . . . . . . . . . . . . . . . . 19  |-  ( d  =  ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  ->  ( (
a `  d )  =  0  <->  ( a `  ( f  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )  =  0 ) )
121118, 120anbi12d 692 . . . . . . . . . . . . . . . . . 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 ) ) )
122121anbi1d 686 . . . . . . . . . . . . . . . . 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 ) ) ) )
123 reseq1 5126 . . . . . . . . . . . . . . . . . . . 20  |-  ( e  =  ( f  |`  NN )  ->  ( e  |`  ( 1 ... N
) )  =  ( ( f  |`  NN )  |`  ( 1 ... N
) ) )
124123eqeq2d 2441 . . . . . . . . . . . . . . . . . . 19  |-  ( e  =  ( f  |`  NN )  ->  ( c  =  ( e  |`  ( 1 ... N
) )  <->  c  =  ( ( f  |`  NN )  |`  ( 1 ... N ) ) ) )
125 fveq2 5714 . . . . . . . . . . . . . . . . . . . 20  |-  ( e  =  ( f  |`  NN )  ->  ( b `
 e )  =  ( b `  (
f  |`  NN ) ) )
126125eqeq1d 2438 . . . . . . . . . . . . . . . . . . 19  |-  ( e  =  ( f  |`  NN )  ->  ( ( b `  e )  =  0  <->  ( b `  ( f  |`  NN ) )  =  0 ) )
127124, 126anbi12d 692 . . . . . . . . . . . . . . . . . 18  |-  ( e  =  ( f  |`  NN )  ->  ( ( c  =  ( e  |`  ( 1 ... N
) )  /\  (
b `  e )  =  0 )  <->  ( c  =  ( ( f  |`  NN )  |`  (
1 ... N ) )  /\  ( b `  ( f  |`  NN ) )  =  0 ) ) )
128127anbi2d 685 . . . . . . . . . . . . . . . . 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 ) ) ) )
129122, 128rspc2ev 3047 . . . . . . . . . . . . . . . 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 ) ) )
130100, 104, 116, 129syl3anc 1184 . . . . . . . . . . . . . . 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 ) ) )
131130ex 424 . . . . . . . . . . . . . 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 ) ) ) )
132131rexlimdva 2817 . . . . . . . . . . . . 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 ) ) ) )
13395, 132impbid 184 . . . . . . . . . . . 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 ) ) ) )
134 simplrl 737 . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
135 mzpf 26725 . . . . . . . . . . . . . . . . . . 19  |-  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  -> 
a : ( ZZ 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) --> ZZ )
136134, 135syl 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 )
137 nn0ssz 10286 . . . . . . . . . . . . . . . . . . . . . 22  |-  NN0  C_  ZZ
138 mapss 7042 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ZZ  e.  _V  /\  NN0  C_  ZZ )  ->  ( NN0  ^m  ZZ )  C_  ( ZZ  ^m  ZZ ) )
1393, 137, 138mp2an 654 . . . . . . . . . . . . . . . . . . . . 21  |-  ( NN0 
^m  ZZ )  C_  ( ZZ  ^m  ZZ )
140139sseli 3331 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  e.  ( NN0  ^m  ZZ )  ->  f  e.  ( ZZ  ^m  ZZ ) )
141 elmapssres 26703 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( f  e.  ( ZZ 
^m  ZZ )  /\  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) 
C_  ZZ )  -> 
( f  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) )  e.  ( ZZ  ^m  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )
142140, 97, 141sylancl 644 . . . . . . . . . . . . . . . . . . 19  |-  ( f  e.  ( NN0  ^m  ZZ )  ->  ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  e.  ( ZZ 
^m  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) )
143142adantl 453 . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
144136, 143ffvelrnd 5857 . . . . . . . . . . . . . . . . 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 )
145144zred 10359 . . . . . . . . . . . . . . . 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 )
146 simplrr 738 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  /\  f  e.  ( NN0  ^m  ZZ ) )  ->  b  e.  (mzPoly `  NN )
)
147 mzpf 26725 . . . . . . . . . . . . . . . . . . 19  |-  ( b  e.  (mzPoly `  NN )  ->  b : ( ZZ  ^m  NN ) --> ZZ )
148146, 147syl 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 )
149 elmapssres 26703 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( f  e.  ( ZZ 
^m  ZZ )  /\  NN  C_  ZZ )  -> 
( f  |`  NN )  e.  ( ZZ  ^m  NN ) )
150140, 101, 149sylancl 644 . . . . . . . . . . . . . . . . . . 19  |-  ( f  e.  ( NN0  ^m  ZZ )  ->  ( f  |`  NN )  e.  ( ZZ  ^m  NN ) )
151150adantl 453 . . . . . . . . . . . . . . . . . 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 ) )
152148, 151ffvelrnd 5857 . . . . . . . . . . . . . . . . 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 )
153152zred 10359 . . . . . . . . . . . . . . . 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 )
154 sumsqeq0 11443 . . . . . . . . . . . . . . . 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 ) )
155145, 153, 154syl2anc 643 . . . . . . . . . . . . . . 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 ) )
156140adantl 453 . . . . . . . . . . . . . . . . 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 ) )
157 reseq1 5126 . . . . . . . . . . . . . . . . . . . . 21  |-  ( g  =  f  ->  (
g  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) )  =  ( f  |`  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )
158157fveq2d 5718 . . . . . . . . . . . . . . . . . . . 20  |-  ( g  =  f  ->  (
a `  ( g  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) )  =  ( a `  ( f  |`  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) ) ) )
159158oveq1d 6082 . . . . . . . . . . . . . . . . . . 19  |-  ( g  =  f  ->  (
( a `  (
g  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) ) ^
2 )  =  ( ( a `  (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) ) ^
2 ) )
160 reseq1 5126 . . . . . . . . . . . . . . . . . . . . 21  |-  ( g  =  f  ->  (
g  |`  NN )  =  ( f  |`  NN ) )
161160fveq2d 5718 . . . . . . . . . . . . . . . . . . . 20  |-  ( g  =  f  ->  (
b `  ( g  |`  NN ) )  =  ( b `  (
f  |`  NN ) ) )
162161oveq1d 6082 . . . . . . . . . . . . . . . . . . 19  |-  ( g  =  f  ->  (
( b `  (
g  |`  NN ) ) ^ 2 )  =  ( ( b `  ( f  |`  NN ) ) ^ 2 ) )
163159, 162oveq12d 6085 . . . . . . . . . . . . . . . . . 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 ) ) )
164 eqid 2430 . . . . . . . . . . . . . . . . . 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 ) ) )
165 ovex 6092 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( a `  (
f  |`  ( ZZ  \ 
( ZZ>= `  ( N  +  1 ) ) ) ) ) ^
2 )  +  ( ( b `  (
f  |`  NN ) ) ^ 2 ) )  e.  _V
166163, 164, 165fvmpt 5792 . . . . . . . . . . . . . . . . 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 ) ) )
167156, 166syl 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 ) ) )
168167eqeq1d 2438 . . . . . . . . . . . . . . 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 ) )
169155, 168bitr4d 248 . . . . . . . . . . . . . 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 ) )
170169anbi2d 685 . . . . . . . . . . . . 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 ) ) )
171170rexbidva 2709 . . . . . . . . . . . 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 ) ) )
172133, 171bitrd 245 . . . . . . . . . . 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 ) ) )
17331, 172syl5bbr 251 . . . . . . . . . 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 ) ) )
174173abbidv 2544 . . . . . . . . 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 ) } )
17530, 174syl5eq 2474 . . . . . . . 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 ) } )
176 simpl 444 . . . . . . . . 9  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  N  e.  NN0 )
177 fzssuz 11077 . . . . . . . . . . . 12  |-  ( 1 ... N )  C_  ( ZZ>= `  1 )
178 uzssz 10489 . . . . . . . . . . . 12  |-  ( ZZ>= ` 
1 )  C_  ZZ
179177, 178sstri 3344 . . . . . . . . . . 11  |-  ( 1 ... N )  C_  ZZ
1803, 179pm3.2i 442 . . . . . . . . . 10  |-  ( ZZ  e.  _V  /\  (
1 ... N )  C_  ZZ )
181180a1i 11 . . . . . . . . 9  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  ( ZZ  e.  _V  /\  (
1 ... N )  C_  ZZ ) )
1823a1i 11 . . . . . . . . . . . 12  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  ZZ  e.  _V )
18397a1i 11 . . . . . . . . . . . 12  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) )  C_  ZZ )
184 simprl 733 . . . . . . . . . . . 12  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  a  e.  (mzPoly `  ( ZZ  \  ( ZZ>= `  ( N  +  1 ) ) ) ) )
185 mzpresrename 26739 . . . . . . . . . . . 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 ) )
186182, 183, 184, 185syl3anc 1184 . . . . . . . . . . 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 )
)
187 2nn0 10222 . . . . . . . . . . 11  |-  2  e.  NN0
188 mzpexpmpt 26734 . . . . . . . . . . 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 ) )
189186, 187, 188sylancl 644 . . . . . . . . . 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 )
)
190101a1i 11 . . . . . . . . . . . 12  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  NN  C_  ZZ )
191 simprr 734 . . . . . . . . . . . 12  |-  ( ( N  e.  NN0  /\  ( a  e.  (mzPoly `  ( ZZ  \  ( ZZ>=
`  ( N  + 
1 ) ) ) )  /\  b  e.  (mzPoly `  NN )
) )  ->  b  e.  (mzPoly `  NN )
)
192 mzpresrename 26739 . . . . . . . . . . . 12  |-  ( ( ZZ  e.  _V  /\  NN  C_  ZZ  /\  b  e.  (mzPoly `  NN )
)  ->  ( g  e.  ( ZZ  ^m  ZZ )  |->  ( b `  ( g  |`  NN ) ) )  e.  (mzPoly `  ZZ ) )
193182, 190, 191, 192syl3anc 1184 . . . . . . . . . . 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 ) )
194 mzpexpmpt 26734 . . . . . . . . . . 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 ) )
195193, 187, 194sylancl 644 . . . . . . . . . 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 ) )
196 mzpaddmpt 26730 . . . . . . . . . 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 ) )
197189, 195, 196syl2anc 643 . . . . . . . . 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 ) )
198 eldioph2 26752 . . . . . . . . 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
) )
199176, 181, 197, 198syl3anc 1184 . . . . . . . 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
) )
200175, 199eqeltrd 2504 . . . . . . 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 )
)
201 ineq12 3524 . . . . . . . 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 ) } ) )
202201eleq1d 2496 . . . . . . 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 )
) )
203200, 202syl5ibrcom 214 . . . . . 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 ) ) )
204203rexlimdvva 2824 . . . . 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 ) ) )
20529, 204syl5bir 210 . . . 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