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

Metamath Proof Explorer

Theorem deg1ge

Description: Conversely, a nonzero coefficient sets a lower bound on the degree. (Contributed by Stefan O'Rear, 23-Mar-2015)

Ref Expression
Hypotheses deg1leb.d 
|- D = ( deg1 ` R )
deg1leb.p 
|- P = ( Poly1 ` R )
deg1leb.b 
|- B = ( Base ` P )
deg1leb.y 
|- .0. = ( 0g ` R )
deg1leb.a 
|- A = ( coe1 ` F )
Assertion deg1ge 
|- ( ( F e. B /\ G e. NN0 /\ ( A ` G ) =/= .0. ) -> G <_ ( D ` F ) )

Proof

Step Hyp Ref Expression
1 deg1leb.d 
 |-  D = ( deg1 ` R )
2 deg1leb.p 
 |-  P = ( Poly1 ` R )
3 deg1leb.b 
 |-  B = ( Base ` P )
4 deg1leb.y 
 |-  .0. = ( 0g ` R )
5 deg1leb.a 
 |-  A = ( coe1 ` F )
6 1 2 3 deg1xrcl 
 |-  ( F e. B -> ( D ` F ) e. RR* )
7 nn0re 
 |-  ( G e. NN0 -> G e. RR )
8 7 rexrd 
 |-  ( G e. NN0 -> G e. RR* )
9 xrltnle 
 |-  ( ( ( D ` F ) e. RR* /\ G e. RR* ) -> ( ( D ` F ) < G <-> -. G <_ ( D ` F ) ) )
10 6 8 9 syl2an 
 |-  ( ( F e. B /\ G e. NN0 ) -> ( ( D ` F ) < G <-> -. G <_ ( D ` F ) ) )
11 1 2 3 4 5 deg1lt 
 |-  ( ( F e. B /\ G e. NN0 /\ ( D ` F ) < G ) -> ( A ` G ) = .0. )
12 11 3expia 
 |-  ( ( F e. B /\ G e. NN0 ) -> ( ( D ` F ) < G -> ( A ` G ) = .0. ) )
13 10 12 sylbird 
 |-  ( ( F e. B /\ G e. NN0 ) -> ( -. G <_ ( D ` F ) -> ( A ` G ) = .0. ) )
14 13 necon1ad 
 |-  ( ( F e. B /\ G e. NN0 ) -> ( ( A ` G ) =/= .0. -> G <_ ( D ` F ) ) )
15 14 3impia 
 |-  ( ( F e. B /\ G e. NN0 /\ ( A ` G ) =/= .0. ) -> G <_ ( D ` F ) )