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 = inf 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 → inf d ∈ ℕ | ∃ p ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ p = d ∧ p ⁡ a = 0 ℝ < = inf d ∈ ℕ | ∃ p ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ p = d ∧ p ⁡ A = 0 ℝ <
6 df-dgraa ⊢ deg 𝔸 = a ∈ 𝔸 ⟼ inf d ∈ ℕ | ∃ p ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ p = d ∧ p ⁡ a = 0 ℝ <
7 ltso ⊢ < Or ℝ
8 7 infex ⊢ inf d ∈ ℕ | ∃ p ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ p = d ∧ p ⁡ A = 0 ℝ < ∈ V
9 5 6 8 fvmpt ⊢ A ∈ 𝔸 → deg 𝔸 ⁡ A = inf d ∈ ℕ | ∃ p ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ p = d ∧ p ⁡ A = 0 ℝ <