This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem deg1lt0

Description: A polynomial is zero iff it has negative degree. (Contributed by Stefan O'Rear, 1-Apr-2015)

Ref Expression
Hypotheses deg1z.d 
|- D = ( deg1 ` R )
deg1z.p 
|- P = ( Poly1 ` R )
deg1z.z 
|- .0. = ( 0g ` P )
deg1nn0cl.b 
|- B = ( Base ` P )
Assertion deg1lt0 
|- ( ( R e. Ring /\ F e. B ) -> ( ( D ` F ) < 0 <-> F = .0. ) )

Proof

Step Hyp Ref Expression
1 deg1z.d 
 |-  D = ( deg1 ` R )
2 deg1z.p 
 |-  P = ( Poly1 ` R )
3 deg1z.z 
 |-  .0. = ( 0g ` P )
4 deg1nn0cl.b 
 |-  B = ( Base ` P )
5 1 2 3 4 deg1nn0cl 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( D ` F ) e. NN0 )
6 nn0nlt0 
 |-  ( ( D ` F ) e. NN0 -> -. ( D ` F ) < 0 )
7 5 6 syl 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> -. ( D ` F ) < 0 )
8 7 3expia 
 |-  ( ( R e. Ring /\ F e. B ) -> ( F =/= .0. -> -. ( D ` F ) < 0 ) )
9 8 necon4ad 
 |-  ( ( R e. Ring /\ F e. B ) -> ( ( D ` F ) < 0 -> F = .0. ) )
10 1 2 3 deg1z 
 |-  ( R e. Ring -> ( D ` .0. ) = -oo )
11 mnflt0 
 |-  -oo < 0
12 10 11 eqbrtrdi 
 |-  ( R e. Ring -> ( D ` .0. ) < 0 )
13 12 adantr 
 |-  ( ( R e. Ring /\ F e. B ) -> ( D ` .0. ) < 0 )
14 fveq2 
 |-  ( F = .0. -> ( D ` F ) = ( D ` .0. ) )
15 14 breq1d 
 |-  ( F = .0. -> ( ( D ` F ) < 0 <-> ( D ` .0. ) < 0 ) )
16 13 15 syl5ibrcom 
 |-  ( ( R e. Ring /\ F e. B ) -> ( F = .0. -> ( D ` F ) < 0 ) )
17 9 16 impbid 
 |-  ( ( R e. Ring /\ F e. B ) -> ( ( D ` F ) < 0 <-> F = .0. ) )