Theorem deg1addlt

Description: If both factors have degree bounded by L , then the sum of the polynomials also has degree bounded by L . See also deg1addle . (Contributed by Thierry Arnoux, 2-Apr-2025)

	Ref	Expression
Hypotheses	deg1addlt.y	$$⊢Y={\mathrm{Poly}}_1\left(R\right)$$
	deg1addlt.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
	deg1addlt.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	deg1addlt.b	$$⊢B={\mathrm{Base}}_Y$$
	deg1addlt.p	$$⊢\underset{\dot{}}{+}={+}_Y$$
	deg1addlt.f	$$⊢\phi \to F\in B$$
	deg1addlt.g	$$⊢\phi \to G\in B$$
	deg1addlt.l	$$⊢\phi \to L\in {ℝ}^{*}$$
	deg1addlt.1	$$⊢\phi \to D\left(F\right)<L$$
	deg1addlt.2	$$⊢\phi \to D\left(G\right)<L$$
Assertion	deg1addlt	$$⊢\phi \to D\left(F\underset{\dot{}}{+}G\right)<L$$

Proof

Step	Hyp	Ref	Expression
1		deg1addlt.y	$$⊢Y={\mathrm{Poly}}_1\left(R\right)$$
2		deg1addlt.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
3		deg1addlt.r	$$⊢\phi \to R\in \mathrm{Ring}$$
4		deg1addlt.b	$$⊢B={\mathrm{Base}}_Y$$
5		deg1addlt.p	$$⊢\underset{\dot{}}{+}={+}_Y$$
6		deg1addlt.f	$$⊢\phi \to F\in B$$
7		deg1addlt.g	$$⊢\phi \to G\in B$$
8		deg1addlt.l	$$⊢\phi \to L\in {ℝ}^{*}$$
9		deg1addlt.1	$$⊢\phi \to D\left(F\right)<L$$
10		deg1addlt.2	$$⊢\phi \to D\left(G\right)<L$$
11	1	ply1ring	$$⊢R\in \mathrm{Ring}\to Y\in \mathrm{Ring}$$
12	3 11	syl	$$⊢\phi \to Y\in \mathrm{Ring}$$
13	4 5	ringacl	$$⊢\left(Y\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to F\underset{\dot{}}{+}G\in B$$
14	12 6 7 13	syl3anc	$$⊢\phi \to F\underset{\dot{}}{+}G\in B$$
15	2 1 4	deg1xrcl	$$⊢F\underset{\dot{}}{+}G\in B\to D\left(F\underset{\dot{}}{+}G\right)\in {ℝ}^{*}$$
16	14 15	syl	$$⊢\phi \to D\left(F\underset{\dot{}}{+}G\right)\in {ℝ}^{*}$$
17	2 1 4	deg1xrcl	$$⊢G\in B\to D\left(G\right)\in {ℝ}^{*}$$
18	7 17	syl	$$⊢\phi \to D\left(G\right)\in {ℝ}^{*}$$
19	2 1 4	deg1xrcl	$$⊢F\in B\to D\left(F\right)\in {ℝ}^{*}$$
20	6 19	syl	$$⊢\phi \to D\left(F\right)\in {ℝ}^{*}$$
21	18 20	ifcld	$$⊢\phi \to if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)\in {ℝ}^{*}$$
22	1 2 3 4 5 6 7	deg1addle	$$⊢\phi \to D\left(F\underset{\dot{}}{+}G\right)\le if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)$$
23		xrmaxlt	$$⊢\left(D\left(F\right)\in {ℝ}^{*}\wedge D\left(G\right)\in {ℝ}^{*}\wedge L\in {ℝ}^{*}\right)\to \left(if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)<L\leftrightarrow \left(D\left(F\right)<L\wedge D\left(G\right)<L\right)\right)$$
24	20 18 8 23	syl3anc	$$⊢\phi \to \left(if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)<L\leftrightarrow \left(D\left(F\right)<L\wedge D\left(G\right)<L\right)\right)$$
25	9 10 24	mpbir2and	$$⊢\phi \to if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)<L$$
26	16 21 8 22 25	xrlelttrd	$$⊢\phi \to D\left(F\underset{\dot{}}{+}G\right)<L$$