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	⊢ 𝑌 = ( Poly₁ ‘ 𝑅 )
	deg1addlt.d	⊢ 𝐷 = ( deg₁ ‘ 𝑅 )
	deg1addlt.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	deg1addlt.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
	deg1addlt.p	⊢ + = ( +_g ‘ 𝑌 )
	deg1addlt.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	deg1addlt.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
	deg1addlt.l	⊢ ( 𝜑 → 𝐿 ∈ ℝ^* )
	deg1addlt.1	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) < 𝐿 )
	deg1addlt.2	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) < 𝐿 )
Assertion	deg1addlt	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 + 𝐺 ) ) < 𝐿 )

Proof

Step	Hyp	Ref	Expression
1		deg1addlt.y	⊢ 𝑌 = ( Poly₁ ‘ 𝑅 )
2		deg1addlt.d	⊢ 𝐷 = ( deg₁ ‘ 𝑅 )
3		deg1addlt.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
4		deg1addlt.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
5		deg1addlt.p	⊢ + = ( +_g ‘ 𝑌 )
6		deg1addlt.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
7		deg1addlt.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
8		deg1addlt.l	⊢ ( 𝜑 → 𝐿 ∈ ℝ^* )
9		deg1addlt.1	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) < 𝐿 )
10		deg1addlt.2	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) < 𝐿 )
11	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑌 ∈ Ring )
12	3 11	syl	⊢ ( 𝜑 → 𝑌 ∈ Ring )
13	4 5	ringacl	⊢ ( ( 𝑌 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 + 𝐺 ) ∈ 𝐵 )
14	12 6 7 13	syl3anc	⊢ ( 𝜑 → ( 𝐹 + 𝐺 ) ∈ 𝐵 )
15	2 1 4	deg1xrcl	⊢ ( ( 𝐹 + 𝐺 ) ∈ 𝐵 → ( 𝐷 ‘ ( 𝐹 + 𝐺 ) ) ∈ ℝ^* )
16	14 15	syl	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 + 𝐺 ) ) ∈ ℝ^* )
17	2 1 4	deg1xrcl	⊢ ( 𝐺 ∈ 𝐵 → ( 𝐷 ‘ 𝐺 ) ∈ ℝ^* )
18	7 17	syl	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ∈ ℝ^* )
19	2 1 4	deg1xrcl	⊢ ( 𝐹 ∈ 𝐵 → ( 𝐷 ‘ 𝐹 ) ∈ ℝ^* )
20	6 19	syl	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ∈ ℝ^* )
21	18 20	ifcld	⊢ ( 𝜑 → if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) ∈ ℝ^* )
22	1 2 3 4 5 6 7	deg1addle	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 + 𝐺 ) ) ≤ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) )
23		xrmaxlt	⊢ ( ( ( 𝐷 ‘ 𝐹 ) ∈ ℝ^* ∧ ( 𝐷 ‘ 𝐺 ) ∈ ℝ^* ∧ 𝐿 ∈ ℝ^* ) → ( if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) < 𝐿 ↔ ( ( 𝐷 ‘ 𝐹 ) < 𝐿 ∧ ( 𝐷 ‘ 𝐺 ) < 𝐿 ) ) )
24	20 18 8 23	syl3anc	⊢ ( 𝜑 → ( if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) < 𝐿 ↔ ( ( 𝐷 ‘ 𝐹 ) < 𝐿 ∧ ( 𝐷 ‘ 𝐺 ) < 𝐿 ) ) )
25	9 10 24	mpbir2and	⊢ ( 𝜑 → if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) < 𝐿 )
26	16 21 8 22 25	xrlelttrd	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 + 𝐺 ) ) < 𝐿 )

Metamath Proof Explorer

Theorem deg1addlt

Proof