Metamath Proof Explorer

Theorem elqaalem3

Description: Lemma for elqaa . (Contributed by Mario Carneiro, 23-Jul-2014) (Revised by AV, 3-Oct-2020)

Ref Expression
Hypotheses elqaa.1 
|- ( ph -> A e. CC )
elqaa.2 
|- ( ph -> F e. ( ( Poly ` QQ ) \ { 0p } ) )
elqaa.3 
|- ( ph -> ( F ` A ) = 0 )
elqaa.4 
|- B = ( coeff ` F )
elqaa.5 
|- N = ( k e. NN0 |-> inf ( { n e. NN | ( ( B ` k ) x. n ) e. ZZ } , RR , < ) )
elqaa.6 
|- R = ( seq 0 ( x. , N ) ` ( deg ` F ) )
Assertion elqaalem3 
|- ( ph -> A e. AA )

Proof

Step Hyp Ref Expression
1 elqaa.1 
 |-  ( ph -> A e. CC )
2 elqaa.2 
 |-  ( ph -> F e. ( ( Poly ` QQ ) \ { 0p } ) )
3 elqaa.3 
 |-  ( ph -> ( F ` A ) = 0 )
4 elqaa.4 
 |-  B = ( coeff ` F )
5 elqaa.5 
 |-  N = ( k e. NN0 |-> inf ( { n e. NN | ( ( B ` k ) x. n ) e. ZZ } , RR , < ) )
6 elqaa.6 
 |-  R = ( seq 0 ( x. , N ) ` ( deg ` F ) )
7 cnex 
 |-  CC e. _V
8 7 a1i 
 |-  ( ph -> CC e. _V )
9 6 fvexi 
 |-  R e. _V
10 9 a1i 
 |-  ( ( ph /\ z e. CC ) -> R e. _V )
11 fvexd 
 |-  ( ( ph /\ z e. CC ) -> ( F ` z ) e. _V )
12 fconstmpt 
 |-  ( CC X. { R } ) = ( z e. CC |-> R )
13 12 a1i 
 |-  ( ph -> ( CC X. { R } ) = ( z e. CC |-> R ) )
14 2 eldifad 
 |-  ( ph -> F e. ( Poly ` QQ ) )
15 plyf 
 |-  ( F e. ( Poly ` QQ ) -> F : CC --> CC )
16 14 15 syl 
 |-  ( ph -> F : CC --> CC )
17 16 feqmptd 
 |-  ( ph -> F = ( z e. CC |-> ( F ` z ) ) )
18 8 10 11 13 17 offval2 
 |-  ( ph -> ( ( CC X. { R } ) oF x. F ) = ( z e. CC |-> ( R x. ( F ` z ) ) ) )
19 fzfid 
 |-  ( ( ph /\ z e. CC ) -> ( 0 ... ( deg ` F ) ) e. Fin )
20 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
21 0zd 
 |-  ( ph -> 0 e. ZZ )
22 ssrab2 
 |-  { n e. NN | ( ( B ` m ) x. n ) e. ZZ } C_ NN
23 fveq2 
 |-  ( k = m -> ( B ` k ) = ( B ` m ) )
24 23 oveq1d 
 |-  ( k = m -> ( ( B ` k ) x. n ) = ( ( B ` m ) x. n ) )
25 24 eleq1d 
 |-  ( k = m -> ( ( ( B ` k ) x. n ) e. ZZ <-> ( ( B ` m ) x. n ) e. ZZ ) )
26 25 rabbidv 
 |-  ( k = m -> { n e. NN | ( ( B ` k ) x. n ) e. ZZ } = { n e. NN | ( ( B ` m ) x. n ) e. ZZ } )
27 26 infeq1d 
 |-  ( k = m -> inf ( { n e. NN | ( ( B ` k ) x. n ) e. ZZ } , RR , < ) = inf ( { n e. NN | ( ( B ` m ) x. n ) e. ZZ } , RR , < ) )
28 ltso 
 |-  < Or RR
29 28 infex 
 |-  inf ( { n e. NN | ( ( B ` m ) x. n ) e. ZZ } , RR , < ) e. _V
