Metamath Proof Explorer

Theorem aannenlem2

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 aannenlem2 
|- AA = U. ran H

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 fveqeq2 
 |-  ( b = g -> ( ( c ` b ) = 0 <-> ( c ` g ) = 0 ) )
3 2 rexbidv 
 |-  ( b = g -> ( E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) } ( c ` b ) = 0 <-> E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) } ( c ` g ) = 0 ) )
4 simp3 
 |-  ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( h ` g ) = 0 /\ g e. CC ) -> g e. CC )
5 neeq1 
 |-  ( d = h -> ( d =/= 0p <-> h =/= 0p ) )
6 fveq2 
 |-  ( d = h -> ( deg ` d ) = ( deg ` h ) )
7 6 breq1d 
 |-  ( d = h -> ( ( deg ` d ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) <-> ( deg ` h ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) )
8 fveq2 
 |-  ( d = h -> ( coeff ` d ) = ( coeff ` h ) )
9 8 fveq1d 
 |-  ( d = h -> ( ( coeff ` d ) ` e ) = ( ( coeff ` h ) ` e ) )
10 9 fveq2d 
 |-  ( d = h -> ( abs ` ( ( coeff ` d ) ` e ) ) = ( abs ` ( ( coeff ` h ) ` e ) ) )
11 10 breq1d 
 |-  ( d = h -> ( ( abs ` ( ( coeff ` d ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) <-> ( abs ` ( ( coeff ` h ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) )
12 11 ralbidv 
 |-  ( d = h -> ( A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) <-> A. e e. NN0 ( abs ` ( ( coeff ` h ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) )
13 5 7 12 3anbi123d 
 |-  ( d = h -> ( ( d =/= 0p /\ ( deg ` d ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) <-> ( h =/= 0p /\ ( deg ` h ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) /\ A. e e. NN0 ( abs ` ( ( coeff ` h ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) ) )
14 eldifi 
 |-  ( h e. ( ( Poly ` ZZ ) \ { 0p } ) -> h e. ( Poly ` ZZ ) )
15 14 adantr 
 |-  ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ g e. CC ) -> h e. ( Poly ` ZZ ) )
16 15 3adant2 
 |-  ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( h ` g ) = 0 /\ g e. CC ) -> h e. ( Poly ` ZZ ) )
17 eldifsni 
 |-  ( h e. ( ( Poly ` ZZ ) \ { 0p } ) -> h =/= 0p )
18 17 adantr 
 |-  ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ g e. CC ) -> h =/= 0p )
19 0nn0 
 |-  0 e. NN0
20 dgrcl 
 |-  ( h e. ( Poly ` ZZ ) -> ( deg ` h ) e. NN0 )
21 15 20 syl 
 |-  ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ g e. CC ) -> ( deg ` h ) e. NN0 )
22 prssi 
 |-  ( ( 0 e. NN0 /\ ( deg ` h ) e. NN0 ) -> { 0 , ( deg ` h ) } C_ NN0 )
23 19 21 22 sylancr 
 |-  ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ g e. CC ) -> { 0 , ( deg ` h ) } C_ NN0 )
24 ssrab2 
 |-  { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } C_ NN0
25 24 a1i 
 |-  ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ g e. CC ) -> { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } C_ NN0 )
26 23 25 unssd 
 |-  ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ g e. CC ) -> ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) C_ NN0 )
27 nn0ssre 
 |-  NN0 C_ RR
28 ressxr 
 |-  RR C_ RR*
29 27 28 sstri 
 |-  NN0 C_ RR*
30 26 29 sstrdi 
 |-  ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ g e. CC ) -> ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) C_ RR* )
31 fvex 
 |-  ( deg ` h ) e. _V
32 31 prid2 
 |-  ( deg ` h ) e. { 0 , ( deg ` h ) }
33 elun1 
 |-  ( ( deg ` h ) e. { 0 , ( deg ` h ) } -> ( deg ` h ) e. ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) )
34 32 33 ax-mp 
 |-  ( deg ` h ) e. ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } )
35 supxrub 
 |-  ( ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) C_ RR* /\ ( deg ` h ) e. ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) ) -> ( deg ` h ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) )
36 30 34 35 sylancl 
 |-  ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ g e. CC ) -> ( deg ` h ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) )
37 30 adantr 
 |-  ( ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ g e. CC ) /\ e e. NN0 ) -> ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) C_ RR* )
38 fveq2 
 |-  ( ( ( coeff ` h ) ` e ) = 0 -> ( abs ` ( ( coeff ` h ) ` e ) ) = ( abs ` 0 ) )
39 abs0 
 |-  ( abs ` 0 ) = 0
40 38 39 eqtrdi 
 |-  ( ( ( coeff ` h ) ` e ) = 0 -> ( abs ` ( ( coeff ` h ) ` e ) ) = 0 )
41 c0ex 
 |-  0 e. _V
42 41 prid1 
 |-  0 e. { 0 , ( deg ` h ) }
43 elun1 
 |-  ( 0 e. { 0 , ( deg ` h ) } -> 0 e. ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) )
44 42 43 ax-mp 
 |-  0 e. ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } )
45 40 44 eqeltrdi 
 |-  ( ( ( coeff ` h ) ` e ) = 0 -> ( abs ` ( ( coeff ` h ) ` e ) ) e. ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) )
46 45 adantl 
 |-  ( ( ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ g e. CC ) /\ e e. NN0 ) /\ ( ( coeff ` h ) ` e ) = 0 ) -> ( abs ` ( ( coeff ` h ) ` e ) ) e. ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) )
47 eqeq1 
 |-  ( g = ( abs ` ( ( coeff ` h ) ` e ) ) -> ( g = ( abs ` ( ( coeff ` h ) ` i ) ) <-> ( abs ` ( ( coeff ` h ) ` e ) ) = ( abs ` ( ( coeff ` h ) ` i ) ) ) )
48 47 rexbidv 
 |-  ( g = ( abs ` ( ( coeff ` h ) ` e ) ) -> ( E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) <-> E. i e. ( 0 ... ( deg ` h ) ) ( abs ` ( ( coeff ` h ) ` e ) ) = ( abs ` ( ( coeff ` h ) ` i ) ) ) )
49 0z 
 |-  0 e. ZZ
50 eqid 
 |-  ( coeff ` h ) = ( coeff ` h )
51 50 coef2 
 |-  ( ( h e. ( Poly ` ZZ ) /\ 0 e. ZZ ) -> ( coeff ` h ) : NN0 --> ZZ )
52 15 49 51 sylancl 
 |-  ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ g e. CC ) -> ( coeff ` h ) : NN0 --> ZZ )
53 52 ffvelrnda 
 |-  ( ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ g e. CC ) /\ e e. NN0 ) -> ( ( coeff ` h ) ` e ) e. ZZ )
