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=supa∈ℕ|∃b∈Poly⁡ℚ∖0𝑝deg⁡b=a∧b⁡A=0ℝ<
13 11 12 syl ⊢P∈Poly⁡ℚ∧P≠0𝑝∧A∈ℂ∧P⁡A=0→deg𝔸⁡A=supa∈ℕ|∃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→supa∈ℕ|∃b∈Poly⁡ℚ∖0𝑝deg⁡b=a∧b⁡A=0ℝ<≤deg⁡P
32 16 30 31 sylancr ⊢P∈Poly⁡ℚ∧P≠0𝑝∧A∈ℂ∧P⁡A=0→supa∈ℕ|∃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