30 27 5 29 fvmpt 
 |-  ( m e. NN0 -> ( N ` m ) = inf ( { n e. NN | ( ( B ` m ) x. n ) e. ZZ } , RR , < ) )
31 30 adantl 
 |-  ( ( ph /\ m e. NN0 ) -> ( N ` m ) = inf ( { n e. NN | ( ( B ` m ) x. n ) e. ZZ } , RR , < ) )
32 nnuz 
 |-  NN = ( ZZ>= ` 1 )
33 22 32 sseqtri 
 |-  { n e. NN | ( ( B ` m ) x. n ) e. ZZ } C_ ( ZZ>= ` 1 )
34 0z 
 |-  0 e. ZZ
35 zq 
 |-  ( 0 e. ZZ -> 0 e. QQ )
36 34 35 ax-mp 
 |-  0 e. QQ
37 4 coef2 
 |-  ( ( F e. ( Poly ` QQ ) /\ 0 e. QQ ) -> B : NN0 --> QQ )
38 14 36 37 sylancl 
 |-  ( ph -> B : NN0 --> QQ )
39 38 ffvelcdmda 
 |-  ( ( ph /\ m e. NN0 ) -> ( B ` m ) e. QQ )
40 qmulz 
 |-  ( ( B ` m ) e. QQ -> E. n e. NN ( ( B ` m ) x. n ) e. ZZ )
41 39 40 syl 
 |-  ( ( ph /\ m e. NN0 ) -> E. n e. NN ( ( B ` m ) x. n ) e. ZZ )
42 rabn0 
 |-  ( { n e. NN | ( ( B ` m ) x. n ) e. ZZ } =/= (/) <-> E. n e. NN ( ( B ` m ) x. n ) e. ZZ )
43 41 42 sylibr 
 |-  ( ( ph /\ m e. NN0 ) -> { n e. NN | ( ( B ` m ) x. n ) e. ZZ } =/= (/) )
44 infssuzcl 
 |-  ( ( { n e. NN | ( ( B ` m ) x. n ) e. ZZ } C_ ( ZZ>= ` 1 ) /\ { n e. NN | ( ( B ` m ) x. n ) e. ZZ } =/= (/) ) -> inf ( { n e. NN | ( ( B ` m ) x. n ) e. ZZ } , RR , < ) e. { n e. NN | ( ( B ` m ) x. n ) e. ZZ } )
45 33 43 44 sylancr 
 |-  ( ( ph /\ m e. NN0 ) -> inf ( { n e. NN | ( ( B ` m ) x. n ) e. ZZ } , RR , < ) e. { n e. NN | ( ( B ` m ) x. n ) e. ZZ } )
46 31 45 eqeltrd 
 |-  ( ( ph /\ m e. NN0 ) -> ( N ` m ) e. { n e. NN | ( ( B ` m ) x. n ) e. ZZ } )
47 22 46 sselid 
 |-  ( ( ph /\ m e. NN0 ) -> ( N ` m ) e. NN )
48 nnmulcl 
 |-  ( ( m e. NN /\ k e. NN ) -> ( m x. k ) e. NN )
49 48 adantl 
 |-  ( ( ph /\ ( m e. NN /\ k e. NN ) ) -> ( m x. k ) e. NN )
50 20 21 47 49 seqf 
 |-  ( ph -> seq 0 ( x. , N ) : NN0 --> NN )
51 dgrcl 
 |-  ( F e. ( Poly ` QQ ) -> ( deg ` F ) e. NN0 )
52 14 51 syl 
 |-  ( ph -> ( deg ` F ) e. NN0 )
53 50 52 ffvelcdmd 
 |-  ( ph -> ( seq 0 ( x. , N ) ` ( deg ` F ) ) e. NN )
54 6 53 eqeltrid 
 |-  ( ph -> R e. NN )
55 54 nncnd 
 |-  ( ph -> R e. CC )
56 55 adantr 
 |-  ( ( ph /\ z e. CC ) -> R e. CC )
