Metamath Proof Explorer

Theorem aannenlem1

Description: Lemma for aannen . (Contributed by Stefan O'Rear, 16-Nov-2014)

Ref Expression
Hypothesis aannenlem.a 
|- H = ( a e. NN0 |-> { b e. CC | E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ a /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ a ) } ( c ` b ) = 0 } )
Assertion aannenlem1 
|- ( A e. NN0 -> ( H ` A ) e. Fin )

Proof

Step Hyp Ref Expression
1 aannenlem.a 
 |-  H = ( a e. NN0 |-> { b e. CC | E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ a /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ a ) } ( c ` b ) = 0 } )
2 breq2 
 |-  ( a = A -> ( ( deg ` d ) <_ a <-> ( deg ` d ) <_ A ) )
3 breq2 
 |-  ( a = A -> ( ( abs ` ( ( coeff ` d ) ` e ) ) <_ a <-> ( abs ` ( ( coeff ` d ) ` e ) ) <_ A ) )
4 3 ralbidv 
 |-  ( a = A -> ( A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ a <-> A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A ) )
5 2 4 3anbi23d 
 |-  ( a = A -> ( ( d =/= 0p /\ ( deg ` d ) <_ a /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ a ) <-> ( d =/= 0p /\ ( deg ` d ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A ) ) )
6 5 rabbidv 
 |-  ( a = A -> { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ a /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ a ) } = { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A ) } )
7 6 rexeqdv 
 |-  ( a = A -> ( E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ a /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ a ) } ( c ` b ) = 0 <-> E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A ) } ( c ` b ) = 0 ) )
8 7 rabbidv 
 |-  ( a = A -> { b e. CC | E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ a /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ a ) } ( c ` b ) = 0 } = { b e. CC | E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A ) } ( c ` b ) = 0 } )
9 cnex 
 |-  CC e. _V
10 9 rabex 
 |-  { b e. CC | E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A ) } ( c ` b ) = 0 } e. _V
11 8 1 10 fvmpt 
 |-  ( A e. NN0 -> ( H ` A ) = { b e. CC | E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A ) } ( c ` b ) = 0 } )
12 iunrab 
 |-  U_ c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A ) } { b e. CC | ( c ` b ) = 0 } = { b e. CC | E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A ) } ( c ` b ) = 0 }
13 fzfi 
 |-  ( -u A ... A ) e. Fin
14 fzfi 
 |-  ( 0 ... A ) e. Fin
15 mapfi 
 |-  ( ( ( -u A ... A ) e. Fin /\ ( 0 ... A ) e. Fin ) -> ( ( -u A ... A ) ^m ( 0 ... A ) ) e. Fin )
16 13 14 15 mp2an 
 |-  ( ( -u A ... A ) ^m ( 0 ... A ) ) e. Fin
17 16 a1i 
 |-  ( A e. NN0 -> ( ( -u A ... A ) ^m ( 0 ... A ) ) e. Fin )
18 ovex 
 |-  ( ( -u A ... A ) ^m ( 0 ... A ) ) e. _V
19 neeq1 
 |-  ( d = a -> ( d =/= 0p <-> a =/= 0p ) )
20 fveq2 
 |-  ( d = a -> ( deg ` d ) = ( deg ` a ) )
21 20 breq1d 
 |-  ( d = a -> ( ( deg ` d ) <_ A <-> ( deg ` a ) <_ A ) )
22 fveq2 
 |-  ( d = a -> ( coeff ` d ) = ( coeff ` a ) )
