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