Metamath Proof Explorer

Theorem aareccl

Description: The reciprocal of an algebraic number is algebraic. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Assertion aareccl 
|- ( ( A e. AA /\ A =/= 0 ) -> ( 1 / A ) e. AA )

Proof

Step Hyp Ref Expression
1 elaa 
 |-  ( A e. AA <-> ( A e. CC /\ E. f e. ( ( Poly ` ZZ ) \ { 0p } ) ( f ` A ) = 0 ) )
2 1 simprbi 
 |-  ( A e. AA -> E. f e. ( ( Poly ` ZZ ) \ { 0p } ) ( f ` A ) = 0 )
3 2 adantr 
 |-  ( ( A e. AA /\ A =/= 0 ) -> E. f e. ( ( Poly ` ZZ ) \ { 0p } ) ( f ` A ) = 0 )
4 aacn 
 |-  ( A e. AA -> A e. CC )
5 reccl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( 1 / A ) e. CC )
6 4 5 sylan 
 |-  ( ( A e. AA /\ A =/= 0 ) -> ( 1 / A ) e. CC )
7 6 adantr 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> ( 1 / A ) e. CC )
8 zsscn 
 |-  ZZ C_ CC
9 8 a1i 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> ZZ C_ CC )
10 simprl 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> f e. ( ( Poly ` ZZ ) \ { 0p } ) )
11 eldifsn 
 |-  ( f e. ( ( Poly ` ZZ ) \ { 0p } ) <-> ( f e. ( Poly ` ZZ ) /\ f =/= 0p ) )
12 10 11 sylib 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> ( f e. ( Poly ` ZZ ) /\ f =/= 0p ) )
13 12 simpld 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> f e. ( Poly ` ZZ ) )
14 dgrcl 
 |-  ( f e. ( Poly ` ZZ ) -> ( deg ` f ) e. NN0 )
15 13 14 syl 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> ( deg ` f ) e. NN0 )
16 13 adantr 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ k e. ( 0 ... ( deg ` f ) ) ) -> f e. ( Poly ` ZZ ) )
17 0z 
 |-  0 e. ZZ
18 eqid 
 |-  ( coeff ` f ) = ( coeff ` f )
19 18 coef2 
 |-  ( ( f e. ( Poly ` ZZ ) /\ 0 e. ZZ ) -> ( coeff ` f ) : NN0 --> ZZ )
20 16 17 19 sylancl 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ k e. ( 0 ... ( deg ` f ) ) ) -> ( coeff ` f ) : NN0 --> ZZ )
21 fznn0sub 
 |-  ( k e. ( 0 ... ( deg ` f ) ) -> ( ( deg ` f ) - k ) e. NN0 )
22 21 adantl 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ k e. ( 0 ... ( deg ` f ) ) ) -> ( ( deg ` f ) - k ) e. NN0 )
23 20 22 ffvelcdmd 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ k e. ( 0 ... ( deg ` f ) ) ) -> ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) e. ZZ )
24 9 15 23 elplyd 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( z ^ k ) ) ) e. ( Poly ` ZZ ) )
25 0cn 
 |-  0 e. CC
26 eqid 
 |-  ( coeff ` ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( z ^ k ) ) ) ) = ( coeff ` ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( z ^ k ) ) ) )
27 26 coefv0 
 |-  ( ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( z ^ k ) ) ) e. ( Poly ` ZZ ) -> ( ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( z ^ k ) ) ) ` 0 ) = ( ( coeff ` ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( z ^ k ) ) ) ) ` 0 ) )
