Metamath Proof Explorer


Theorem dgraacl

Description: Closure of the degree function on algebraic numbers. (Contributed by Stefan O'Rear, 25-Nov-2014)

Ref Expression
Assertion dgraacl A 𝔸 deg 𝔸 A

Proof

Step Hyp Ref Expression
1 dgraalem A 𝔸 deg 𝔸 A a Poly 0 𝑝 deg a = deg 𝔸 A a A = 0
2 1 simpld A 𝔸 deg 𝔸 A