23 22 fveq1d 
 |-  ( d = a -> ( ( coeff ` d ) ` e ) = ( ( coeff ` a ) ` e ) )
24 23 fveq2d 
 |-  ( d = a -> ( abs ` ( ( coeff ` d ) ` e ) ) = ( abs ` ( ( coeff ` a ) ` e ) ) )
25 24 breq1d 
 |-  ( d = a -> ( ( abs ` ( ( coeff ` d ) ` e ) ) <_ A <-> ( abs ` ( ( coeff ` a ) ` e ) ) <_ A ) )
26 25 ralbidv 
 |-  ( d = a -> ( A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A <-> A. e e. NN0 ( abs ` ( ( coeff ` a ) ` e ) ) <_ A ) )
27 19 21 26 3anbi123d 
 |-  ( d = a -> ( ( d =/= 0p /\ ( deg ` d ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A ) <-> ( a =/= 0p /\ ( deg ` a ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` a ) ` e ) ) <_ A ) ) )
28 27 elrab 
 |-  ( a e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A ) } <-> ( a e. ( Poly ` ZZ ) /\ ( a =/= 0p /\ ( deg ` a ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` a ) ` e ) ) <_ A ) ) )
29 simp3 
 |-  ( ( a =/= 0p /\ ( deg ` a ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` a ) ` e ) ) <_ A ) -> A. e e. NN0 ( abs ` ( ( coeff ` a ) ` e ) ) <_ A )
30 29 anim2i 
 |-  ( ( a e. ( Poly ` ZZ ) /\ ( a =/= 0p /\ ( deg ` a ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` a ) ` e ) ) <_ A ) ) -> ( a e. ( Poly ` ZZ ) /\ A. e e. NN0 ( abs ` ( ( coeff ` a ) ` e ) ) <_ A ) )
31 28 30 sylbi 
 |-  ( a e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A ) } -> ( a e. ( Poly ` ZZ ) /\ A. e e. NN0 ( abs ` ( ( coeff ` a ) ` e ) ) <_ A ) )
32 0z 
 |-  0 e. ZZ
33 eqid 
 |-  ( coeff ` a ) = ( coeff ` a )
34 33 coef2 
 |-  ( ( a e. ( Poly ` ZZ ) /\ 0 e. ZZ ) -> ( coeff ` a ) : NN0 --> ZZ )
35 32 34 mpan2 
 |-  ( a e. ( Poly ` ZZ ) -> ( coeff ` a ) : NN0 --> ZZ )
36 35 ad2antrl 
 |-  ( ( A e. NN0 /\ ( a e. ( Poly ` ZZ ) /\ A. e e. NN0 ( abs ` ( ( coeff ` a ) ` e ) ) <_ A ) ) -> ( coeff ` a ) : NN0 --> ZZ )
37 36 ffnd 
 |-  ( ( A e. NN0 /\ ( a e. ( Poly ` ZZ ) /\ A. e e. NN0 ( abs ` ( ( coeff ` a ) ` e ) ) <_ A ) ) -> ( coeff ` a ) Fn NN0 )
38 35 adantl 
 |-  ( ( A e. NN0 /\ a e. ( Poly ` ZZ ) ) -> ( coeff ` a ) : NN0 --> ZZ )
39 38 ffvelcdmda 
 |-  ( ( ( A e. NN0 /\ a e. ( Poly ` ZZ ) ) /\ e e. NN0 ) -> ( ( coeff ` a ) ` e ) e. ZZ )
40 39 zred 
 |-  ( ( ( A e. NN0 /\ a e. ( Poly ` ZZ ) ) /\ e e. NN0 ) -> ( ( coeff ` a ) ` e ) e. RR )
41 nn0re 
 |-  ( A e. NN0 -> A e. RR )
42 41 ad2antrr 
 |-  ( ( ( A e. NN0 /\ a e. ( Poly ` ZZ ) ) /\ e e. NN0 ) -> A e. RR )
