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 sselid 
 |-  ( 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 sselid 
 |-  ( 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 sselid 
 |-  ( 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 sselid 
 |-  ( 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 sselid 
 |-  ( ( 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 182 elfzelzd 
 |-  ( j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) -> j e. ZZ )
184 183 ad2antlr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. j < M ) -> j e. ZZ )
185 simpr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. j < M ) -> -. j < M )
186 43 ad2antrr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. j < M ) -> M e. RR )
187 184 zred 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. j < M ) -> j e. RR )
188 186 187 lenltd 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. j < M ) -> ( M <_ j <-> -. j < M ) )
189 185 188 mpbird 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. j < M ) -> M <_ j )
190 elfzle2 
 |-  ( j e. ( 0 ... ( deg ` G ) ) -> j <_ ( deg ` G ) )
191 182 190 syl 
 |-  ( j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) -> j <_ ( deg ` G ) )
192 191 ad2antlr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. j < M ) -> j <_ ( deg ` G ) )
193 180 181 184 189 192 elfzd 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. j < M ) -> j e. ( M ... ( deg ` G ) ) )
194 eldifn 
 |-  ( j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) -> -. j e. ( M ... ( deg ` G ) ) )
195 194 ad2antlr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. j < M ) -> -. j e. ( M ... ( deg ` G ) ) )
196 193 195 condan 
 |-  ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) -> j < M )
197 196 adantr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. ( ( coeff ` G ) ` j ) = 0 ) -> j < M )
198 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 , < ) )
199 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 ) )
200 elfznn0 
 |-  ( j e. ( 0 ... ( deg ` G ) ) -> j e. NN0 )
201 182 200 syl 
 |-  ( j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) -> j e. NN0 )
202 201 adantr 
 |-  ( ( j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) /\ -. ( ( coeff ` G ) ` j ) = 0 ) -> j e. NN0 )
203 neqne 
 |-  ( -. ( ( coeff ` G ) ` j ) = 0 -> ( ( coeff ` G ) ` j ) =/= 0 )
204 203 adantl 
 |-  ( ( j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) /\ -. ( ( coeff ` G ) ` j ) = 0 ) -> ( ( coeff ` G ) ` j ) =/= 0 )
205 202 204 jca 
 |-  ( ( j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) /\ -. ( ( coeff ` G ) ` j ) = 0 ) -> ( j e. NN0 /\ ( ( coeff ` G ) ` j ) =/= 0 ) )
206 fveq2 
 |-  ( n = j -> ( ( coeff ` G ) ` n ) = ( ( coeff ` G ) ` j ) )
207 206 neeq1d 
 |-  ( n = j -> ( ( ( coeff ` G ) ` n ) =/= 0 <-> ( ( coeff ` G ) ` j ) =/= 0 ) )
208 207 elrab 
 |-  ( j e. { n e. NN0 | ( ( coeff ` G ) ` n ) =/= 0 } <-> ( j e. NN0 /\ ( ( coeff ` G ) ` j ) =/= 0 ) )
209 205 208 sylibr 
 |-  ( ( j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) /\ -. ( ( coeff ` G ) ` j ) = 0 ) -> j e. { n e. NN0 | ( ( coeff ` G ) ` n ) =/= 0 } )
210 209 adantll 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. ( ( coeff ` G ) ` j ) = 0 ) -> j e. { n e. NN0 | ( ( coeff ` G ) ` n ) =/= 0 } )
211 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 )
212 199 210 211 syl2anc 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. ( ( coeff ` G ) ` j ) = 0 ) -> inf ( { n e. NN0 | ( ( coeff ` G ) ` n ) =/= 0 } , RR , < ) <_ j )
213 198 212 eqbrtrd 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. ( ( coeff ` G ) ` j ) = 0 ) -> M <_ j )
214 43 ad2antrr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. ( ( coeff ` G ) ` j ) = 0 ) -> M e. RR )
215 183 zred 
 |-  ( j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) -> j e. RR )
216 215 ad2antlr 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. ( ( coeff ` G ) ` j ) = 0 ) -> j e. RR )
217 214 216 lenltd 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. ( ( coeff ` G ) ` j ) = 0 ) -> ( M <_ j <-> -. j < M ) )
218 213 217 mpbid 
 |-  ( ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) /\ -. ( ( coeff ` G ) ` j ) = 0 ) -> -. j < M )
219 197 218 condan 
 |-  ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) -> ( ( coeff ` G ) ` j ) = 0 )
220 219 oveq1d 
 |-  ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) -> ( ( ( coeff ` G ) ` j ) x. ( A ^ j ) ) = ( 0 x. ( A ^ j ) ) )
221 128 adantr 
 |-  ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) -> A e. CC )
