Metamath Proof Explorer

Theorem elaa2lem

Description: Elementhood in the set of nonzero algebraic numbers. ' Only if ' part of elaa2 . (Contributed by Glauco Siliprandi, 5-Apr-2020) (Revised by AV, 1-Oct-2020)

Ref Expression
Hypotheses elaa2lem.a 
|- ( ph -> A e. AA )
elaa2lem.an0 
|- ( ph -> A =/= 0 )
elaa2lem.g 
|- ( ph -> G e. ( Poly ` ZZ ) )
elaa2lem.gn0 
|- ( ph -> G =/= 0p )
elaa2lem.ga 
|- ( ph -> ( G ` A ) = 0 )
elaa2lem.m 
|- M = inf ( { n e. NN0 | ( ( coeff ` G ) ` n ) =/= 0 } , RR , < )
elaa2lem.i 
|- I = ( k e. NN0 |-> ( ( coeff ` G ) ` ( k + M ) ) )
elaa2lem.f 
|- F = ( z e. CC |-> sum_ k e. ( 0 ... ( ( deg ` G ) - M ) ) ( ( I ` k ) x. ( z ^ k ) ) )
Assertion elaa2lem 
|- ( ph -> E. f e. ( Poly ` ZZ ) ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 ) )

Proof

Step Hyp Ref Expression
1 elaa2lem.a 
 |-  ( ph -> A e. AA )
2 elaa2lem.an0 
 |-  ( ph -> A =/= 0 )
3 elaa2lem.g 
 |-  ( ph -> G e. ( Poly ` ZZ ) )
4 elaa2lem.gn0 
 |-  ( ph -> G =/= 0p )
5 elaa2lem.ga 
 |-  ( ph -> ( G ` A ) = 0 )
6 elaa2lem.m 
 |-  M = inf ( { n e. NN0 | ( ( coeff ` G ) ` n ) =/= 0 } , RR , < )
7 elaa2lem.i 
 |-  I = ( k e. NN0 |-> ( ( coeff ` G ) ` ( k + M ) ) )
8 elaa2lem.f 
 |-  F = ( z e. CC |-> sum_ k e. ( 0 ... ( ( deg ` G ) - M ) ) ( ( I ` k ) x. ( z ^ k ) ) )
9 8 a1i 
 |-  ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... ( ( deg ` G ) - M ) ) ( ( I ` k ) x. ( z ^ k ) ) ) )
10 zsscn 
 |-  ZZ C_ CC
11 10 a1i 
 |-  ( ph -> ZZ C_ CC )
12 dgrcl 
 |-  ( G e. ( Poly ` ZZ ) -> ( deg ` G ) e. NN0 )
13 3 12 syl 
 |-  ( ph -> ( deg ` G ) e. NN0 )
14 13 nn0zd 
 |-  ( ph -> ( deg ` G ) e. ZZ )
15 ssrab2 
 |-  { n e. NN0 | ( ( coeff ` G ) ` n ) =/= 0 } C_ NN0
16 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
17 15 16 sseqtri 
 |-  { n e. NN0 | ( ( coeff ` G ) ` n ) =/= 0 } C_ ( ZZ>= ` 0 )
18 17 a1i 
 |-  ( ph -> { n e. NN0 | ( ( coeff ` G ) ` n ) =/= 0 } C_ ( ZZ>= ` 0 ) )
19 4 neneqd 
 |-  ( ph -> -. G = 0p )
20 eqid 
 |-  ( deg ` G ) = ( deg ` G )
21 eqid 
 |-  ( coeff ` G ) = ( coeff ` G )
22 20 21 dgreq0 
 |-  ( G e. ( Poly ` ZZ ) -> ( G = 0p <-> ( ( coeff ` G ) ` ( deg ` G ) ) = 0 ) )
23 3 22 syl 
 |-  ( ph -> ( G = 0p <-> ( ( coeff ` G ) ` ( deg ` G ) ) = 0 ) )
24 19 23 mtbid 
 |-  ( ph -> -. ( ( coeff ` G ) ` ( deg ` G ) ) = 0 )
25 24 neqned 
 |-  ( ph -> ( ( coeff ` G ) ` ( deg ` G ) ) =/= 0 )
26 13 25 jca 
 |-  ( ph -> ( ( deg ` G ) e. NN0 /\ ( ( coeff ` G ) ` ( deg ` G ) ) =/= 0 ) )
27 fveq2 
 |-  ( n = ( deg ` G ) -> ( ( coeff ` G ) ` n ) = ( ( coeff ` G ) ` ( deg ` G ) ) )
28 27 neeq1d 
 |-  ( n = ( deg ` G ) -> ( ( ( coeff ` G ) ` n ) =/= 0 <-> ( ( coeff ` G ) ` ( deg ` G ) ) =/= 0 ) )
29 28 elrab 
 |-  ( ( deg ` G ) e. { n e. NN0 | ( ( coeff ` G ) ` n ) =/= 0 } <-> ( ( deg ` G ) e. NN0 /\ ( ( coeff ` G ) ` ( deg ` G ) ) =/= 0 ) )
30 26 29 sylibr 
 |-  ( ph -> ( deg ` G ) e. { n e. NN0 | ( ( coeff ` G ) ` n ) =/= 0 } )
31 30 ne0d 
 |-  ( ph -> { n e. NN0 | ( ( coeff ` G ) ` n ) =/= 0 } =/= (/) )
32 infssuzcl 
 |-  ( ( { n e. NN0 | ( ( coeff ` G ) ` n ) =/= 0 } C_ ( ZZ>= ` 0 ) /\ { n e. NN0 | ( ( coeff ` G ) ` n ) =/= 0 } =/= (/) ) -> inf ( { n e. NN0 | ( ( coeff ` G ) ` n ) =/= 0 } , RR , < ) e. { n e. NN0 | ( ( coeff ` G ) ` n ) =/= 0 } )
33 18 31 32 syl2anc 
 |-  ( ph -> inf ( { n e. NN0 | ( ( coeff ` G ) ` n ) =/= 0 } , RR , < ) e. { n e. NN0 | ( ( coeff ` G ) ` n ) =/= 0 } )
34 15 33 sseldi 
 |-  ( ph -> inf ( { n e. NN0 | ( ( coeff ` G ) ` n ) =/= 0 } , RR , < ) e. NN0 )
35 6 34 eqeltrid 
 |-  ( ph -> M e. NN0 )
36 35 nn0zd 
 |-  ( ph -> M e. ZZ )
37 14 36 zsubcld 
 |-  ( ph -> ( ( deg ` G ) - M ) e. ZZ )