54 nn0abscl 
 |-  ( ( ( coeff ` h ) ` e ) e. ZZ -> ( abs ` ( ( coeff ` h ) ` e ) ) e. NN0 )
55 53 54 syl 
 |-  ( ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ g e. CC ) /\ e e. NN0 ) -> ( abs ` ( ( coeff ` h ) ` e ) ) e. NN0 )
56 55 adantr 
 |-  ( ( ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ g e. CC ) /\ e e. NN0 ) /\ ( ( coeff ` h ) ` e ) =/= 0 ) -> ( abs ` ( ( coeff ` h ) ` e ) ) e. NN0 )
57 simplr 
 |-  ( ( ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ g e. CC ) /\ e e. NN0 ) /\ ( ( coeff ` h ) ` e ) =/= 0 ) -> e e. NN0 )
58 21 ad2antrr 
 |-  ( ( ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ g e. CC ) /\ e e. NN0 ) /\ ( ( coeff ` h ) ` e ) =/= 0 ) -> ( deg ` h ) e. NN0 )
59 15 ad2antrr 
 |-  ( ( ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ g e. CC ) /\ e e. NN0 ) /\ ( ( coeff ` h ) ` e ) =/= 0 ) -> h e. ( Poly ` ZZ ) )
60 simpr 
 |-  ( ( ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ g e. CC ) /\ e e. NN0 ) /\ ( ( coeff ` h ) ` e ) =/= 0 ) -> ( ( coeff ` h ) ` e ) =/= 0 )
61 eqid 
 |-  ( deg ` h ) = ( deg ` h )
62 50 61 dgrub 
 |-  ( ( h e. ( Poly ` ZZ ) /\ e e. NN0 /\ ( ( coeff ` h ) ` e ) =/= 0 ) -> e <_ ( deg ` h ) )
63 59 57 60 62 syl3anc 
 |-  ( ( ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ g e. CC ) /\ e e. NN0 ) /\ ( ( coeff ` h ) ` e ) =/= 0 ) -> e <_ ( deg ` h ) )
