Definition df-dgraa

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) (Revised by AV, 29-Sep-2020)

	Ref	Expression
Assertion	df-dgraa	⊢ degAA = ( 𝑥 ∈ 𝔸 ↦ inf ( { 𝑑 ∈ ℕ ∣ ∃ 𝑝 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑝 ) = 𝑑 ∧ ( 𝑝 ‘ 𝑥 ) = 0 ) } , ℝ , < ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdgraa	⊢ degAA
1		vx	⊢ 𝑥
2		caa	⊢ 𝔸
3		vd	⊢ 𝑑
4		cn	⊢ ℕ
5		vp	⊢ 𝑝
6		cply	⊢ Poly
7		cq	⊢ ℚ
8	7 6	cfv	⊢ ( Poly ‘ ℚ )
9		c0p	⊢ 0𝑝
10	9	csn	⊢ { 0𝑝 }
11	8 10	cdif	⊢ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } )
12		cdgr	⊢ deg
13	5	cv	⊢ 𝑝
14	13 12	cfv	⊢ ( deg ‘ 𝑝 )
15	3	cv	⊢ 𝑑
16	14 15	wceq	⊢ ( deg ‘ 𝑝 ) = 𝑑
17	1	cv	⊢ 𝑥
18	17 13	cfv	⊢ ( 𝑝 ‘ 𝑥 )
19		cc0	⊢ 0
20	18 19	wceq	⊢ ( 𝑝 ‘ 𝑥 ) = 0
21	16 20	wa	⊢ ( ( deg ‘ 𝑝 ) = 𝑑 ∧ ( 𝑝 ‘ 𝑥 ) = 0 )
22	21 5 11	wrex	⊢ ∃ 𝑝 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑝 ) = 𝑑 ∧ ( 𝑝 ‘ 𝑥 ) = 0 )
23	22 3 4	crab	⊢ { 𝑑 ∈ ℕ ∣ ∃ 𝑝 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑝 ) = 𝑑 ∧ ( 𝑝 ‘ 𝑥 ) = 0 ) }
24		cr	⊢ ℝ
25		clt	⊢ <
26	23 24 25	cinf	⊢ inf ( { 𝑑 ∈ ℕ ∣ ∃ 𝑝 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑝 ) = 𝑑 ∧ ( 𝑝 ‘ 𝑥 ) = 0 ) } , ℝ , < )
27	1 2 26	cmpt	⊢ ( 𝑥 ∈ 𝔸 ↦ inf ( { 𝑑 ∈ ℕ ∣ ∃ 𝑝 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑝 ) = 𝑑 ∧ ( 𝑝 ‘ 𝑥 ) = 0 ) } , ℝ , < ) )
28	0 27	wceq	⊢ degAA = ( 𝑥 ∈ 𝔸 ↦ inf ( { 𝑑 ∈ ℕ ∣ ∃ 𝑝 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑝 ) = 𝑑 ∧ ( 𝑝 ‘ 𝑥 ) = 0 ) } , ℝ , < ) )