Definition df-dgraa 40967

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 40965	. 2 class degAA
2		vx	. . 3 setvar 𝑥
3		caa 25474	. . 3 class 𝔸
4		vp	. . . . . . . . . 10 setvar 𝑝
5	4	cv 1538	. . . . . . . . 9 class 𝑝
6		cdgr 25348	. . . . . . . . 9 class deg
7	5, 6	cfv 6433	. . . . . . . 8 class (deg‘𝑝)
8		vd	. . . . . . . . 9 setvar 𝑑
9	8	cv 1538	. . . . . . . 8 class 𝑑
10	7, 9	wceq 1539	. . . . . . 7 wff (deg‘𝑝) = 𝑑
11	2	cv 1538	. . . . . . . . 9 class 𝑥
12	11, 5	cfv 6433	. . . . . . . 8 class (𝑝‘𝑥)
13		cc0 10871	. . . . . . . 8 class 0
14	12, 13	wceq 1539	. . . . . . 7 wff (𝑝‘𝑥) = 0
15	10, 14	wa 396	. . . . . 6 wff ((deg‘𝑝) = 𝑑 ∧ (𝑝‘𝑥) = 0)
16		cq 12688	. . . . . . . 8 class ℚ
17		cply 25345	. . . . . . . 8 class Poly
18	16, 17	cfv 6433	. . . . . . 7 class (Poly‘ℚ)
19		c0p 24833	. . . . . . . 8 class 0𝑝
20	19	csn 4561	. . . . . . 7 class {0𝑝}
21	18, 20	cdif 3884	. . . . . 6 class ((Poly‘ℚ) ∖ {0𝑝})
22	15, 4, 21	wrex 3065	. . . . 5 wff ∃𝑝 ∈ ((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑑 ∧ (𝑝‘𝑥) = 0)
23		cn 11973	. . . . 5 class ℕ
24	22, 8, 23	crab 3068	. . . 4 class {𝑑 ∈ ℕ ∣ ∃𝑝 ∈ ((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑑 ∧ (𝑝‘𝑥) = 0)}
25		cr 10870	. . . 4 class ℝ
26		clt 11009	. . . 4 class <
27	24, 25, 26	cinf 9200	. . 3 class inf({𝑑 ∈ ℕ ∣ ∃𝑝 ∈ ((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑑 ∧ (𝑝‘𝑥) = 0)}, ℝ, < )
28	2, 3, 27	cmpt 5157	. 2 class (𝑥 ∈ 𝔸 ↦ inf({𝑑 ∈ ℕ ∣ ∃𝑝 ∈ ((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑑 ∧ (𝑝‘𝑥) = 0)}, ℝ, < ))
29	1, 28	wceq 1539	1 wff degAA = (𝑥 ∈ 𝔸 ↦ inf({𝑑 ∈ ℕ ∣ ∃𝑝 ∈ ((Poly‘ℚ) ∖ {0𝑝})((deg‘𝑝) = 𝑑 ∧ (𝑝‘𝑥) = 0)}, ℝ, < ))

This definition is referenced by:  dgraaval  40969  dgraaf  40972