Description: The degree of a sum of polynomials is at most the maximum of the degrees. (Contributed by Mario Carneiro, 24-Jul-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dgradd.1 | ⊢ 𝑀 = ( deg ‘ 𝐹 ) | |
dgradd.2 | ⊢ 𝑁 = ( deg ‘ 𝐺 ) | ||
Assertion | dgradd | ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( deg ‘ ( 𝐹 ∘f + 𝐺 ) ) ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dgradd.1 | ⊢ 𝑀 = ( deg ‘ 𝐹 ) | |
2 | dgradd.2 | ⊢ 𝑁 = ( deg ‘ 𝐺 ) | |
3 | eqid | ⊢ ( coeff ‘ 𝐹 ) = ( coeff ‘ 𝐹 ) | |
4 | eqid | ⊢ ( coeff ‘ 𝐺 ) = ( coeff ‘ 𝐺 ) | |
5 | 3 4 1 2 | coeaddlem | ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( coeff ‘ ( 𝐹 ∘f + 𝐺 ) ) = ( ( coeff ‘ 𝐹 ) ∘f + ( coeff ‘ 𝐺 ) ) ∧ ( deg ‘ ( 𝐹 ∘f + 𝐺 ) ) ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) |
6 | 5 | simprd | ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( deg ‘ ( 𝐹 ∘f + 𝐺 ) ) ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) |