Metamath Proof Explorer

Theorem dgraa0p

Description: A rational polynomial of degree less than an algebraic number cannot be zero at that number unless it is the zero polynomial. (Contributed by Stefan O'Rear, 25-Nov-2014)

Ref Expression
Assertion dgraa0p 
|- ( ( A e. AA /\ P e. ( Poly ` QQ ) /\ ( deg ` P ) < ( degAA ` A ) ) -> ( ( P ` A ) = 0 <-> P = 0p ) )

Proof

Step Hyp Ref Expression
1 simpl3 
 |-  ( ( ( A e. AA /\ P e. ( Poly ` QQ ) /\ ( deg ` P ) < ( degAA ` A ) ) /\ P =/= 0p ) -> ( deg ` P ) < ( degAA ` A ) )
2 simpl2 
 |-  ( ( ( A e. AA /\ P e. ( Poly ` QQ ) /\ ( deg ` P ) < ( degAA ` A ) ) /\ P =/= 0p ) -> P e. ( Poly ` QQ ) )
3 dgrcl 
 |-  ( P e. ( Poly ` QQ ) -> ( deg ` P ) e. NN0 )
4 2 3 syl 
 |-  ( ( ( A e. AA /\ P e. ( Poly ` QQ ) /\ ( deg ` P ) < ( degAA ` A ) ) /\ P =/= 0p ) -> ( deg ` P ) e. NN0 )
5 4 nn0red 
 |-  ( ( ( A e. AA /\ P e. ( Poly ` QQ ) /\ ( deg ` P ) < ( degAA ` A ) ) /\ P =/= 0p ) -> ( deg ` P ) e. RR )
6 simpl1 
 |-  ( ( ( A e. AA /\ P e. ( Poly ` QQ ) /\ ( deg ` P ) < ( degAA ` A ) ) /\ P =/= 0p ) -> A e. AA )
7 dgraacl 
 |-  ( A e. AA -> ( degAA ` A ) e. NN )
8 6 7 syl 
 |-  ( ( ( A e. AA /\ P e. ( Poly ` QQ ) /\ ( deg ` P ) < ( degAA ` A ) ) /\ P =/= 0p ) -> ( degAA ` A ) e. NN )
9 8 nnred 
 |-  ( ( ( A e. AA /\ P e. ( Poly ` QQ ) /\ ( deg ` P ) < ( degAA ` A ) ) /\ P =/= 0p ) -> ( degAA ` A ) e. RR )
10 5 9 ltnled 
 |-  ( ( ( A e. AA /\ P e. ( Poly ` QQ ) /\ ( deg ` P ) < ( degAA ` A ) ) /\ P =/= 0p ) -> ( ( deg ` P ) < ( degAA ` A ) <-> -. ( degAA ` A ) <_ ( deg ` P ) ) )
11 1 10 mpbid 
 |-  ( ( ( A e. AA /\ P e. ( Poly ` QQ ) /\ ( deg ` P ) < ( degAA ` A ) ) /\ P =/= 0p ) -> -. ( degAA ` A ) <_ ( deg ` P ) )
12 simpl2 
 |-  ( ( ( A e. AA /\ P e. ( Poly ` QQ ) /\ ( deg ` P ) < ( degAA ` A ) ) /\ ( P =/= 0p /\ ( P ` A ) = 0 ) ) -> P e. ( Poly ` QQ ) )
13 simprl 
 |-  ( ( ( A e. AA /\ P e. ( Poly ` QQ ) /\ ( deg ` P ) < ( degAA ` A ) ) /\ ( P =/= 0p /\ ( P ` A ) = 0 ) ) -> P =/= 0p )
14 simpl1 
 |-  ( ( ( A e. AA /\ P e. ( Poly ` QQ ) /\ ( deg ` P ) < ( degAA ` A ) ) /\ ( P =/= 0p /\ ( P ` A ) = 0 ) ) -> A e. AA )
15 aacn 
 |-  ( A e. AA -> A e. CC )
16 14 15 syl 
 |-  ( ( ( A e. AA /\ P e. ( Poly ` QQ ) /\ ( deg ` P ) < ( degAA ` A ) ) /\ ( P =/= 0p /\ ( P ` A ) = 0 ) ) -> A e. CC )
17 simprr 
 |-  ( ( ( A e. AA /\ P e. ( Poly ` QQ ) /\ ( deg ` P ) < ( degAA ` A ) ) /\ ( P =/= 0p /\ ( P ` A ) = 0 ) ) -> ( P ` A ) = 0 )
18 dgraaub 
 |-  ( ( ( P e. ( Poly ` QQ ) /\ P =/= 0p ) /\ ( A e. CC /\ ( P ` A ) = 0 ) ) -> ( degAA ` A ) <_ ( deg ` P ) )
19 12 13 16 17 18 syl22anc 
 |-  ( ( ( A e. AA /\ P e. ( Poly ` QQ ) /\ ( deg ` P ) < ( degAA ` A ) ) /\ ( P =/= 0p /\ ( P ` A ) = 0 ) ) -> ( degAA ` A ) <_ ( deg ` P ) )
20 19 expr 
 |-  ( ( ( A e. AA /\ P e. ( Poly ` QQ ) /\ ( deg ` P ) < ( degAA ` A ) ) /\ P =/= 0p ) -> ( ( P ` A ) = 0 -> ( degAA ` A ) <_ ( deg ` P ) ) )
21 11 20 mtod 
 |-  ( ( ( A e. AA /\ P e. ( Poly ` QQ ) /\ ( deg ` P ) < ( degAA ` A ) ) /\ P =/= 0p ) -> -. ( P ` A ) = 0 )
22 21 ex 
 |-  ( ( A e. AA /\ P e. ( Poly ` QQ ) /\ ( deg ` P ) < ( degAA ` A ) ) -> ( P =/= 0p -> -. ( P ` A ) = 0 ) )
23 22 necon4ad 
 |-  ( ( A e. AA /\ P e. ( Poly ` QQ ) /\ ( deg ` P ) < ( degAA ` A ) ) -> ( ( P ` A ) = 0 -> P = 0p ) )
24 0pval 
 |-  ( A e. CC -> ( 0p ` A ) = 0 )
25 15 24 syl 
 |-  ( A e. AA -> ( 0p ` A ) = 0 )
26 fveq1 
 |-  ( P = 0p -> ( P ` A ) = ( 0p ` A ) )
27 26 eqeq1d 
 |-  ( P = 0p -> ( ( P ` A ) = 0 <-> ( 0p ` A ) = 0 ) )
28 25 27 syl5ibrcom 
 |-  ( A e. AA -> ( P = 0p -> ( P ` A ) = 0 ) )
29 28 3ad2ant1 
 |-  ( ( A e. AA /\ P e. ( Poly ` QQ ) /\ ( deg ` P ) < ( degAA ` A ) ) -> ( P = 0p -> ( P ` A ) = 0 ) )
30 23 29 impbid 
 |-  ( ( A e. AA /\ P e. ( Poly ` QQ ) /\ ( deg ` P ) < ( degAA ` A ) ) -> ( ( P ` A ) = 0 <-> P = 0p ) )