64 elfz2nn0 
 |-  ( e e. ( 0 ... ( deg ` h ) ) <-> ( e e. NN0 /\ ( deg ` h ) e. NN0 /\ e <_ ( deg ` h ) ) )
65 57 58 63 64 syl3anbrc 
 |-  ( ( ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ g e. CC ) /\ e e. NN0 ) /\ ( ( coeff ` h ) ` e ) =/= 0 ) -> e e. ( 0 ... ( deg ` h ) ) )
66 eqid 
 |-  ( abs ` ( ( coeff ` h ) ` e ) ) = ( abs ` ( ( coeff ` h ) ` e ) )
67 2fveq3 
 |-  ( i = e -> ( abs ` ( ( coeff ` h ) ` i ) ) = ( abs ` ( ( coeff ` h ) ` e ) ) )
68 67 rspceeqv 
 |-  ( ( e e. ( 0 ... ( deg ` h ) ) /\ ( abs ` ( ( coeff ` h ) ` e ) ) = ( abs ` ( ( coeff ` h ) ` e ) ) ) -> E. i e. ( 0 ... ( deg ` h ) ) ( abs ` ( ( coeff ` h ) ` e ) ) = ( abs ` ( ( coeff ` h ) ` i ) ) )
69 65 66 68 sylancl 
 |-  ( ( ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ g e. CC ) /\ e e. NN0 ) /\ ( ( coeff ` h ) ` e ) =/= 0 ) -> E. i e. ( 0 ... ( deg ` h ) ) ( abs ` ( ( coeff ` h ) ` e ) ) = ( abs ` ( ( coeff ` h ) ` i ) ) )
70 48 56 69 elrabd 
 |-  ( ( ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ g e. CC ) /\ e e. NN0 ) /\ ( ( coeff ` h ) ` e ) =/= 0 ) -> ( abs ` ( ( coeff ` h ) ` e ) ) e. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } )
71 elun2 
 |-  ( ( abs ` ( ( coeff ` h ) ` e ) ) e. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } -> ( abs ` ( ( coeff ` h ) ` e ) ) e. ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) )
72 70 71 syl 
 |-  ( ( ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ g e. CC ) /\ e e. NN0 ) /\ ( ( coeff ` h ) ` e ) =/= 0 ) -> ( abs ` ( ( coeff ` h ) ` e ) ) e. ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) )
73 46 72 pm2.61dane 
 |-  ( ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ g e. CC ) /\ e e. NN0 ) -> ( abs ` ( ( coeff ` h ) ` e ) ) e. ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) )
74 supxrub 
 |-  ( ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) C_ RR* /\ ( abs ` ( ( coeff ` h ) ` e ) ) e. ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) ) -> ( abs ` ( ( coeff ` h ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) )
75 37 73 74 syl2anc 
 |-  ( ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ g e. CC ) /\ e e. NN0 ) -> ( abs ` ( ( coeff ` h ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) )
76 75 ralrimiva 
 |-  ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ g e. CC ) -> A. e e. NN0 ( abs ` ( ( coeff ` h ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) )
77 18 36 76 3jca 
 |-  ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ g e. CC ) -> ( h =/= 0p /\ ( deg ` h ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) /\ A. e e. NN0 ( abs ` ( ( coeff ` h ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) )
78 77 3adant2 
 |-  ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( h ` g ) = 0 /\ g e. CC ) -> ( h =/= 0p /\ ( deg ` h ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) /\ A. e e. NN0 ( abs ` ( ( coeff ` h ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) )
79 13 16 78 elrabd 
 |-  ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( h ` g ) = 0 /\ g e. CC ) -> h e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) } )
80 simp2 
 |-  ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( h ` g ) = 0 /\ g e. CC ) -> ( h ` g ) = 0 )
81 fveq1 
 |-  ( c = h -> ( c ` g ) = ( h ` g ) )
82 81 eqeq1d 
 |-  ( c = h -> ( ( c ` g ) = 0 <-> ( h ` g ) = 0 ) )
83 82 rspcev 
 |-  ( ( h e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) } /\ ( h ` g ) = 0 ) -> E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) } ( c ` g ) = 0 )
84 79 80 83 syl2anc 
 |-  ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( h ` g ) = 0 /\ g e. CC ) -> E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) } ( c ` g ) = 0 )
85 3 4 84 elrabd 
 |-  ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( h ` g ) = 0 /\ g e. CC ) -> g e. { b e. CC | E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) } ( c ` b ) = 0 } )
86 prfi 
 |-  { 0 , ( deg ` h ) } e. Fin
