Definition df-dgraa 36731

Description: Define the degree of an algebraic number as the smallest degree of any nonzero polynomial which has said number as a root. (Contributed by Stefan O'Rear, 25-Nov-2014.) (Revised by AV, 29-Sep-2020.)

Assertion

Ref	Expression
df-dgraa	⊢ degAA = (𝑥 ∈ 𝔸 ↦ inf({𝑑 ∈ ℕ ∣ ∃𝑝 ∈ ((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑑 ∧ (𝑝‘𝑥) = 0)}, ℝ, < ))

Distinct variable group:   𝑥,𝑑,𝑝

Detailed syntax breakdown of Definition df-dgraa

Step	Hyp	Ref	Expression
1		cdgraa 36729	. 2 class degAA
2		vx	. . 3 setvar 𝑥
3		caa 23873	. . 3 class 𝔸
4		vp	. . . . . . . . . 10 setvar 𝑝
5	4	cv 1474	. . . . . . . . 9 class 𝑝
6		cdgr 23747	. . . . . . . . 9 class deg
7	5, 6	cfv 5804	. . . . . . . 8 class (deg‘𝑝)
8		vd	. . . . . . . . 9 setvar 𝑑
9	8	cv 1474	. . . . . . . 8 class 𝑑
10	7, 9	wceq 1475	. . . . . . 7 wff (deg‘𝑝) = 𝑑
11	2	cv 1474	. . . . . . . . 9 class 𝑥
12	11, 5	cfv 5804	. . . . . . . 8 class (𝑝‘𝑥)
13		cc0 9815	. . . . . . . 8 class 0
14	12, 13	wceq 1475	. . . . . . 7 wff (𝑝‘𝑥) = 0
15	10, 14	wa 383	. . . . . 6 wff ((deg‘𝑝) = 𝑑 ∧ (𝑝‘𝑥) = 0)
16		cq 11664	. . . . . . . 8 class ℚ
17		cply 23744	. . . . . . . 8 class Poly
18	16, 17	cfv 5804	. . . . . . 7 class (Poly‘ℚ)
19		c0p 23242	. . . . . . . 8 class 0𝑝
20	19	csn 4125	. . . . . . 7 class {0𝑝}
21	18, 20	cdif 3537	. . . . . 6 class ((Poly‘ℚ) ∖ {0𝑝})
22	15, 4, 21	wrex 2897	. . . . 5 wff ∃𝑝 ∈ ((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑑 ∧ (𝑝‘𝑥) = 0)
23		cn 10897	. . . . 5 class ℕ
24	22, 8, 23	crab 2900	. . . 4 class {𝑑 ∈ ℕ ∣ ∃𝑝 ∈ ((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑑 ∧ (𝑝‘𝑥) = 0)}
25		cr 9814	. . . 4 class ℝ
26		clt 9953	. . . 4 class <
27	24, 25, 26	cinf 8230	. . 3 class inf({𝑑 ∈ ℕ ∣ ∃𝑝 ∈ ((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑑 ∧ (𝑝‘𝑥) = 0)}, ℝ, < )
28	2, 3, 27	cmpt 4643	. 2 class (𝑥 ∈ 𝔸 ↦ inf({𝑑 ∈ ℕ ∣ ∃𝑝 ∈ ((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑑 ∧ (𝑝‘𝑥) = 0)}, ℝ, < ))
29	1, 28	wceq 1475	1 wff degAA = (𝑥 ∈ 𝔸 ↦ inf({𝑑 ∈ ℕ ∣ ∃𝑝 ∈ ((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑑 ∧ (𝑝‘𝑥) = 0)}, ℝ, < ))

This definition is referenced by:  dgraaval  36733  dgraaf  36736