38 6 a1i 
 |-  ( ph -> M = inf ( { n e. NN0 | ( ( coeff ` G ) ` n ) =/= 0 } , RR , < ) )
39 infssuzle 
 |-  ( ( { n e. NN0 | ( ( coeff ` G ) ` n ) =/= 0 } C_ ( ZZ>= ` 0 ) /\ ( deg ` G ) e. { n e. NN0 | ( ( coeff ` G ) ` n ) =/= 0 } ) -> inf ( { n e. NN0 | ( ( coeff ` G ) ` n ) =/= 0 } , RR , < ) <_ ( deg ` G ) )
40 18 30 39 syl2anc 
 |-  ( ph -> inf ( { n e. NN0 | ( ( coeff ` G ) ` n ) =/= 0 } , RR , < ) <_ ( deg ` G ) )
41 38 40 eqbrtrd 
 |-  ( ph -> M <_ ( deg ` G ) )
42 13 nn0red 
 |-  ( ph -> ( deg ` G ) e. RR )
43 35 nn0red 
 |-  ( ph -> M e. RR )
44 42 43 subge0d 
 |-  ( ph -> ( 0 <_ ( ( deg ` G ) - M ) <-> M <_ ( deg ` G ) ) )
45 41 44 mpbird 
 |-  ( ph -> 0 <_ ( ( deg ` G ) - M ) )
46 37 45 jca 
 |-  ( ph -> ( ( ( deg ` G ) - M ) e. ZZ /\ 0 <_ ( ( deg ` G ) - M ) ) )
47 elnn0z 
 |-  ( ( ( deg ` G ) - M ) e. NN0 <-> ( ( ( deg ` G ) - M ) e. ZZ /\ 0 <_ ( ( deg ` G ) - M ) ) )
48 46 47 sylibr 
 |-  ( ph -> ( ( deg ` G ) - M ) e. NN0 )
49 0zd 
 |-  ( G e. ( Poly ` ZZ ) -> 0 e. ZZ )
50 21 coef2 
 |-  ( ( G e. ( Poly ` ZZ ) /\ 0 e. ZZ ) -> ( coeff ` G ) : NN0 --> ZZ )
51 3 49 50 syl2anc2 
 |-  ( ph -> ( coeff ` G ) : NN0 --> ZZ )
52 51 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> ( coeff ` G ) : NN0 --> ZZ )
53 simpr 
 |-  ( ( ph /\ k e. NN0 ) -> k e. NN0 )
54 35 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> M e. NN0 )
55 53 54 nn0addcld 
 |-  ( ( ph /\ k e. NN0 ) -> ( k + M ) e. NN0 )
56 52 55 ffvelrnd 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( coeff ` G ) ` ( k + M ) ) e. ZZ )
57 56 7 fmptd 
 |-  ( ph -> I : NN0 --> ZZ )
58 elplyr 
 |-  ( ( ZZ C_ CC /\ ( ( deg ` G ) - M ) e. NN0 /\ I : NN0 --> ZZ ) -> ( z e. CC |-> sum_ k e. ( 0 ... ( ( deg ` G ) - M ) ) ( ( I ` k ) x. ( z ^ k ) ) ) e. ( Poly ` ZZ ) )
59 11 48 57 58 syl3anc 
 |-  ( ph -> ( z e. CC |-> sum_ k e. ( 0 ... ( ( deg ` G ) - M ) ) ( ( I ` k ) x. ( z ^ k ) ) ) e. ( Poly ` ZZ ) )
60 9 59 eqeltrd 
 |-  ( ph -> F e. ( Poly ` ZZ ) )
61 simpr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ k <_ ( ( deg ` G ) - M ) ) -> k <_ ( ( deg ` G ) - M ) )
62 61 iftrued 
 |-  ( ( ( ph /\ k e. NN0 ) /\ k <_ ( ( deg ` G ) - M ) ) -> if ( k <_ ( ( deg ` G ) - M ) , ( ( coeff ` G ) ` ( k + M ) ) , 0 ) = ( ( coeff ` G ) ` ( k + M ) ) )
63 iffalse 
 |-  ( -. k <_ ( ( deg ` G ) - M ) -> if ( k <_ ( ( deg ` G ) - M ) , ( ( coeff ` G ) ` ( k + M ) ) , 0 ) = 0 )
64 63 adantl 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. k <_ ( ( deg ` G ) - M ) ) -> if ( k <_ ( ( deg ` G ) - M ) , ( ( coeff ` G ) ` ( k + M ) ) , 0 ) = 0 )
65 simpr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. k <_ ( ( deg ` G ) - M ) ) -> -. k <_ ( ( deg ` G ) - M ) )
66 42 ad2antrr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. k <_ ( ( deg ` G ) - M ) ) -> ( deg ` G ) e. RR )
67 43 ad2antrr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. k <_ ( ( deg ` G ) - M ) ) -> M e. RR )
68 66 67 resubcld 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. k <_ ( ( deg ` G ) - M ) ) -> ( ( deg ` G ) - M ) e. RR )
69 nn0re 
 |-  ( k e. NN0 -> k e. RR )
70 69 ad2antlr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. k <_ ( ( deg ` G ) - M ) ) -> k e. RR )
71 68 70 ltnled 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. k <_ ( ( deg ` G ) - M ) ) -> ( ( ( deg ` G ) - M ) < k <-> -. k <_ ( ( deg ` G ) - M ) ) )
72 65 71 mpbird 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. k <_ ( ( deg ` G ) - M ) ) -> ( ( deg ` G ) - M ) < k )
73 66 67 70 ltsubaddd 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. k <_ ( ( deg ` G ) - M ) ) -> ( ( ( deg ` G ) - M ) < k <-> ( deg ` G ) < ( k + M ) ) )
74 72 73 mpbid 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. k <_ ( ( deg ` G ) - M ) ) -> ( deg ` G ) < ( k + M ) )
75 olc 
 |-  ( ( deg ` G ) < ( k + M ) -> ( G = 0p \/ ( deg ` G ) < ( k + M ) ) )