87 fzfi 
 |-  ( 0 ... ( deg ` h ) ) e. Fin
88 abrexfi 
 |-  ( ( 0 ... ( deg ` h ) ) e. Fin -> { g | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } e. Fin )
89 87 88 ax-mp 
 |-  { g | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } e. Fin
90 rabssab 
 |-  { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } C_ { g | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) }
91 ssfi 
 |-  ( ( { g | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } e. Fin /\ { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } C_ { g | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) -> { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } e. Fin )
92 89 90 91 mp2an 
 |-  { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } e. Fin
93 unfi 
 |-  ( ( { 0 , ( deg ` h ) } e. Fin /\ { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } e. Fin ) -> ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) e. Fin )
94 86 92 93 mp2an 
 |-  ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) e. Fin
95 34 ne0ii 
 |-  ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) =/= (/)
96 xrltso 
 |-  < Or RR*
97 fisupcl 
 |-  ( ( < Or RR* /\ ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) e. Fin /\ ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) =/= (/) /\ ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) C_ RR* ) ) -> sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) e. ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) )
98 96 97 mpan 
 |-  ( ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) e. Fin /\ ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) =/= (/) /\ ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) C_ RR* ) -> sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) e. ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) )
99 94 95 30 98 mp3an12i 
 |-  ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ g e. CC ) -> sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) e. ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) )
100 26 99 sseldd 
 |-  ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ g e. CC ) -> sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) e. NN0 )
101 100 3adant2 
 |-  ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( h ` g ) = 0 /\ g e. CC ) -> sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) e. NN0 )
102 eqidd 
 |-  ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( h ` g ) = 0 /\ g e. CC ) -> { b e. CC | E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) } ( c ` b ) = 0 } = { b e. CC | E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) } ( c ` b ) = 0 } )
103 breq2 
 |-  ( a = sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) -> ( ( deg ` d ) <_ a <-> ( deg ` d ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) )
104 breq2 
 |-  ( a = sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) -> ( ( abs ` ( ( coeff ` d ) ` e ) ) <_ a <-> ( abs ` ( ( coeff ` d ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) )
105 104 ralbidv 
 |-  ( a = sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) -> ( A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ a <-> A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) )
106 103 105 3anbi23d 
 |-  ( a = sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) -> ( ( d =/= 0p /\ ( deg ` d ) <_ a /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ a ) <-> ( d =/= 0p /\ ( deg ` d ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) ) )
107 106 rabbidv 
 |-  ( a = sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) -> { 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 ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) } )
108 107 rexeqdv 
 |-  ( a = sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) -> ( 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 ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) } ( c ` b ) = 0 ) )
109 108 rabbidv 
 |-  ( a = sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) -> { 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 ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) } ( c ` b ) = 0 } )
110 109 rspceeqv 
 |-  ( ( sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) e. NN0 /\ { b e. CC | E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) } ( c ` b ) = 0 } = { b e. CC | E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) } ( c ` b ) = 0 } ) -> E. a e. NN0 { b e. CC | E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) } ( 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 } )
111 101 102 110 syl2anc 
 |-  ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( h ` g ) = 0 /\ g e. CC ) -> E. a e. NN0 { b e. CC | E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) } ( 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 } )
112 cnex 
 |-  CC e. _V
113 112 rabex 
 |-  { b e. CC | E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) } ( c ` b ) = 0 } e. _V
114 eleq2 
 |-  ( f = { b e. CC | E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) } ( c ` b ) = 0 } -> ( g e. f <-> g e. { b e. CC | E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) } ( c ` b ) = 0 } ) )
115 eqeq1 
 |-  ( f = { b e. CC | E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) } ( c ` b ) = 0 } -> ( f = { 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 ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) } ( 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 } ) )
116 115 rexbidv 
 |-  ( f = { b e. CC | E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) } ( c ` b ) = 0 } -> ( E. a e. NN0 f = { 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. a e. NN0 { b e. CC | E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) } ( 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 } ) )
