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 ) )