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={\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	deg1ge	$$⊢\left(F\in B\wedge G\in {\mathbb{N}}_0\wedge A\left(G\right)\ne \underset{\dot{}}{0}\right)\to G\le D\left(F\right)$$

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	1 2 3	deg1xrcl	$$⊢F\in B\to D\left(F\right)\in {ℝ}^{*}$$
7		nn0re	$$⊢G\in {\mathbb{N}}_0\to G\in ℝ$$
8	7	rexrd	$$⊢G\in {\mathbb{N}}_0\to G\in {ℝ}^{*}$$
9		xrltnle	$$⊢\left(D\left(F\right)\in {ℝ}^{*}\wedge G\in {ℝ}^{*}\right)\to \left(D\left(F\right)<G\leftrightarrow \neg G\le D\left(F\right)\right)$$
10	6 8 9	syl2an	$$⊢\left(F\in B\wedge G\in {\mathbb{N}}_0\right)\to \left(D\left(F\right)<G\leftrightarrow \neg G\le D\left(F\right)\right)$$
11	1 2 3 4 5	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}$$
12	11	3expia	$$⊢\left(F\in B\wedge G\in {\mathbb{N}}_0\right)\to \left(D\left(F\right)<G\to A\left(G\right)=\underset{\dot{}}{0}\right)$$
13	10 12	sylbird	$$⊢\left(F\in B\wedge G\in {\mathbb{N}}_0\right)\to \left(\neg G\le D\left(F\right)\to A\left(G\right)=\underset{\dot{}}{0}\right)$$
14	13	necon1ad	$$⊢\left(F\in B\wedge G\in {\mathbb{N}}_0\right)\to \left(A\left(G\right)\ne \underset{\dot{}}{0}\to G\le D\left(F\right)\right)$$
15	14	3impia	$$⊢\left(F\in B\wedge G\in {\mathbb{N}}_0\wedge A\left(G\right)\ne \underset{\dot{}}{0}\right)\to G\le D\left(F\right)$$