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 25691
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 25690 . 2 class 𝔸
2 vf . . 3 setvar 𝑓
3 cz 12504 . . . . 5 class
4 cply 25561 . . . . 5 class Poly
53, 4cfv 6497 . . . 4 class (Poly‘ℤ)
6 c0p 25049 . . . . 5 class 0𝑝
76csn 4587 . . . 4 class {0𝑝}
85, 7cdif 3908 . . 3 class ((Poly‘ℤ) ∖ {0𝑝})
92cv 1541 . . . . 5 class 𝑓
109ccnv 5633 . . . 4 class 𝑓
11 cc0 11056 . . . . 5 class 0
1211csn 4587 . . . 4 class {0}
1310, 12cima 5637 . . 3 class (𝑓 “ {0})
142, 8, 13ciun 4955 . 2 class 𝑓 ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑓 “ {0})
151, 14wceq 1542 1 wff 𝔸 = 𝑓 ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑓 “ {0})
Colors of variables: wff setvar class
This definition is referenced by:  elaa  25692
  Copyright terms: Public domain W3C validator