Definition df-aa 26263

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

Step	Hyp	Ref	Expression
1		caa 26262	. 2 class 𝔸
2		vf	. . 3 setvar 𝑓
3		cz 12589	. . . . 5 class ℤ
4		cply 26131	. . . . 5 class Poly
5	3, 4	cfv 6548	. . . 4 class (Poly‘ℤ)
6		c0p 25611	. . . . 5 class 0𝑝
7	6	csn 4629	. . . 4 class {0𝑝}
8	5, 7	cdif 3944	. . 3 class ((Poly‘ℤ) ∖ {0𝑝})
9	2	cv 1533	. . . . 5 class 𝑓
10	9	ccnv 5677	. . . 4 class ◡𝑓
11		cc0 11139	. . . . 5 class 0
12	11	csn 4629	. . . 4 class {0}
13	10, 12	cima 5681	. . 3 class (◡𝑓 “ {0})
14	2, 8, 13	ciun 4996	. 2 class ∪ 𝑓 ∈ ((Poly‘ℤ) ∖ {0𝑝})(◡𝑓 “ {0})
15	1, 14	wceq 1534	1 wff 𝔸 = ∪ 𝑓 ∈ ((Poly‘ℤ) ∖ {0𝑝})(◡𝑓 “ {0})

This definition is referenced by:  elaa  26264

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »