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 23791
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 23790 . 2 class 𝔸
2 vf . . 3 setvar 𝑓
3 cz 11210 . . . . 5 class
4 cply 23661 . . . . 5 class Poly
53, 4cfv 5790 . . . 4 class (Poly‘ℤ)
6 c0p 23159 . . . . 5 class 0𝑝
76csn 4124 . . . 4 class {0𝑝}
85, 7cdif 3536 . . 3 class ((Poly‘ℤ) ∖ {0𝑝})
92cv 1473 . . . . 5 class 𝑓
109ccnv 5027 . . . 4 class 𝑓
11 cc0 9792 . . . . 5 class 0
1211csn 4124 . . . 4 class {0}
1310, 12cima 5031 . . 3 class (𝑓 “ {0})
142, 8, 13ciun 4449 . 2 class 𝑓 ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑓 “ {0})
151, 14wceq 1474 1 wff 𝔸 = 𝑓 ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑓 “ {0})
Colors of variables: wff setvar class
This definition is referenced by:  elaa  23792
  Copyright terms: Public domain W3C validator