43 40 42 absled 
 |-  ( ( ( A e. NN0 /\ a e. ( Poly ` ZZ ) ) /\ e e. NN0 ) -> ( ( abs ` ( ( coeff ` a ) ` e ) ) <_ A <-> ( -u A <_ ( ( coeff ` a ) ` e ) /\ ( ( coeff ` a ) ` e ) <_ A ) ) )
44 nn0z 
 |-  ( A e. NN0 -> A e. ZZ )
45 44 ad2antrr 
 |-  ( ( ( A e. NN0 /\ a e. ( Poly ` ZZ ) ) /\ e e. NN0 ) -> A e. ZZ )
46 45 znegcld 
 |-  ( ( ( A e. NN0 /\ a e. ( Poly ` ZZ ) ) /\ e e. NN0 ) -> -u A e. ZZ )
47 elfz 
 |-  ( ( ( ( coeff ` a ) ` e ) e. ZZ /\ -u A e. ZZ /\ A e. ZZ ) -> ( ( ( coeff ` a ) ` e ) e. ( -u A ... A ) <-> ( -u A <_ ( ( coeff ` a ) ` e ) /\ ( ( coeff ` a ) ` e ) <_ A ) ) )
48 39 46 45 47 syl3anc 
 |-  ( ( ( A e. NN0 /\ a e. ( Poly ` ZZ ) ) /\ e e. NN0 ) -> ( ( ( coeff ` a ) ` e ) e. ( -u A ... A ) <-> ( -u A <_ ( ( coeff ` a ) ` e ) /\ ( ( coeff ` a ) ` e ) <_ A ) ) )
49 43 48 bitr4d 
 |-  ( ( ( A e. NN0 /\ a e. ( Poly ` ZZ ) ) /\ e e. NN0 ) -> ( ( abs ` ( ( coeff ` a ) ` e ) ) <_ A <-> ( ( coeff ` a ) ` e ) e. ( -u A ... A ) ) )
50 49 biimpd 
 |-  ( ( ( A e. NN0 /\ a e. ( Poly ` ZZ ) ) /\ e e. NN0 ) -> ( ( abs ` ( ( coeff ` a ) ` e ) ) <_ A -> ( ( coeff ` a ) ` e ) e. ( -u A ... A ) ) )
51 50 ralimdva 
 |-  ( ( A e. NN0 /\ a e. ( Poly ` ZZ ) ) -> ( A. e e. NN0 ( abs ` ( ( coeff ` a ) ` e ) ) <_ A -> A. e e. NN0 ( ( coeff ` a ) ` e ) e. ( -u A ... A ) ) )
52 51 impr 
 |-  ( ( A e. NN0 /\ ( a e. ( Poly ` ZZ ) /\ A. e e. NN0 ( abs ` ( ( coeff ` a ) ` e ) ) <_ A ) ) -> A. e e. NN0 ( ( coeff ` a ) ` e ) e. ( -u A ... A ) )
53 fnfvrnss 
 |-  ( ( ( coeff ` a ) Fn NN0 /\ A. e e. NN0 ( ( coeff ` a ) ` e ) e. ( -u A ... A ) ) -> ran ( coeff ` a ) C_ ( -u A ... A ) )
54 37 52 53 syl2anc 
 |-  ( ( A e. NN0 /\ ( a e. ( Poly ` ZZ ) /\ A. e e. NN0 ( abs ` ( ( coeff ` a ) ` e ) ) <_ A ) ) -> ran ( coeff ` a ) C_ ( -u A ... A ) )
55 df-f 
 |-  ( ( coeff ` a ) : NN0 --> ( -u A ... A ) <-> ( ( coeff ` a ) Fn NN0 /\ ran ( coeff ` a ) C_ ( -u A ... A ) ) )
56 37 54 55 sylanbrc 
 |-  ( ( A e. NN0 /\ ( a e. ( Poly ` ZZ ) /\ A. e e. NN0 ( abs ` ( ( coeff ` a ) ` e ) ) <_ A ) ) -> ( coeff ` a ) : NN0 --> ( -u A ... A ) )
57 fz0ssnn0 
 |-  ( 0 ... A ) C_ NN0
