Metamath Proof Explorer

Theorem dgrsub

Description: The degree of a difference of polynomials is at most the maximum of the degrees. (Contributed by Mario Carneiro, 26-Jul-2014)

Ref Expression
Hypotheses dgrsub.1 ⊢ M = deg ⁡ F
dgrsub.2 ⊢ N = deg ⁡ G
Assertion dgrsub ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S → deg ⁡ F − f G ≤ if M ≤ N N M

Proof

Step Hyp Ref Expression
1 dgrsub.1 ⊢ M = deg ⁡ F
2 dgrsub.2 ⊢ N = deg ⁡ G
3 plyssc ⊢ Poly ⁡ S ⊆ Poly ⁡ ℂ
4 3 sseli ⊢ F ∈ Poly ⁡ S → F ∈ Poly ⁡ ℂ
5 ssid ⊢ ℂ ⊆ ℂ
6 neg1cn ⊢ − 1 ∈ ℂ
7 plyconst ⊢ ℂ ⊆ ℂ ∧ − 1 ∈ ℂ → ℂ × − 1 ∈ Poly ⁡ ℂ
8 5 6 7 mp2an ⊢ ℂ × − 1 ∈ Poly ⁡ ℂ
9 3 sseli ⊢ G ∈ Poly ⁡ S → G ∈ Poly ⁡ ℂ
10 plymulcl ⊢ ℂ × − 1 ∈ Poly ⁡ ℂ ∧ G ∈ Poly ⁡ ℂ → ℂ × − 1 × f G ∈ Poly ⁡ ℂ
11 8 9 10 sylancr ⊢ G ∈ Poly ⁡ S → ℂ × − 1 × f G ∈ Poly ⁡ ℂ
12 eqid ⊢ deg ⁡ ℂ × − 1 × f G = deg ⁡ ℂ × − 1 × f G
13 1 12 dgradd ⊢ F ∈ Poly ⁡ ℂ ∧ ℂ × − 1 × f G ∈ Poly ⁡ ℂ → deg ⁡ F + f ℂ × − 1 × f G ≤ if M ≤ deg ⁡ ℂ × − 1 × f G deg ⁡ ℂ × − 1 × f G M
14 4 11 13 syl2an ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S → deg ⁡ F + f ℂ × − 1 × f G ≤ if M ≤ deg ⁡ ℂ × − 1 × f G deg ⁡ ℂ × − 1 × f G M
15 cnex ⊢ ℂ ∈ V
16 plyf ⊢ F ∈ Poly ⁡ S → F : ℂ ⟶ ℂ
17 plyf ⊢ G ∈ Poly ⁡ S → G : ℂ ⟶ ℂ
18 ofnegsub ⊢ ℂ ∈ V ∧ F : ℂ ⟶ ℂ ∧ G : ℂ ⟶ ℂ → F + f ℂ × − 1 × f G = F − f G
19 15 16 17 18 mp3an3an ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S → F + f ℂ × − 1 × f G = F − f G
20 19 fveq2d ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S → deg ⁡ F + f ℂ × − 1 × f G = deg ⁡ F − f G
21 neg1ne0 ⊢ − 1 ≠ 0
22 dgrmulc ⊢ − 1 ∈ ℂ ∧ − 1 ≠ 0 ∧ G ∈ Poly ⁡ S → deg ⁡ ℂ × − 1 × f G = deg ⁡ G
23 6 21 22 mp3an12 ⊢ G ∈ Poly ⁡ S → deg ⁡ ℂ × − 1 × f G = deg ⁡ G
24 23 2 eqtr4di ⊢ G ∈ Poly ⁡ S → deg ⁡ ℂ × − 1 × f G = N
25 24 adantl ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S → deg ⁡ ℂ × − 1 × f G = N
26 25 breq2d ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S → M ≤ deg ⁡ ℂ × − 1 × f G ↔ M ≤ N
27 26 25 ifbieq1d ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S → if M ≤ deg ⁡ ℂ × − 1 × f G deg ⁡ ℂ × − 1 × f G M = if M ≤ N N M
28 14 20 27 3brtr3d ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S → deg ⁡ F − f G ≤ if M ≤ N N M