28 24 27 syl 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> ( ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( z ^ k ) ) ) ` 0 ) = ( ( coeff ` ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( z ^ k ) ) ) ) ` 0 ) )
29 23 zcnd 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ k e. ( 0 ... ( deg ` f ) ) ) -> ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) e. CC )
30 eqidd 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( z ^ k ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( z ^ k ) ) ) )
31 24 15 29 30 coeeq2 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> ( coeff ` ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( z ^ k ) ) ) ) = ( k e. NN0 |-> if ( k <_ ( deg ` f ) , ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) , 0 ) ) )
32 31 fveq1d 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> ( ( coeff ` ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( z ^ k ) ) ) ) ` 0 ) = ( ( k e. NN0 |-> if ( k <_ ( deg ` f ) , ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) , 0 ) ) ` 0 ) )
33 0nn0 
 |-  0 e. NN0
34 breq1 
 |-  ( k = 0 -> ( k <_ ( deg ` f ) <-> 0 <_ ( deg ` f ) ) )
35 oveq2 
 |-  ( k = 0 -> ( ( deg ` f ) - k ) = ( ( deg ` f ) - 0 ) )
36 35 fveq2d 
 |-  ( k = 0 -> ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) = ( ( coeff ` f ) ` ( ( deg ` f ) - 0 ) ) )
37 34 36 ifbieq1d 
 |-  ( k = 0 -> if ( k <_ ( deg ` f ) , ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) , 0 ) = if ( 0 <_ ( deg ` f ) , ( ( coeff ` f ) ` ( ( deg ` f ) - 0 ) ) , 0 ) )
38 eqid 
 |-  ( k e. NN0 |-> if ( k <_ ( deg ` f ) , ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) , 0 ) ) = ( k e. NN0 |-> if ( k <_ ( deg ` f ) , ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) , 0 ) )
39 fvex 
 |-  ( ( coeff ` f ) ` ( ( deg ` f ) - 0 ) ) e. _V
40 c0ex 
 |-  0 e. _V
41 39 40 ifex 
 |-  if ( 0 <_ ( deg ` f ) , ( ( coeff ` f ) ` ( ( deg ` f ) - 0 ) ) , 0 ) e. _V
42 37 38 41 fvmpt 
 |-  ( 0 e. NN0 -> ( ( k e. NN0 |-> if ( k <_ ( deg ` f ) , ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) , 0 ) ) ` 0 ) = if ( 0 <_ ( deg ` f ) , ( ( coeff ` f ) ` ( ( deg ` f ) - 0 ) ) , 0 ) )
43 33 42 ax-mp 
 |-  ( ( k e. NN0 |-> if ( k <_ ( deg ` f ) , ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) , 0 ) ) ` 0 ) = if ( 0 <_ ( deg ` f ) , ( ( coeff ` f ) ` ( ( deg ` f ) - 0 ) ) , 0 )
44 15 nn0ge0d 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> 0 <_ ( deg ` f ) )
45 44 iftrued 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> if ( 0 <_ ( deg ` f ) , ( ( coeff ` f ) ` ( ( deg ` f ) - 0 ) ) , 0 ) = ( ( coeff ` f ) ` ( ( deg ` f ) - 0 ) ) )
46 15 nn0cnd 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> ( deg ` f ) e. CC )
47 46 subid1d 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> ( ( deg ` f ) - 0 ) = ( deg ` f ) )
48 47 fveq2d 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> ( ( coeff ` f ) ` ( ( deg ` f ) - 0 ) ) = ( ( coeff ` f ) ` ( deg ` f ) ) )
49 45 48 eqtrd 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> if ( 0 <_ ( deg ` f ) , ( ( coeff ` f ) ` ( ( deg ` f ) - 0 ) ) , 0 ) = ( ( coeff ` f ) ` ( deg ` f ) ) )
50 43 49 eqtrid 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> ( ( k e. NN0 |-> if ( k <_ ( deg ` f ) , ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) , 0 ) ) ` 0 ) = ( ( coeff ` f ) ` ( deg ` f ) ) )
51 28 32 50 3eqtrd 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> ( ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( z ^ k ) ) ) ` 0 ) = ( ( coeff ` f ) ` ( deg ` f ) ) )
52 12 simprd 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> f =/= 0p )
53 eqid 
 |-  ( deg ` f ) = ( deg ` f )
54 53 18 dgreq0 
 |-  ( f e. ( Poly ` ZZ ) -> ( f = 0p <-> ( ( coeff ` f ) ` ( deg ` f ) ) = 0 ) )
