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 ( ( ( 𝑃 ∈ ( Poly ‘ ℚ ) ∧ 𝑃 ≠ 0𝑝 ) ∧ ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → ( degAA ‘ 𝐴 ) ≤ ( deg ‘ 𝑃 ) )

Proof

Step Hyp Ref Expression
1 simprl ⊢ ( ( ( 𝑃 ∈ ( Poly ‘ ℚ ) ∧ 𝑃 ≠ 0𝑝 ) ∧ ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → 𝐴 ∈ ℂ )
2 eldifsn ⊢ ( 𝑃 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ↔ ( 𝑃 ∈ ( Poly ‘ ℚ ) ∧ 𝑃 ≠ 0𝑝 ) )
3 2 biimpri ⊢ ( ( 𝑃 ∈ ( Poly ‘ ℚ ) ∧ 𝑃 ≠ 0𝑝 ) → 𝑃 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) )
4 3 adantr ⊢ ( ( ( 𝑃 ∈ ( Poly ‘ ℚ ) ∧ 𝑃 ≠ 0𝑝 ) ∧ ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → 𝑃 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) )
5 simprr ⊢ ( ( ( 𝑃 ∈ ( Poly ‘ ℚ ) ∧ 𝑃 ≠ 0𝑝 ) ∧ ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → ( 𝑃 ‘ 𝐴 ) = 0 )
6 fveq1 ⊢ ( 𝑎 = 𝑃 → ( 𝑎 ‘ 𝐴 ) = ( 𝑃 ‘ 𝐴 ) )
7 6 eqeq1d ⊢ ( 𝑎 = 𝑃 → ( ( 𝑎 ‘ 𝐴 ) = 0 ↔ ( 𝑃 ‘ 𝐴 ) = 0 ) )
8 7 rspcev ⊢ ( ( 𝑃 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) → ∃ 𝑎 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( 𝑎 ‘ 𝐴 ) = 0 )
9 4 5 8 syl2anc ⊢ ( ( ( 𝑃 ∈ ( Poly ‘ ℚ ) ∧ 𝑃 ≠ 0𝑝 ) ∧ ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → ∃ 𝑎 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( 𝑎 ‘ 𝐴 ) = 0 )
10 elqaa ⊢ ( 𝐴 ∈ 𝔸 ↔ ( 𝐴 ∈ ℂ ∧ ∃ 𝑎 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( 𝑎 ‘ 𝐴 ) = 0 ) )
11 1 9 10 sylanbrc ⊢ ( ( ( 𝑃 ∈ ( Poly ‘ ℚ ) ∧ 𝑃 ≠ 0𝑝 ) ∧ ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → 𝐴 ∈ 𝔸 )
12 dgraaval ⊢ ( 𝐴 ∈ 𝔸 → ( degAA ‘ 𝐴 ) = inf ( { 𝑎 ∈ ℕ ∣ ∃ 𝑏 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑏 ) = 𝑎 ∧ ( 𝑏 ‘ 𝐴 ) = 0 ) } , ℝ , < ) )
13 11 12 syl ⊢ ( ( ( 𝑃 ∈ ( Poly ‘ ℚ ) ∧ 𝑃 ≠ 0𝑝 ) ∧ ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → ( degAA ‘ 𝐴 ) = inf ( { 𝑎 ∈ ℕ ∣ ∃ 𝑏 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑏 ) = 𝑎 ∧ ( 𝑏 ‘ 𝐴 ) = 0 ) } , ℝ , < ) )
14 ssrab2 ⊢ { 𝑎 ∈ ℕ ∣ ∃ 𝑏 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑏 ) = 𝑎 ∧ ( 𝑏 ‘ 𝐴 ) = 0 ) } ⊆ ℕ
15 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
16 14 15 sseqtri ⊢ { 𝑎 ∈ ℕ ∣ ∃ 𝑏 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑏 ) = 𝑎 ∧ ( 𝑏 ‘ 𝐴 ) = 0 ) } ⊆ ( ℤ≥ ‘ 1 )
17 dgrnznn ⊢ ( ( ( 𝑃 ∈ ( Poly ‘ ℚ ) ∧ 𝑃 ≠ 0𝑝 ) ∧ ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → ( deg ‘ 𝑃 ) ∈ ℕ )
18 eqid ⊢ ( deg ‘ 𝑃 ) = ( deg ‘ 𝑃 )
19 5 18 jctil ⊢ ( ( ( 𝑃 ∈ ( Poly ‘ ℚ ) ∧ 𝑃 ≠ 0𝑝 ) ∧ ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → ( ( deg ‘ 𝑃 ) = ( deg ‘ 𝑃 ) ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) )
20 fveqeq2 ⊢ ( 𝑏 = 𝑃 → ( ( deg ‘ 𝑏 ) = ( deg ‘ 𝑃 ) ↔ ( deg ‘ 𝑃 ) = ( deg ‘ 𝑃 ) ) )
21 fveq1 ⊢ ( 𝑏 = 𝑃 → ( 𝑏 ‘ 𝐴 ) = ( 𝑃 ‘ 𝐴 ) )
22 21 eqeq1d ⊢ ( 𝑏 = 𝑃 → ( ( 𝑏 ‘ 𝐴 ) = 0 ↔ ( 𝑃 ‘ 𝐴 ) = 0 ) )
23 20 22 anbi12d ⊢ ( 𝑏 = 𝑃 → ( ( ( deg ‘ 𝑏 ) = ( deg ‘ 𝑃 ) ∧ ( 𝑏 ‘ 𝐴 ) = 0 ) ↔ ( ( deg ‘ 𝑃 ) = ( deg ‘ 𝑃 ) ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) )
24 23 rspcev ⊢ ( ( 𝑃 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ∧ ( ( deg ‘ 𝑃 ) = ( deg ‘ 𝑃 ) ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → ∃ 𝑏 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑏 ) = ( deg ‘ 𝑃 ) ∧ ( 𝑏 ‘ 𝐴 ) = 0 ) )
25 4 19 24 syl2anc ⊢ ( ( ( 𝑃 ∈ ( Poly ‘ ℚ ) ∧ 𝑃 ≠ 0𝑝 ) ∧ ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → ∃ 𝑏 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑏 ) = ( deg ‘ 𝑃 ) ∧ ( 𝑏 ‘ 𝐴 ) = 0 ) )
26 eqeq2 ⊢ ( 𝑎 = ( deg ‘ 𝑃 ) → ( ( deg ‘ 𝑏 ) = 𝑎 ↔ ( deg ‘ 𝑏 ) = ( deg ‘ 𝑃 ) ) )
27 26 anbi1d ⊢ ( 𝑎 = ( deg ‘ 𝑃 ) → ( ( ( deg ‘ 𝑏 ) = 𝑎 ∧ ( 𝑏 ‘ 𝐴 ) = 0 ) ↔ ( ( deg ‘ 𝑏 ) = ( deg ‘ 𝑃 ) ∧ ( 𝑏 ‘ 𝐴 ) = 0 ) ) )
28 27 rexbidv ⊢ ( 𝑎 = ( deg ‘ 𝑃 ) → ( ∃ 𝑏 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑏 ) = 𝑎 ∧ ( 𝑏 ‘ 𝐴 ) = 0 ) ↔ ∃ 𝑏 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑏 ) = ( deg ‘ 𝑃 ) ∧ ( 𝑏 ‘ 𝐴 ) = 0 ) ) )
29 28 elrab ⊢ ( ( deg ‘ 𝑃 ) ∈ { 𝑎 ∈ ℕ ∣ ∃ 𝑏 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑏 ) = 𝑎 ∧ ( 𝑏 ‘ 𝐴 ) = 0 ) } ↔ ( ( deg ‘ 𝑃 ) ∈ ℕ ∧ ∃ 𝑏 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑏 ) = ( deg ‘ 𝑃 ) ∧ ( 𝑏 ‘ 𝐴 ) = 0 ) ) )
30 17 25 29 sylanbrc ⊢ ( ( ( 𝑃 ∈ ( Poly ‘ ℚ ) ∧ 𝑃 ≠ 0𝑝 ) ∧ ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → ( deg ‘ 𝑃 ) ∈ { 𝑎 ∈ ℕ ∣ ∃ 𝑏 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑏 ) = 𝑎 ∧ ( 𝑏 ‘ 𝐴 ) = 0 ) } )
31 infssuzle ⊢ ( ( { 𝑎 ∈ ℕ ∣ ∃ 𝑏 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑏 ) = 𝑎 ∧ ( 𝑏 ‘ 𝐴 ) = 0 ) } ⊆ ( ℤ≥ ‘ 1 ) ∧ ( deg ‘ 𝑃 ) ∈ { 𝑎 ∈ ℕ ∣ ∃ 𝑏 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑏 ) = 𝑎 ∧ ( 𝑏 ‘ 𝐴 ) = 0 ) } ) → inf ( { 𝑎 ∈ ℕ ∣ ∃ 𝑏 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑏 ) = 𝑎 ∧ ( 𝑏 ‘ 𝐴 ) = 0 ) } , ℝ , < ) ≤ ( deg ‘ 𝑃 ) )
32 16 30 31 sylancr ⊢ ( ( ( 𝑃 ∈ ( Poly ‘ ℚ ) ∧ 𝑃 ≠ 0𝑝 ) ∧ ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → inf ( { 𝑎 ∈ ℕ ∣ ∃ 𝑏 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑏 ) = 𝑎 ∧ ( 𝑏 ‘ 𝐴 ) = 0 ) } , ℝ , < ) ≤ ( deg ‘ 𝑃 ) )
33 13 32 eqbrtrd ⊢ ( ( ( 𝑃 ∈ ( Poly ‘ ℚ ) ∧ 𝑃 ≠ 0𝑝 ) ∧ ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → ( degAA ‘ 𝐴 ) ≤ ( deg ‘ 𝑃 ) )