Metamath Proof Explorer

Theorem elqaa

Description: The set of numbers generated by the roots of polynomials in the rational numbers is the same as the set of algebraic numbers, which by elaa are defined only in terms of polynomials over the integers. (Contributed by Mario Carneiro, 23-Jul-2014) (Proof shortened by AV, 3-Oct-2020)

Ref Expression
Assertion elqaa 
|- ( A e. AA <-> ( A e. CC /\ E. f e. ( ( Poly ` QQ ) \ { 0p } ) ( f ` A ) = 0 ) )

Proof

Step Hyp Ref Expression
1 elaa 
 |-  ( A e. AA <-> ( A e. CC /\ E. f e. ( ( Poly ` ZZ ) \ { 0p } ) ( f ` A ) = 0 ) )
2 zssq 
 |-  ZZ C_ QQ
3 qsscn 
 |-  QQ C_ CC
4 plyss 
 |-  ( ( ZZ C_ QQ /\ QQ C_ CC ) -> ( Poly ` ZZ ) C_ ( Poly ` QQ ) )
5 2 3 4 mp2an 
 |-  ( Poly ` ZZ ) C_ ( Poly ` QQ )
6 ssdif 
 |-  ( ( Poly ` ZZ ) C_ ( Poly ` QQ ) -> ( ( Poly ` ZZ ) \ { 0p } ) C_ ( ( Poly ` QQ ) \ { 0p } ) )
7 ssrexv 
 |-  ( ( ( Poly ` ZZ ) \ { 0p } ) C_ ( ( Poly ` QQ ) \ { 0p } ) -> ( E. f e. ( ( Poly ` ZZ ) \ { 0p } ) ( f ` A ) = 0 -> E. f e. ( ( Poly ` QQ ) \ { 0p } ) ( f ` A ) = 0 ) )
8 5 6 7 mp2b 
 |-  ( E. f e. ( ( Poly ` ZZ ) \ { 0p } ) ( f ` A ) = 0 -> E. f e. ( ( Poly ` QQ ) \ { 0p } ) ( f ` A ) = 0 )
9 8 anim2i 
 |-  ( ( A e. CC /\ E. f e. ( ( Poly ` ZZ ) \ { 0p } ) ( f ` A ) = 0 ) -> ( A e. CC /\ E. f e. ( ( Poly ` QQ ) \ { 0p } ) ( f ` A ) = 0 ) )
10 1 9 sylbi 
 |-  ( A e. AA -> ( A e. CC /\ E. f e. ( ( Poly ` QQ ) \ { 0p } ) ( f ` A ) = 0 ) )
11 simpll 
 |-  ( ( ( A e. CC /\ f e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( f ` A ) = 0 ) -> A e. CC )
12 simplr 
 |-  ( ( ( A e. CC /\ f e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( f ` A ) = 0 ) -> f e. ( ( Poly ` QQ ) \ { 0p } ) )
13 simpr 
 |-  ( ( ( A e. CC /\ f e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( f ` A ) = 0 ) -> ( f ` A ) = 0 )
14 eqid 
 |-  ( coeff ` f ) = ( coeff ` f )
15 fveq2 
 |-  ( m = k -> ( ( coeff ` f ) ` m ) = ( ( coeff ` f ) ` k ) )
16 15 oveq1d 
 |-  ( m = k -> ( ( ( coeff ` f ) ` m ) x. j ) = ( ( ( coeff ` f ) ` k ) x. j ) )
17 16 eleq1d 
 |-  ( m = k -> ( ( ( ( coeff ` f ) ` m ) x. j ) e. ZZ <-> ( ( ( coeff ` f ) ` k ) x. j ) e. ZZ ) )
18 17 rabbidv 
 |-  ( m = k -> { j e. NN | ( ( ( coeff ` f ) ` m ) x. j ) e. ZZ } = { j e. NN | ( ( ( coeff ` f ) ` k ) x. j ) e. ZZ } )
19 oveq2 
 |-  ( j = n -> ( ( ( coeff ` f ) ` k ) x. j ) = ( ( ( coeff ` f ) ` k ) x. n ) )
20 19 eleq1d 
 |-  ( j = n -> ( ( ( ( coeff ` f ) ` k ) x. j ) e. ZZ <-> ( ( ( coeff ` f ) ` k ) x. n ) e. ZZ ) )
21 20 cbvrabv 
 |-  { j e. NN | ( ( ( coeff ` f ) ` k ) x. j ) e. ZZ } = { n e. NN | ( ( ( coeff ` f ) ` k ) x. n ) e. ZZ }
22 18 21 eqtrdi 
 |-  ( m = k -> { j e. NN | ( ( ( coeff ` f ) ` m ) x. j ) e. ZZ } = { n e. NN | ( ( ( coeff ` f ) ` k ) x. n ) e. ZZ } )
23 22 infeq1d 
 |-  ( m = k -> inf ( { j e. NN | ( ( ( coeff ` f ) ` m ) x. j ) e. ZZ } , RR , < ) = inf ( { n e. NN | ( ( ( coeff ` f ) ` k ) x. n ) e. ZZ } , RR , < ) )
24 23 cbvmptv 
 |-  ( m e. NN0 |-> inf ( { j e. NN | ( ( ( coeff ` f ) ` m ) x. j ) e. ZZ } , RR , < ) ) = ( k e. NN0 |-> inf ( { n e. NN | ( ( ( coeff ` f ) ` k ) x. n ) e. ZZ } , RR , < ) )
25 eqid 
 |-  ( seq 0 ( x. , ( m e. NN0 |-> inf ( { j e. NN | ( ( ( coeff ` f ) ` m ) x. j ) e. ZZ } , RR , < ) ) ) ` ( deg ` f ) ) = ( seq 0 ( x. , ( m e. NN0 |-> inf ( { j e. NN | ( ( ( coeff ` f ) ` m ) x. j ) e. ZZ } , RR , < ) ) ) ` ( deg ` f ) )
26 11 12 13 14 24 25 elqaalem3 
 |-  ( ( ( A e. CC /\ f e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( f ` A ) = 0 ) -> A e. AA )
27 26 r19.29an 
 |-  ( ( A e. CC /\ E. f e. ( ( Poly ` QQ ) \ { 0p } ) ( f ` A ) = 0 ) -> A e. AA )
28 10 27 impbii 
 |-  ( A e. AA <-> ( A e. CC /\ E. f e. ( ( Poly ` QQ ) \ { 0p } ) ( f ` A ) = 0 ) )