Definition df-aa

Description: Define the set of algebraic numbers. An algebraic number is a root of a nonzero polynomial over the integers. Here we construct it as the union of all kernels (preimages of { 0 } ) of all polynomials in ( PolyZZ ) , except the zero polynomial 0p . (Contributed by Mario Carneiro, 22-Jul-2014)

	Ref	Expression
Assertion	df-aa	|- AA = U_ f e. ( ( Poly ` ZZ ) \ { 0p } ) ( `' f " { 0 } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		caa	|- AA
1		vf	|- f
2		cply	|- Poly
3		cz	|- ZZ
4	3 2	cfv	|- ( Poly ` ZZ )
5		c0p	|- 0p
6	5	csn	|- { 0p }
7	4 6	cdif	|- ( ( Poly ` ZZ ) \ { 0p } )
8	1	cv	|- f
9	8	ccnv	|- `' f
10		cc0	|- 0
11	10	csn	|- { 0 }
12	9 11	cima	|- ( `' f " { 0 } )
13	1 7 12	ciun	|- U_ f e. ( ( Poly ` ZZ ) \ { 0p } ) ( `' f " { 0 } )
14	0 13	wceq	|- AA = U_ f e. ( ( Poly ` ZZ ) \ { 0p } ) ( `' f " { 0 } )