76 74 75 syl 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. k <_ ( ( deg ` G ) - M ) ) -> ( G = 0p \/ ( deg ` G ) < ( k + M ) ) )
77 3 ad2antrr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. k <_ ( ( deg ` G ) - M ) ) -> G e. ( Poly ` ZZ ) )
78 55 adantr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. k <_ ( ( deg ` G ) - M ) ) -> ( k + M ) e. NN0 )
79 20 21 dgrlt 
 |-  ( ( G e. ( Poly ` ZZ ) /\ ( k + M ) e. NN0 ) -> ( ( G = 0p \/ ( deg ` G ) < ( k + M ) ) <-> ( ( deg ` G ) <_ ( k + M ) /\ ( ( coeff ` G ) ` ( k + M ) ) = 0 ) ) )
80 77 78 79 syl2anc 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. k <_ ( ( deg ` G ) - M ) ) -> ( ( G = 0p \/ ( deg ` G ) < ( k + M ) ) <-> ( ( deg ` G ) <_ ( k + M ) /\ ( ( coeff ` G ) ` ( k + M ) ) = 0 ) ) )
81 76 80 mpbid 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. k <_ ( ( deg ` G ) - M ) ) -> ( ( deg ` G ) <_ ( k + M ) /\ ( ( coeff ` G ) ` ( k + M ) ) = 0 ) )
82 81 simprd 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. k <_ ( ( deg ` G ) - M ) ) -> ( ( coeff ` G ) ` ( k + M ) ) = 0 )
83 64 82 eqtr4d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. k <_ ( ( deg ` G ) - M ) ) -> if ( k <_ ( ( deg ` G ) - M ) , ( ( coeff ` G ) ` ( k + M ) ) , 0 ) = ( ( coeff ` G ) ` ( k + M ) ) )
84 62 83 pm2.61dan 
 |-  ( ( ph /\ k e. NN0 ) -> if ( k <_ ( ( deg ` G ) - M ) , ( ( coeff ` G ) ` ( k + M ) ) , 0 ) = ( ( coeff ` G ) ` ( k + M ) ) )
85 84 mpteq2dva 
 |-  ( ph -> ( k e. NN0 |-> if ( k <_ ( ( deg ` G ) - M ) , ( ( coeff ` G ) ` ( k + M ) ) , 0 ) ) = ( k e. NN0 |-> ( ( coeff ` G ) ` ( k + M ) ) ) )
86 51 11 fssd 
 |-  ( ph -> ( coeff ` G ) : NN0 --> CC )
87 86 adantr 
 |-  ( ( ph /\ k e. ( 0 ... ( ( deg ` G ) - M ) ) ) -> ( coeff ` G ) : NN0 --> CC )
88 elfznn0 
 |-  ( k e. ( 0 ... ( ( deg ` G ) - M ) ) -> k e. NN0 )
89 88 adantl 
 |-  ( ( ph /\ k e. ( 0 ... ( ( deg ` G ) - M ) ) ) -> k e. NN0 )
90 35 adantr 
 |-  ( ( ph /\ k e. ( 0 ... ( ( deg ` G ) - M ) ) ) -> M e. NN0 )
