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

Definition df-aa 24115
 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‘ℤ), except the zero polynomial 0𝑝. (Contributed by Mario Carneiro, 22-Jul-2014.)
Assertion
Ref Expression
df-aa 𝔸 = 𝑓 ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑓 “ {0})

Detailed syntax breakdown of Definition df-aa
StepHypRef Expression
1 caa 24114 . 2 class 𝔸
2 vf . . 3 setvar 𝑓
3 cz 11415 . . . . 5 class
4 cply 23985 . . . . 5 class Poly
53, 4cfv 5926 . . . 4 class (Poly‘ℤ)
6 c0p 23481 . . . . 5 class 0𝑝
76csn 4210 . . . 4 class {0𝑝}
85, 7cdif 3604 . . 3 class ((Poly‘ℤ) ∖ {0𝑝})
92cv 1522 . . . . 5 class 𝑓
109ccnv 5142 . . . 4 class 𝑓
11 cc0 9974 . . . . 5 class 0
1211csn 4210 . . . 4 class {0}
1310, 12cima 5146 . . 3 class (𝑓 “ {0})
142, 8, 13ciun 4552 . 2 class 𝑓 ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑓 “ {0})
151, 14wceq 1523 1 wff 𝔸 = 𝑓 ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑓 “ {0})
 Colors of variables: wff setvar class This definition is referenced by:  elaa  24116
 Copyright terms: Public domain W3C validator