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
|
syl5eq |
|- ( 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
|
syl5eq |
|- ( 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
|
syl5eq |
|- ( ( ( ( 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
|
ffvelrnd |
|- ( ( ( 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
|
ffvelrnd |
|- ( ( ( 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
|
syl5eq |
|- ( ( 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
|
syl5bir |
|- ( 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 ) ) |