Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-dgraa Unicode version

Definition df-dgraa 27450
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.)
Assertion
Ref Expression
df-dgraa  |- degAA  =  (
x  e.  AA  |->  sup ( { d  e.  NN  |  E. p  e.  ( (Poly `  QQ )  \  { 0 p } ) ( (deg
`  p )  =  d  /\  ( p `
 x )  =  0 ) } ,  RR ,  `'  <  ) )
Distinct variable group:    x, d, p

Detailed syntax breakdown of Definition df-dgraa
StepHypRef Expression
1 cdgraa 27448 . 2  class degAA
2 vx . . 3  set  x
3 caa 19710 . . 3  class  AA
4 vp . . . . . . . . . 10  set  p
54cv 1631 . . . . . . . . 9  class  p
6 cdgr 19585 . . . . . . . . 9  class deg
75, 6cfv 5271 . . . . . . . 8  class  (deg `  p )
8 vd . . . . . . . . 9  set  d
98cv 1631 . . . . . . . 8  class  d
107, 9wceq 1632 . . . . . . 7  wff  (deg `  p )  =  d
112cv 1631 . . . . . . . . 9  class  x
1211, 5cfv 5271 . . . . . . . 8  class  ( p `
 x )
13 cc0 8753 . . . . . . . 8  class  0
1412, 13wceq 1632 . . . . . . 7  wff  ( p `
 x )  =  0
1510, 14wa 358 . . . . . 6  wff  ( (deg
`  p )  =  d  /\  ( p `
 x )  =  0 )
16 cq 10332 . . . . . . . 8  class  QQ
17 cply 19582 . . . . . . . 8  class Poly
1816, 17cfv 5271 . . . . . . 7  class  (Poly `  QQ )
19 c0p 19040 . . . . . . . 8  class  0 p
2019csn 3653 . . . . . . 7  class  { 0 p }
2118, 20cdif 3162 . . . . . 6  class  ( (Poly `  QQ )  \  {
0 p } )
2215, 4, 21wrex 2557 . . . . 5  wff  E. p  e.  ( (Poly `  QQ )  \  { 0 p } ) ( (deg
`  p )  =  d  /\  ( p `
 x )  =  0 )
23 cn 9762 . . . . 5  class  NN
2422, 8, 23crab 2560 . . . 4  class  { d  e.  NN  |  E. p  e.  ( (Poly `  QQ )  \  {
0 p } ) ( (deg `  p
)  =  d  /\  ( p `  x
)  =  0 ) }
25 cr 8752 . . . 4  class  RR
26 clt 8883 . . . . 5  class  <
2726ccnv 4704 . . . 4  class  `'  <
2824, 25, 27csup 7209 . . 3  class  sup ( { d  e.  NN  |  E. p  e.  ( (Poly `  QQ )  \  { 0 p }
) ( (deg `  p )  =  d  /\  ( p `  x )  =  0 ) } ,  RR ,  `'  <  )
292, 3, 28cmpt 4093 . 2  class  ( x  e.  AA  |->  sup ( { d  e.  NN  |  E. p  e.  ( (Poly `  QQ )  \  { 0 p }
) ( (deg `  p )  =  d  /\  ( p `  x )  =  0 ) } ,  RR ,  `'  <  ) )
301, 29wceq 1632 1  wff degAA  =  (
x  e.  AA  |->  sup ( { d  e.  NN  |  E. p  e.  ( (Poly `  QQ )  \  { 0 p } ) ( (deg
`  p )  =  d  /\  ( p `
 x )  =  0 ) } ,  RR ,  `'  <  ) )
Colors of variables: wff set class
This definition is referenced by:  dgraaval  27452  dgraaf  27455
  Copyright terms: Public domain W3C validator