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 
|- ( ( ( P e. ( Poly ` QQ ) /\ P =/= 0p ) /\ ( A e. CC /\ ( P ` A ) = 0 ) ) -> ( degAA ` A ) <_ ( deg ` P ) )

Proof

Step Hyp Ref Expression
1 simprl 
 |-  ( ( ( P e. ( Poly ` QQ ) /\ P =/= 0p ) /\ ( A e. CC /\ ( P ` A ) = 0 ) ) -> A e. CC )
2 eldifsn 
 |-  ( P e. ( ( Poly ` QQ ) \ { 0p } ) <-> ( P e. ( Poly ` QQ ) /\ P =/= 0p ) )
3 2 biimpri 
 |-  ( ( P e. ( Poly ` QQ ) /\ P =/= 0p ) -> P e. ( ( Poly ` QQ ) \ { 0p } ) )
4 3 adantr 
 |-  ( ( ( P e. ( Poly ` QQ ) /\ P =/= 0p ) /\ ( A e. CC /\ ( P ` A ) = 0 ) ) -> P e. ( ( Poly ` QQ ) \ { 0p } ) )
5 simprr 
 |-  ( ( ( P e. ( Poly ` QQ ) /\ P =/= 0p ) /\ ( A e. CC /\ ( P ` A ) = 0 ) ) -> ( P ` A ) = 0 )
6 fveq1 
 |-  ( a = P -> ( a ` A ) = ( P ` A ) )
7 6 eqeq1d 
 |-  ( a = P -> ( ( a ` A ) = 0 <-> ( P ` A ) = 0 ) )
8 7 rspcev 
 |-  ( ( P e. ( ( Poly ` QQ ) \ { 0p } ) /\ ( P ` A ) = 0 ) -> E. a e. ( ( Poly ` QQ ) \ { 0p } ) ( a ` A ) = 0 )
9 4 5 8 syl2anc 
 |-  ( ( ( P e. ( Poly ` QQ ) /\ P =/= 0p ) /\ ( A e. CC /\ ( P ` A ) = 0 ) ) -> E. a e. ( ( Poly ` QQ ) \ { 0p } ) ( a ` A ) = 0 )
10 elqaa 
 |-  ( A e. AA <-> ( A e. CC /\ E. a e. ( ( Poly ` QQ ) \ { 0p } ) ( a ` A ) = 0 ) )
11 1 9 10 sylanbrc 
 |-  ( ( ( P e. ( Poly ` QQ ) /\ P =/= 0p ) /\ ( A e. CC /\ ( P ` A ) = 0 ) ) -> A e. AA )
12 dgraaval 
 |-  ( A e. AA -> ( degAA ` A ) = inf ( { a e. NN | E. b e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` b ) = a /\ ( b ` A ) = 0 ) } , RR , < ) )
13 11 12 syl 
 |-  ( ( ( P e. ( Poly ` QQ ) /\ P =/= 0p ) /\ ( A e. CC /\ ( P ` A ) = 0 ) ) -> ( degAA ` A ) = inf ( { a e. NN | E. b e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` b ) = a /\ ( b ` A ) = 0 ) } , RR , < ) )
14 ssrab2 
 |-  { a e. NN | E. b e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` b ) = a /\ ( b ` A ) = 0 ) } C_ NN
15 nnuz 
 |-  NN = ( ZZ>= ` 1 )
16 14 15 sseqtri 
 |-  { a e. NN | E. b e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` b ) = a /\ ( b ` A ) = 0 ) } C_ ( ZZ>= ` 1 )
17 dgrnznn 
 |-  ( ( ( P e. ( Poly ` QQ ) /\ P =/= 0p ) /\ ( A e. CC /\ ( P ` A ) = 0 ) ) -> ( deg ` P ) e. NN )
18 eqid 
 |-  ( deg ` P ) = ( deg ` P )
19 5 18 jctil 
 |-  ( ( ( P e. ( Poly ` QQ ) /\ P =/= 0p ) /\ ( A e. CC /\ ( P ` A ) = 0 ) ) -> ( ( deg ` P ) = ( deg ` P ) /\ ( P ` A ) = 0 ) )