117 114 116 anbi12d 
 |-  ( f = { b e. CC | E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) } ( c ` b ) = 0 } -> ( ( g e. f /\ E. a e. NN0 f = { 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 } ) <-> ( g e. { b e. CC | E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) } ( c ` b ) = 0 } /\ E. a e. NN0 { b e. CC | E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) } ( 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 } ) ) )
118 113 117 spcev 
 |-  ( ( g e. { b e. CC | E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) } ( c ` b ) = 0 } /\ E. a e. NN0 { b e. CC | E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ sup ( ( { 0 , ( deg ` h ) } u. { g e. NN0 | E. i e. ( 0 ... ( deg ` h ) ) g = ( abs ` ( ( coeff ` h ) ` i ) ) } ) , RR* , < ) ) } ( 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 } ) -> E. f ( g e. f /\ E. a e. NN0 f = { 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 } ) )
119 85 111 118 syl2anc 
 |-  ( ( h e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( h ` g ) = 0 /\ g e. CC ) -> E. f ( g e. f /\ E. a e. NN0 f = { 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 } ) )
120 119 3exp 
 |-  ( h e. ( ( Poly ` ZZ ) \ { 0p } ) -> ( ( h ` g ) = 0 -> ( g e. CC -> E. f ( g e. f /\ E. a e. NN0 f = { 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 } ) ) ) )
121 120 rexlimiv 
 |-  ( E. h e. ( ( Poly ` ZZ ) \ { 0p } ) ( h ` g ) = 0 -> ( g e. CC -> E. f ( g e. f /\ E. a e. NN0 f = { 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 } ) ) )
122 121 impcom 
 |-  ( ( g e. CC /\ E. h e. ( ( Poly ` ZZ ) \ { 0p } ) ( h ` g ) = 0 ) -> E. f ( g e. f /\ E. a e. NN0 f = { 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 } ) )
123 eleq2 
 |-  ( f = { 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 } -> ( g e. f <-> g e. { 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 } ) )
124 2 rexbidv 
 |-  ( b = g -> ( 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 ` g ) = 0 ) )
125 124 elrab 
 |-  ( g e. { 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 } <-> ( g e. CC /\ E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ a /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ a ) } ( c ` g ) = 0 ) )
126 simp1 
 |-  ( ( h =/= 0p /\ ( deg ` h ) <_ a /\ A. e e. NN0 ( abs ` ( ( coeff ` h ) ` e ) ) <_ a ) -> h =/= 0p )
127 126 anim2i 
 |-  ( ( h e. ( Poly ` ZZ ) /\ ( h =/= 0p /\ ( deg ` h ) <_ a /\ A. e e. NN0 ( abs ` ( ( coeff ` h ) ` e ) ) <_ a ) ) -> ( h e. ( Poly ` ZZ ) /\ h =/= 0p ) )
128 6 breq1d 
 |-  ( d = h -> ( ( deg ` d ) <_ a <-> ( deg ` h ) <_ a ) )
129 10 breq1d 
 |-  ( d = h -> ( ( abs ` ( ( coeff ` d ) ` e ) ) <_ a <-> ( abs ` ( ( coeff ` h ) ` e ) ) <_ a ) )
130 129 ralbidv 
 |-  ( d = h -> ( A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ a <-> A. e e. NN0 ( abs ` ( ( coeff ` h ) ` e ) ) <_ a ) )
131 5 128 130 3anbi123d 
 |-  ( d = h -> ( ( d =/= 0p /\ ( deg ` d ) <_ a /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ a ) <-> ( h =/= 0p /\ ( deg ` h ) <_ a /\ A. e e. NN0 ( abs ` ( ( coeff ` h ) ` e ) ) <_ a ) ) )
132 131 elrab 
 |-  ( h e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ a /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ a ) } <-> ( h e. ( Poly ` ZZ ) /\ ( h =/= 0p /\ ( deg ` h ) <_ a /\ A. e e. NN0 ( abs ` ( ( coeff ` h ) ` e ) ) <_ a ) ) )
133 eldifsn 
 |-  ( h e. ( ( Poly ` ZZ ) \ { 0p } ) <-> ( h e. ( Poly ` ZZ ) /\ h =/= 0p ) )
134 127 132 133 3imtr4i 
 |-  ( h e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ a /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ a ) } -> h e. ( ( Poly ` ZZ ) \ { 0p } ) )
135 134 ssriv 
 |-  { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ a /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ a ) } C_ ( ( Poly ` ZZ ) \ { 0p } )