58 fssres 
 |-  ( ( ( coeff ` a ) : NN0 --> ( -u A ... A ) /\ ( 0 ... A ) C_ NN0 ) -> ( ( coeff ` a ) |` ( 0 ... A ) ) : ( 0 ... A ) --> ( -u A ... A ) )
59 56 57 58 sylancl 
 |-  ( ( A e. NN0 /\ ( a e. ( Poly ` ZZ ) /\ A. e e. NN0 ( abs ` ( ( coeff ` a ) ` e ) ) <_ A ) ) -> ( ( coeff ` a ) |` ( 0 ... A ) ) : ( 0 ... A ) --> ( -u A ... A ) )
60 ovex 
 |-  ( -u A ... A ) e. _V
61 ovex 
 |-  ( 0 ... A ) e. _V
62 60 61 elmap 
 |-  ( ( ( coeff ` a ) |` ( 0 ... A ) ) e. ( ( -u A ... A ) ^m ( 0 ... A ) ) <-> ( ( coeff ` a ) |` ( 0 ... A ) ) : ( 0 ... A ) --> ( -u A ... A ) )
63 59 62 sylibr 
 |-  ( ( A e. NN0 /\ ( a e. ( Poly ` ZZ ) /\ A. e e. NN0 ( abs ` ( ( coeff ` a ) ` e ) ) <_ A ) ) -> ( ( coeff ` a ) |` ( 0 ... A ) ) e. ( ( -u A ... A ) ^m ( 0 ... A ) ) )
64 63 ex 
 |-  ( A e. NN0 -> ( ( a e. ( Poly ` ZZ ) /\ A. e e. NN0 ( abs ` ( ( coeff ` a ) ` e ) ) <_ A ) -> ( ( coeff ` a ) |` ( 0 ... A ) ) e. ( ( -u A ... A ) ^m ( 0 ... A ) ) ) )
65 31 64 syl5 
 |-  ( A e. NN0 -> ( a e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A ) } -> ( ( coeff ` a ) |` ( 0 ... A ) ) e. ( ( -u A ... A ) ^m ( 0 ... A ) ) ) )
66 simp2 
 |-  ( ( a =/= 0p /\ ( deg ` a ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` a ) ` e ) ) <_ A ) -> ( deg ` a ) <_ A )
67 66 anim2i 
 |-  ( ( a e. ( Poly ` ZZ ) /\ ( a =/= 0p /\ ( deg ` a ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` a ) ` e ) ) <_ A ) ) -> ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) )
68 28 67 sylbi 
 |-  ( a e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A ) } -> ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) )
69 neeq1 
 |-  ( d = b -> ( d =/= 0p <-> b =/= 0p ) )
70 fveq2 
 |-  ( d = b -> ( deg ` d ) = ( deg ` b ) )
71 70 breq1d 
 |-  ( d = b -> ( ( deg ` d ) <_ A <-> ( deg ` b ) <_ A ) )
72 fveq2 
 |-  ( d = b -> ( coeff ` d ) = ( coeff ` b ) )
73 72 fveq1d 
 |-  ( d = b -> ( ( coeff ` d ) ` e ) = ( ( coeff ` b ) ` e ) )
74 73 fveq2d 
 |-  ( d = b -> ( abs ` ( ( coeff ` d ) ` e ) ) = ( abs ` ( ( coeff ` b ) ` e ) ) )
75 74 breq1d 
 |-  ( d = b -> ( ( abs ` ( ( coeff ` d ) ` e ) ) <_ A <-> ( abs ` ( ( coeff ` b ) ` e ) ) <_ A ) )
76 75 ralbidv 
 |-  ( d = b -> ( A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A <-> A. e e. NN0 ( abs ` ( ( coeff ` b ) ` e ) ) <_ A ) )
77 69 71 76 3anbi123d 
 |-  ( d = b -> ( ( d =/= 0p /\ ( deg ` d ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A ) <-> ( b =/= 0p /\ ( deg ` b ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` b ) ` e ) ) <_ A ) ) )
78 77 elrab 
 |-  ( b e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A ) } <-> ( b e. ( Poly ` ZZ ) /\ ( b =/= 0p /\ ( deg ` b ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` b ) ` e ) ) <_ A ) ) )
79 simp2 
 |-  ( ( b =/= 0p /\ ( deg ` b ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` b ) ` e ) ) <_ A ) -> ( deg ` b ) <_ A )
80 79 anim2i 
 |-  ( ( b e. ( Poly ` ZZ ) /\ ( b =/= 0p /\ ( deg ` b ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` b ) ` e ) ) <_ A ) ) -> ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) )
81 78 80 sylbi 
 |-  ( b e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A ) } -> ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) )
82 simplll 
 |-  ( ( ( ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) /\ ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) ) /\ ( A e. NN0 /\ ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) ) ) -> a e. ( Poly ` ZZ ) )
83 plyf 
 |-  ( a e. ( Poly ` ZZ ) -> a : CC --> CC )
84 ffn 
 |-  ( a : CC --> CC -> a Fn CC )
85 82 83 84 3syl 
 |-  ( ( ( ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) /\ ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) ) /\ ( A e. NN0 /\ ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) ) ) -> a Fn CC )
86 simplrl 
 |-  ( ( ( ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) /\ ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) ) /\ ( A e. NN0 /\ ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) ) ) -> b e. ( Poly ` ZZ ) )
87 plyf 
 |-  ( b e. ( Poly ` ZZ ) -> b : CC --> CC )
