deg1lt0

Description: A polynomial is zero iff it has negative degree. (Contributed by Stefan O'Rear, 1-Apr-2015)

	Ref	Expression
Hypotheses	deg1z.d	$⊢ D = \deg_{1} (R)$
	deg1z.p	$⊢ P = {Poly}_{1} (R)$
	deg1z.z	$⊢ \underset{˙}{0} = 0_{P}$
	deg1nn0cl.b	$⊢ B = {Base}_{P}$
Assertion	deg1lt0	$⊢ (R \in Ring \land F \in B) \to (D (F) < 0 \leftrightarrow F = \underset{˙}{0})$

Step	Hyp	Ref	Expression
1		deg1z.d	$⊢ D = \deg_{1} (R)$
2		deg1z.p	$⊢ P = {Poly}_{1} (R)$
3		deg1z.z	$⊢ \underset{˙}{0} = 0_{P}$
4		deg1nn0cl.b	$⊢ B = {Base}_{P}$
5	1 2 3 4	deg1nn0cl	$⊢ (R \in Ring \land F \in B \land F \neq \underset{˙}{0}) \to D (F) \in ℕ_{0}$
6		nn0nlt0	$⊢ D (F) \in ℕ_{0} \to \neg D (F) < 0$
7	5 6	syl	$⊢ (R \in Ring \land F \in B \land F \neq \underset{˙}{0}) \to \neg D (F) < 0$
8	7	3expia	$⊢ (R \in Ring \land F \in B) \to (F \neq \underset{˙}{0} \to \neg D (F) < 0)$
9	8	necon4ad	$⊢ (R \in Ring \land F \in B) \to (D (F) < 0 \to F = \underset{˙}{0})$
10	1 2 3	deg1z	$⊢ R \in Ring \to D (\underset{˙}{0}) = −∞$
11		mnflt0	$⊢ −∞ < 0$
12	10 11	eqbrtrdi	$⊢ R \in Ring \to D (\underset{˙}{0}) < 0$
13	12	adantr	$⊢ (R \in Ring \land F \in B) \to D (\underset{˙}{0}) < 0$
14		fveq2	$⊢ F = \underset{˙}{0} \to D (F) = D (\underset{˙}{0})$
15	14	breq1d	$⊢ F = \underset{˙}{0} \to (D (F) < 0 \leftrightarrow D (\underset{˙}{0}) < 0)$
16	13 15	syl5ibrcom	$⊢ (R \in Ring \land F \in B) \to (F = \underset{˙}{0} \to D (F) < 0)$
17	9 16	impbid	$⊢ (R \in Ring \land F \in B) \to (D (F) < 0 \leftrightarrow F = \underset{˙}{0})$

Metamath Proof Explorer