136 ssrexv 
 |-  ( { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ a /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ a ) } C_ ( ( Poly ` ZZ ) \ { 0p } ) -> ( E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ a /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ a ) } ( c ` g ) = 0 -> E. c e. ( ( Poly ` ZZ ) \ { 0p } ) ( c ` g ) = 0 ) )
137 82 cbvrexvw 
 |-  ( E. c e. ( ( Poly ` ZZ ) \ { 0p } ) ( c ` g ) = 0 <-> E. h e. ( ( Poly ` ZZ ) \ { 0p } ) ( h ` g ) = 0 )
138 136 137 syl6ib 
 |-  ( { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ a /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ a ) } C_ ( ( Poly ` ZZ ) \ { 0p } ) -> ( E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ a /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ a ) } ( c ` g ) = 0 -> E. h e. ( ( Poly ` ZZ ) \ { 0p } ) ( h ` g ) = 0 ) )
139 135 138 ax-mp 
 |-  ( E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ a /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ a ) } ( c ` g ) = 0 -> E. h e. ( ( Poly ` ZZ ) \ { 0p } ) ( h ` g ) = 0 )
140 139 anim2i 
 |-  ( ( g e. CC /\ E. c e. { d e. ( Poly ` ZZ ) | ( d =/= 0p /\ ( deg ` d ) <_ a /\ A. e e. NN0 ( abs ` ( ( coeff ` d ) ` e ) ) <_ a ) } ( c ` g ) = 0 ) -> ( g e. CC /\ E. h e. ( ( Poly ` ZZ ) \ { 0p } ) ( h ` g ) = 0 ) )
141 125 140 sylbi 
 |-  ( g e. { 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 } -> ( g e. CC /\ E. h e. ( ( Poly ` ZZ ) \ { 0p } ) ( h ` g ) = 0 ) )
142 123 141 syl6bi 
 |-  ( f = { 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 } -> ( g e. f -> ( g e. CC /\ E. h e. ( ( Poly ` ZZ ) \ { 0p } ) ( h ` g ) = 0 ) ) )
143 142 rexlimivw 
 |-  ( E. a e. NN0 f = { 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 } -> ( g e. f -> ( g e. CC /\ E. h e. ( ( Poly ` ZZ ) \ { 0p } ) ( h ` g ) = 0 ) ) )
144 143 impcom 
 |-  ( ( g e. f /\ E. a e. NN0 f = { 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 } ) -> ( g e. CC /\ E. h e. ( ( Poly ` ZZ ) \ { 0p } ) ( h ` g ) = 0 ) )
145 144 exlimiv 
 |-  ( E. f ( g e. f /\ E. a e. NN0 f = { 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 } ) -> ( g e. CC /\ E. h e. ( ( Poly ` ZZ ) \ { 0p } ) ( h ` g ) = 0 ) )
146 122 145 impbii 
 |-  ( ( g e. CC /\ E. h e. ( ( Poly ` ZZ ) \ { 0p } ) ( h ` g ) = 0 ) <-> E. f ( g e. f /\ E. a e. NN0 f = { 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 } ) )
147 elaa 
 |-  ( g e. AA <-> ( g e. CC /\ E. h e. ( ( Poly ` ZZ ) \ { 0p } ) ( h ` g ) = 0 ) )
148 eluniab 
 |-  ( g e. U. { f | E. a e. NN0 f = { 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. f ( g e. f /\ E. a e. NN0 f = { 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 } ) )
149 146 147 148 3bitr4i 
 |-  ( g e. AA <-> g e. U. { f | E. a e. NN0 f = { 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 } } )
150 149 eqriv 
 |-  AA = U. { f | E. a e. NN0 f = { 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 } }
151 1 rnmpt 
 |-  ran H = { f | E. a e. NN0 f = { 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 } }
152 151 unieqi 
 |-  U. ran H = U. { f | E. a e. NN0 f = { 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 } }
153 150 152 eqtr4i 
 |-  AA = U. ran H