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 
|- ( A e. AA -> ( ( degAA ` A ) e. NN /\ E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 ) ) )

Proof

Step Hyp Ref Expression
1 dgraaval 
 |-  ( A e. AA -> ( degAA ` A ) = inf ( { a e. NN | E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = a /\ ( p ` A ) = 0 ) } , RR , < ) )
2 ssrab2 
 |-  { a e. NN | E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = a /\ ( p ` A ) = 0 ) } C_ NN
3 nnuz 
 |-  NN = ( ZZ>= ` 1 )
4 2 3 sseqtri 
 |-  { a e. NN | E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = a /\ ( p ` A ) = 0 ) } C_ ( ZZ>= ` 1 )
5 eldifsn 
 |-  ( b e. ( ( Poly ` QQ ) \ { 0p } ) <-> ( b e. ( Poly ` QQ ) /\ b =/= 0p ) )
6 5 biimpi 
 |-  ( b e. ( ( Poly ` QQ ) \ { 0p } ) -> ( b e. ( Poly ` QQ ) /\ b =/= 0p ) )
7 6 ad2antrr 
 |-  ( ( ( b e. ( ( Poly ` QQ ) \ { 0p } ) /\ ( b ` A ) = 0 ) /\ A e. CC ) -> ( b e. ( Poly ` QQ ) /\ b =/= 0p ) )
8 simpr 
 |-  ( ( ( b e. ( ( Poly ` QQ ) \ { 0p } ) /\ ( b ` A ) = 0 ) /\ A e. CC ) -> A e. CC )
9 simplr 
 |-  ( ( ( b e. ( ( Poly ` QQ ) \ { 0p } ) /\ ( b ` A ) = 0 ) /\ A e. CC ) -> ( b ` A ) = 0 )
10 dgrnznn 
 |-  ( ( ( b e. ( Poly ` QQ ) /\ b =/= 0p ) /\ ( A e. CC /\ ( b ` A ) = 0 ) ) -> ( deg ` b ) e. NN )
11 7 8 9 10 syl12anc 
 |-  ( ( ( b e. ( ( Poly ` QQ ) \ { 0p } ) /\ ( b ` A ) = 0 ) /\ A e. CC ) -> ( deg ` b ) e. NN )
12 simpll 
 |-  ( ( ( b e. ( ( Poly ` QQ ) \ { 0p } ) /\ ( b ` A ) = 0 ) /\ A e. CC ) -> b e. ( ( Poly ` QQ ) \ { 0p } ) )
13 eqid 
 |-  ( deg ` b ) = ( deg ` b )
14 9 13 jctil 
 |-  ( ( ( b e. ( ( Poly ` QQ ) \ { 0p } ) /\ ( b ` A ) = 0 ) /\ A e. CC ) -> ( ( deg ` b ) = ( deg ` b ) /\ ( b ` A ) = 0 ) )
15 eqeq2 
 |-  ( a = ( deg ` b ) -> ( ( deg ` p ) = a <-> ( deg ` p ) = ( deg ` b ) ) )
16 15 anbi1d 
 |-  ( a = ( deg ` b ) -> ( ( ( deg ` p ) = a /\ ( p ` A ) = 0 ) <-> ( ( deg ` p ) = ( deg ` b ) /\ ( p ` A ) = 0 ) ) )
17 fveqeq2 
 |-  ( p = b -> ( ( deg ` p ) = ( deg ` b ) <-> ( deg ` b ) = ( deg ` b ) ) )
18 fveq1 
 |-  ( p = b -> ( p ` A ) = ( b ` A ) )
19 18 eqeq1d 
 |-  ( p = b -> ( ( p ` A ) = 0 <-> ( b ` A ) = 0 ) )
20 17 19 anbi12d 
 |-  ( p = b -> ( ( ( deg ` p ) = ( deg ` b ) /\ ( p ` A ) = 0 ) <-> ( ( deg ` b ) = ( deg ` b ) /\ ( b ` A ) = 0 ) ) )
21 16 20 rspc2ev 
 |-  ( ( ( deg ` b ) e. NN /\ b e. ( ( Poly ` QQ ) \ { 0p } ) /\ ( ( deg ` b ) = ( deg ` b ) /\ ( b ` A ) = 0 ) ) -> E. a e. NN E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = a /\ ( p ` A ) = 0 ) )
22 11 12 14 21 syl3anc 
 |-  ( ( ( b e. ( ( Poly ` QQ ) \ { 0p } ) /\ ( b ` A ) = 0 ) /\ A e. CC ) -> E. a e. NN E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = a /\ ( p ` A ) = 0 ) )
23 22 ex 
 |-  ( ( b e. ( ( Poly ` QQ ) \ { 0p } ) /\ ( b ` A ) = 0 ) -> ( A e. CC -> E. a e. NN E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = a /\ ( p ` A ) = 0 ) ) )
24 23 rexlimiva 
 |-  ( E. b e. ( ( Poly ` QQ ) \ { 0p } ) ( b ` A ) = 0 -> ( A e. CC -> E. a e. NN E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = a /\ ( p ` A ) = 0 ) ) )
25 24 impcom 
 |-  ( ( A e. CC /\ E. b e. ( ( Poly ` QQ ) \ { 0p } ) ( b ` A ) = 0 ) -> E. a e. NN E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = a /\ ( p ` A ) = 0 ) )
26 elqaa 
 |-  ( A e. AA <-> ( A e. CC /\ E. b e. ( ( Poly ` QQ ) \ { 0p } ) ( b ` A ) = 0 ) )
27 rabn0 
 |-  ( { a e. NN | E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = a /\ ( p ` A ) = 0 ) } =/= (/) <-> E. a e. NN E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = a /\ ( p ` A ) = 0 ) )
28 25 26 27 3imtr4i 
 |-  ( A e. AA -> { a e. NN | E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = a /\ ( p ` A ) = 0 ) } =/= (/) )
29 infssuzcl 
 |-  ( ( { a e. NN | E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = a /\ ( p ` A ) = 0 ) } C_ ( ZZ>= ` 1 ) /\ { a e. NN | E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = a /\ ( p ` A ) = 0 ) } =/= (/) ) -> inf ( { a e. NN | E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = a /\ ( p ` A ) = 0 ) } , RR , < ) e. { a e. NN | E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = a /\ ( p ` A ) = 0 ) } )
30 4 28 29 sylancr 
 |-  ( A e. AA -> inf ( { a e. NN | E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = a /\ ( p ` A ) = 0 ) } , RR , < ) e. { a e. NN | E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = a /\ ( p ` A ) = 0 ) } )
31 1 30 eqeltrd 
 |-  ( A e. AA -> ( degAA ` A ) e. { a e. NN | E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = a /\ ( p ` A ) = 0 ) } )
32 eqeq2 
 |-  ( a = ( degAA ` A ) -> ( ( deg ` p ) = a <-> ( deg ` p ) = ( degAA ` A ) ) )
33 32 anbi1d 
 |-  ( a = ( degAA ` A ) -> ( ( ( deg ` p ) = a /\ ( p ` A ) = 0 ) <-> ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 ) ) )
34 33 rexbidv 
 |-  ( a = ( degAA ` A ) -> ( E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = a /\ ( p ` A ) = 0 ) <-> E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 ) ) )
35 34 elrab 
 |-  ( ( degAA ` A ) e. { a e. NN | E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = a /\ ( p ` A ) = 0 ) } <-> ( ( degAA ` A ) e. NN /\ E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 ) ) )
36 31 35 sylib 
 |-  ( A e. AA -> ( ( degAA ` A ) e. NN /\ E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 ) ) )