55 13 54 syl 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> ( f = 0p <-> ( ( coeff ` f ) ` ( deg ` f ) ) = 0 ) )
56 55 necon3bid 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> ( f =/= 0p <-> ( ( coeff ` f ) ` ( deg ` f ) ) =/= 0 ) )
57 52 56 mpbid 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> ( ( coeff ` f ) ` ( deg ` f ) ) =/= 0 )
58 51 57 eqnetrd 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> ( ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( z ^ k ) ) ) ` 0 ) =/= 0 )
59 ne0p 
 |-  ( ( 0 e. CC /\ ( ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( z ^ k ) ) ) ` 0 ) =/= 0 ) -> ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( z ^ k ) ) ) =/= 0p )
60 25 58 59 sylancr 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( z ^ k ) ) ) =/= 0p )
61 eldifsn 
 |-  ( ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( z ^ k ) ) ) e. ( ( Poly ` ZZ ) \ { 0p } ) <-> ( ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( z ^ k ) ) ) e. ( Poly ` ZZ ) /\ ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( z ^ k ) ) ) =/= 0p ) )
62 24 60 61 sylanbrc 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( z ^ k ) ) ) e. ( ( Poly ` ZZ ) \ { 0p } ) )
63 oveq1 
 |-  ( z = ( 1 / A ) -> ( z ^ k ) = ( ( 1 / A ) ^ k ) )
64 63 oveq2d 
 |-  ( z = ( 1 / A ) -> ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( z ^ k ) ) = ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( ( 1 / A ) ^ k ) ) )
65 64 sumeq2sdv 
 |-  ( z = ( 1 / A ) -> sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( ( 1 / A ) ^ k ) ) )
66 eqid 
 |-  ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( z ^ k ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( z ^ k ) ) )
67 sumex 
 |-  sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( ( 1 / A ) ^ k ) ) e. _V
68 65 66 67 fvmpt 
 |-  ( ( 1 / A ) e. CC -> ( ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( z ^ k ) ) ) ` ( 1 / A ) ) = sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( ( 1 / A ) ^ k ) ) )
69 7 68 syl 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> ( ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( z ^ k ) ) ) ` ( 1 / A ) ) = sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( ( 1 / A ) ^ k ) ) )
70 18 coef3 
 |-  ( f e. ( Poly ` ZZ ) -> ( coeff ` f ) : NN0 --> CC )
71 13 70 syl 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> ( coeff ` f ) : NN0 --> CC )
72 elfznn0 
 |-  ( n e. ( 0 ... ( deg ` f ) ) -> n e. NN0 )
73 ffvelcdm 
 |-  ( ( ( coeff ` f ) : NN0 --> CC /\ n e. NN0 ) -> ( ( coeff ` f ) ` n ) e. CC )
74 71 72 73 syl2an 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ n e. ( 0 ... ( deg ` f ) ) ) -> ( ( coeff ` f ) ` n ) e. CC )
75 4 ad2antrr 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> A e. CC )
76 expcl 
 |-  ( ( A e. CC /\ n e. NN0 ) -> ( A ^ n ) e. CC )
