Metamath Proof Explorer

Theorem dgraalem

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

Ref Expression
Assertion dgraalem ⊢ A ∈ 𝔸 → deg 𝔸 ⁡ A ∈ ℕ ∧ ∃ p ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ p = deg 𝔸 ⁡ A ∧ p ⁡ A = 0

Proof

Step Hyp Ref Expression
1 dgraaval ⊢ A ∈ 𝔸 → deg 𝔸 ⁡ A = sup a ∈ ℕ | ∃ p ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ p = a ∧ p ⁡ A = 0 ℝ <
2 ssrab2 ⊢ a ∈ ℕ | ∃ p ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ p = a ∧ p ⁡ A = 0 ⊆ ℕ
3 nnuz ⊢ ℕ = ℤ ≥ 1
4 2 3 sseqtri ⊢ a ∈ ℕ | ∃ p ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ p = a ∧ p ⁡ A = 0 ⊆ ℤ ≥ 1
5 eldifsn ⊢ b ∈ Poly ⁡ ℚ ∖ 0 𝑝 ↔ b ∈ Poly ⁡ ℚ ∧ b ≠ 0 𝑝
6 5 biimpi ⊢ b ∈ Poly ⁡ ℚ ∖ 0 𝑝 → b ∈ Poly ⁡ ℚ ∧ b ≠ 0 𝑝
7 6 ad2antrr ⊢ b ∈ Poly ⁡ ℚ ∖ 0 𝑝 ∧ b ⁡ A = 0 ∧ A ∈ ℂ → b ∈ Poly ⁡ ℚ ∧ b ≠ 0 𝑝
8 simpr ⊢ b ∈ Poly ⁡ ℚ ∖ 0 𝑝 ∧ b ⁡ A = 0 ∧ A ∈ ℂ → A ∈ ℂ
9 simplr ⊢ b ∈ Poly ⁡ ℚ ∖ 0 𝑝 ∧ b ⁡ A = 0 ∧ A ∈ ℂ → b ⁡ A = 0
10 dgrnznn ⊢ b ∈ Poly ⁡ ℚ ∧ b ≠ 0 𝑝 ∧ A ∈ ℂ ∧ b ⁡ A = 0 → deg ⁡ b ∈ ℕ
11 7 8 9 10 syl12anc ⊢ b ∈ Poly ⁡ ℚ ∖ 0 𝑝 ∧ b ⁡ A = 0 ∧ A ∈ ℂ → deg ⁡ b ∈ ℕ
12 simpll ⊢ b ∈ Poly ⁡ ℚ ∖ 0 𝑝 ∧ b ⁡ A = 0 ∧ A ∈ ℂ → b ∈ Poly ⁡ ℚ ∖ 0 𝑝
13 eqid ⊢ deg ⁡ b = deg ⁡ b
14 9 13 jctil ⊢ b ∈ Poly ⁡ ℚ ∖ 0 𝑝 ∧ b ⁡ A = 0 ∧ A ∈ ℂ → deg ⁡ b = deg ⁡ b ∧ b ⁡ A = 0
15 eqeq2 ⊢ a = deg ⁡ b → deg ⁡ p = a ↔ deg ⁡ p = deg ⁡ b
16 15 anbi1d ⊢ a = deg ⁡ b → deg ⁡ p = a ∧ p ⁡ A = 0 ↔ deg ⁡ p = deg ⁡ b ∧ p ⁡ A = 0
17 fveqeq2 ⊢ p = b → deg ⁡ p = deg ⁡ b ↔ deg ⁡ b = deg ⁡ b
18 fveq1 ⊢ p = b → p ⁡ A = b ⁡ A
19 18 eqeq1d ⊢ p = b → p ⁡ A = 0 ↔ b ⁡ A = 0
20 17 19 anbi12d ⊢ p = b → deg ⁡ p = deg ⁡ b ∧ p ⁡ A = 0 ↔ deg ⁡ b = deg ⁡ b ∧ b ⁡ A = 0
21 16 20 rspc2ev ⊢ deg ⁡ b ∈ ℕ ∧ b ∈ Poly ⁡ ℚ ∖ 0 𝑝 ∧ deg ⁡ b = deg ⁡ b ∧ b ⁡ A = 0 → ∃ a ∈ ℕ ∃ p ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ p = a ∧ p ⁡ A = 0
22 11 12 14 21 syl3anc ⊢ b ∈ Poly ⁡ ℚ ∖ 0 𝑝 ∧ b ⁡ A = 0 ∧ A ∈ ℂ → ∃ a ∈ ℕ ∃ p ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ p = a ∧ p ⁡ A = 0
23 22 ex ⊢ b ∈ Poly ⁡ ℚ ∖ 0 𝑝 ∧ b ⁡ A = 0 → A ∈ ℂ → ∃ a ∈ ℕ ∃ p ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ p = a ∧ p ⁡ A = 0
24 23 rexlimiva ⊢ ∃ b ∈ Poly ⁡ ℚ ∖ 0 𝑝 b ⁡ A = 0 → A ∈ ℂ → ∃ a ∈ ℕ ∃ p ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ p = a ∧ p ⁡ A = 0
25 24 impcom ⊢ A ∈ ℂ ∧ ∃ b ∈ Poly ⁡ ℚ ∖ 0 𝑝 b ⁡ A = 0 → ∃ a ∈ ℕ ∃ p ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ p = a ∧ p ⁡ A = 0
26 elqaa ⊢ A ∈ 𝔸 ↔ A ∈ ℂ ∧ ∃ b ∈ Poly ⁡ ℚ ∖ 0 𝑝 b ⁡ A = 0
27 rabn0 ⊢ a ∈ ℕ | ∃ p ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ p = a ∧ p ⁡ A = 0 ≠ ∅ ↔ ∃ a ∈ ℕ ∃ p ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ p = a ∧ p ⁡ A = 0
28 25 26 27 3imtr4i ⊢ A ∈ 𝔸 → a ∈ ℕ | ∃ p ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ p = a ∧ p ⁡ A = 0 ≠ ∅
29 infssuzcl ⊢ a ∈ ℕ | ∃ p ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ p = a ∧ p ⁡ A = 0 ⊆ ℤ ≥ 1 ∧ a ∈ ℕ | ∃ p ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ p = a ∧ p ⁡ A = 0 ≠ ∅ → sup a ∈ ℕ | ∃ p ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ p = a ∧ p ⁡ A = 0 ℝ < ∈ a ∈ ℕ | ∃ p ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ p = a ∧ p ⁡ A = 0
30 4 28 29 sylancr ⊢ A ∈ 𝔸 → sup a ∈ ℕ | ∃ p ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ p = a ∧ p ⁡ A = 0 ℝ < ∈ a ∈ ℕ | ∃ p ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ p = a ∧ p ⁡ A = 0
31 1 30 eqeltrd ⊢ A ∈ 𝔸 → deg 𝔸 ⁡ A ∈ a ∈ ℕ | ∃ p ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ p = a ∧ p ⁡ A = 0
32 eqeq2 ⊢ a = deg 𝔸 ⁡ A → deg ⁡ p = a ↔ deg ⁡ p = deg 𝔸 ⁡ A
33 32 anbi1d ⊢ a = deg 𝔸 ⁡ A → deg ⁡ p = a ∧ p ⁡ A = 0 ↔ deg ⁡ p = deg 𝔸 ⁡ A ∧ p ⁡ A = 0
34 33 rexbidv ⊢ a = deg 𝔸 ⁡ A → ∃ p ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ p = a ∧ p ⁡ A = 0 ↔ ∃ p ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ p = deg 𝔸 ⁡ A ∧ p ⁡ A = 0
35 34 elrab ⊢ deg 𝔸 ⁡ A ∈ a ∈ ℕ | ∃ p ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ p = a ∧ p ⁡ A = 0 ↔ deg 𝔸 ⁡ A ∈ ℕ ∧ ∃ p ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ p = deg 𝔸 ⁡ A ∧ p ⁡ A = 0
36 31 35 sylib ⊢ A ∈ 𝔸 → deg 𝔸 ⁡ A ∈ ℕ ∧ ∃ p ∈ Poly ⁡ ℚ ∖ 0 𝑝 deg ⁡ p = deg 𝔸 ⁡ A ∧ p ⁡ A = 0