57 elfznn0 
 |-  ( m e. ( 0 ... ( deg ` F ) ) -> m e. NN0 )
58 4 coef3 
 |-  ( F e. ( Poly ` QQ ) -> B : NN0 --> CC )
59 14 58 syl 
 |-  ( ph -> B : NN0 --> CC )
60 59 adantr 
 |-  ( ( ph /\ z e. CC ) -> B : NN0 --> CC )
61 60 ffvelcdmda 
 |-  ( ( ( ph /\ z e. CC ) /\ m e. NN0 ) -> ( B ` m ) e. CC )
62 expcl 
 |-  ( ( z e. CC /\ m e. NN0 ) -> ( z ^ m ) e. CC )
63 62 adantll 
 |-  ( ( ( ph /\ z e. CC ) /\ m e. NN0 ) -> ( z ^ m ) e. CC )
64 61 63 mulcld 
 |-  ( ( ( ph /\ z e. CC ) /\ m e. NN0 ) -> ( ( B ` m ) x. ( z ^ m ) ) e. CC )
65 57 64 sylan2 
 |-  ( ( ( ph /\ z e. CC ) /\ m e. ( 0 ... ( deg ` F ) ) ) -> ( ( B ` m ) x. ( z ^ m ) ) e. CC )
66 19 56 65 fsummulc2 
 |-  ( ( ph /\ z e. CC ) -> ( R x. sum_ m e. ( 0 ... ( deg ` F ) ) ( ( B ` m ) x. ( z ^ m ) ) ) = sum_ m e. ( 0 ... ( deg ` F ) ) ( R x. ( ( B ` m ) x. ( z ^ m ) ) ) )
67 eqid 
 |-  ( deg ` F ) = ( deg ` F )
68 4 67 coeid2 
 |-  ( ( F e. ( Poly ` QQ ) /\ z e. CC ) -> ( F ` z ) = sum_ m e. ( 0 ... ( deg ` F ) ) ( ( B ` m ) x. ( z ^ m ) ) )
69 14 68 sylan 
 |-  ( ( ph /\ z e. CC ) -> ( F ` z ) = sum_ m e. ( 0 ... ( deg ` F ) ) ( ( B ` m ) x. ( z ^ m ) ) )
70 69 oveq2d 
 |-  ( ( ph /\ z e. CC ) -> ( R x. ( F ` z ) ) = ( R x. sum_ m e. ( 0 ... ( deg ` F ) ) ( ( B ` m ) x. ( z ^ m ) ) ) )
71 56 adantr 
 |-  ( ( ( ph /\ z e. CC ) /\ m e. NN0 ) -> R e. CC )
72 71 61 63 mulassd 
 |-  ( ( ( ph /\ z e. CC ) /\ m e. NN0 ) -> ( ( R x. ( B ` m ) ) x. ( z ^ m ) ) = ( R x. ( ( B ` m ) x. ( z ^ m ) ) ) )
