Theorem deg1le0eq0

Description: A polynomial with nonpositive degree is the zero polynomial iff its constant term is zero. Biconditional version of deg1scl . (Contributed by Thierry Arnoux, 22-Mar-2025)

	Ref	Expression
Hypotheses	deg1sclb.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
	deg1sclb.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	deg1sclb.z	$$⊢\underset{\dot{}}{0}=0_R$$
	deg1sclb.1	$$⊢B={\mathrm{Base}}_P$$
	deg1sclb.2	$$⊢O=0_P$$
	deg1sclb.3	$$⊢\phi \to R\in \mathrm{Ring}$$
	deg1sclb.4	$$⊢\phi \to F\in B$$
	deg1sclb.5	$$⊢\phi \to D\left(F\right)\le 0$$
Assertion	deg1le0eq0	$$⊢\phi \to \left(F=O\leftrightarrow {\mathrm{coe}}_1\left(F\right)\left(0\right)=\underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		deg1sclb.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
2		deg1sclb.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
3		deg1sclb.z	$$⊢\underset{\dot{}}{0}=0_R$$
4		deg1sclb.1	$$⊢B={\mathrm{Base}}_P$$
5		deg1sclb.2	$$⊢O=0_P$$
6		deg1sclb.3	$$⊢\phi \to R\in \mathrm{Ring}$$
7		deg1sclb.4	$$⊢\phi \to F\in B$$
8		deg1sclb.5	$$⊢\phi \to D\left(F\right)\le 0$$
9		eqid	$$⊢\mathrm{algSc}\left(P\right)=\mathrm{algSc}\left(P\right)$$
10	1 2 4 9	deg1le0	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\right)\to \left(D\left(F\right)\le 0\leftrightarrow F=\mathrm{algSc}\left(P\right)\left({\mathrm{coe}}_1\left(F\right)\left(0\right)\right)\right)$$
11	10	biimpa	$$⊢\left(\left(R\in \mathrm{Ring}\wedge F\in B\right)\wedge D\left(F\right)\le 0\right)\to F=\mathrm{algSc}\left(P\right)\left({\mathrm{coe}}_1\left(F\right)\left(0\right)\right)$$
12	6 7 8 11	syl21anc	$$⊢\phi \to F=\mathrm{algSc}\left(P\right)\left({\mathrm{coe}}_1\left(F\right)\left(0\right)\right)$$
13	12	adantr	$$⊢\left(\phi \wedge F=O\right)\to F=\mathrm{algSc}\left(P\right)\left({\mathrm{coe}}_1\left(F\right)\left(0\right)\right)$$
14		simpr	$$⊢\left(\phi \wedge F=O\right)\to F=O$$
15	13 14	eqtr3d	$$⊢\left(\phi \wedge F=O\right)\to \mathrm{algSc}\left(P\right)\left({\mathrm{coe}}_1\left(F\right)\left(0\right)\right)=O$$
16	6	adantr	$$⊢\left(\phi \wedge {\mathrm{coe}}_1\left(F\right)\left(0\right)\ne \underset{\dot{}}{0}\right)\to R\in \mathrm{Ring}$$
17		0nn0	$$⊢0\in {\mathbb{N}}_0$$
18		eqid	$$⊢{\mathrm{coe}}_1\left(F\right)={\mathrm{coe}}_1\left(F\right)$$
19		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
20	18 4 2 19	coe1fvalcl	$$⊢\left(F\in B\wedge 0\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(F\right)\left(0\right)\in {\mathrm{Base}}_R$$
21	7 17 20	sylancl	$$⊢\phi \to {\mathrm{coe}}_1\left(F\right)\left(0\right)\in {\mathrm{Base}}_R$$
22	21	adantr	$$⊢\left(\phi \wedge {\mathrm{coe}}_1\left(F\right)\left(0\right)\ne \underset{\dot{}}{0}\right)\to {\mathrm{coe}}_1\left(F\right)\left(0\right)\in {\mathrm{Base}}_R$$
23		simpr	$$⊢\left(\phi \wedge {\mathrm{coe}}_1\left(F\right)\left(0\right)\ne \underset{\dot{}}{0}\right)\to {\mathrm{coe}}_1\left(F\right)\left(0\right)\ne \underset{\dot{}}{0}$$
24	2 9 3 5 19	ply1scln0	$$⊢\left(R\in \mathrm{Ring}\wedge {\mathrm{coe}}_1\left(F\right)\left(0\right)\in {\mathrm{Base}}_R\wedge {\mathrm{coe}}_1\left(F\right)\left(0\right)\ne \underset{\dot{}}{0}\right)\to \mathrm{algSc}\left(P\right)\left({\mathrm{coe}}_1\left(F\right)\left(0\right)\right)\ne O$$
25	16 22 23 24	syl3anc	$$⊢\left(\phi \wedge {\mathrm{coe}}_1\left(F\right)\left(0\right)\ne \underset{\dot{}}{0}\right)\to \mathrm{algSc}\left(P\right)\left({\mathrm{coe}}_1\left(F\right)\left(0\right)\right)\ne O$$
26	25	ex	$$⊢\phi \to \left({\mathrm{coe}}_1\left(F\right)\left(0\right)\ne \underset{\dot{}}{0}\to \mathrm{algSc}\left(P\right)\left({\mathrm{coe}}_1\left(F\right)\left(0\right)\right)\ne O\right)$$
27	26	necon4d	$$⊢\phi \to \left(\mathrm{algSc}\left(P\right)\left({\mathrm{coe}}_1\left(F\right)\left(0\right)\right)=O\to {\mathrm{coe}}_1\left(F\right)\left(0\right)=\underset{\dot{}}{0}\right)$$
28	27	imp	$$⊢\left(\phi \wedge \mathrm{algSc}\left(P\right)\left({\mathrm{coe}}_1\left(F\right)\left(0\right)\right)=O\right)\to {\mathrm{coe}}_1\left(F\right)\left(0\right)=\underset{\dot{}}{0}$$
29	15 28	syldan	$$⊢\left(\phi \wedge F=O\right)\to {\mathrm{coe}}_1\left(F\right)\left(0\right)=\underset{\dot{}}{0}$$
30	12	adantr	$$⊢\left(\phi \wedge {\mathrm{coe}}_1\left(F\right)\left(0\right)=\underset{\dot{}}{0}\right)\to F=\mathrm{algSc}\left(P\right)\left({\mathrm{coe}}_1\left(F\right)\left(0\right)\right)$$
31		simpr	$$⊢\left(\phi \wedge {\mathrm{coe}}_1\left(F\right)\left(0\right)=\underset{\dot{}}{0}\right)\to {\mathrm{coe}}_1\left(F\right)\left(0\right)=\underset{\dot{}}{0}$$
32	31	fveq2d	$$⊢\left(\phi \wedge {\mathrm{coe}}_1\left(F\right)\left(0\right)=\underset{\dot{}}{0}\right)\to \mathrm{algSc}\left(P\right)\left({\mathrm{coe}}_1\left(F\right)\left(0\right)\right)=\mathrm{algSc}\left(P\right)\left(\underset{\dot{}}{0}\right)$$
33	2 9 3 5 6	ply1ascl0	$$⊢\phi \to \mathrm{algSc}\left(P\right)\left(\underset{\dot{}}{0}\right)=O$$
34	33	adantr	$$⊢\left(\phi \wedge {\mathrm{coe}}_1\left(F\right)\left(0\right)=\underset{\dot{}}{0}\right)\to \mathrm{algSc}\left(P\right)\left(\underset{\dot{}}{0}\right)=O$$
35	30 32 34	3eqtrd	$$⊢\left(\phi \wedge {\mathrm{coe}}_1\left(F\right)\left(0\right)=\underset{\dot{}}{0}\right)\to F=O$$
36	29 35	impbida	$$⊢\phi \to \left(F=O\leftrightarrow {\mathrm{coe}}_1\left(F\right)\left(0\right)=\underset{\dot{}}{0}\right)$$