Metamath Proof Explorer

Theorem diophin

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)

Ref Expression
Assertion diophin 
|- ( ( A e. ( Dioph ` N ) /\ B e. ( Dioph ` N ) ) -> ( A i^i B ) e. ( Dioph ` N ) )

Proof

Step Hyp Ref Expression
1 eldiophelnn0 
 |-  ( A e. ( Dioph ` N ) -> N e. NN0 )
2 id 
 |-  ( N e. NN0 -> N e. NN0 )
3 zex 
 |-  ZZ e. _V
4 difexg 
 |-  ( ZZ e. _V -> ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) e. _V )
5 3 4 mp1i 
 |-  ( N e. NN0 -> ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) e. _V )
6 ominf 
 |-  -. _om e. Fin
7 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
8 lzenom 
 |-  ( N e. ZZ -> ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ~~ _om )
9 enfi 
 |-  ( ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ~~ _om -> ( ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) e. Fin <-> _om e. Fin ) )
10 7 8 9 3syl 
 |-  ( N e. NN0 -> ( ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) e. Fin <-> _om e. Fin ) )
11 6 10 mtbiri 
 |-  ( N e. NN0 -> -. ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) e. Fin )
12 fz1eqin 
 |-  ( N e. NN0 -> ( 1 ... N ) = ( ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) i^i NN ) )
13 inss1 
 |-  ( ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) i^i NN ) C_ ( ZZ \ ( ZZ>= ` ( N + 1 ) ) )
14 12 13 eqsstrdi 
 |-  ( N e. NN0 -> ( 1 ... N ) C_ ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) )
15 eldioph2b 
 |-  ( ( ( 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 ) } ) )
16 2 5 11 14 15 syl22anc 
 |-  ( 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 
 |-  NN e. _V
18 17 a1i 
 |-  ( N e. NN0 -> NN e. _V )
19 1z 
 |-  1 e. ZZ
20 nnuz 
 |-  NN = ( ZZ>= ` 1 )
21 20 uzinf 
 |-  ( 1 e. ZZ -> -. NN e. Fin )
22 19 21 mp1i 
 |-  ( N e. NN0 -> -. NN e. Fin )
23 elfznn 
 |-  ( a e. ( 1 ... N ) -> a e. NN )
24 23 ssriv 
 |-  ( 1 ... N ) C_ NN
25 24 a1i 
 |-  ( N e. NN0 -> ( 1 ... N ) C_ NN )
26 eldioph2b 
 |-  ( ( ( 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 ) } ) )
27 2 18 22 25 26 syl22anc 
 |-  ( 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 ) } ) )
