# Metamath Proof Explorer

## 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
deg1leb.a ${⊢}{A}={\mathrm{coe}}_{1}\left({F}\right)$
Assertion deg1ge

### 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
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 {ℕ}_{0}\to {G}\in ℝ$
8 7 rexrd ${⊢}{G}\in {ℕ}_{0}\to {G}\in {ℝ}^{*}$
9 xrltnle ${⊢}\left({D}\left({F}\right)\in {ℝ}^{*}\wedge {G}\in {ℝ}^{*}\right)\to \left({D}\left({F}\right)<{G}↔¬{G}\le {D}\left({F}\right)\right)$
10 6 8 9 syl2an ${⊢}\left({F}\in {B}\wedge {G}\in {ℕ}_{0}\right)\to \left({D}\left({F}\right)<{G}↔¬{G}\le {D}\left({F}\right)\right)$
11 1 2 3 4 5 deg1lt
12 11 3expia
13 10 12 sylbird