Theorem deg1nn0clb

Description: A polynomial is nonzero iff it has definite degree. (Contributed by Stefan O'Rear, 23-Mar-2015)

	Ref	Expression
Hypotheses	deg1z.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
	deg1z.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	deg1z.z	$$⊢\underset{\dot{}}{0}=0_P$$
	deg1nn0cl.b	$$⊢B={\mathrm{Base}}_P$$
Assertion	deg1nn0clb	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\right)\to \left(F\ne \underset{\dot{}}{0}\leftrightarrow D\left(F\right)\in {\mathbb{N}}_0\right)$$

Proof

Step	Hyp	Ref	Expression
1		deg1z.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
2		deg1z.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
3		deg1z.z	$$⊢\underset{\dot{}}{0}=0_P$$
4		deg1nn0cl.b	$$⊢B={\mathrm{Base}}_P$$
5	1 2 3 4	deg1nn0cl	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge F\ne \underset{\dot{}}{0}\right)\to D\left(F\right)\in {\mathbb{N}}_0$$
6	5	3expia	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\right)\to \left(F\ne \underset{\dot{}}{0}\to D\left(F\right)\in {\mathbb{N}}_0\right)$$
7		mnfnre	$$⊢\mathrm{-\infty }\notin ℝ$$
8	7	neli	$$⊢\neg \mathrm{-\infty }\in ℝ$$
9		nn0re	$$⊢\mathrm{-\infty }\in {\mathbb{N}}_0\to \mathrm{-\infty }\in ℝ$$
10	8 9	mto	$$⊢\neg \mathrm{-\infty }\in {\mathbb{N}}_0$$
11	1 2 3	deg1z	$$⊢R\in \mathrm{Ring}\to D\left(\underset{\dot{}}{0}\right)=\mathrm{-\infty }$$
12	11	adantr	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\right)\to D\left(\underset{\dot{}}{0}\right)=\mathrm{-\infty }$$
13	12	eleq1d	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\right)\to \left(D\left(\underset{\dot{}}{0}\right)\in {\mathbb{N}}_0\leftrightarrow \mathrm{-\infty }\in {\mathbb{N}}_0\right)$$
14	10 13	mtbiri	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\right)\to \neg D\left(\underset{\dot{}}{0}\right)\in {\mathbb{N}}_0$$
15		fveq2	$$⊢F=\underset{\dot{}}{0}\to D\left(F\right)=D\left(\underset{\dot{}}{0}\right)$$
16	15	eleq1d	$$⊢F=\underset{\dot{}}{0}\to \left(D\left(F\right)\in {\mathbb{N}}_0\leftrightarrow D\left(\underset{\dot{}}{0}\right)\in {\mathbb{N}}_0\right)$$
17	16	notbid	$$⊢F=\underset{\dot{}}{0}\to \left(\neg D\left(F\right)\in {\mathbb{N}}_0\leftrightarrow \neg D\left(\underset{\dot{}}{0}\right)\in {\mathbb{N}}_0\right)$$
18	14 17	syl5ibrcom	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\right)\to \left(F=\underset{\dot{}}{0}\to \neg D\left(F\right)\in {\mathbb{N}}_0\right)$$
19	18	necon2ad	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\right)\to \left(D\left(F\right)\in {\mathbb{N}}_0\to F\ne \underset{\dot{}}{0}\right)$$
20	6 19	impbid	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\right)\to \left(F\ne \underset{\dot{}}{0}\leftrightarrow D\left(F\right)\in {\mathbb{N}}_0\right)$$