Theorem dgraaf

Description: Degree function on algebraic numbers is a function. (Contributed by Stefan O'Rear, 25-Nov-2014) (Proof shortened by AV, 29-Sep-2020)

	Ref	Expression
Assertion	dgraaf	$$⊢{\mathrm{deg}}_{𝔸}:𝔸⟶\mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		ltso	$$⊢<\mathrm{Or}ℝ$$
2	1	infex	$$⊢inf\left(\left\{b\in \mathbb{N}|\exists p\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\left(\mathrm{deg}\left(p\right)=b\wedge p\left(a\right)=0\right)\right\},ℝ,<\right)\in \mathrm{V}$$
3		df-dgraa	$$⊢{\mathrm{deg}}_{𝔸}=\left(a\in 𝔸⟼inf\left(\left\{b\in \mathbb{N}|\exists p\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\left(\mathrm{deg}\left(p\right)=b\wedge p\left(a\right)=0\right)\right\},ℝ,<\right)\right)$$
4	2 3	fnmpti	$$⊢{\mathrm{deg}}_{𝔸}Fn𝔸$$
5		dgraacl	$$⊢a\in 𝔸\to {\mathrm{deg}}_{𝔸}\left(a\right)\in \mathbb{N}$$
6	5	rgen	$$⊢\forall a\in 𝔸{\mathrm{deg}}_{𝔸}\left(a\right)\in \mathbb{N}$$
7		ffnfv	$$⊢{\mathrm{deg}}_{𝔸}:𝔸⟶\mathbb{N}\leftrightarrow \left({\mathrm{deg}}_{𝔸}Fn𝔸\wedge \forall a\in 𝔸{\mathrm{deg}}_{𝔸}\left(a\right)\in \mathbb{N}\right)$$
8	4 6 7	mpbir2an	$$⊢{\mathrm{deg}}_{𝔸}:𝔸⟶\mathbb{N}$$