Metamath Proof Explorer

Theorem dgraaub

Description: Upper bound on degree of an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014) (Proof shortened by AV, 29-Sep-2020)

Ref Expression
Assertion dgraaub ⊢ P ∈ Poly ⁡ ℚ ∧ P ≠ 0 𝑝 ∧ A ∈ ℂ ∧ P ⁡ A = 0 → deg 𝔸 ⁡ A ≤ deg ⁡ P

Proof

Step Hyp Ref Expression
1 simprl ⊢ P ∈ Poly ⁡ ℚ ∧ P ≠ 0 𝑝 ∧ A ∈ ℂ ∧ P ⁡ A = 0 → A ∈ ℂ
2 eldifsn ⊢ P ∈ Poly ⁡ ℚ ∖ 0 𝑝 ↔ P ∈ Poly ⁡ ℚ ∧ P ≠ 0 𝑝
3 2 biranri ⊢ P ∈ Poly ⁡ ℚ ∧ P ≠ 0 𝑝 ∧ A ∈ ℂ ∧ P ⁡ A = 0 → P ∈ Poly ⁡ ℚ ∖ 0 𝑝
4 simprr ⊢ P ∈ Poly ⁡ ℚ ∧ P ≠ 0 𝑝 ∧ A ∈ ℂ ∧ P ⁡ A = 0 → P ⁡ A = 0
5 fveq1 ⊢ a = P → a ⁡ A = P ⁡ A
6 5 eqeq1d ⊢ a = P → a ⁡ A = 0 ↔ P ⁡ A = 0
7 6 rspcev ⊢ P ∈ Poly ⁡ ℚ ∖ 0 𝑝 ∧ P ⁡ A = 0 → ∃ a ∈ Poly ⁡ ℚ ∖ 0 𝑝 a ⁡ A = 0
8 3 4 7 syl2anc ⊢ P ∈ Poly ⁡ ℚ ∧ P ≠ 0 𝑝 ∧ A ∈ ℂ ∧ P ⁡ A = 0 → ∃ a ∈ Poly ⁡ ℚ ∖ 0 𝑝 a ⁡ A = 0
9 elqaa ⊢ A ∈ 𝔸 ↔ A ∈ ℂ ∧ ∃ a ∈ Poly ⁡ ℚ ∖ 0 𝑝 a ⁡ A = 0
10 1 8 9 sylanbrc ⊢ P ∈ Poly ⁡ ℚ ∧ P ≠ 0 𝑝 ∧ A ∈ ℂ ∧ P ⁡ A = 0 → A ∈ 𝔸
11 dgraaval ⊢ A ∈ 𝔸 → deg 𝔸 ⁡ A = inf a ∈ ℕ | ∃ b ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ b = a ∧ b ⁡ A = 0 ℝ <
12 10 11 syl ⊢ P ∈ Poly ⁡ ℚ ∧ P ≠ 0 𝑝 ∧ A ∈ ℂ ∧ P ⁡ A = 0 → deg 𝔸 ⁡ A = inf a ∈ ℕ | ∃ b ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ b = a ∧ b ⁡ A = 0 ℝ <
13 ssrab2 ⊢ a ∈ ℕ | ∃ b ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ b = a ∧ b ⁡ A = 0 ⊆ ℕ
14 nnuz ⊢ ℕ = ℤ ≥ 1
15 13 14 sseqtri ⊢ a ∈ ℕ | ∃ b ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ b = a ∧ b ⁡ A = 0 ⊆ ℤ ≥ 1
16 dgrnznn ⊢ P ∈ Poly ⁡ ℚ ∧ P ≠ 0 𝑝 ∧ A ∈ ℂ ∧ P ⁡ A = 0 → deg ⁡ P ∈ ℕ
17 eqid ⊢ deg ⁡ P = deg ⁡ P
18 4 17 jctil ⊢ P ∈ Poly ⁡ ℚ ∧ P ≠ 0 𝑝 ∧ A ∈ ℂ ∧ P ⁡ A = 0 → deg ⁡ P = deg ⁡ P ∧ P ⁡ A = 0
19 fveqeq2 ⊢ b = P → deg ⁡ b = deg ⁡ P ↔ deg ⁡ P = deg ⁡ P
20 fveq1 ⊢ b = P → b ⁡ A = P ⁡ A
21 20 eqeq1d ⊢ b = P → b ⁡ A = 0 ↔ P ⁡ A = 0
22 19 21 anbi12d ⊢ b = P → deg ⁡ b = deg ⁡ P ∧ b ⁡ A = 0 ↔ deg ⁡ P = deg ⁡ P ∧ P ⁡ A = 0
23 22 rspcev ⊢ P ∈ Poly ⁡ ℚ ∖ 0 𝑝 ∧ deg ⁡ P = deg ⁡ P ∧ P ⁡ A = 0 → ∃ b ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ b = deg ⁡ P ∧ b ⁡ A = 0
24 3 18 23 syl2anc ⊢ P ∈ Poly ⁡ ℚ ∧ P ≠ 0 𝑝 ∧ A ∈ ℂ ∧ P ⁡ A = 0 → ∃ b ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ b = deg ⁡ P ∧ b ⁡ A = 0
25 eqeq2 ⊢ a = deg ⁡ P → deg ⁡ b = a ↔ deg ⁡ b = deg ⁡ P
26 25 anbi1d ⊢ a = deg ⁡ P → deg ⁡ b = a ∧ b ⁡ A = 0 ↔ deg ⁡ b = deg ⁡ P ∧ b ⁡ A = 0
27 26 rexbidv ⊢ a = deg ⁡ P → ∃ b ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ b = a ∧ b ⁡ A = 0 ↔ ∃ b ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ b = deg ⁡ P ∧ b ⁡ A = 0
28 27 elrab ⊢ deg ⁡ P ∈ a ∈ ℕ | ∃ b ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ b = a ∧ b ⁡ A = 0 ↔ deg ⁡ P ∈ ℕ ∧ ∃ b ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ b = deg ⁡ P ∧ b ⁡ A = 0
29 16 24 28 sylanbrc ⊢ P ∈ Poly ⁡ ℚ ∧ P ≠ 0 𝑝 ∧ A ∈ ℂ ∧ P ⁡ A = 0 → deg ⁡ P ∈ a ∈ ℕ | ∃ b ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ b = a ∧ b ⁡ A = 0
30 infssuzle ⊢ a ∈ ℕ | ∃ b ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ b = a ∧ b ⁡ A = 0 ⊆ ℤ ≥ 1 ∧ deg ⁡ P ∈ a ∈ ℕ | ∃ b ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ b = a ∧ b ⁡ A = 0 → inf a ∈ ℕ | ∃ b ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ b = a ∧ b ⁡ A = 0 ℝ < ≤ deg ⁡ P
31 15 29 30 sylancr ⊢ P ∈ Poly ⁡ ℚ ∧ P ≠ 0 𝑝 ∧ A ∈ ℂ ∧ P ⁡ A = 0 → inf a ∈ ℕ | ∃ b ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ b = a ∧ b ⁡ A = 0 ℝ < ≤ deg ⁡ P
32 12 31 eqbrtrd ⊢ P ∈ Poly ⁡ ℚ ∧ P ≠ 0 𝑝 ∧ A ∈ ℂ ∧ P ⁡ A = 0 → deg 𝔸 ⁡ A ≤ deg ⁡ P