Definition df-aa 20237

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 (Poly ` ZZ ), except the zero polynomial 0 p. (Contributed by Mario Carneiro, 22-Jul-2014.)

Assertion

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

Detailed syntax breakdown of Definition df-aa

Step	Hyp	Ref	Expression
1		caa 20236	. 2 class AA
2		vf	. . 3 set f
3		cz 10287	. . . . 5 class ZZ
4		cply 20108	. . . . 5 class Poly
5	3, 4	cfv 5457	. . . 4 class (Poly ` ZZ )
6		c0p 19564	. . . . 5 class 0 p
7	6	csn 3816	. . . 4 class { 0 p }
8	5, 7	cdif 3319	. . 3 class ( (Poly ` ZZ ) \ { 0 p } )
9	2	cv 1652	. . . . 5 class f
10	9	ccnv 4880	. . . 4 class `' f
11		cc0 8995	. . . . 5 class 0
12	11	csn 3816	. . . 4 class { 0 }
13	10, 12	cima 4884	. . 3 class ( `' f " { 0 } )
14	2, 8, 13	ciun 4095	. 2 class U_ f e. ( (Poly ` ZZ ) \ { 0 p } ) ( `' f " { 0 } )
15	1, 14	wceq 1653	1 wff AA = U_ f e. ( (Poly ` ZZ ) \ { 0 p } ) ( `' f " { 0 } )

This definition is referenced by:  elaa  20238