222 201 adantl 
 |-  ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) -> j e. NN0 )
223 221 222 expcld 
 |-  ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) -> ( A ^ j ) e. CC )
224 223 mul02d 
 |-  ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) -> ( 0 x. ( A ^ j ) ) = 0 )
225 220 224 eqtrd 
 |-  ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) -> ( ( ( coeff ` G ) ` j ) x. ( A ^ j ) ) = 0 )
226 225 oveq1d 
 |-  ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) -> ( ( ( ( coeff ` G ) ` j ) x. ( A ^ j ) ) / ( A ^ M ) ) = ( 0 / ( A ^ M ) ) )
227 128 2 36 expne0d 
 |-  ( ph -> ( A ^ M ) =/= 0 )
228 166 227 div0d 
 |-  ( ph -> ( 0 / ( A ^ M ) ) = 0 )
229 228 adantr 
 |-  ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) -> ( 0 / ( A ^ M ) ) = 0 )
230 226 229 eqtrd 
 |-  ( ( ph /\ j e. ( ( 0 ... ( deg ` G ) ) \ ( M ... ( deg ` G ) ) ) ) -> ( ( ( ( coeff ` G ) ` j ) x. ( A ^ j ) ) / ( A ^ M ) ) = 0 )
231 fzfid 
 |-  ( ph -> ( 0 ... ( deg ` G ) ) e. Fin )
232 177 179 230 231 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 ) ) )
233 135 174 232 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 ) ) )
234 89 56 syldan 
 |-  ( ( ph /\ k e. ( 0 ... ( ( deg ` G ) - M ) ) ) -> ( ( coeff ` G ) ` ( k + M ) ) e. ZZ )
235 7 fvmpt2 
 |-  ( ( k e. NN0 /\ ( ( coeff ` G ) ` ( k + M ) ) e. ZZ ) -> ( I ` k ) = ( ( coeff ` G ) ` ( k + M ) ) )
236 89 234 235 syl2anc 
 |-  ( ( ph /\ k e. ( 0 ... ( ( deg ` G ) - M ) ) ) -> ( I ` k ) = ( ( coeff ` G ) ` ( k + M ) ) )
237 236 adantlr 
 |-  ( ( ( ph /\ z = A ) /\ k e. ( 0 ... ( ( deg ` G ) - M ) ) ) -> ( I ` k ) = ( ( coeff ` G ) ` ( k + M ) ) )
238 oveq1 
 |-  ( z = A -> ( z ^ k ) = ( A ^ k ) )
239 238 ad2antlr 
 |-  ( ( ( ph /\ z = A ) /\ k e. ( 0 ... ( ( deg ` G ) - M ) ) ) -> ( z ^ k ) = ( A ^ k ) )
240 237 239 oveq12d 
 |-  ( ( ( ph /\ z = A ) /\ k e. ( 0 ... ( ( deg ` G ) - M ) ) ) -> ( ( I ` k ) x. ( z ^ k ) ) = ( ( ( coeff ` G ) ` ( k + M ) ) x. ( A ^ k ) ) )
241 240 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 ) ) )
242 fzfid 
 |-  ( ph -> ( 0 ... ( ( deg ` G ) - M ) ) e. Fin )
243 242 131 fsumcl 
 |-  ( ph -> sum_ k e. ( 0 ... ( ( deg ` G ) - M ) ) ( ( ( coeff ` G ) ` ( k + M ) ) x. ( A ^ k ) ) e. CC )
244 9 241 128 243 fvmptd 
 |-  ( ph -> ( F ` A ) = sum_ k e. ( 0 ... ( ( deg ` G ) - M ) ) ( ( ( coeff ` G ) ` ( k + M ) ) x. ( A ^ k ) ) )