73 57 72 sylan2 
 |-  ( ( ( ph /\ z e. CC ) /\ m e. ( 0 ... ( deg ` F ) ) ) -> ( ( R x. ( B ` m ) ) x. ( z ^ m ) ) = ( R x. ( ( B ` m ) x. ( z ^ m ) ) ) )
74 73 sumeq2dv 
 |-  ( ( ph /\ z e. CC ) -> sum_ m e. ( 0 ... ( deg ` F ) ) ( ( R x. ( B ` m ) ) x. ( z ^ m ) ) = sum_ m e. ( 0 ... ( deg ` F ) ) ( R x. ( ( B ` m ) x. ( z ^ m ) ) ) )
75 66 70 74 3eqtr4d 
 |-  ( ( ph /\ z e. CC ) -> ( R x. ( F ` z ) ) = sum_ m e. ( 0 ... ( deg ` F ) ) ( ( R x. ( B ` m ) ) x. ( z ^ m ) ) )
76 75 mpteq2dva 
 |-  ( ph -> ( z e. CC |-> ( R x. ( F ` z ) ) ) = ( z e. CC |-> sum_ m e. ( 0 ... ( deg ` F ) ) ( ( R x. ( B ` m ) ) x. ( z ^ m ) ) ) )
77 18 76 eqtrd 
 |-  ( ph -> ( ( CC X. { R } ) oF x. F ) = ( z e. CC |-> sum_ m e. ( 0 ... ( deg ` F ) ) ( ( R x. ( B ` m ) ) x. ( z ^ m ) ) ) )
78 zsscn 
 |-  ZZ C_ CC
79 78 a1i 
 |-  ( ph -> ZZ C_ CC )
80 55 adantr 
 |-  ( ( ph /\ m e. NN0 ) -> R e. CC )
81 47 nncnd 
 |-  ( ( ph /\ m e. NN0 ) -> ( N ` m ) e. CC )
82 47 nnne0d 
 |-  ( ( ph /\ m e. NN0 ) -> ( N ` m ) =/= 0 )
83 80 81 82 divcan2d 
 |-  ( ( ph /\ m e. NN0 ) -> ( ( N ` m ) x. ( R / ( N ` m ) ) ) = R )
84 83 oveq2d 
 |-  ( ( ph /\ m e. NN0 ) -> ( ( B ` m ) x. ( ( N ` m ) x. ( R / ( N ` m ) ) ) ) = ( ( B ` m ) x. R ) )
85 59 ffvelcdmda 
 |-  ( ( ph /\ m e. NN0 ) -> ( B ` m ) e. CC )
86 80 81 82 divcld 
 |-  ( ( ph /\ m e. NN0 ) -> ( R / ( N ` m ) ) e. CC )
87 85 81 86 mulassd 
 |-  ( ( ph /\ m e. NN0 ) -> ( ( ( B ` m ) x. ( N ` m ) ) x. ( R / ( N ` m ) ) ) = ( ( B ` m ) x. ( ( N ` m ) x. ( R / ( N ` m ) ) ) ) )
88 80 85 mulcomd 
 |-  ( ( ph /\ m e. NN0 ) -> ( R x. ( B ` m ) ) = ( ( B ` m ) x. R ) )
89 84 87 88 3eqtr4rd 
 |-  ( ( ph /\ m e. NN0 ) -> ( R x. ( B ` m ) ) = ( ( ( B ` m ) x. ( N ` m ) ) x. ( R / ( N ` m ) ) ) )
90 57 89 sylan2 
 |-  ( ( ph /\ m e. ( 0 ... ( deg ` F ) ) ) -> ( R x. ( B ` m ) ) = ( ( ( B ` m ) x. ( N ` m ) ) x. ( R / ( N ` m ) ) ) )
91 oveq2 
 |-  ( n = ( N ` m ) -> ( ( B ` m ) x. n ) = ( ( B ` m ) x. ( N ` m ) ) )
92 91 eleq1d 
 |-  ( n = ( N ` m ) -> ( ( ( B ` m ) x. n ) e. ZZ <-> ( ( B ` m ) x. ( N ` m ) ) e. ZZ ) )
93 92 elrab 
 |-  ( ( N ` m ) e. { n e. NN | ( ( B ` m ) x. n ) e. ZZ } <-> ( ( N ` m ) e. NN /\ ( ( B ` m ) x. ( N ` m ) ) e. ZZ ) )
94 93 simprbi 
 |-  ( ( N ` m ) e. { n e. NN | ( ( B ` m ) x. n ) e. ZZ } -> ( ( B ` m ) x. ( N ` m ) ) e. ZZ )
95 46 94 syl 
 |-  ( ( ph /\ m e. NN0 ) -> ( ( B ` m ) x. ( N ` m ) ) e. ZZ )
96 57 95 sylan2 
 |-  ( ( ph /\ m e. ( 0 ... ( deg ` F ) ) ) -> ( ( B ` m ) x. ( N ` m ) ) e. ZZ )
97 eqid 
 |-  ( x e. _V , y e. _V |-> ( ( x x. y ) mod ( N ` m ) ) ) = ( x e. _V , y e. _V |-> ( ( x x. y ) mod ( N ` m ) ) )
98 1 2 3 4 5 6 97 elqaalem2 
 |-  ( ( ph /\ m e. ( 0 ... ( deg ` F ) ) ) -> ( R mod ( N ` m ) ) = 0 )
99 54 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( deg ` F ) ) ) -> R e. NN )
100 57 47 sylan2 
 |-  ( ( ph /\ m e. ( 0 ... ( deg ` F ) ) ) -> ( N ` m ) e. NN )
101 nnre 
 |-  ( R e. NN -> R e. RR )
102 nnrp 
 |-  ( ( N ` m ) e. NN -> ( N ` m ) e. RR+ )
103 mod0 
 |-  ( ( R e. RR /\ ( N ` m ) e. RR+ ) -> ( ( R mod ( N ` m ) ) = 0 <-> ( R / ( N ` m ) ) e. ZZ ) )
