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=supa∈ℕ|∃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≠∅→supa∈ℕ|∃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∈𝔸→supa∈ℕ|∃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