91 89 90 nn0addcld 
 |-  ( ( ph /\ k e. ( 0 ... ( ( deg ` G ) - M ) ) ) -> ( k + M ) e. NN0 )
92 87 91 ffvelrnd 
 |-  ( ( ph /\ k e. ( 0 ... ( ( deg ` G ) - M ) ) ) -> ( ( coeff ` G ) ` ( k + M ) ) e. CC )
93 eqidd 
 |-  ( ( ph /\ z e. CC ) -> ( 0 ... ( ( deg ` G ) - M ) ) = ( 0 ... ( ( deg ` G ) - M ) ) )
94 simpl 
 |-  ( ( ph /\ k e. ( 0 ... ( ( deg ` G ) - M ) ) ) -> ph )
95 7 a1i 
 |-  ( ph -> I = ( k e. NN0 |-> ( ( coeff ` G ) ` ( k + M ) ) ) )
96 95 56 fvmpt2d 
 |-  ( ( ph /\ k e. NN0 ) -> ( I ` k ) = ( ( coeff ` G ) ` ( k + M ) ) )
97 94 89 96 syl2anc 
 |-  ( ( ph /\ k e. ( 0 ... ( ( deg ` G ) - M ) ) ) -> ( I ` k ) = ( ( coeff ` G ) ` ( k + M ) ) )
98 97 adantlr 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... ( ( deg ` G ) - M ) ) ) -> ( I ` k ) = ( ( coeff ` G ) ` ( k + M ) ) )
99 98 oveq1d 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... ( ( deg ` G ) - M ) ) ) -> ( ( I ` k ) x. ( z ^ k ) ) = ( ( ( coeff ` G ) ` ( k + M ) ) x. ( z ^ k ) ) )
100 93 99 sumeq12rdv 
 |-  ( ( ph /\ z e. CC ) -> sum_ k e. ( 0 ... ( ( deg ` G ) - M ) ) ( ( I ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... ( ( deg ` G ) - M ) ) ( ( ( coeff ` G ) ` ( k + M ) ) x. ( z ^ k ) ) )
101 100 mpteq2dva 
 |-  ( ph -> ( z e. CC |-> sum_ k e. ( 0 ... ( ( deg ` G ) - M ) ) ( ( I ` k ) x. ( z ^ k ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... ( ( deg ` G ) - M ) ) ( ( ( coeff ` G ) ` ( k + M ) ) x. ( z ^ k ) ) ) )
102 9 101 eqtrd 
 |-  ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... ( ( deg ` G ) - M ) ) ( ( ( coeff ` G ) ` ( k + M ) ) x. ( z ^ k ) ) ) )
103 60 48 92 102 coeeq2 
 |-  ( ph -> ( coeff ` F ) = ( k e. NN0 |-> if ( k <_ ( ( deg ` G ) - M ) , ( ( coeff ` G ) ` ( k + M ) ) , 0 ) ) )
104 85 103 95 3eqtr4d 
 |-  ( ph -> ( coeff ` F ) = I )
105 104 fveq1d 
 |-  ( ph -> ( ( coeff ` F ) ` 0 ) = ( I ` 0 ) )
106 oveq1 
 |-  ( k = 0 -> ( k + M ) = ( 0 + M ) )
107 106 adantl 
 |-  ( ( ph /\ k = 0 ) -> ( k + M ) = ( 0 + M ) )
108 10 36 sseldi 
 |-  ( ph -> M e. CC )
109 108 addid2d 
 |-  ( ph -> ( 0 + M ) = M )
110 109 adantr 
 |-  ( ( ph /\ k = 0 ) -> ( 0 + M ) = M )
111 107 110 eqtrd 
 |-  ( ( ph /\ k = 0 ) -> ( k + M ) = M )
112 111 fveq2d 
 |-  ( ( ph /\ k = 0 ) -> ( ( coeff ` G ) ` ( k + M ) ) = ( ( coeff ` G ) ` M ) )
113 0nn0 
 |-  0 e. NN0
114 113 a1i 
 |-  ( ph -> 0 e. NN0 )
115 51 35 ffvelrnd 
 |-  ( ph -> ( ( coeff ` G ) ` M ) e. ZZ )
116 95 112 114 115 fvmptd 
 |-  ( ph -> ( I ` 0 ) = ( ( coeff ` G ) ` M ) )
117 eqidd 
 |-  ( ph -> ( ( coeff ` G ) ` M ) = ( ( coeff ` G ) ` M ) )
118 105 116 117 3eqtrd 
 |-  ( ph -> ( ( coeff ` F ) ` 0 ) = ( ( coeff ` G ) ` M ) )
119 38 33 eqeltrd 
 |-  ( ph -> M e. { n e. NN0 | ( ( coeff ` G ) ` n ) =/= 0 } )
120 fveq2 
 |-  ( n = M -> ( ( coeff ` G ) ` n ) = ( ( coeff ` G ) ` M ) )
121 120 neeq1d 
 |-  ( n = M -> ( ( ( coeff ` G ) ` n ) =/= 0 <-> ( ( coeff ` G ) ` M ) =/= 0 ) )
122 121 elrab 
 |-  ( M e. { n e. NN0 | ( ( coeff ` G ) ` n ) =/= 0 } <-> ( M e. NN0 /\ ( ( coeff ` G ) ` M ) =/= 0 ) )
123 119 122 sylib 
 |-  ( ph -> ( M e. NN0 /\ ( ( coeff ` G ) ` M ) =/= 0 ) )
124 123 simprd 
 |-  ( ph -> ( ( coeff ` G ) ` M ) =/= 0 )
125 118 124 eqnetrd 
 |-  ( ph -> ( ( coeff ` F ) ` 0 ) =/= 0 )
126 3 49 syl 
 |-  ( ph -> 0 e. ZZ )
127 aasscn 
 |-  AA C_ CC
128 127 1 sseldi 
 |-  ( ph -> A e. CC )
129 94 128 syl 
 |-  ( ( ph /\ k e. ( 0 ... ( ( deg ` G ) - M ) ) ) -> A e. CC )
130 129 89 expcld 
 |-  ( ( ph /\ k e. ( 0 ... ( ( deg ` G ) - M ) ) ) -> ( A ^ k ) e. CC )
131 92 130 mulcld 
 |-  ( ( ph /\ k e. ( 0 ... ( ( deg ` G ) - M ) ) ) -> ( ( ( coeff ` G ) ` ( k + M ) ) x. ( A ^ k ) ) e. CC )
132 fvoveq1 
 |-  ( k = ( j - M ) -> ( ( coeff ` G ) ` ( k + M ) ) = ( ( coeff ` G ) ` ( ( j - M ) + M ) ) )
133 oveq2 
 |-  ( k = ( j - M ) -> ( A ^ k ) = ( A ^ ( j - M ) ) )
134 132 133 oveq12d 
 |-  ( k = ( j - M ) -> ( ( ( coeff ` G ) ` ( k + M ) ) x. ( A ^ k ) ) = ( ( ( coeff ` G ) ` ( ( j - M ) + M ) ) x. ( A ^ ( j - M ) ) ) )
135 36 126 37 131 134 fsumshft 
 |-  ( ph -> sum_ k e. ( 0 ... ( ( deg ` G ) - M ) ) ( ( ( coeff ` G ) ` ( k + M ) ) x. ( A ^ k ) ) = sum_ j e. ( ( 0 + M ) ... ( ( ( deg ` G ) - M ) + M ) ) ( ( ( coeff ` G ) ` ( ( j - M ) + M ) ) x. ( A ^ ( j - M ) ) ) )
136 10 14 sseldi 
 |-  ( ph -> ( deg ` G ) e. CC )
137 136 108 npcand 
 |-  ( ph -> ( ( ( deg ` G ) - M ) + M ) = ( deg ` G ) )
138 109 137 oveq12d 
 |-  ( ph -> ( ( 0 + M ) ... ( ( ( deg ` G ) - M ) + M ) ) = ( M ... ( deg ` G ) ) )
139 138 sumeq1d 
 |-  ( ph -> sum_ j e. ( ( 0 + M ) ... ( ( ( deg ` G ) - M ) + M ) ) ( ( ( coeff ` G ) ` ( ( j - M ) + M ) ) x. ( A ^ ( j - M ) ) ) = sum_ j e. ( M ... ( deg ` G ) ) ( ( ( coeff ` G ) ` ( ( j - M ) + M ) ) x. ( A ^ ( j - M ) ) ) )
140 elfzelz 
 |-  ( j e. ( M ... ( deg ` G ) ) -> j e. ZZ )
