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
|
ffvelrnda |
|- ( ( 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
|
sseldi |
|- ( ( 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
|
ffvelrnd |
|- ( 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
|
ffvelrnda |
|- ( ( ( 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
|
ffvelrnda |
|- ( ( 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
|
ffvelrnda |
|- ( ( 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
|
syl5ib |
|- ( 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 ) |