77 75 72 76 syl2an 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ n e. ( 0 ... ( deg ` f ) ) ) -> ( A ^ n ) e. CC )
78 74 77 mulcld 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ n e. ( 0 ... ( deg ` f ) ) ) -> ( ( ( coeff ` f ) ` n ) x. ( A ^ n ) ) e. CC )
79 75 15 expcld 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> ( A ^ ( deg ` f ) ) e. CC )
80 79 adantr 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ n e. ( 0 ... ( deg ` f ) ) ) -> ( A ^ ( deg ` f ) ) e. CC )
81 simplr 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> A =/= 0 )
82 15 nn0zd 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> ( deg ` f ) e. ZZ )
83 75 81 82 expne0d 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> ( A ^ ( deg ` f ) ) =/= 0 )
84 83 adantr 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ n e. ( 0 ... ( deg ` f ) ) ) -> ( A ^ ( deg ` f ) ) =/= 0 )
85 78 80 84 divcld 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ n e. ( 0 ... ( deg ` f ) ) ) -> ( ( ( ( coeff ` f ) ` n ) x. ( A ^ n ) ) / ( A ^ ( deg ` f ) ) ) e. CC )
86 fveq2 
 |-  ( n = ( ( 0 + ( deg ` f ) ) - k ) -> ( ( coeff ` f ) ` n ) = ( ( coeff ` f ) ` ( ( 0 + ( deg ` f ) ) - k ) ) )
87 oveq2 
 |-  ( n = ( ( 0 + ( deg ` f ) ) - k ) -> ( A ^ n ) = ( A ^ ( ( 0 + ( deg ` f ) ) - k ) ) )
88 86 87 oveq12d 
 |-  ( n = ( ( 0 + ( deg ` f ) ) - k ) -> ( ( ( coeff ` f ) ` n ) x. ( A ^ n ) ) = ( ( ( coeff ` f ) ` ( ( 0 + ( deg ` f ) ) - k ) ) x. ( A ^ ( ( 0 + ( deg ` f ) ) - k ) ) ) )
89 88 oveq1d 
 |-  ( n = ( ( 0 + ( deg ` f ) ) - k ) -> ( ( ( ( coeff ` f ) ` n ) x. ( A ^ n ) ) / ( A ^ ( deg ` f ) ) ) = ( ( ( ( coeff ` f ) ` ( ( 0 + ( deg ` f ) ) - k ) ) x. ( A ^ ( ( 0 + ( deg ` f ) ) - k ) ) ) / ( A ^ ( deg ` f ) ) ) )
90 85 89 fsumrev2 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> sum_ n e. ( 0 ... ( deg ` f ) ) ( ( ( ( coeff ` f ) ` n ) x. ( A ^ n ) ) / ( A ^ ( deg ` f ) ) ) = sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( ( coeff ` f ) ` ( ( 0 + ( deg ` f ) ) - k ) ) x. ( A ^ ( ( 0 + ( deg ` f ) ) - k ) ) ) / ( A ^ ( deg ` f ) ) ) )
91 46 adantr 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ k e. ( 0 ... ( deg ` f ) ) ) -> ( deg ` f ) e. CC )
92 91 addlidd 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ k e. ( 0 ... ( deg ` f ) ) ) -> ( 0 + ( deg ` f ) ) = ( deg ` f ) )
93 92 oveq1d 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ k e. ( 0 ... ( deg ` f ) ) ) -> ( ( 0 + ( deg ` f ) ) - k ) = ( ( deg ` f ) - k ) )
94 93 fveq2d 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ k e. ( 0 ... ( deg ` f ) ) ) -> ( ( coeff ` f ) ` ( ( 0 + ( deg ` f ) ) - k ) ) = ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) )
95 93 oveq2d 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ k e. ( 0 ... ( deg ` f ) ) ) -> ( A ^ ( ( 0 + ( deg ` f ) ) - k ) ) = ( A ^ ( ( deg ` f ) - k ) ) )
96 75 adantr 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ k e. ( 0 ... ( deg ` f ) ) ) -> A e. CC )
97 81 adantr 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ k e. ( 0 ... ( deg ` f ) ) ) -> A =/= 0 )
98 elfznn0 
 |-  ( k e. ( 0 ... ( deg ` f ) ) -> k e. NN0 )