141 140 adantl 
 |-  ( ( ph /\ j e. ( M ... ( deg ` G ) ) ) -> j e. ZZ )
142 10 141 sseldi 
 |-  ( ( ph /\ j e. ( M ... ( deg ` G ) ) ) -> j e. CC )
143 108 adantr 
 |-  ( ( ph /\ j e. ( M ... ( deg ` G ) ) ) -> M e. CC )
144 142 143 npcand 
 |-  ( ( ph /\ j e. ( M ... ( deg ` G ) ) ) -> ( ( j - M ) + M ) = j )
145 144 fveq2d 
 |-  ( ( ph /\ j e. ( M ... ( deg ` G ) ) ) -> ( ( coeff ` G ) ` ( ( j - M ) + M ) ) = ( ( coeff ` G ) ` j ) )
146 145 oveq1d 
 |-  ( ( ph /\ j e. ( M ... ( deg ` G ) ) ) -> ( ( ( coeff ` G ) ` ( ( j - M ) + M ) ) x. ( A ^ ( j - M ) ) ) = ( ( ( coeff ` G ) ` j ) x. ( A ^ ( j - M ) ) ) )
147 128 adantr 
 |-  ( ( ph /\ j e. ( M ... ( deg ` G ) ) ) -> A e. CC )
148 2 adantr 
 |-  ( ( ph /\ j e. ( M ... ( deg ` G ) ) ) -> A =/= 0 )
149 36 adantr 
 |-  ( ( ph /\ j e. ( M ... ( deg ` G ) ) ) -> M e. ZZ )
150 147 148 149 141 expsubd 
 |-  ( ( ph /\ j e. ( M ... ( deg ` G ) ) ) -> ( A ^ ( j - M ) ) = ( ( A ^ j ) / ( A ^ M ) ) )
151 150 oveq2d 
 |-  ( ( ph /\ j e. ( M ... ( deg ` G ) ) ) -> ( ( ( coeff ` G ) ` j ) x. ( A ^ ( j - M ) ) ) = ( ( ( coeff ` G ) ` j ) x. ( ( A ^ j ) / ( A ^ M ) ) ) )
152 86 adantr 
 |-  ( ( ph /\ j e. ( M ... ( deg ` G ) ) ) -> ( coeff ` G ) : NN0 --> CC )
153 0red 
 |-  ( ( ph /\ j e. ( M ... ( deg ` G ) ) ) -> 0 e. RR )
154 43 adantr 
 |-  ( ( ph /\ j e. ( M ... ( deg ` G ) ) ) -> M e. RR )
155 141 zred 
 |-  ( ( ph /\ j e. ( M ... ( deg ` G ) ) ) -> j e. RR )
156 35 nn0ge0d 
 |-  ( ph -> 0 <_ M )
157 156 adantr 
 |-  ( ( ph /\ j e. ( M ... ( deg ` G ) ) ) -> 0 <_ M )
158 elfzle1 
 |-  ( j e. ( M ... ( deg ` G ) ) -> M <_ j )
159 158 adantl 
 |-  ( ( ph /\ j e. ( M ... ( deg ` G ) ) ) -> M <_ j )
160 153 154 155 157 159 letrd 
 |-  ( ( ph /\ j e. ( M ... ( deg ` G ) ) ) -> 0 <_ j )
161 141 160 jca 
 |-  ( ( ph /\ j e. ( M ... ( deg ` G ) ) ) -> ( j e. ZZ /\ 0 <_ j ) )
162 elnn0z 
 |-  ( j e. NN0 <-> ( j e. ZZ /\ 0 <_ j ) )
163 161 162 sylibr 
 |-  ( ( ph /\ j e. ( M ... ( deg ` G ) ) ) -> j e. NN0 )
164 152 163 ffvelrnd 
 |-  ( ( ph /\ j e. ( M ... ( deg ` G ) ) ) -> ( ( coeff ` G ) ` j ) e. CC )
165 147 163 expcld 
 |-  ( ( ph /\ j e. ( M ... ( deg ` G ) ) ) -> ( A ^ j ) e. CC )
166 128 35 expcld 
 |-  ( ph -> ( A ^ M ) e. CC )
167 166 adantr 
 |-  ( ( ph /\ j e. ( M ... ( deg ` G ) ) ) -> ( A ^ M ) e. CC )
168 147 148 149 expne0d 
 |-  ( ( ph /\ j e. ( M ... ( deg ` G ) ) ) -> ( A ^ M ) =/= 0 )
