Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-aa Structured version   Unicode version

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 ) of all polynomials in Poly, except the zero polynomial . (Contributed by Mario Carneiro, 22-Jul-2014.)
Assertion
Ref Expression
df-aa Poly

Detailed syntax breakdown of Definition df-aa
StepHypRef Expression
1 caa 20236 . 2
2 vf . . 3
3 cz 10287 . . . . 5
4 cply 20108 . . . . 5 Poly
53, 4cfv 5457 . . . 4 Poly
6 c0p 19564 . . . . 5
76csn 3816 . . . 4
85, 7cdif 3319 . . 3 Poly
92cv 1652 . . . . 5
109ccnv 4880 . . . 4
11 cc0 8995 . . . . 5
1211csn 3816 . . . 4
1310, 12cima 4884 . . 3
142, 8, 13ciun 4095 . 2 Poly
151, 14wceq 1653 1 Poly
 Colors of variables: wff set class This definition is referenced by:  elaa  20238
 Copyright terms: Public domain W3C validator