88 ffn 
 |-  ( b : CC --> CC -> b Fn CC )
89 86 87 88 3syl 
 |-  ( ( ( ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) /\ ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) ) /\ ( A e. NN0 /\ ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) ) ) -> b Fn CC )
90 simplrr 
 |-  ( ( ( ( ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) /\ ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) ) /\ ( A e. NN0 /\ ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) ) ) /\ c e. CC ) -> ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) )
91 90 adantr 
 |-  ( ( ( ( ( ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) /\ ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) ) /\ ( A e. NN0 /\ ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) ) ) /\ c e. CC ) /\ d e. ( 0 ... A ) ) -> ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) )
92 91 fveq1d 
 |-  ( ( ( ( ( ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) /\ ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) ) /\ ( A e. NN0 /\ ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) ) ) /\ c e. CC ) /\ d e. ( 0 ... A ) ) -> ( ( ( coeff ` a ) |` ( 0 ... A ) ) ` d ) = ( ( ( coeff ` b ) |` ( 0 ... A ) ) ` d ) )
93 fvres 
 |-  ( d e. ( 0 ... A ) -> ( ( ( coeff ` a ) |` ( 0 ... A ) ) ` d ) = ( ( coeff ` a ) ` d ) )
94 93 adantl 
 |-  ( ( ( ( ( ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) /\ ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) ) /\ ( A e. NN0 /\ ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) ) ) /\ c e. CC ) /\ d e. ( 0 ... A ) ) -> ( ( ( coeff ` a ) |` ( 0 ... A ) ) ` d ) = ( ( coeff ` a ) ` d ) )
95 fvres 
 |-  ( d e. ( 0 ... A ) -> ( ( ( coeff ` b ) |` ( 0 ... A ) ) ` d ) = ( ( coeff ` b ) ` d ) )
96 95 adantl 
 |-  ( ( ( ( ( ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) /\ ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) ) /\ ( A e. NN0 /\ ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) ) ) /\ c e. CC ) /\ d e. ( 0 ... A ) ) -> ( ( ( coeff ` b ) |` ( 0 ... A ) ) ` d ) = ( ( coeff ` b ) ` d ) )
97 92 94 96 3eqtr3d 
 |-  ( ( ( ( ( ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) /\ ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) ) /\ ( A e. NN0 /\ ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) ) ) /\ c e. CC ) /\ d e. ( 0 ... A ) ) -> ( ( coeff ` a ) ` d ) = ( ( coeff ` b ) ` d ) )
98 97 oveq1d 
 |-  ( ( ( ( ( ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) /\ ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) ) /\ ( A e. NN0 /\ ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) ) ) /\ c e. CC ) /\ d e. ( 0 ... A ) ) -> ( ( ( coeff ` a ) ` d ) x. ( c ^ d ) ) = ( ( ( coeff ` b ) ` d ) x. ( c ^ d ) ) )
99 98 sumeq2dv 
 |-  ( ( ( ( ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) /\ ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) ) /\ ( A e. NN0 /\ ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) ) ) /\ c e. CC ) -> sum_ d e. ( 0 ... A ) ( ( ( coeff ` a ) ` d ) x. ( c ^ d ) ) = sum_ d e. ( 0 ... A ) ( ( ( coeff ` b ) ` d ) x. ( c ^ d ) ) )
100 simp-4l 
 |-  ( ( ( ( ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) /\ ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) ) /\ ( A e. NN0 /\ ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) ) ) /\ c e. CC ) -> a e. ( Poly ` ZZ ) )
101 simp-4r 
 |-  ( ( ( ( ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) /\ ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) ) /\ ( A e. NN0 /\ ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) ) ) /\ c e. CC ) -> ( deg ` a ) <_ A )
102 dgrcl 
 |-  ( a e. ( Poly ` ZZ ) -> ( deg ` a ) e. NN0 )
103 nn0z 
 |-  ( ( deg ` a ) e. NN0 -> ( deg ` a ) e. ZZ )