169 164 165 167 168 divassd 
 |-  ( ( ph /\ j e. ( M ... ( deg ` G ) ) ) -> ( ( ( ( coeff ` G ) ` j ) x. ( A ^ j ) ) / ( A ^ M ) ) = ( ( ( coeff ` G ) ` j ) x. ( ( A ^ j ) / ( A ^ M ) ) ) )
170 169 eqcomd 
 |-  ( ( ph /\ j e. ( M ... ( deg ` G ) ) ) -> ( ( ( coeff ` G ) ` j ) x. ( ( A ^ j ) / ( A ^ M ) ) ) = ( ( ( ( coeff ` G ) ` j ) x. ( A ^ j ) ) / ( A ^ M ) ) )
171 151 170 eqtr2d 
 |-  ( ( ph /\ j e. ( M ... ( deg ` G ) ) ) -> ( ( ( ( coeff ` G ) ` j ) x. ( A ^ j ) ) / ( A ^ M ) ) = ( ( ( coeff ` G ) ` j ) x. ( A ^ ( j - M ) ) ) )
172 146 171 eqtr4d 
 |-  ( ( ph /\ j e. ( M ... ( deg ` G ) ) ) -> ( ( ( coeff ` G ) ` ( ( j - M ) + M ) ) x. ( A ^ ( j - M ) ) ) = ( ( ( ( coeff ` G ) ` j ) x. ( A ^ j ) ) / ( A ^ M ) ) )
173 172 sumeq2dv 
 |-  ( ph -> sum_ j e. ( M ... ( deg ` G ) ) ( ( ( coeff ` G ) ` ( ( j - M ) + M ) ) x. ( A ^ ( j - M ) ) ) = sum_ j e. ( M ... ( deg ` G ) ) ( ( ( ( coeff ` G ) ` j ) x. ( A ^ j ) ) / ( A ^ M ) ) )
174 139 173 eqtrd 
 |-  ( ph -> sum_ j e. ( ( 0 + M ) ... ( ( ( deg ` G ) - M ) + M ) ) ( ( ( coeff ` G ) ` ( ( j - M ) + M ) ) x. ( A ^ ( j - M ) ) ) = sum_ j e. ( M ... ( deg ` G ) ) ( ( ( ( coeff ` G ) ` j ) x. ( A ^ j ) ) / ( A ^ M ) ) )
175 35 16 eleqtrdi 
 |-  ( ph -> M e. ( ZZ>= ` 0 ) )
176 fzss1 
 |-  ( M e. ( ZZ>= ` 0 ) -> ( M ... ( deg ` G ) ) C_ ( 0 ... ( deg ` G ) ) )
177 175 176 syl 
 |-  ( ph -> ( M ... ( deg ` G ) ) C_ ( 0 ... ( deg ` G ) ) )
178 164 165 mulcld 
 |-  ( ( ph /\ j e. ( M ... ( deg ` G ) ) ) -> ( ( ( coeff ` G ) ` j ) x. ( A ^ j ) ) e. CC )
179 178 167 168 divcld 
 |-  ( ( ph /\ j e. ( M ... ( deg ` G ) ) ) -> ( ( ( ( coeff ` G ) ` j ) x. ( A ^ j ) ) / ( A ^ M ) ) e. CC )
180 36 ad2antrr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. j < M ) -> M e. ZZ )
181 14 ad2antrr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. j < M ) -> ( deg ` G ) e. ZZ )
182 eldifi 
 |-  ( j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) -> j e. ( 0 ... ( deg ` G ) ) )
183 elfznn0 
 |-  ( j e. ( 0 ... ( deg ` G ) ) -> j e. NN0 )
184 183 nn0zd 
 |-  ( j e. ( 0 ... ( deg ` G ) ) -> j e. ZZ )
185 182 184 syl 
 |-  ( j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) -> j e. ZZ )
186 185 ad2antlr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. j < M ) -> j e. ZZ )
187 180 181 186 3jca 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. j < M ) -> ( M e. ZZ /\ ( deg ` G ) e. ZZ /\ j e. ZZ ) )
188 simpr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. j < M ) -> -. j < M )
189 43 ad2antrr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. j < M ) -> M e. RR )
190 186 zred 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. j < M ) -> j e. RR )
191 189 190 lenltd 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. j < M ) -> ( M <_ j <-> -. j < M ) )
192 188 191 mpbird 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. j < M ) -> M <_ j )
193 elfzle2 
 |-  ( j e. ( 0 ... ( deg ` G ) ) -> j <_ ( deg ` G ) )
194 182 193 syl 
 |-  ( j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) -> j <_ ( deg ` G ) )
195 194 ad2antlr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. j < M ) -> j <_ ( deg ` G ) )
196 187 192 195 jca32 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. j < M ) -> ( ( M e. ZZ /\ ( deg ` G ) e. ZZ /\ j e. ZZ ) /\ ( M <_ j /\ j <_ ( deg ` G ) ) ) )
197 elfz2 
 |-  ( j e. ( M ... ( deg ` G ) ) <-> ( ( M e. ZZ /\ ( deg ` G ) e. ZZ /\ j e. ZZ ) /\ ( M <_ j /\ j <_ ( deg ` G ) ) ) )
198 196 197 sylibr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. j < M ) -> j e. ( M ... ( deg ` G ) ) )
199 eldifn 
 |-  ( j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) -> -. j e. ( M ... ( deg ` G ) ) )
200 199 ad2antlr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. j < M ) -> -. j e. ( M ... ( deg ` G ) ) )
201 198 200 condan 
 |-  ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) -> j < M )
202 201 adantr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. ( ( coeff ` G ) ` j ) = 0 ) -> j < M )
203 6 a1i 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. ( ( coeff ` G ) ` j ) = 0 ) -> M = inf ( { n e. NN0 | ( ( coeff ` G ) ` n ) =/= 0 } , RR , < ) )
204 17 a1i 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. ( ( coeff ` G ) ` j ) = 0 ) -> { n e. NN0 | ( ( coeff ` G ) ` n ) =/= 0 } C_ ( ZZ>= ` 0 ) )
205 182 183 syl 
 |-  ( j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) -> j e. NN0 )
206 205 adantr 
 |-  ( ( j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) /\ -. ( ( coeff ` G ) ` j ) = 0 ) -> j e. NN0 )
