Definition df-dgraa 37712

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 = ( x e. AA |-> inf ( { d e. NN | E. p e. ( (Poly ` QQ ) \ { 0p } ) ( (deg ` p ) = d /\ ( p ` x ) = 0 ) } , RR , < ) )

Distinct variable group:   x, d, p

Detailed syntax breakdown of Definition df-dgraa

Step	Hyp	Ref	Expression
1		cdgraa 37710	. 2 class degAA
2		vx	. . 3 setvar x
3		caa 24069	. . 3 class AA
4		vp	. . . . . . . . . 10 setvar p
5	4	cv 1482	. . . . . . . . 9 class p
6		cdgr 23943	. . . . . . . . 9 class deg
7	5, 6	cfv 5888	. . . . . . . 8 class (deg ` p )
8		vd	. . . . . . . . 9 setvar d
9	8	cv 1482	. . . . . . . 8 class d
10	7, 9	wceq 1483	. . . . . . 7 wff (deg ` p ) = d
11	2	cv 1482	. . . . . . . . 9 class x
12	11, 5	cfv 5888	. . . . . . . 8 class ( p ` x )
13		cc0 9936	. . . . . . . 8 class 0
14	12, 13	wceq 1483	. . . . . . 7 wff ( p ` x ) = 0
15	10, 14	wa 384	. . . . . 6 wff ( (deg ` p ) = d /\ ( p ` x ) = 0 )
16		cq 11788	. . . . . . . 8 class QQ
17		cply 23940	. . . . . . . 8 class Poly
18	16, 17	cfv 5888	. . . . . . 7 class (Poly ` QQ )
19		c0p 23436	. . . . . . . 8 class 0p
20	19	csn 4177	. . . . . . 7 class { 0p }
21	18, 20	cdif 3571	. . . . . 6 class ( (Poly ` QQ ) \ { 0p } )
22	15, 4, 21	wrex 2913	. . . . 5 wff E. p e. ( (Poly ` QQ ) \ { 0p } ) ( (deg ` p ) = d /\ ( p ` x ) = 0 )
23		cn 11020	. . . . 5 class NN
24	22, 8, 23	crab 2916	. . . 4 class { d e. NN | E. p e. ( (Poly ` QQ ) \ { 0p } ) ( (deg ` p ) = d /\ ( p ` x ) = 0 ) }
25		cr 9935	. . . 4 class RR
26		clt 10074	. . . 4 class <
27	24, 25, 26	cinf 8347	. . 3 class inf ( { d e. NN | E. p e. ( (Poly ` QQ ) \ { 0p } ) ( (deg ` p ) = d /\ ( p ` x ) = 0 ) } , RR , < )
28	2, 3, 27	cmpt 4729	. 2 class ( x e. AA |-> inf ( { d e. NN | E. p e. ( (Poly ` QQ ) \ { 0p } ) ( (deg ` p ) = d /\ ( p ` x ) = 0 ) } , RR , < ) )
29	1, 28	wceq 1483	1 wff degAA = ( x e. AA |-> inf ( { d e. NN | E. p e. ( (Poly ` QQ ) \ { 0p } ) ( (deg ` p ) = d /\ ( p ` x ) = 0 ) } , RR , < ) )

This definition is referenced by:  dgraaval  37714  dgraaf  37717