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 ) ) )