Definition df-dgraa 39762

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 39760	. 2 class degAA
2		vx	. . 3 setvar 𝑥
3		caa 24903	. . 3 class 𝔸
4		vp	. . . . . . . . . 10 setvar 𝑝
5	4	cv 1536	. . . . . . . . 9 class 𝑝
6		cdgr 24777	. . . . . . . . 9 class deg
7	5, 6	cfv 6355	. . . . . . . 8 class (deg‘𝑝)
8		vd	. . . . . . . . 9 setvar 𝑑
9	8	cv 1536	. . . . . . . 8 class 𝑑
10	7, 9	wceq 1537	. . . . . . 7 wff (deg‘𝑝) = 𝑑
11	2	cv 1536	. . . . . . . . 9 class 𝑥
12	11, 5	cfv 6355	. . . . . . . 8 class (𝑝‘𝑥)
13		cc0 10537	. . . . . . . 8 class 0
14	12, 13	wceq 1537	. . . . . . 7 wff (𝑝‘𝑥) = 0
15	10, 14	wa 398	. . . . . 6 wff ((deg‘𝑝) = 𝑑 ∧ (𝑝‘𝑥) = 0)
16		cq 12349	. . . . . . . 8 class ℚ
17		cply 24774	. . . . . . . 8 class Poly
18	16, 17	cfv 6355	. . . . . . 7 class (Poly‘ℚ)
19		c0p 24270	. . . . . . . 8 class 0𝑝
20	19	csn 4567	. . . . . . 7 class {0𝑝}
21	18, 20	cdif 3933	. . . . . 6 class ((Poly‘ℚ) ∖ {0𝑝})
22	15, 4, 21	wrex 3139	. . . . 5 wff ∃𝑝 ∈ ((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑑 ∧ (𝑝‘𝑥) = 0)
23		cn 11638	. . . . 5 class ℕ
24	22, 8, 23	crab 3142	. . . 4 class {𝑑 ∈ ℕ ∣ ∃𝑝 ∈ ((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑑 ∧ (𝑝‘𝑥) = 0)}
25		cr 10536	. . . 4 class ℝ
26		clt 10675	. . . 4 class <
27	24, 25, 26	cinf 8905	. . 3 class inf({𝑑 ∈ ℕ ∣ ∃𝑝 ∈ ((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑑 ∧ (𝑝‘𝑥) = 0)}, ℝ, < )
28	2, 3, 27	cmpt 5146	. 2 class (𝑥 ∈ 𝔸 ↦ inf({𝑑 ∈ ℕ ∣ ∃𝑝 ∈ ((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑑 ∧ (𝑝‘𝑥) = 0)}, ℝ, < ))
29	1, 28	wceq 1537	1 wff degAA = (𝑥 ∈ 𝔸 ↦ inf({𝑑 ∈ ℕ ∣ ∃𝑝 ∈ ((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑑 ∧ (𝑝‘𝑥) = 0)}, ℝ, < ))

This definition is referenced by:  dgraaval  39764  dgraaf  39767