245 21 20 coeid2 
 |-  ( ( G e. ( Poly ` ZZ ) /\ A e. CC ) -> ( G ` A ) = sum_ j e. ( 0 ... ( deg ` G ) ) ( ( ( coeff ` G ) ` j ) x. ( A ^ j ) ) )
246 3 128 245 syl2anc 
 |-  ( ph -> ( G ` A ) = sum_ j e. ( 0 ... ( deg ` G ) ) ( ( ( coeff ` G ) ` j ) x. ( A ^ j ) ) )
247 246 oveq1d 
 |-  ( ph -> ( ( G ` A ) / ( A ^ M ) ) = ( sum_ j e. ( 0 ... ( deg ` G ) ) ( ( ( coeff ` G ) ` j ) x. ( A ^ j ) ) / ( A ^ M ) ) )
248 86 adantr 
 |-  ( ( ph /\ j e. ( 0 ... ( deg ` G ) ) ) -> ( coeff ` G ) : NN0 --> CC )
249 200 adantl 
 |-  ( ( ph /\ j e. ( 0 ... ( deg ` G ) ) ) -> j e. NN0 )
250 248 249 ffvelrnd 
 |-  ( ( ph /\ j e. ( 0 ... ( deg ` G ) ) ) -> ( ( coeff ` G ) ` j ) e. CC )
251 128 adantr 
 |-  ( ( ph /\ j e. ( 0 ... ( deg ` G ) ) ) -> A e. CC )
252 251 249 expcld 
 |-  ( ( ph /\ j e. ( 0 ... ( deg ` G ) ) ) -> ( A ^ j ) e. CC )
253 250 252 mulcld 
 |-  ( ( ph /\ j e. ( 0 ... ( deg ` G ) ) ) -> ( ( ( coeff ` G ) ` j ) x. ( A ^ j ) ) e. CC )
254 231 166 253 227 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 ) ) )
255 247 254 eqtrd 
 |-  ( ph -> ( ( G ` A ) / ( A ^ M ) ) = sum_ j e. ( 0 ... ( deg ` G ) ) ( ( ( ( coeff ` G ) ` j ) x. ( A ^ j ) ) / ( A ^ M ) ) )
256 233 244 255 3eqtr4d 
 |-  ( ph -> ( F ` A ) = ( ( G ` A ) / ( A ^ M ) ) )
257 5 oveq1d 
 |-  ( ph -> ( ( G ` A ) / ( A ^ M ) ) = ( 0 / ( A ^ M ) ) )
258 256 257 228 3eqtrd 
 |-  ( ph -> ( F ` A ) = 0 )
259 125 258 jca 
 |-  ( ph -> ( ( ( coeff ` F ) ` 0 ) =/= 0 /\ ( F ` A ) = 0 ) )
260 fveq2 
 |-  ( f = F -> ( coeff ` f ) = ( coeff ` F ) )
261 260 fveq1d 
 |-  ( f = F -> ( ( coeff ` f ) ` 0 ) = ( ( coeff ` F ) ` 0 ) )
262 261 neeq1d 
 |-  ( f = F -> ( ( ( coeff ` f ) ` 0 ) =/= 0 <-> ( ( coeff ` F ) ` 0 ) =/= 0 ) )
263 fveq1 
 |-  ( f = F -> ( f ` A ) = ( F ` A ) )
264 263 eqeq1d 
 |-  ( f = F -> ( ( f ` A ) = 0 <-> ( F ` A ) = 0 ) )
265 262 264 anbi12d 
 |-  ( f = F -> ( ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 ) <-> ( ( ( coeff ` F ) ` 0 ) =/= 0 /\ ( F ` A ) = 0 ) ) )
266 265 rspcev 
 |-  ( ( F e. ( Poly ` ZZ ) /\ ( ( ( coeff ` F ) ` 0 ) =/= 0 /\ ( F ` A ) = 0 ) ) -> E. f e. ( Poly ` ZZ ) ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 ) )
267 60 259 266 syl2anc 
 |-  ( ph -> E. f e. ( Poly ` ZZ ) ( ( ( coeff ` f ) ` 0 ) =/= 0 /\ ( f ` A ) = 0 ) )