104 100 102 103 3syl 
 |-  ( ( ( ( ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) /\ ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) ) /\ ( A e. NN0 /\ ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) ) ) /\ c e. CC ) -> ( deg ` a ) e. ZZ )
105 simplrl 
 |-  ( ( ( ( ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) /\ ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) ) /\ ( A e. NN0 /\ ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) ) ) /\ c e. CC ) -> A e. NN0 )
106 105 nn0zd 
 |-  ( ( ( ( ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) /\ ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) ) /\ ( A e. NN0 /\ ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) ) ) /\ c e. CC ) -> A e. ZZ )
107 eluz 
 |-  ( ( ( deg ` a ) e. ZZ /\ A e. ZZ ) -> ( A e. ( ZZ>= ` ( deg ` a ) ) <-> ( deg ` a ) <_ A ) )
108 104 106 107 syl2anc 
 |-  ( ( ( ( ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) /\ ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) ) /\ ( A e. NN0 /\ ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) ) ) /\ c e. CC ) -> ( A e. ( ZZ>= ` ( deg ` a ) ) <-> ( deg ` a ) <_ A ) )
109 101 108 mpbird 
 |-  ( ( ( ( ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) /\ ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) ) /\ ( A e. NN0 /\ ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) ) ) /\ c e. CC ) -> A e. ( ZZ>= ` ( deg ` a ) ) )
110 simpr 
 |-  ( ( ( ( ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) /\ ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) ) /\ ( A e. NN0 /\ ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) ) ) /\ c e. CC ) -> c e. CC )
111 eqid 
 |-  ( deg ` a ) = ( deg ` a )
112 33 111 coeid3 
 |-  ( ( a e. ( Poly ` ZZ ) /\ A e. ( ZZ>= ` ( deg ` a ) ) /\ c e. CC ) -> ( a ` c ) = sum_ d e. ( 0 ... A ) ( ( ( coeff ` a ) ` d ) x. ( c ^ d ) ) )
113 100 109 110 112 syl3anc 
 |-  ( ( ( ( ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) /\ ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) ) /\ ( A e. NN0 /\ ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) ) ) /\ c e. CC ) -> ( a ` c ) = sum_ d e. ( 0 ... A ) ( ( ( coeff ` a ) ` d ) x. ( c ^ d ) ) )
114 simp1rl 
 |-  ( ( ( ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) /\ ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) ) /\ ( A e. NN0 /\ ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) ) /\ c e. CC ) -> b e. ( Poly ` ZZ ) )
115 114 3expa 
 |-  ( ( ( ( ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) /\ ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) ) /\ ( A e. NN0 /\ ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) ) ) /\ c e. CC ) -> b e. ( Poly ` ZZ ) )
116 simplrr 
 |-  ( ( ( ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) /\ ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) ) /\ ( A e. NN0 /\ ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) ) ) -> ( deg ` b ) <_ A )
117 116 adantr 
 |-  ( ( ( ( ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) /\ ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) ) /\ ( A e. NN0 /\ ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) ) ) /\ c e. CC ) -> ( deg ` b ) <_ A )
118 dgrcl 
 |-  ( b e. ( Poly ` ZZ ) -> ( deg ` b ) e. NN0 )
119 nn0z 
 |-  ( ( deg ` b ) e. NN0 -> ( deg ` b ) e. ZZ )
120 115 118 119 3syl 
 |-  ( ( ( ( ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) /\ ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) ) /\ ( A e. NN0 /\ ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) ) ) /\ c e. CC ) -> ( deg ` b ) e. ZZ )
121 eluz 
 |-  ( ( ( deg ` b ) e. ZZ /\ A e. ZZ ) -> ( A e. ( ZZ>= ` ( deg ` b ) ) <-> ( deg ` b ) <_ A ) )
122 120 106 121 syl2anc 
 |-  ( ( ( ( ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) /\ ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) ) /\ ( A e. NN0 /\ ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) ) ) /\ c e. CC ) -> ( A e. ( ZZ>= ` ( deg ` b ) ) <-> ( deg ` b ) <_ A ) )
123 117 122 mpbird 
 |-  ( ( ( ( ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) /\ ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) ) /\ ( A e. NN0 /\ ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) ) ) /\ c e. CC ) -> A e. ( ZZ>= ` ( deg ` b ) ) )
124 eqid 
 |-  ( coeff ` b ) = ( coeff ` b )
125 eqid 
 |-  ( deg ` b ) = ( deg ` b )
126 124 125 coeid3 
 |-  ( ( b e. ( Poly ` ZZ ) /\ A e. ( ZZ>= ` ( deg ` b ) ) /\ c e. CC ) -> ( b ` c ) = sum_ d e. ( 0 ... A ) ( ( ( coeff ` b ) ` d ) x. ( c ^ d ) ) )
127 115 123 110 126 syl3anc 
 |-  ( ( ( ( ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) /\ ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) ) /\ ( A e. NN0 /\ ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) ) ) /\ c e. CC ) -> ( b ` c ) = sum_ d e. ( 0 ... A ) ( ( ( coeff ` b ) ` d ) x. ( c ^ d ) ) )
