Theorem dgraacl

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

	Ref	Expression
Assertion	dgraacl	⊢ ( 𝐴 ∈ 𝔸 → ( degAA ‘ 𝐴 ) ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		dgraalem	⊢ ( 𝐴 ∈ 𝔸 → ( ( degAA ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑎 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑎 ) = ( degAA ‘ 𝐴 ) ∧ ( 𝑎 ‘ 𝐴 ) = 0 ) ) )
2	1	simpld	⊢ ( 𝐴 ∈ 𝔸 → ( degAA ‘ 𝐴 ) ∈ ℕ )