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	$$⊢{\mathrm{deg}}_{𝔸}=\left(x\in 𝔸⟼sup\left(\left\{d\in \mathbb{N}|\exists p\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\left(\mathrm{deg}\left(p\right)=d\wedge p\left(x\right)=0\right)\right\},ℝ,<\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdgraa	$$class{\mathrm{deg}}_{𝔸}$$
1		vx	$$setvarx$$
2		caa	$$class𝔸$$
3		vd	$$setvard$$
4		cn	$$class\mathbb{N}$$
5		vp	$$setvarp$$
6		cply	$$class\mathrm{Poly}$$
7		cq	$$class\mathbb{Q}$$
8	7 6	cfv	$$class\mathrm{Poly}\left(\mathbb{Q}\right)$$
9		c0p	$$class{0}_{𝑝}$$
10	9	csn	$$class\left\{0_{𝑝}\right\}$$
11	8 10	cdif	$$class\left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)$$
12		cdgr	$$class\mathrm{deg}$$
13	5	cv	$$setvarp$$
14	13 12	cfv	$$class\mathrm{deg}\left(p\right)$$
15	3	cv	$$setvard$$
16	14 15	wceq	$$wff\mathrm{deg}\left(p\right)=d$$
17	1	cv	$$setvarx$$
18	17 13	cfv	$$classp\left(x\right)$$
19		cc0	$$class0$$
20	18 19	wceq	$$wffp\left(x\right)=0$$
21	16 20	wa	$$wff\left(\mathrm{deg}\left(p\right)=d\wedge p\left(x\right)=0\right)$$
22	21 5 11	wrex	$$wff\exists p\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\left(\mathrm{deg}\left(p\right)=d\wedge p\left(x\right)=0\right)$$
23	22 3 4	crab	$$class\left\{d\in \mathbb{N}|\exists p\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\left(\mathrm{deg}\left(p\right)=d\wedge p\left(x\right)=0\right)\right\}$$
24		cr	$$classℝ$$
25		clt	$$class<$$
26	23 24 25	cinf	$$classsup\left(\left\{d\in \mathbb{N}|\exists p\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\left(\mathrm{deg}\left(p\right)=d\wedge p\left(x\right)=0\right)\right\},ℝ,<\right)$$
27	1 2 26	cmpt	$$class\left(x\in 𝔸⟼sup\left(\left\{d\in \mathbb{N}|\exists p\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\left(\mathrm{deg}\left(p\right)=d\wedge p\left(x\right)=0\right)\right\},ℝ,<\right)\right)$$
28	0 27	wceq	$$wff{\mathrm{deg}}_{𝔸}=\left(x\in 𝔸⟼sup\left(\left\{d\in \mathbb{N}|\exists p\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\left(\mathrm{deg}\left(p\right)=d\wedge p\left(x\right)=0\right)\right\},ℝ,<\right)\right)$$