104 101 102 103 syl2an 
 |-  ( ( R e. NN /\ ( N ` m ) e. NN ) -> ( ( R mod ( N ` m ) ) = 0 <-> ( R / ( N ` m ) ) e. ZZ ) )
105 99 100 104 syl2anc 
 |-  ( ( ph /\ m e. ( 0 ... ( deg ` F ) ) ) -> ( ( R mod ( N ` m ) ) = 0 <-> ( R / ( N ` m ) ) e. ZZ ) )
106 98 105 mpbid 
 |-  ( ( ph /\ m e. ( 0 ... ( deg ` F ) ) ) -> ( R / ( N ` m ) ) e. ZZ )
107 96 106 zmulcld 
 |-  ( ( ph /\ m e. ( 0 ... ( deg ` F ) ) ) -> ( ( ( B ` m ) x. ( N ` m ) ) x. ( R / ( N ` m ) ) ) e. ZZ )
108 90 107 eqeltrd 
 |-  ( ( ph /\ m e. ( 0 ... ( deg ` F ) ) ) -> ( R x. ( B ` m ) ) e. ZZ )
109 79 52 108 elplyd 
 |-  ( ph -> ( z e. CC |-> sum_ m e. ( 0 ... ( deg ` F ) ) ( ( R x. ( B ` m ) ) x. ( z ^ m ) ) ) e. ( Poly ` ZZ ) )
110 77 109 eqeltrd 
 |-  ( ph -> ( ( CC X. { R } ) oF x. F ) e. ( Poly ` ZZ ) )
111 eldifsn 
 |-  ( F e. ( ( Poly ` QQ ) \ { 0p } ) <-> ( F e. ( Poly ` QQ ) /\ F =/= 0p ) )
112 2 111 sylib 
 |-  ( ph -> ( F e. ( Poly ` QQ ) /\ F =/= 0p ) )
113 112 simprd 
 |-  ( ph -> F =/= 0p )
114 oveq1 
 |-  ( ( ( CC X. { R } ) oF x. F ) = 0p -> ( ( ( CC X. { R } ) oF x. F ) oF / ( CC X. { R } ) ) = ( 0p oF / ( CC X. { R } ) ) )
115 16 ffvelcdmda 
 |-  ( ( ph /\ z e. CC ) -> ( F ` z ) e. CC )
116 54 nnne0d 
 |-  ( ph -> R =/= 0 )
117 116 adantr 
 |-  ( ( ph /\ z e. CC ) -> R =/= 0 )
118 115 56 117 divcan3d 
 |-  ( ( ph /\ z e. CC ) -> ( ( R x. ( F ` z ) ) / R ) = ( F ` z ) )
119 118 mpteq2dva 
 |-  ( ph -> ( z e. CC |-> ( ( R x. ( F ` z ) ) / R ) ) = ( z e. CC |-> ( F ` z ) ) )
120 ovexd 
 |-  ( ( ph /\ z e. CC ) -> ( R x. ( F ` z ) ) e. _V )
121 8 120 10 18 13 offval2 
 |-  ( ph -> ( ( ( CC X. { R } ) oF x. F ) oF / ( CC X. { R } ) ) = ( z e. CC |-> ( ( R x. ( F ` z ) ) / R ) ) )
122 119 121 17 3eqtr4d 
 |-  ( ph -> ( ( ( CC X. { R } ) oF x. F ) oF / ( CC X. { R } ) ) = F )
123 55 116 div0d 
 |-  ( ph -> ( 0 / R ) = 0 )
124 123 mpteq2dv 
 |-  ( ph -> ( z e. CC |-> ( 0 / R ) ) = ( z e. CC |-> 0 ) )
125 0cnd 
 |-  ( ( ph /\ z e. CC ) -> 0 e. CC )
126 df-0p 
 |-  0p = ( CC X. { 0 } )
127 fconstmpt 
 |-  ( CC X. { 0 } ) = ( z e. CC |-> 0 )
128 126 127 eqtri 
 |-  0p = ( z e. CC |-> 0 )
129 128 a1i 
 |-  ( ph -> 0p = ( z e. CC |-> 0 ) )
130 8 125 10 129 13 offval2 
 |-  ( ph -> ( 0p oF / ( CC X. { R } ) ) = ( z e. CC |-> ( 0 / R ) ) )
131 124 130 129 3eqtr4d 
 |-  ( ph -> ( 0p oF / ( CC X. { R } ) ) = 0p )
132 122 131 eqeq12d 
 |-  ( ph -> ( ( ( ( CC X. { R } ) oF x. F ) oF / ( CC X. { R } ) ) = ( 0p oF / ( CC X. { R } ) ) <-> F = 0p ) )
133 114 132 imbitrid 
 |-  ( ph -> ( ( ( CC X. { R } ) oF x. F ) = 0p -> F = 0p ) )
134 133 necon3d 
 |-  ( ph -> ( F =/= 0p -> ( ( CC X. { R } ) oF x. F ) =/= 0p ) )
135 113 134 mpd 
 |-  ( ph -> ( ( CC X. { R } ) oF x. F ) =/= 0p )
136 eldifsn 
 |-  ( ( ( CC X. { R } ) oF x. F ) e. ( ( Poly ` ZZ ) \ { 0p } ) <-> ( ( ( CC X. { R } ) oF x. F ) e. ( Poly ` ZZ ) /\ ( ( CC X. { R } ) oF x. F ) =/= 0p ) )
137 110 135 136 sylanbrc 
 |-  ( ph -> ( ( CC X. { R } ) oF x. F ) e. ( ( Poly ` ZZ ) \ { 0p } ) )
138 9 fconst 
 |-  ( CC X. { R } ) : CC --> { R }
139 ffn 
 |-  ( ( CC X. { R } ) : CC --> { R } -> ( CC X. { R } ) Fn CC )
140 138 139 mp1i 
 |-  ( ph -> ( CC X. { R } ) Fn CC )
141 16 ffnd 
 |-  ( ph -> F Fn CC )
142 inidm 
 |-  ( CC i^i CC ) = CC
143 9 fvconst2 
 |-  ( A e. CC -> ( ( CC X. { R } ) ` A ) = R )
144 143 adantl 
 |-  ( ( ph /\ A e. CC ) -> ( ( CC X. { R } ) ` A ) = R )
145 3 adantr 
 |-  ( ( ph /\ A e. CC ) -> ( F ` A ) = 0 )
146 140 141 8 8 142 144 145 ofval 
 |-  ( ( ph /\ A e. CC ) -> ( ( ( CC X. { R } ) oF x. F ) ` A ) = ( R x. 0 ) )
147 1 146 mpdan 
 |-  ( ph -> ( ( ( CC X. { R } ) oF x. F ) ` A ) = ( R x. 0 ) )
148 55 mul01d 
 |-  ( ph -> ( R x. 0 ) = 0 )
149 147 148 eqtrd 
 |-  ( ph -> ( ( ( CC X. { R } ) oF x. F ) ` A ) = 0 )
150 fveq1 
 |-  ( f = ( ( CC X. { R } ) oF x. F ) -> ( f ` A ) = ( ( ( CC X. { R } ) oF x. F ) ` A ) )
151 150 eqeq1d 
 |-  ( f = ( ( CC X. { R } ) oF x. F ) -> ( ( f ` A ) = 0 <-> ( ( ( CC X. { R } ) oF x. F ) ` A ) = 0 ) )
152 151 rspcev 
 |-  ( ( ( ( CC X. { R } ) oF x. F ) e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( ( ( CC X. { R } ) oF x. F ) ` A ) = 0 ) -> E. f e. ( ( Poly ` ZZ ) \ { 0p } ) ( f ` A ) = 0 )
153 137 149 152 syl2anc 
 |-  ( ph -> E. f e. ( ( Poly ` ZZ ) \ { 0p } ) ( f ` A ) = 0 )
154 elaa 
 |-  ( A e. AA <-> ( A e. CC /\ E. f e. ( ( Poly ` ZZ ) \ { 0p } ) ( f ` A ) = 0 ) )
155 1 153 154 sylanbrc 
 |-  ( ph -> A e. AA )