128 99 113 127 3eqtr4d 
 |-  ( ( ( ( ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) /\ ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) ) /\ ( A e. NN0 /\ ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) ) ) /\ c e. CC ) -> ( a ` c ) = ( b ` c ) )
129 85 89 128 eqfnfvd 
 |-  ( ( ( ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) /\ ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) ) /\ ( A e. NN0 /\ ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) ) ) -> a = b )
130 129 expr 
 |-  ( ( ( ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) /\ ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) ) /\ A e. NN0 ) -> ( ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) -> a = b ) )
131 fveq2 
 |-  ( a = b -> ( coeff ` a ) = ( coeff ` b ) )
132 131 reseq1d 
 |-  ( a = b -> ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) )
133 130 132 impbid1 
 |-  ( ( ( ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) /\ ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) ) /\ A e. NN0 ) -> ( ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) <-> a = b ) )
134 133 expcom 
 |-  ( A e. NN0 -> ( ( ( a e. ( Poly ` ZZ ) /\ ( deg ` a ) <_ A ) /\ ( b e. ( Poly ` ZZ ) /\ ( deg ` b ) <_ A ) ) -> ( ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) <-> a = b ) ) )
135 68 81 134 syl2ani 
 |-  ( A e. NN0 -> ( ( a e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A ) } /\ b e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A ) } ) -> ( ( ( coeff ` a ) |` ( 0 ... A ) ) = ( ( coeff ` b ) |` ( 0 ... A ) ) <-> a = b ) ) )
136 65 135 dom2d 
 |-  ( A e. NN0 -> ( ( ( -u A ... A ) ^m ( 0 ... A ) ) e. _V -> { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A ) } ~<_ ( ( -u A ... A ) ^m ( 0 ... A ) ) ) )
137 18 136 mpi 
 |-  ( A e. NN0 -> { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A ) } ~<_ ( ( -u A ... A ) ^m ( 0 ... A ) ) )
138 domfi 
 |-  ( ( ( ( -u A ... A ) ^m ( 0 ... A ) ) e. Fin /\ { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A ) } ~<_ ( ( -u A ... A ) ^m ( 0 ... A ) ) ) -> { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A ) } e. Fin )
139 17 137 138 syl2anc 
 |-  ( A e. NN0 -> { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A ) } e. Fin )
140 neeq1 
 |-  ( d = c -> ( d =/= 0p <-> c =/= 0p ) )
141 fveq2 
 |-  ( d = c -> ( deg ` d ) = ( deg ` c ) )
142 141 breq1d 
 |-  ( d = c -> ( ( deg ` d ) <_ A <-> ( deg ` c ) <_ A ) )
143 fveq2 
 |-  ( d = c -> ( coeff ` d ) = ( coeff ` c ) )
144 143 fveq1d 
 |-  ( d = c -> ( ( coeff ` d ) ` e ) = ( ( coeff ` c ) ` e ) )
145 144 fveq2d 
 |-  ( d = c -> ( abs ` ( ( coeff ` d ) ` e ) ) = ( abs ` ( ( coeff ` c ) ` e ) ) )
146 145 breq1d 
 |-  ( d = c -> ( ( abs ` ( ( coeff ` d ) ` e ) ) <_ A <-> ( abs ` ( ( coeff ` c ) ` e ) ) <_ A ) )
147 146 ralbidv 
 |-  ( d = c -> ( A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A <-> A. e e. NN0 ( abs ` ( ( coeff ` c ) ` e ) ) <_ A ) )
148 140 142 147 3anbi123d 
 |-  ( d = c -> ( ( d =/= 0p /\ ( deg ` d ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A ) <-> ( c =/= 0p /\ ( deg ` c ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` c ) ` e ) ) <_ A ) ) )
149 148 elrab 
 |-  ( c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A ) } <-> ( c e. ( Poly ` ZZ ) /\ ( c =/= 0p /\ ( deg ` c ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` c ) ` e ) ) <_ A ) ) )
150 simp1 
 |-  ( ( c =/= 0p /\ ( deg ` c ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` c ) ` e ) ) <_ A ) -> c =/= 0p )