20 fveqeq2 
 |-  ( b = P -> ( ( deg ` b ) = ( deg ` P ) <-> ( deg ` P ) = ( deg ` P ) ) )
21 fveq1 
 |-  ( b = P -> ( b ` A ) = ( P ` A ) )
22 21 eqeq1d 
 |-  ( b = P -> ( ( b ` A ) = 0 <-> ( P ` A ) = 0 ) )
23 20 22 anbi12d 
 |-  ( b = P -> ( ( ( deg ` b ) = ( deg ` P ) /\ ( b ` A ) = 0 ) <-> ( ( deg ` P ) = ( deg ` P ) /\ ( P ` A ) = 0 ) ) )
24 23 rspcev 
 |-  ( ( P e. ( ( Poly ` QQ ) \ { 0p } ) /\ ( ( deg ` P ) = ( deg ` P ) /\ ( P ` A ) = 0 ) ) -> E. b e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` b ) = ( deg ` P ) /\ ( b ` A ) = 0 ) )
25 4 19 24 syl2anc 
 |-  ( ( ( P e. ( Poly ` QQ ) /\ P =/= 0p ) /\ ( A e. CC /\ ( P ` A ) = 0 ) ) -> E. b e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` b ) = ( deg ` P ) /\ ( b ` A ) = 0 ) )
26 eqeq2 
 |-  ( a = ( deg ` P ) -> ( ( deg ` b ) = a <-> ( deg ` b ) = ( deg ` P ) ) )
27 26 anbi1d 
 |-  ( a = ( deg ` P ) -> ( ( ( deg ` b ) = a /\ ( b ` A ) = 0 ) <-> ( ( deg ` b ) = ( deg ` P ) /\ ( b ` A ) = 0 ) ) )
28 27 rexbidv 
 |-  ( a = ( deg ` P ) -> ( E. b e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` b ) = a /\ ( b ` A ) = 0 ) <-> E. b e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` b ) = ( deg ` P ) /\ ( b ` A ) = 0 ) ) )
29 28 elrab 
 |-  ( ( deg ` P ) e. { a e. NN | E. b e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` b ) = a /\ ( b ` A ) = 0 ) } <-> ( ( deg ` P ) e. NN /\ E. b e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` b ) = ( deg ` P ) /\ ( b ` A ) = 0 ) ) )
30 17 25 29 sylanbrc 
 |-  ( ( ( P e. ( Poly ` QQ ) /\ P =/= 0p ) /\ ( A e. CC /\ ( P ` A ) = 0 ) ) -> ( deg ` P ) e. { a e. NN | E. b e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` b ) = a /\ ( b ` A ) = 0 ) } )
31 infssuzle 
 |-  ( ( { a e. NN | E. b e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` b ) = a /\ ( b ` A ) = 0 ) } C_ ( ZZ>= ` 1 ) /\ ( deg ` P ) e. { a e. NN | E. b e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` b ) = a /\ ( b ` A ) = 0 ) } ) -> inf ( { a e. NN | E. b e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` b ) = a /\ ( b ` A ) = 0 ) } , RR , < ) <_ ( deg ` P ) )
32 16 30 31 sylancr 
 |-  ( ( ( P e. ( Poly ` QQ ) /\ P =/= 0p ) /\ ( A e. CC /\ ( P ` A ) = 0 ) ) -> inf ( { a e. NN | E. b e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` b ) = a /\ ( b ` A ) = 0 ) } , RR , < ) <_ ( deg ` P ) )
33 13 32 eqbrtrd 
 |-  ( ( ( P e. ( Poly ` QQ ) /\ P =/= 0p ) /\ ( A e. CC /\ ( P ` A ) = 0 ) ) -> ( degAA ` A ) <_ ( deg ` P ) )