99 98 adantl 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ k e. ( 0 ... ( deg ` f ) ) ) -> k e. NN0 )
100 99 nn0zd 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ k e. ( 0 ... ( deg ` f ) ) ) -> k e. ZZ )
101 82 adantr 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ k e. ( 0 ... ( deg ` f ) ) ) -> ( deg ` f ) e. ZZ )
102 96 97 100 101 expsubd 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ k e. ( 0 ... ( deg ` f ) ) ) -> ( A ^ ( ( deg ` f ) - k ) ) = ( ( A ^ ( deg ` f ) ) / ( A ^ k ) ) )
103 95 102 eqtrd 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ k e. ( 0 ... ( deg ` f ) ) ) -> ( A ^ ( ( 0 + ( deg ` f ) ) - k ) ) = ( ( A ^ ( deg ` f ) ) / ( A ^ k ) ) )
104 94 103 oveq12d 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ k e. ( 0 ... ( deg ` f ) ) ) -> ( ( ( coeff ` f ) ` ( ( 0 + ( deg ` f ) ) - k ) ) x. ( A ^ ( ( 0 + ( deg ` f ) ) - k ) ) ) = ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( ( A ^ ( deg ` f ) ) / ( A ^ k ) ) ) )
105 104 oveq1d 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ k e. ( 0 ... ( deg ` f ) ) ) -> ( ( ( ( coeff ` f ) ` ( ( 0 + ( deg ` f ) ) - k ) ) x. ( A ^ ( ( 0 + ( deg ` f ) ) - k ) ) ) / ( A ^ ( deg ` f ) ) ) = ( ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( ( A ^ ( deg ` f ) ) / ( A ^ k ) ) ) / ( A ^ ( deg ` f ) ) ) )
106 79 adantr 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ k e. ( 0 ... ( deg ` f ) ) ) -> ( A ^ ( deg ` f ) ) e. CC )
107 expcl 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( A ^ k ) e. CC )
108 75 98 107 syl2an 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ k e. ( 0 ... ( deg ` f ) ) ) -> ( A ^ k ) e. CC )
109 96 97 100 expne0d 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ k e. ( 0 ... ( deg ` f ) ) ) -> ( A ^ k ) =/= 0 )
110 106 108 109 divcld 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ k e. ( 0 ... ( deg ` f ) ) ) -> ( ( A ^ ( deg ` f ) ) / ( A ^ k ) ) e. CC )
111 83 adantr 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ k e. ( 0 ... ( deg ` f ) ) ) -> ( A ^ ( deg ` f ) ) =/= 0 )
112 29 110 106 111 divassd 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ k e. ( 0 ... ( deg ` f ) ) ) -> ( ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( ( A ^ ( deg ` f ) ) / ( A ^ k ) ) ) / ( A ^ ( deg ` f ) ) ) = ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( ( ( A ^ ( deg ` f ) ) / ( A ^ k ) ) / ( A ^ ( deg ` f ) ) ) ) )
113 106 111 dividd 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ k e. ( 0 ... ( deg ` f ) ) ) -> ( ( A ^ ( deg ` f ) ) / ( A ^ ( deg ` f ) ) ) = 1 )
114 113 oveq1d 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ k e. ( 0 ... ( deg ` f ) ) ) -> ( ( ( A ^ ( deg ` f ) ) / ( A ^ ( deg ` f ) ) ) / ( A ^ k ) ) = ( 1 / ( A ^ k ) ) )
115 106 108 106 109 111 divdiv32d 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ k e. ( 0 ... ( deg ` f ) ) ) -> ( ( ( A ^ ( deg ` f ) ) / ( A ^ k ) ) / ( A ^ ( deg ` f ) ) ) = ( ( ( A ^ ( deg ` f ) ) / ( A ^ ( deg ` f ) ) ) / ( A ^ k ) ) )
116 96 97 100 exprecd 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ k e. ( 0 ... ( deg ` f ) ) ) -> ( ( 1 / A ) ^ k ) = ( 1 / ( A ^ k ) ) )
117 114 115 116 3eqtr4d 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ k e. ( 0 ... ( deg ` f ) ) ) -> ( ( ( A ^ ( deg ` f ) ) / ( A ^ k ) ) / ( A ^ ( deg ` f ) ) ) = ( ( 1 / A ) ^ k ) )
118 117 oveq2d 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ k e. ( 0 ... ( deg ` f ) ) ) -> ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( ( ( A ^ ( deg ` f ) ) / ( A ^ k ) ) / ( A ^ ( deg ` f ) ) ) ) = ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( ( 1 / A ) ^ k ) ) )
119 105 112 118 3eqtrd 
 |-  ( ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) /\ k e. ( 0 ... ( deg ` f ) ) ) -> ( ( ( ( coeff ` f ) ` ( ( 0 + ( deg ` f ) ) - k ) ) x. ( A ^ ( ( 0 + ( deg ` f ) ) - k ) ) ) / ( A ^ ( deg ` f ) ) ) = ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( ( 1 / A ) ^ k ) ) )
120 119 sumeq2dv 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( ( coeff ` f ) ` ( ( 0 + ( deg ` f ) ) - k ) ) x. ( A ^ ( ( 0 + ( deg ` f ) ) - k ) ) ) / ( A ^ ( deg ` f ) ) ) = sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( ( 1 / A ) ^ k ) ) )
121 90 120 eqtrd 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> sum_ n e. ( 0 ... ( deg ` f ) ) ( ( ( ( coeff ` f ) ` n ) x. ( A ^ n ) ) / ( A ^ ( deg ` f ) ) ) = sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( ( 1 / A ) ^ k ) ) )
122 18 53 coeid2 
 |-  ( ( f e. ( Poly ` ZZ ) /\ A e. CC ) -> ( f ` A ) = sum_ n e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` n ) x. ( A ^ n ) ) )
123 13 75 122 syl2anc 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> ( f ` A ) = sum_ n e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` n ) x. ( A ^ n ) ) )
124 simprr 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> ( f ` A ) = 0 )
125 123 124 eqtr3d 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> sum_ n e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` n ) x. ( A ^ n ) ) = 0 )
126 125 oveq1d 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> ( sum_ n e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` n ) x. ( A ^ n ) ) / ( A ^ ( deg ` f ) ) ) = ( 0 / ( A ^ ( deg ` f ) ) ) )
127 fzfid 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> ( 0 ... ( deg ` f ) ) e. Fin )
128 127 79 78 83 fsumdivc 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> ( sum_ n e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` n ) x. ( A ^ n ) ) / ( A ^ ( deg ` f ) ) ) = sum_ n e. ( 0 ... ( deg ` f ) ) ( ( ( ( coeff ` f ) ` n ) x. ( A ^ n ) ) / ( A ^ ( deg ` f ) ) ) )
129 79 83 div0d 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> ( 0 / ( A ^ ( deg ` f ) ) ) = 0 )
130 126 128 129 3eqtr3d 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> sum_ n e. ( 0 ... ( deg ` f ) ) ( ( ( ( coeff ` f ) ` n ) x. ( A ^ n ) ) / ( A ^ ( deg ` f ) ) ) = 0 )
131 69 121 130 3eqtr2d 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> ( ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( z ^ k ) ) ) ` ( 1 / A ) ) = 0 )
132 fveq1 
 |-  ( g = ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( z ^ k ) ) ) -> ( g ` ( 1 / A ) ) = ( ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( z ^ k ) ) ) ` ( 1 / A ) ) )
133 132 eqeq1d 
 |-  ( g = ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( z ^ k ) ) ) -> ( ( g ` ( 1 / A ) ) = 0 <-> ( ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( z ^ k ) ) ) ` ( 1 / A ) ) = 0 ) )
134 133 rspcev 
 |-  ( ( ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( z ^ k ) ) ) e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` ( ( deg ` f ) - k ) ) x. ( z ^ k ) ) ) ` ( 1 / A ) ) = 0 ) -> E. g e. ( ( Poly ` ZZ ) \ { 0p } ) ( g ` ( 1 / A ) ) = 0 )
135 62 131 134 syl2anc 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> E. g e. ( ( Poly ` ZZ ) \ { 0p } ) ( g ` ( 1 / A ) ) = 0 )
136 elaa 
 |-  ( ( 1 / A ) e. AA <-> ( ( 1 / A ) e. CC /\ E. g e. ( ( Poly ` ZZ ) \ { 0p } ) ( g ` ( 1 / A ) ) = 0 ) )
137 7 135 136 sylanbrc 
 |-  ( ( ( A e. AA /\ A =/= 0 ) /\ ( f e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( f ` A ) = 0 ) ) -> ( 1 / A ) e. AA )
138 3 137 rexlimddv 
 |-  ( ( A e. AA /\ A =/= 0 ) -> ( 1 / A ) e. AA )