Theorem deg1lt

Description: If the degree of a univariate polynomial is less than some index, then that coefficient must be zero. (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	deg1lt	|- ( ( F e. B /\ G e. NN0 /\ ( D ` F ) < G ) -> ( A ` G ) = .0. )

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		simp3	|- ( ( F e. B /\ G e. NN0 /\ ( D ` F ) < G ) -> ( D ` F ) < G )
7		breq2	|- ( x = G -> ( ( D ` F ) < x <-> ( D ` F ) < G ) )
8		fveqeq2	|- ( x = G -> ( ( A ` x ) = .0. <-> ( A ` G ) = .0. ) )
9	7 8	imbi12d	|- ( x = G -> ( ( ( D ` F ) < x -> ( A ` x ) = .0. ) <-> ( ( D ` F ) < G -> ( A ` G ) = .0. ) ) )
10	1 2 3	deg1xrcl	|- ( F e. B -> ( D ` F ) e. RR* )
11	10	3ad2ant1	|- ( ( F e. B /\ G e. NN0 /\ ( D ` F ) < G ) -> ( D ` F ) e. RR* )
12	11	xrleidd	|- ( ( F e. B /\ G e. NN0 /\ ( D ` F ) < G ) -> ( D ` F ) <_ ( D ` F ) )
13		simp1	|- ( ( F e. B /\ G e. NN0 /\ ( D ` F ) < G ) -> F e. B )
14	1 2 3 4 5	deg1leb	|- ( ( F e. B /\ ( D ` F ) e. RR* ) -> ( ( D ` F ) <_ ( D ` F ) <-> A. x e. NN0 ( ( D ` F ) < x -> ( A ` x ) = .0. ) ) )
15	13 10 14	syl2anc2	|- ( ( F e. B /\ G e. NN0 /\ ( D ` F ) < G ) -> ( ( D ` F ) <_ ( D ` F ) <-> A. x e. NN0 ( ( D ` F ) < x -> ( A ` x ) = .0. ) ) )
16	12 15	mpbid	|- ( ( F e. B /\ G e. NN0 /\ ( D ` F ) < G ) -> A. x e. NN0 ( ( D ` F ) < x -> ( A ` x ) = .0. ) )
17		simp2	|- ( ( F e. B /\ G e. NN0 /\ ( D ` F ) < G ) -> G e. NN0 )
18	9 16 17	rspcdva	|- ( ( F e. B /\ G e. NN0 /\ ( D ` F ) < G ) -> ( ( D ` F ) < G -> ( A ` G ) = .0. ) )
19	6 18	mpd	|- ( ( F e. B /\ G e. NN0 /\ ( D ` F ) < G ) -> ( A ` G ) = .0. )