151 150 anim2i 
 |-  ( ( c e. ( Poly ` ZZ ) /\ ( c =/= 0p /\ ( deg ` c ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` c ) ` e ) ) <_ A ) ) -> ( c e. ( Poly ` ZZ ) /\ c =/= 0p ) )
152 149 151 sylbi 
 |-  ( c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A ) } -> ( c e. ( Poly ` ZZ ) /\ c =/= 0p ) )
153 fveqeq2 
 |-  ( b = a -> ( ( c ` b ) = 0 <-> ( c ` a ) = 0 ) )
154 153 elrab 
 |-  ( a e. { b e. CC | ( c ` b ) = 0 } <-> ( a e. CC /\ ( c ` a ) = 0 ) )
155 plyf 
 |-  ( c e. ( Poly ` ZZ ) -> c : CC --> CC )
156 155 ffnd 
 |-  ( c e. ( Poly ` ZZ ) -> c Fn CC )
157 156 adantr 
 |-  ( ( c e. ( Poly ` ZZ ) /\ c =/= 0p ) -> c Fn CC )
158 fniniseg 
 |-  ( c Fn CC -> ( a e. ( `' c " { 0 } ) <-> ( a e. CC /\ ( c ` a ) = 0 ) ) )
159 157 158 syl 
 |-  ( ( c e. ( Poly ` ZZ ) /\ c =/= 0p ) -> ( a e. ( `' c " { 0 } ) <-> ( a e. CC /\ ( c ` a ) = 0 ) ) )
160 154 159 bitr4id 
 |-  ( ( c e. ( Poly ` ZZ ) /\ c =/= 0p ) -> ( a e. { b e. CC | ( c ` b ) = 0 } <-> a e. ( `' c " { 0 } ) ) )
161 160 eqrdv 
 |-  ( ( c e. ( Poly ` ZZ ) /\ c =/= 0p ) -> { b e. CC | ( c ` b ) = 0 } = ( `' c " { 0 } ) )
162 eqid 
 |-  ( `' c " { 0 } ) = ( `' c " { 0 } )
163 162 fta1 
 |-  ( ( c e. ( Poly ` ZZ ) /\ c =/= 0p ) -> ( ( `' c " { 0 } ) e. Fin /\ ( # ` ( `' c " { 0 } ) ) <_ ( deg ` c ) ) )
164 163 simpld 
 |-  ( ( c e. ( Poly ` ZZ ) /\ c =/= 0p ) -> ( `' c " { 0 } ) e. Fin )
165 161 164 eqeltrd 
 |-  ( ( c e. ( Poly ` ZZ ) /\ c =/= 0p ) -> { b e. CC | ( c ` b ) = 0 } e. Fin )
166 165 a1i 
 |-  ( A e. NN0 -> ( ( c e. ( Poly ` ZZ ) /\ c =/= 0p ) -> { b e. CC | ( c ` b ) = 0 } e. Fin ) )
167 152 166 syl5 
 |-  ( A e. NN0 -> ( c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A ) } -> { b e. CC | ( c ` b ) = 0 } e. Fin ) )
168 167 ralrimiv 
 |-  ( A e. NN0 -> A. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A ) } { b e. CC | ( c ` b ) = 0 } e. Fin )
169 iunfi 
 |-  ( ( { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A ) } e. Fin /\ A. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A ) } { b e. CC | ( c ` b ) = 0 } e. Fin ) -> U_ c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A ) } { b e. CC | ( c ` b ) = 0 } e. Fin )
170 139 168 169 syl2anc 
 |-  ( A e. NN0 -> U_ c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A ) } { b e. CC | ( c ` b ) = 0 } e. Fin )
171 12 170 eqeltrrid 
 |-  ( A e. NN0 -> { b e. CC | E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ A /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ A ) } ( c ` b ) = 0 } e. Fin )
172 11 171 eqeltrd 
 |-  ( A e. NN0 -> ( H ` A ) e. Fin )