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={\mathrm{deg}}_1\left(R\right)$$
	deg1leb.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	deg1leb.b	$$⊢B={\mathrm{Base}}_P$$
	deg1leb.y	$$⊢\underset{\dot{}}{0}=0_R$$
	deg1leb.a	$$⊢A={\mathrm{coe}}_1\left(F\right)$$
Assertion	deg1lt	$$⊢\left(F\in B\wedge G\in {\mathbb{N}}_0\wedge D\left(F\right)<G\right)\to A\left(G\right)=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		deg1leb.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
2		deg1leb.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
3		deg1leb.b	$$⊢B={\mathrm{Base}}_P$$
4		deg1leb.y	$$⊢\underset{\dot{}}{0}=0_R$$
5		deg1leb.a	$$⊢A={\mathrm{coe}}_1\left(F\right)$$
6		simp3	$$⊢\left(F\in B\wedge G\in {\mathbb{N}}_0\wedge D\left(F\right)<G\right)\to D\left(F\right)<G$$
7		breq2	$$⊢x=G\to \left(D\left(F\right)<x\leftrightarrow D\left(F\right)<G\right)$$
8		fveqeq2	$$⊢x=G\to \left(A\left(x\right)=\underset{\dot{}}{0}\leftrightarrow A\left(G\right)=\underset{\dot{}}{0}\right)$$
9	7 8	imbi12d	$$⊢x=G\to \left(\left(D\left(F\right)<x\to A\left(x\right)=\underset{\dot{}}{0}\right)\leftrightarrow \left(D\left(F\right)<G\to A\left(G\right)=\underset{\dot{}}{0}\right)\right)$$
10	1 2 3	deg1xrcl	$$⊢F\in B\to D\left(F\right)\in {ℝ}^{*}$$
11	10	3ad2ant1	$$⊢\left(F\in B\wedge G\in {\mathbb{N}}_0\wedge D\left(F\right)<G\right)\to D\left(F\right)\in {ℝ}^{*}$$
12	11	xrleidd	$$⊢\left(F\in B\wedge G\in {\mathbb{N}}_0\wedge D\left(F\right)<G\right)\to D\left(F\right)\le D\left(F\right)$$
13		simp1	$$⊢\left(F\in B\wedge G\in {\mathbb{N}}_0\wedge D\left(F\right)<G\right)\to F\in B$$
14	1 2 3 4 5	deg1leb	$$⊢\left(F\in B\wedge D\left(F\right)\in {ℝ}^{*}\right)\to \left(D\left(F\right)\le D\left(F\right)\leftrightarrow \forall x\in {\mathbb{N}}_0\left(D\left(F\right)<x\to A\left(x\right)=\underset{\dot{}}{0}\right)\right)$$
15	13 10 14	syl2anc2	$$⊢\left(F\in B\wedge G\in {\mathbb{N}}_0\wedge D\left(F\right)<G\right)\to \left(D\left(F\right)\le D\left(F\right)\leftrightarrow \forall x\in {\mathbb{N}}_0\left(D\left(F\right)<x\to A\left(x\right)=\underset{\dot{}}{0}\right)\right)$$
16	12 15	mpbid	$$⊢\left(F\in B\wedge G\in {\mathbb{N}}_0\wedge D\left(F\right)<G\right)\to \forall x\in {\mathbb{N}}_0\left(D\left(F\right)<x\to A\left(x\right)=\underset{\dot{}}{0}\right)$$
17		simp2	$$⊢\left(F\in B\wedge G\in {\mathbb{N}}_0\wedge D\left(F\right)<G\right)\to G\in {\mathbb{N}}_0$$
18	9 16 17	rspcdva	$$⊢\left(F\in B\wedge G\in {\mathbb{N}}_0\wedge D\left(F\right)<G\right)\to \left(D\left(F\right)<G\to A\left(G\right)=\underset{\dot{}}{0}\right)$$
19	6 18	mpd	$$⊢\left(F\in B\wedge G\in {\mathbb{N}}_0\wedge D\left(F\right)<G\right)\to A\left(G\right)=\underset{\dot{}}{0}$$