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 = ( Poly1 ` R )
	deg1addlt.d	|- D = ( deg1 ` R )
	deg1addlt.r	|- ( ph -> R e. Ring )
	deg1addlt.b	|- B = ( Base ` Y )
	deg1addlt.p	|- .+ = ( +g ` Y )
	deg1addlt.f	|- ( ph -> F e. B )
	deg1addlt.g	|- ( ph -> G e. B )
	deg1addlt.l	|- ( ph -> L e. RR* )
	deg1addlt.1	|- ( ph -> ( D ` F ) < L )
	deg1addlt.2	|- ( ph -> ( D ` G ) < L )
Assertion	deg1addlt	|- ( ph -> ( D ` ( F .+ G ) ) < L )

Proof

Step	Hyp	Ref	Expression
1		deg1addlt.y	|- Y = ( Poly1 ` R )
2		deg1addlt.d	|- D = ( deg1 ` R )
3		deg1addlt.r	|- ( ph -> R e. Ring )
4		deg1addlt.b	|- B = ( Base ` Y )
5		deg1addlt.p	|- .+ = ( +g ` Y )
6		deg1addlt.f	|- ( ph -> F e. B )
7		deg1addlt.g	|- ( ph -> G e. B )
8		deg1addlt.l	|- ( ph -> L e. RR* )
9		deg1addlt.1	|- ( ph -> ( D ` F ) < L )
10		deg1addlt.2	|- ( ph -> ( D ` G ) < L )
11	1	ply1ring	|- ( R e. Ring -> Y e. Ring )
12	3 11	syl	|- ( ph -> Y e. Ring )
13	4 5	ringacl	|- ( ( Y e. Ring /\ F e. B /\ G e. B ) -> ( F .+ G ) e. B )
14	12 6 7 13	syl3anc	|- ( ph -> ( F .+ G ) e. B )
15	2 1 4	deg1xrcl	|- ( ( F .+ G ) e. B -> ( D ` ( F .+ G ) ) e. RR* )
16	14 15	syl	|- ( ph -> ( D ` ( F .+ G ) ) e. RR* )
17	2 1 4	deg1xrcl	|- ( G e. B -> ( D ` G ) e. RR* )
18	7 17	syl	|- ( ph -> ( D ` G ) e. RR* )
19	2 1 4	deg1xrcl	|- ( F e. B -> ( D ` F ) e. RR* )
20	6 19	syl	|- ( ph -> ( D ` F ) e. RR* )
21	18 20	ifcld	|- ( ph -> if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) e. RR* )
22	1 2 3 4 5 6 7	deg1addle	|- ( ph -> ( D ` ( F .+ G ) ) <_ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) )
23		xrmaxlt	|- ( ( ( D ` F ) e. RR* /\ ( D ` G ) e. RR* /\ L e. RR* ) -> ( if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) < L <-> ( ( D ` F ) < L /\ ( D ` G ) < L ) ) )
24	20 18 8 23	syl3anc	|- ( ph -> ( if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) < L <-> ( ( D ` F ) < L /\ ( D ` G ) < L ) ) )
25	9 10 24	mpbir2and	|- ( ph -> if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) < L )
26	16 21 8 22 25	xrlelttrd	|- ( ph -> ( D ` ( F .+ G ) ) < L )