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