Definition df-dgraa 43133

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 43131	. 2 class degAA
2		vx	. . 3 setvar 𝑥
3		caa 26279	. . 3 class 𝔸
4		vp	. . . . . . . . . 10 setvar 𝑝
5	4	cv 1539	. . . . . . . . 9 class 𝑝
6		cdgr 26149	. . . . . . . . 9 class deg
7	5, 6	cfv 6536	. . . . . . . 8 class (deg‘𝑝)
8		vd	. . . . . . . . 9 setvar 𝑑
9	8	cv 1539	. . . . . . . 8 class 𝑑
10	7, 9	wceq 1540	. . . . . . 7 wff (deg‘𝑝) = 𝑑
11	2	cv 1539	. . . . . . . . 9 class 𝑥
12	11, 5	cfv 6536	. . . . . . . 8 class (𝑝‘𝑥)
13		cc0 11134	. . . . . . . 8 class 0
14	12, 13	wceq 1540	. . . . . . 7 wff (𝑝‘𝑥) = 0
15	10, 14	wa 395	. . . . . 6 wff ((deg‘𝑝) = 𝑑 ∧ (𝑝‘𝑥) = 0)
16		cq 12969	. . . . . . . 8 class ℚ
17		cply 26146	. . . . . . . 8 class Poly
18	16, 17	cfv 6536	. . . . . . 7 class (Poly‘ℚ)
19		c0p 25627	. . . . . . . 8 class 0𝑝
20	19	csn 4606	. . . . . . 7 class {0𝑝}
21	18, 20	cdif 3928	. . . . . 6 class ((Poly‘ℚ) ∖ {0𝑝})
22	15, 4, 21	wrex 3061	. . . . 5 wff ∃𝑝 ∈ ((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑑 ∧ (𝑝‘𝑥) = 0)
23		cn 12245	. . . . 5 class ℕ
24	22, 8, 23	crab 3420	. . . 4 class {𝑑 ∈ ℕ ∣ ∃𝑝 ∈ ((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑑 ∧ (𝑝‘𝑥) = 0)}
25		cr 11133	. . . 4 class ℝ
26		clt 11274	. . . 4 class <
27	24, 25, 26	cinf 9458	. . 3 class inf({𝑑 ∈ ℕ ∣ ∃𝑝 ∈ ((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑑 ∧ (𝑝‘𝑥) = 0)}, ℝ, < )
28	2, 3, 27	cmpt 5206	. 2 class (𝑥 ∈ 𝔸 ↦ inf({𝑑 ∈ ℕ ∣ ∃𝑝 ∈ ((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑑 ∧ (𝑝‘𝑥) = 0)}, ℝ, < ))
29	1, 28	wceq 1540	1 wff degAA = (𝑥 ∈ 𝔸 ↦ inf({𝑑 ∈ ℕ ∣ ∃𝑝 ∈ ((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑑 ∧ (𝑝‘𝑥) = 0)}, ℝ, < ))

This definition is referenced by:  dgraaval  43135  dgraaf  43138