Metamath Proof Explorer

Definition df-dgraa

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)

Ref Expression
Assertion df-dgraa ⊢ deg 𝔸 = x ∈ 𝔸 ⟼ inf d ∈ ℕ | ∃ p ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ p = d ∧ p ⁡ x = 0 ℝ <

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdgraa class deg 𝔸
1 vx setvar x
2 caa class 𝔸
3 vd setvar d
4 cn class ℕ
5 vp setvar p
6 cply class Poly
7 cq class ℚ
8 7 6 cfv class Poly ⁡ ℚ
9 c0p class 0 𝑝
10 9 csn class 0 𝑝
11 8 10 cdif class Poly ⁡ ℚ ∖ 0 𝑝
12 cdgr class deg
13 5 cv setvar p
14 13 12 cfv class deg ⁡ p
15 3 cv setvar d
16 14 15 wceq wff deg ⁡ p = d
17 1 cv setvar x
18 17 13 cfv class p ⁡ x
19 cc0 class 0
20 18 19 wceq wff p ⁡ x = 0
21 16 20 wa wff deg ⁡ p = d ∧ p ⁡ x = 0
22 21 5 11 wrex wff ∃ p ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ p = d ∧ p ⁡ x = 0
23 22 3 4 crab class d ∈ ℕ | ∃ p ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ p = d ∧ p ⁡ x = 0
24 cr class ℝ
25 clt class <
26 23 24 25 cinf class inf d ∈ ℕ | ∃ p ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ p = d ∧ p ⁡ x = 0 ℝ <
27 1 2 26 cmpt class x ∈ 𝔸 ⟼ inf d ∈ ℕ | ∃ p ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ p = d ∧ p ⁡ x = 0 ℝ <
28 0 27 wceq wff deg 𝔸 = x ∈ 𝔸 ⟼ inf d ∈ ℕ | ∃ p ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ p = d ∧ p ⁡ x = 0 ℝ <