Metamath Proof Explorer


Theorem dgraaval

Description: Value of the degree function on an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014) (Revised by AV, 29-Sep-2020)

Ref Expression
Assertion dgraaval A 𝔸 deg 𝔸 A = sup d | p Poly 0 𝑝 deg p = d p A = 0 <

Proof

Step Hyp Ref Expression
1 fveqeq2 a = A p a = 0 p A = 0
2 1 anbi2d a = A deg p = d p a = 0 deg p = d p A = 0
3 2 rexbidv a = A p Poly 0 𝑝 deg p = d p a = 0 p Poly 0 𝑝 deg p = d p A = 0
4 3 rabbidv a = A d | p Poly 0 𝑝 deg p = d p a = 0 = d | p Poly 0 𝑝 deg p = d p A = 0
5 4 infeq1d a = A sup d | p Poly 0 𝑝 deg p = d p a = 0 < = sup d | p Poly 0 𝑝 deg p = d p A = 0 <
6 df-dgraa deg 𝔸 = a 𝔸 sup d | p Poly 0 𝑝 deg p = d p a = 0 <
7 ltso < Or
8 7 infex sup d | p Poly 0 𝑝 deg p = d p A = 0 < V
9 5 6 8 fvmpt A 𝔸 deg 𝔸 A = sup d | p Poly 0 𝑝 deg p = d p A = 0 <