Definition df-dgraa 44347

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 44345	. 2 class degAA
2		vx	. . 3 setvar 𝑥
3		caa 26670	. . 3 class 𝔸
4		vp	. . . . . . . . . 10 setvar 𝑝
5	4	cv 1569	. . . . . . . . 9 class 𝑝
6		cdgr 26538	. . . . . . . . 9 class deg
7	5, 6	cfv 6561	. . . . . . . 8 class (deg‘𝑝)
8		vd	. . . . . . . . 9 setvar 𝑑
9	8	cv 1569	. . . . . . . 8 class 𝑑
10	7, 9	wceq 1570	. . . . . . 7 wff (deg‘𝑝) = 𝑑
11	2	cv 1569	. . . . . . . . 9 class 𝑥
12	11, 5	cfv 6561	. . . . . . . 8 class (𝑝‘𝑥)
13		cc0 11230	. . . . . . . 8 class 0
14	12, 13	wceq 1570	. . . . . . 7 wff (𝑝‘𝑥) = 0
15	10, 14	wa 401	. . . . . 6 wff ((deg‘𝑝) = 𝑑 ∧ (𝑝‘𝑥) = 0)
16		cq 13105	. . . . . . . 8 class ℚ
17		cply 26535	. . . . . . . 8 class Poly
18	16, 17	cfv 6561	. . . . . . 7 class (Poly‘ℚ)
19		c0p 26023	. . . . . . . 8 class 0𝑝
20	19	csn 4588	. . . . . . 7 class {0𝑝}
21	18, 20	cdif 4048	. . . . . 6 class ((Poly‘ℚ) ∖ {0𝑝})
22	15, 4, 21	wrex 3090	. . . . 5 wff ∃𝑝 ∈ ((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑑 ∧ (𝑝‘𝑥) = 0)
23		cn 12365	. . . . 5 class ℕ
24	22, 8, 23	crab 3416	. . . 4 class {𝑑 ∈ ℕ ∣ ∃𝑝 ∈ ((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑑 ∧ (𝑝‘𝑥) = 0)}
25		cr 11229	. . . 4 class ℝ
26		clt 11373	. . . 4 class <
27	24, 25, 26	cinf 9463	. . 3 class inf({𝑑 ∈ ℕ ∣ ∃𝑝 ∈ ((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑑 ∧ (𝑝‘𝑥) = 0)}, ℝ, < )
28	2, 3, 27	cmpt 5190	. 2 class (𝑥 ∈ 𝔸 ↦ inf({𝑑 ∈ ℕ ∣ ∃𝑝 ∈ ((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑑 ∧ (𝑝‘𝑥) = 0)}, ℝ, < ))
29	1, 28	wceq 1570	1 wff degAA = (𝑥 ∈ 𝔸 ↦ inf({𝑑 ∈ ℕ ∣ ∃𝑝 ∈ ((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑑 ∧ (𝑝‘𝑥) = 0)}, ℝ, < ))

This definition is used by:  dgraaval  44349  dgraaf  44352