207 neqne 
 |-  ( -. ( ( coeff ` G ) ` j ) = 0 -> ( ( coeff ` G ) ` j ) =/= 0 )
208 207 adantl 
 |-  ( ( j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) /\ -. ( ( coeff ` G ) ` j ) = 0 ) -> ( ( coeff ` G ) ` j ) =/= 0 )
209 206 208 jca 
 |-  ( ( j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) /\ -. ( ( coeff ` G ) ` j ) = 0 ) -> ( j e. NN0 /\ ( ( coeff ` G ) ` j ) =/= 0 ) )
210 fveq2 
 |-  ( n = j -> ( ( coeff ` G ) ` n ) = ( ( coeff ` G ) ` j ) )
211 210 neeq1d 
 |-  ( n = j -> ( ( ( coeff ` G ) ` n ) =/= 0 <-> ( ( coeff ` G ) ` j ) =/= 0 ) )
212 211 elrab 
 |-  ( j e. { n e. NN0 | ( ( coeff ` G ) ` n ) =/= 0 } <-> ( j e. NN0 /\ ( ( coeff ` G ) ` j ) =/= 0 ) )
213 209 212 sylibr 
 |-  ( ( j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) /\ -. ( ( coeff ` G ) ` j ) = 0 ) -> j e. { n e. NN0 | ( ( coeff ` G ) ` n ) =/= 0 } )
214 213 adantll 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. ( ( coeff ` G ) ` j ) = 0 ) -> j e. { n e. NN0 | ( ( coeff ` G ) ` n ) =/= 0 } )
215 infssuzle 
 |-  ( ( { n e. NN0 | ( ( coeff ` G ) ` n ) =/= 0 } C_ ( ZZ>= ` 0 ) /\ j e. { n e. NN0 | ( ( coeff ` G ) ` n ) =/= 0 } ) -> inf ( { n e. NN0 | ( ( coeff ` G ) ` n ) =/= 0 } , RR , < ) <_ j )
216 204 214 215 syl2anc 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. ( ( coeff ` G ) ` j ) = 0 ) -> inf ( { n e. NN0 | ( ( coeff ` G ) ` n ) =/= 0 } , RR , < ) <_ j )
217 203 216 eqbrtrd 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. ( ( coeff ` G ) ` j ) = 0 ) -> M <_ j )
218 43 ad2antrr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. ( ( coeff ` G ) ` j ) = 0 ) -> M e. RR )
219 185 zred 
 |-  ( j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) -> j e. RR )
220 219 ad2antlr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. ( ( coeff ` G ) ` j ) = 0 ) -> j e. RR )
221 218 220 lenltd 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. ( ( coeff ` G ) ` j ) = 0 ) -> ( M <_ j <-> -. j < M ) )
222 217 221 mpbid 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. ( ( coeff ` G ) ` j ) = 0 ) -> -. j < M )
223 202 222 condan 
 |-  ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) -> ( ( coeff ` G ) ` j ) = 0 )
224 223 oveq1d 
 |-  ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) -> ( ( ( coeff ` G ) ` j ) x. ( A ^ j ) ) = ( 0 x. ( A ^ j ) ) )
225 128 adantr 
 |-  ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) -> A e. CC )
226 205 adantl 
 |-  ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) -> j e. NN0 )
227 225 226 expcld 
 |-  ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) -> ( A ^ j ) e. CC )
228 227 mul02d 
 |-  ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) -> ( 0 x. ( A ^ j ) ) = 0 )
229 224 228 eqtrd 
 |-  ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) -> ( ( ( coeff ` G ) ` j ) x. ( A ^ j ) ) = 0 )
230 229 oveq1d 
 |-  ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) -> ( ( ( ( coeff ` G ) ` j ) x. ( A ^ j ) ) / ( A ^ M ) ) = ( 0 / ( A ^ M ) ) )
231 128 2 36 expne0d 
 |-  ( ph -> ( A ^ M ) =/= 0 )
232 166 231 div0d 
 |-  ( ph -> ( 0 / ( A ^ M ) ) = 0 )
233 232 adantr 
 |-  ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) -> ( 0 / ( A ^ M ) ) = 0 )
234 230 233 eqtrd 
 |-  ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) -> ( ( ( ( coeff ` G ) ` j ) x. ( A ^ j ) ) / ( A ^ M ) ) = 0 )
235 fzfid 
 |-  ( ph -> ( 0 ... ( deg ` G ) ) e. Fin )
236 177 179 234 235 fsumss 
 |-  ( ph -> sum_ j e. ( M ... ( deg ` G ) ) ( ( ( ( coeff ` G ) ` j ) x. ( A ^ j ) ) / ( A ^ M ) ) = sum_ j e. ( 0 ... ( deg ` G ) ) ( ( ( ( coeff ` G ) ` j ) x. ( A ^ j ) ) / ( A ^ M ) ) )