28 16 27 anbi12d 
 |-  ( 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 
 |-  ( 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 
 |-  ( { 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 
 |-  ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 ) )
34 12 eqcomd 
 |-  ( N e. NN0 -> ( ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) i^i NN ) = ( 1 ... N ) )
35 34 reseq2d 
 |-  ( N e. NN0 -> ( d |` ( ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) i^i NN ) ) = ( d |` ( 1 ... N ) ) )
36 35 ad3antrrr 
 |-  ( ( ( ( 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 ) ) )
37 34 reseq2d 
 |-  ( N e. NN0 -> ( e |` ( ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) i^i NN ) ) = ( e |` ( 1 ... N ) ) )
38 37 ad3antrrr 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 ) ) )
41 38 39 40 3eqtr2d 
 |-  ( ( ( ( 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 ) ) )
42 36 41 eqtr4d 
 |-  ( ( ( ( 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 
 |-  ( ( 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 ) ) )
44 32 33 42 43 syl3anc 
 |-  ( ( ( ( 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 ) ) )
45 20 uneq2i 
 |-  ( ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) u. NN ) = ( ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) u. ( ZZ>= ` 1 ) )
46 19 a1i 
 |-  ( N e. NN0 -> 1 e. ZZ )
47 nn0p1nn 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN )
48 47 nnge1d 
 |-  ( N e. NN0 -> 1 <_ ( N + 1 ) )
49 lzunuz 
 |-  ( ( N e. ZZ /\ 1 e. ZZ /\ 1 <_ ( N + 1 ) ) -> ( ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) u. ( ZZ>= ` 1 ) ) = ZZ )
50 7 46 48 49 syl3anc 
 |-  ( N e. NN0 -> ( ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) u. ( ZZ>= ` 1 ) ) = ZZ )
51 45 50 eqtrid 
 |-  ( N e. NN0 -> ( ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) u. NN ) = ZZ )
52 51 oveq2d 
 |-  ( N e. NN0 -> ( NN0 ^m ( ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) u. NN ) ) = ( NN0 ^m ZZ ) )
53 52 ad3antrrr 
 |-  ( ( ( ( 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 ) )
54 44 53 eleqtrd 
 |-  ( ( ( ( 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 
 |-  ( c u. c ) = c
56 40 39 uneq12d 
 |-  ( ( ( ( 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 ) ) ) )
57 55 56 eqtr3id 
 |-  ( ( ( ( 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 
 |-  ( ( d u. e ) |` ( 1 ... N ) ) = ( ( d |` ( 1 ... N ) ) u. ( e |` ( 1 ... N ) ) )
59 57 58 eqtr4di 
 |-  ( ( ( ( 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 
 |-  ( d u. e ) = ( e u. d )
61 60 reseq1i 
 |-  ( ( d u. e ) |` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) = ( ( e u. d ) |` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) )
62 incom 
 |-  ( NN i^i ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) = ( ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) i^i NN )
63 62 34 eqtrid 
 |-  ( N e. NN0 -> ( NN i^i ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) = ( 1 ... N ) )
64 63 reseq2d 
 |-  ( N e. NN0 -> ( e |` ( NN i^i ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) ) = ( e |` ( 1 ... N ) ) )
65 64 ad3antrrr 
 |-  ( ( ( ( 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 ) ) )
66 63 reseq2d 
 |-  ( N e. NN0 -> ( d |` ( NN i^i ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) ) = ( d |` ( 1 ... N ) ) )
67 66 ad3antrrr 
 |-  ( ( ( ( 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 ) ) )
68 67 40 39 3eqtr2d 
 |-  ( ( ( ( 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 ) ) )
69 65 68 eqtr4d 
 |-  ( ( ( ( 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 
 |-  ( ( 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 )
71 33 32 69 70 syl3anc 
 |-  ( ( ( ( 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 )
72 61 71 eqtrid 
 |-  ( ( ( ( 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 )
73 72 fveq2d 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 )
75 73 74 eqtrd 
 |-  ( ( ( ( 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 
 |-  ( ( 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 )
77 32 33 42 76 syl3anc 
 |-  ( ( ( ( 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 )
78 77 fveq2d 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 )
80 78 79 eqtrd 
 |-  ( ( ( ( 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 )
81 59 75 80 jca32 
 |-  ( ( ( ( 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 
 |-  ( f = ( d u. e ) -> ( f |` ( 1 ... N ) ) = ( ( d u. e ) |` ( 1 ... N ) ) )
83 82 eqeq2d 
 |-  ( f = ( d u. e ) -> ( c = ( f |` ( 1 ... N ) ) <-> c = ( ( d u. e ) |` ( 1 ... N ) ) ) )
84 reseq1 
 |-  ( f = ( d u. e ) -> ( f |` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) = ( ( d u. e ) |` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) )
85 84 fveqeq2d 
 |-  ( f = ( d u. e ) -> ( ( a ` ( f |` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) ) = 0 <-> ( a ` ( ( d u. e ) |` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) ) = 0 ) )
86 reseq1 
 |-  ( f = ( d u. e ) -> ( f |` NN ) = ( ( d u. e ) |` NN ) )
87 86 fveqeq2d 
 |-  ( f = ( d u. e ) -> ( ( b ` ( f |` NN ) ) = 0 <-> ( b ` ( ( d u. e ) |` NN ) ) = 0 ) )
88 85 87 anbi12d 
 |-  ( 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 ) ) )
89 83 88 anbi12d 
 |-  ( 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 ) ) ) )
90 89 rspcev 
 |-  ( ( ( 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 ) ) )
91 54 81 90 syl2anc 
 |-  ( ( ( ( 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 ) ) )
92 91 ex 
 |-  ( ( ( 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 ) ) ) )
93 92 rexlimdvva 
 |-  ( ( 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 ) ) ) )
94 simpr 
 |-  ( ( ( N e. NN0 /\ ( a e. ( mzPoly ` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) /\ b e. ( mzPoly ` NN ) ) ) /\ f e. ( NN0 ^m ZZ ) ) -> f e. ( NN0 ^m ZZ ) )
95 difss 
 |-  ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) C_ ZZ
96 elmapssres 
 |-  ( ( f e. ( NN0 ^m ZZ ) /\ ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) C_ ZZ ) -> ( f |` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) e. ( NN0 ^m ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) )
97 94 95 96 sylancl 
 |-  ( ( ( 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 ) ) ) ) )
98 97 adantr 
 |-  ( ( ( ( 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 ) ) ) ) )
99 nnssz 
 |-  NN C_ ZZ
100 elmapssres 
 |-  ( ( f e. ( NN0 ^m ZZ ) /\ NN C_ ZZ ) -> ( f |` NN ) e. ( NN0 ^m NN ) )
101 94 99 100 sylancl 
 |-  ( ( ( 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 ) )
102 101 adantr 
 |-  ( ( ( ( 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 ) )
103 simprl 
 |-  ( ( ( ( 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 ) ) )
104 14 ad3antrrr 
 |-  ( ( ( ( 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 ) ) ) )
105 104 resabs1d 
 |-  ( ( ( ( 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 ) ) )
106 103 105 eqtr4d 
 |-  ( ( ( ( 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 ) ) )
107 simprrl 
 |-  ( ( ( ( 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 )
108 106 107 jca 
 |-  ( ( ( ( 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 ) )
109 resabs1 
 |-  ( ( 1 ... N ) C_ NN -> ( ( f |` NN ) |` ( 1 ... N ) ) = ( f |` ( 1 ... N ) ) )
110 24 109 mp1i 
 |-  ( ( ( ( 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 ) ) )
111 103 110 eqtr4d 
 |-  ( ( ( ( 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 ) ) )
112 simprrr 
 |-  ( ( ( ( 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 )
113 108 111 112 jca32 
 |-  ( ( ( ( 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 ) ) )
114 reseq1 
 |-  ( d = ( f |` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) -> ( d |` ( 1 ... N ) ) = ( ( f |` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) |` ( 1 ... N ) ) )
115 114 eqeq2d 
 |-  ( d = ( f |` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) -> ( c = ( d |` ( 1 ... N ) ) <-> c = ( ( f |` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) |` ( 1 ... N ) ) ) )
116 fveqeq2 
 |-  ( d = ( f |` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) -> ( ( a ` d ) = 0 <-> ( a ` ( f |` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) ) = 0 ) )
117 115 116 anbi12d 
 |-  ( 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 ) ) )
118 117 anbi1d 
 |-  ( 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 ) ) ) )
119 reseq1 
 |-  ( e = ( f |` NN ) -> ( e |` ( 1 ... N ) ) = ( ( f |` NN ) |` ( 1 ... N ) ) )
120 119 eqeq2d 
 |-  ( e = ( f |` NN ) -> ( c = ( e |` ( 1 ... N ) ) <-> c = ( ( f |` NN ) |` ( 1 ... N ) ) ) )
121 fveqeq2 
 |-  ( e = ( f |` NN ) -> ( ( b ` e ) = 0 <-> ( b ` ( f |` NN ) ) = 0 ) )
122 120 121 anbi12d 
 |-  ( e = ( f |` NN ) -> ( ( c = ( e |` ( 1 ... N ) ) /\ ( b ` e ) = 0 ) <-> ( c = ( ( f |` NN ) |` ( 1 ... N ) ) /\ ( b ` ( f |` NN ) ) = 0 ) ) )
123 122 anbi2d 
 |-  ( 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 ) ) ) )
124 118 123 rspc2ev 
 |-  ( ( ( 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 ) ) )
125 98 102 113 124 syl3anc 
 |-  ( ( ( ( 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 ) ) )
126 125 rexlimdva2 
 |-  ( ( 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 ) ) ) )
127 93 126 impbid 
 |-  ( ( 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 ) ) ) )
128 simplrl 
 |-  ( ( ( 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 ) ) ) ) )
129 mzpf 
 |-  ( a e. ( mzPoly ` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) -> a : ( ZZ ^m ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) --> ZZ )
130 128 129 syl 
 |-  ( ( ( 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 )
131 nn0ssz 
 |-  NN0 C_ ZZ
132 mapss 
 |-  ( ( ZZ e. _V /\ NN0 C_ ZZ ) -> ( NN0 ^m ZZ ) C_ ( ZZ ^m ZZ ) )
133 3 131 132 mp2an 
 |-  ( NN0 ^m ZZ ) C_ ( ZZ ^m ZZ )
134 133 sseli 
 |-  ( f e. ( NN0 ^m ZZ ) -> f e. ( ZZ ^m ZZ ) )
135 elmapssres 
 |-  ( ( f e. ( ZZ ^m ZZ ) /\ ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) C_ ZZ ) -> ( f |` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) e. ( ZZ ^m ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) )
136 134 95 135 sylancl 
 |-  ( f e. ( NN0 ^m ZZ ) -> ( f |` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) e. ( ZZ ^m ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) )
137 136 adantl 
 |-  ( ( ( 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 ) ) ) ) )
138 130 137 ffvelcdmd 
 |-  ( ( ( 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 )
139 138 zred 
 |-  ( ( ( 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 )
140 simplrr 
 |-  ( ( ( N e. NN0 /\ ( a e. ( mzPoly ` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) /\ b e. ( mzPoly ` NN ) ) ) /\ f e. ( NN0 ^m ZZ ) ) -> b e. ( mzPoly ` NN ) )
141 mzpf 
 |-  ( b e. ( mzPoly ` NN ) -> b : ( ZZ ^m NN ) --> ZZ )
142 140 141 syl 
 |-  ( ( ( N e. NN0 /\ ( a e. ( mzPoly ` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) /\ b e. ( mzPoly ` NN ) ) ) /\ f e. ( NN0 ^m ZZ ) ) -> b : ( ZZ ^m NN ) --> ZZ )
143 elmapssres 
 |-  ( ( f e. ( ZZ ^m ZZ ) /\ NN C_ ZZ ) -> ( f |` NN ) e. ( ZZ ^m NN ) )
144 134 99 143 sylancl 
 |-  ( f e. ( NN0 ^m ZZ ) -> ( f |` NN ) e. ( ZZ ^m NN ) )
145 144 adantl 
 |-  ( ( ( 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 ) )
146 142 145 ffvelcdmd 
 |-  ( ( ( N e. NN0 /\ ( a e. ( mzPoly ` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) /\ b e. ( mzPoly ` NN ) ) ) /\ f e. ( NN0 ^m ZZ ) ) -> ( b ` ( f |` NN ) ) e. ZZ )
147 146 zred 
 |-  ( ( ( N e. NN0 /\ ( a e. ( mzPoly ` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) /\ b e. ( mzPoly ` NN ) ) ) /\ f e. ( NN0 ^m ZZ ) ) -> ( b ` ( f |` NN ) ) e. RR )
148 sumsqeq0 
 |-  ( ( ( 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 ) )
149 139 147 148 syl2anc 
 |-  ( ( ( 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 ) )
150 134 adantl 
 |-  ( ( ( N e. NN0 /\ ( a e. ( mzPoly ` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) /\ b e. ( mzPoly ` NN ) ) ) /\ f e. ( NN0 ^m ZZ ) ) -> f e. ( ZZ ^m ZZ ) )
151 reseq1 
 |-  ( g = f -> ( g |` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) = ( f |` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) )
152 151 fveq2d 
 |-  ( g = f -> ( a ` ( g |` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) ) = ( a ` ( f |` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) ) )
153 152 oveq1d 
 |-  ( g = f -> ( ( a ` ( g |` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) ) ^ 2 ) = ( ( a ` ( f |` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) ) ^ 2 ) )
154 reseq1 
 |-  ( g = f -> ( g |` NN ) = ( f |` NN ) )
155 154 fveq2d 
 |-  ( g = f -> ( b ` ( g |` NN ) ) = ( b ` ( f |` NN ) ) )
156 155 oveq1d 
 |-  ( g = f -> ( ( b ` ( g |` NN ) ) ^ 2 ) = ( ( b ` ( f |` NN ) ) ^ 2 ) )
157 153 156 oveq12d 
 |-  ( g = f -> ( ( ( a ` ( g |` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) ) ^ 2 ) + ( ( b ` ( g |` NN ) ) ^ 2 ) ) = ( ( ( a ` ( f |` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) ) ^ 2 ) + ( ( b ` ( f |` NN ) ) ^ 2 ) ) )
158 eqid 
 |-  ( 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 ) ) )
159 ovex 
 |-  ( ( ( a ` ( f |` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) ) ^ 2 ) + ( ( b ` ( f |` NN ) ) ^ 2 ) ) e. _V
160 157 158 159 fvmpt 
 |-  ( 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 ) ) )
161 150 160 syl 
 |-  ( ( ( 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 ) ) )
162 161 eqeq1d 
 |-  ( ( ( 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 ) )
163 149 162 bitr4d 
 |-  ( ( ( 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 ) )
164 163 anbi2d 
 |-  ( ( ( 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 ) ) )
165 164 rexbidva 
 |-  ( ( 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 ) ) )
166 127 165 bitrd 
 |-  ( ( 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 ) ) )
167 31 166 bitr3id 
 |-  ( ( 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 ) ) )
168 167 abbidv 
 |-  ( ( 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 ) } )
169 30 168 eqtrid 
 |-  ( ( 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 ) } )
170 simpl 
 |-  ( ( N e. NN0 /\ ( a e. ( mzPoly ` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) /\ b e. ( mzPoly ` NN ) ) ) -> N e. NN0 )
171 fzssuz 
 |-  ( 1 ... N ) C_ ( ZZ>= ` 1 )
172 uzssz 
 |-  ( ZZ>= ` 1 ) C_ ZZ
173 171 172 sstri 
 |-  ( 1 ... N ) C_ ZZ
174 3 173 pm3.2i 
 |-  ( ZZ e. _V /\ ( 1 ... N ) C_ ZZ )
175 174 a1i 
 |-  ( ( N e. NN0 /\ ( a e. ( mzPoly ` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) /\ b e. ( mzPoly ` NN ) ) ) -> ( ZZ e. _V /\ ( 1 ... N ) C_ ZZ ) )
176 3 a1i 
 |-  ( ( N e. NN0 /\ ( a e. ( mzPoly ` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) /\ b e. ( mzPoly ` NN ) ) ) -> ZZ e. _V )
177 95 a1i 
 |-  ( ( N e. NN0 /\ ( a e. ( mzPoly ` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) /\ b e. ( mzPoly ` NN ) ) ) -> ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) C_ ZZ )
178 simprl 
 |-  ( ( N e. NN0 /\ ( a e. ( mzPoly ` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) /\ b e. ( mzPoly ` NN ) ) ) -> a e. ( mzPoly ` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) )
179 mzpresrename 
 |-  ( ( 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 ) )
180 176 177 178 179 syl3anc 
 |-  ( ( 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 ) )
181 2nn0 
 |-  2 e. NN0
182 mzpexpmpt 
 |-  ( ( ( 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 ) )
183 180 181 182 sylancl 
 |-  ( ( 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 ) )
184 99 a1i 
 |-  ( ( N e. NN0 /\ ( a e. ( mzPoly ` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) /\ b e. ( mzPoly ` NN ) ) ) -> NN C_ ZZ )
185 simprr 
 |-  ( ( N e. NN0 /\ ( a e. ( mzPoly ` ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ) /\ b e. ( mzPoly ` NN ) ) ) -> b e. ( mzPoly ` NN ) )
186 mzpresrename 
 |-  ( ( ZZ e. _V /\ NN C_ ZZ /\ b e. ( mzPoly ` NN ) ) -> ( g e. ( ZZ ^m ZZ ) |-> ( b ` ( g |` NN ) ) ) e. ( mzPoly ` ZZ ) )
187 176 184 185 186 syl3anc 
 |-  ( ( 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 ) )
188 mzpexpmpt 
 |-  ( ( ( 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 ) )
189 187 181 188 sylancl 
 |-  ( ( 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 ) )
190 mzpaddmpt 
 |-  ( ( ( 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 ) )
191 183 189 190 syl2anc 
 |-  ( ( 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 ) )
192 eldioph2 
 |-  ( ( 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 ) )
193 170 175 191 192 syl3anc 
 |-  ( ( 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 ) )
194 169 193 eqeltrd 
 |-  ( ( 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 ) )
195 ineq12 
 |-  ( ( 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 ) } ) )
196 195 eleq1d 
 |-  ( ( 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 ) ) )
197 194 196 syl5ibrcom 
 |-  ( ( 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 ) ) )
198 197 rexlimdvva 
 |-  ( 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 ) ) )
199 29 198 biimtrrid 
 |-  ( 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 ) ) )
200 28 199 sylbid 
 |-  ( N e. NN0 -> ( ( A e. ( Dioph ` N ) /\ B e. ( Dioph ` N ) ) -> ( A i^i B ) e. ( Dioph ` N ) ) )
201 1 200 syl 
 |-  ( A e. ( Dioph ` N ) -> ( ( A e. ( Dioph ` N ) /\ B e. ( Dioph ` N ) ) -> ( A i^i B ) e. ( Dioph ` N ) ) )
202 201 anabsi5 
 |-  ( ( A e. ( Dioph ` N ) /\ B e. ( Dioph ` N ) ) -> ( A i^i B ) e. ( Dioph ` N ) )