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