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 ( 𝐴 ∈ 𝔸 → ( ( degAA ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑝 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑝 ) = ( degAA ‘ 𝐴 ) ∧ ( 𝑝 ‘ 𝐴 ) = 0 ) ) )

Proof

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