Metamath Proof Explorer

Theorem elaa

Description: Elementhood in the set of algebraic numbers. (Contributed by Mario Carneiro, 22-Jul-2014)

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

Proof

Step Hyp Ref Expression
1 df-aa 
 |-  AA = U_ f e. ( ( Poly ` ZZ ) \ { 0p } ) ( `' f " { 0 } )
2 1 eleq2i 
 |-  ( A e. AA <-> A e. U_ f e. ( ( Poly ` ZZ ) \ { 0p } ) ( `' f " { 0 } ) )
3 eliun 
 |-  ( A e. U_ f e. ( ( Poly ` ZZ ) \ { 0p } ) ( `' f " { 0 } ) <-> E. f e. ( ( Poly ` ZZ ) \ { 0p } ) A e. ( `' f " { 0 } ) )
4 eldifi 
 |-  ( f e. ( ( Poly ` ZZ ) \ { 0p } ) -> f e. ( Poly ` ZZ ) )
5 plyf 
 |-  ( f e. ( Poly ` ZZ ) -> f : CC --> CC )
6 ffn 
 |-  ( f : CC --> CC -> f Fn CC )
7 fniniseg 
 |-  ( f Fn CC -> ( A e. ( `' f " { 0 } ) <-> ( A e. CC /\ ( f ` A ) = 0 ) ) )
8 4 5 6 7 4syl 
 |-  ( f e. ( ( Poly ` ZZ ) \ { 0p } ) -> ( A e. ( `' f " { 0 } ) <-> ( A e. CC /\ ( f ` A ) = 0 ) ) )
9 8 rexbiia 
 |-  ( E. f e. ( ( Poly ` ZZ ) \ { 0p } ) A e. ( `' f " { 0 } ) <-> E. f e. ( ( Poly ` ZZ ) \ { 0p } ) ( A e. CC /\ ( f ` A ) = 0 ) )
10 r19.42v 
 |-  ( E. f e. ( ( Poly ` ZZ ) \ { 0p } ) ( A e. CC /\ ( f ` A ) = 0 ) <-> ( A e. CC /\ E. f e. ( ( Poly ` ZZ ) \ { 0p } ) ( f ` A ) = 0 ) )
11 9 10 bitri 
 |-  ( E. f e. ( ( Poly ` ZZ ) \ { 0p } ) A e. ( `' f " { 0 } ) <-> ( A e. CC /\ E. f e. ( ( Poly ` ZZ ) \ { 0p } ) ( f ` A ) = 0 ) )
12 3 11 bitri 
 |-  ( A e. U_ f e. ( ( Poly ` ZZ ) \ { 0p } ) ( `' f " { 0 } ) <-> ( A e. CC /\ E. f e. ( ( Poly ` ZZ ) \ { 0p } ) ( f ` A ) = 0 ) )
13 2 12 bitri 
 |-  ( A e. AA <-> ( A e. CC /\ E. f e. ( ( Poly ` ZZ ) \ { 0p } ) ( f ` A ) = 0 ) )