237 135 174 236 3eqtrd 
 |-  ( ph -> sum_ k e. ( 0 ... ( ( deg ` G ) - M ) ) ( ( ( coeff ` G ) ` ( k + M ) ) x. ( A ^ k ) ) = sum_ j e. ( 0 ... ( deg ` G ) ) ( ( ( ( coeff ` G ) ` j ) x. ( A ^ j ) ) / ( A ^ M ) ) )
238 89 56 syldan 
 |-  ( ( ph /\ k e. ( 0 ... ( ( deg ` G ) - M ) ) ) -> ( ( coeff ` G ) ` ( k + M ) ) e. ZZ )
239 7 fvmpt2 
 |-  ( ( k e. NN0 /\ ( ( coeff ` G ) ` ( k + M ) ) e. ZZ ) -> ( I ` k ) = ( ( coeff ` G ) ` ( k + M ) ) )
240 89 238 239 syl2anc 
 |-  ( ( ph /\ k e. ( 0 ... ( ( deg ` G ) - M ) ) ) -> ( I ` k ) = ( ( coeff ` G ) ` ( k + M ) ) )
241 240 adantlr 
 |-  ( ( ( ph /\ z = A ) /\ k e. ( 0 ... ( ( deg ` G ) - M ) ) ) -> ( I ` k ) = ( ( coeff ` G ) ` ( k + M ) ) )
242 oveq1 
 |-  ( z = A -> ( z ^ k ) = ( A ^ k ) )
243 242 ad2antlr 
 |-  ( ( ( ph /\ z = A ) /\ k e. ( 0 ... ( ( deg ` G ) - M ) ) ) -> ( z ^ k ) = ( A ^ k ) )
244 241 243 oveq12d 
 |-  ( ( ( ph /\ z = A ) /\ k e. ( 0 ... ( ( deg ` G ) - M ) ) ) -> ( ( I ` k ) x. ( z ^ k ) ) = ( ( ( coeff ` G ) ` ( k + M ) ) x. ( A ^ k ) ) )
245 244 sumeq2dv 
 |-  ( ( ph /\ z = A ) -> sum_ k e. ( 0 ... ( ( deg ` G ) - M ) ) ( ( I ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... ( ( deg ` G ) - M ) ) ( ( ( coeff ` G ) ` ( k + M ) ) x. ( A ^ k ) ) )
246 fzfid 
 |-  ( ph -> ( 0 ... ( ( deg ` G ) - M ) ) e. Fin )
247 246 131 fsumcl 
 |-  ( ph -> sum_ k e. ( 0 ... ( ( deg ` G ) - M ) ) ( ( ( coeff ` G ) ` ( k + M ) ) x. ( A ^ k ) ) e. CC )
248 9 245 128 247 fvmptd 
 |-  ( ph -> ( F ` A ) = sum_ k e. ( 0 ... ( ( deg ` G ) - M ) ) ( ( ( coeff ` G ) ` ( k + M ) ) x. ( A ^ k ) ) )
249 21 20 coeid2 
 |-  ( ( G e. ( Poly ` ZZ ) /\ A e. CC ) -> ( G ` A ) = sum_ j e. ( 0 ... ( deg ` G ) ) ( ( ( coeff ` G ) ` j ) x. ( A ^ j ) ) )
250 3 128 249 syl2anc 
 |-  ( ph -> ( G ` A ) = sum_ j e. ( 0 ... ( deg ` G ) ) ( ( ( coeff ` G ) ` j ) x. ( A ^ j ) ) )
251 250 oveq1d 
 |-  ( ph -> ( ( G ` A ) / ( A ^ M ) ) = ( sum_ j e. ( 0 ... ( deg ` G ) ) ( ( ( coeff ` G ) ` j ) x. ( A ^ j ) ) / ( A ^ M ) ) )
252 86 adantr 
 |-  ( ( ph /\ j e. ( 0 ... ( deg ` G ) ) ) -> ( coeff ` G ) : NN0 --> CC )
253 183 adantl 
 |-  ( ( ph /\ j e. ( 0 ... ( deg ` G ) ) ) -> j e. NN0 )
254 252 253 ffvelrnd 
 |-  ( ( ph /\ j e. ( 0 ... ( deg ` G ) ) ) -> ( ( coeff ` G ) ` j ) e. CC )
255 128 adantr 
 |-  ( ( ph /\ j e. ( 0 ... ( deg ` G ) ) ) -> A e. CC )
256 255 253 expcld 
 |-  ( ( ph /\ j e. ( 0 ... ( deg ` G ) ) ) -> ( A ^ j ) e. CC )
257 254 256 mulcld 
 |-  ( ( ph /\ j e. ( 0 ... ( deg ` G ) ) ) -> ( ( ( coeff ` G ) ` j ) x. ( A ^ j ) ) e. CC )
258 235 166 257 231 fsumdivc 
 |-  ( ph -> ( sum_ j e. ( 0 ... ( deg ` G ) ) ( ( ( coeff ` G ) ` j ) x. ( A ^ j ) ) / ( A ^ M ) ) = sum_ j e. ( 0 ... ( deg ` G ) ) ( ( ( ( coeff ` G ) ` j ) x. ( A ^ j ) ) / ( A ^ M ) ) )
259 251 258 eqtrd 
 |-  ( ph -> ( ( G ` A ) / ( A ^ M ) ) = sum_ j e. ( 0 ... ( deg ` G ) ) ( ( ( ( coeff ` G ) ` j ) x. ( A ^ j ) ) / ( A ^ M ) ) )
260 237 248 259 3eqtr4d 
 |-  ( ph -> ( F ` A ) = ( ( G ` A ) / ( A ^ M ) ) )
261 5 oveq1d 
 |-  ( ph -> ( ( G ` A ) / ( A ^ M ) ) = ( 0 / ( A ^ M ) ) )
262 260 261 232 3eqtrd 
 |-  ( ph -> ( F ` A ) = 0 )
263 125 262 jca 
 |-  ( ph -> ( ( ( coeff ` F ) ` 0 ) =/= 0 /\ ( F ` A ) = 0 ) )
264 fveq2 
 |-  ( f = F -> ( coeff ` f ) = ( coeff ` F ) )
265 264 fveq1d 
 |-  ( f = F -> ( ( coeff ` f ) ` 0 ) = ( ( coeff ` F ) ` 0 ) )
266 265 neeq1d 
 |-  ( f = F -> ( ( ( coeff ` f ) ` 0 ) =/= 0 <-> ( ( coeff ` F ) ` 0 ) =/= 0 ) )
267 fveq1 
 |-  ( f = F -> ( f ` A ) = ( F ` A ) )
268 267 eqeq1d 
 |-  ( f = F -> ( ( f ` A ) = 0 <-> ( F ` A ) = 0 ) )
269 266 268 anbi12d 
 |-  ( f = F -> ( ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 ) <-> ( ( ( coeff ` F ) ` 0 ) =/= 0 /\ ( F ` A ) = 0 ) ) )
270 269 rspcev 
 |-  ( ( F e. ( Poly ` ZZ ) /\ ( ( ( coeff ` F ) ` 0 ) =/= 0 /\ ( F ` A ) = 0 ) ) -> E. f e. ( Poly ` ZZ ) ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 ) )
271 60 263 270 syl2anc 
 |-  ( ph -> E. f e. ( Poly ` ZZ ) ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 ) )