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

Definition df-aa 24914
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 24913 . 2 class 𝔸
2 vf . . 3 setvar 𝑓
3 cz 11973 . . . . 5 class
4 cply 24784 . . . . 5 class Poly
53, 4cfv 6328 . . . 4 class (Poly‘ℤ)
6 c0p 24276 . . . . 5 class 0𝑝
76csn 4528 . . . 4 class {0𝑝}
85, 7cdif 3881 . . 3 class ((Poly‘ℤ) ∖ {0𝑝})
92cv 1537 . . . . 5 class 𝑓
109ccnv 5522 . . . 4 class 𝑓
11 cc0 10530 . . . . 5 class 0
1211csn 4528 . . . 4 class {0}
1310, 12cima 5526 . . 3 class (𝑓 “ {0})
142, 8, 13ciun 4884 . 2 class 𝑓 ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑓 “ {0})
151, 14wceq 1538 1 wff 𝔸 = 𝑓 ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑓 “ {0})
Colors of variables: wff setvar class
This definition is referenced by:  elaa  24915
  Copyright terms: Public domain W3C validator