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 = \deg_{1} (R)$
	deg1leb.p	$⊢ P = {Poly}_{1} (R)$
	deg1leb.b	$⊢ B = {Base}_{P}$
	deg1leb.y	$⊢ \underset{˙}{0} = 0_{R}$
	deg1leb.a	$⊢ A = {coe}_{1} (F)$
Assertion	deg1ge	$⊢ (F \in B \land G \in ℕ_{0} \land A (G) \neq \underset{˙}{0}) \to G \leq D (F)$

Step	Hyp	Ref	Expression
1		deg1leb.d	$⊢ D = \deg_{1} (R)$
2		deg1leb.p	$⊢ P = {Poly}_{1} (R)$
3		deg1leb.b	$⊢ B = {Base}_{P}$
4		deg1leb.y	$⊢ \underset{˙}{0} = 0_{R}$
5		deg1leb.a	$⊢ A = {coe}_{1} (F)$
6	1 2 3	deg1xrcl	$⊢ F \in B \to D (F) \in ℝ^{*}$
7		nn0re	$⊢ G \in ℕ_{0} \to G \in ℝ$
8	7	rexrd	$⊢ G \in ℕ_{0} \to G \in ℝ^{*}$
9		xrltnle	$⊢ (D (F) \in ℝ^{} \land G \in ℝ^{}) \to (D (F) < G \leftrightarrow \neg G \leq D (F))$
10	6 8 9	syl2an	$⊢ (F \in B \land G \in ℕ_{0}) \to (D (F) < G \leftrightarrow \neg G \leq D (F))$
11	1 2 3 4 5	deg1lt	$⊢ (F \in B \land G \in ℕ_{0} \land D (F) < G) \to A (G) = \underset{˙}{0}$
12	11	3expia	$⊢ (F \in B \land G \in ℕ_{0}) \to (D (F) < G \to A (G) = \underset{˙}{0})$
13	10 12	sylbird	$⊢ (F \in B \land G \in ℕ_{0}) \to (\neg G \leq D (F) \to A (G) = \underset{˙}{0})$
14	13	necon1ad	$⊢ (F \in B \land G \in ℕ_{0}) \to (A (G) \neq \underset{˙}{0} \to G \leq D (F))$
15	14	3impia	$⊢ (F \in B \land G \in ℕ_{0} \land A (G) \neq \underset{˙}{0}) \to G \leq D (F)$

Metamath Proof Explorer