Metamath Proof Explorer

Theorem dgrsub2

Description: Subtracting two polynomials with the same degree and top coefficient gives a polynomial of strictly lower degree. (Contributed by Stefan O'Rear, 25-Nov-2014)

Ref Expression
Hypothesis dgrsub2.a ⊢ N = deg ⁡ F
Assertion dgrsub2 ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ T ∧ deg ⁡ G = N ∧ N ∈ ℕ ∧ coeff ⁡ F ⁡ N = coeff ⁡ G ⁡ N → deg ⁡ F − f G < N

Proof

Step Hyp Ref Expression
1 dgrsub2.a ⊢ N = deg ⁡ F
2 simpr2 ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ T ∧ deg ⁡ G = N ∧ N ∈ ℕ ∧ coeff ⁡ F ⁡ N = coeff ⁡ G ⁡ N → N ∈ ℕ
3 dgr0 ⊢ deg ⁡ 0 𝑝 = 0
4 nngt0 ⊢ N ∈ ℕ → 0 < N
5 3 4 eqbrtrid ⊢ N ∈ ℕ → deg ⁡ 0 𝑝 < N
6 fveq2 ⊢ F − f G = 0 𝑝 → deg ⁡ F − f G = deg ⁡ 0 𝑝
7 6 breq1d ⊢ F − f G = 0 𝑝 → deg ⁡ F − f G < N ↔ deg ⁡ 0 𝑝 < N
8 5 7 syl5ibrcom ⊢ N ∈ ℕ → F − f G = 0 𝑝 → deg ⁡ F − f G < N
9 2 8 syl ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ T ∧ deg ⁡ G = N ∧ N ∈ ℕ ∧ coeff ⁡ F ⁡ N = coeff ⁡ G ⁡ N → F − f G = 0 𝑝 → deg ⁡ F − f G < N
10 plyssc ⊢ Poly ⁡ S ⊆ Poly ⁡ ℂ
11 10 sseli ⊢ F ∈ Poly ⁡ S → F ∈ Poly ⁡ ℂ
12 plyssc ⊢ Poly ⁡ T ⊆ Poly ⁡ ℂ
13 12 sseli ⊢ G ∈ Poly ⁡ T → G ∈ Poly ⁡ ℂ
14 eqid ⊢ deg ⁡ F = deg ⁡ F
15 eqid ⊢ deg ⁡ G = deg ⁡ G
16 14 15 dgrsub ⊢ F ∈ Poly ⁡ ℂ ∧ G ∈ Poly ⁡ ℂ → deg ⁡ F − f G ≤ if deg ⁡ F ≤ deg ⁡ G deg ⁡ G deg ⁡ F
17 11 13 16 syl2an ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ T → deg ⁡ F − f G ≤ if deg ⁡ F ≤ deg ⁡ G deg ⁡ G deg ⁡ F
18 17 adantr ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ T ∧ deg ⁡ G = N ∧ N ∈ ℕ ∧ coeff ⁡ F ⁡ N = coeff ⁡ G ⁡ N → deg ⁡ F − f G ≤ if deg ⁡ F ≤ deg ⁡ G deg ⁡ G deg ⁡ F
19 simpr1 ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ T ∧ deg ⁡ G = N ∧ N ∈ ℕ ∧ coeff ⁡ F ⁡ N = coeff ⁡ G ⁡ N → deg ⁡ G = N
20 1 eqcomi ⊢ deg ⁡ F = N
21 20 a1i ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ T ∧ deg ⁡ G = N ∧ N ∈ ℕ ∧ coeff ⁡ F ⁡ N = coeff ⁡ G ⁡ N → deg ⁡ F = N
22 19 21 ifeq12d ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ T ∧ deg ⁡ G = N ∧ N ∈ ℕ ∧ coeff ⁡ F ⁡ N = coeff ⁡ G ⁡ N → if deg ⁡ F ≤ deg ⁡ G deg ⁡ G deg ⁡ F = if deg ⁡ F ≤ deg ⁡ G N N
23 ifid ⊢ if deg ⁡ F ≤ deg ⁡ G N N = N
24 22 23 eqtrdi ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ T ∧ deg ⁡ G = N ∧ N ∈ ℕ ∧ coeff ⁡ F ⁡ N = coeff ⁡ G ⁡ N → if deg ⁡ F ≤ deg ⁡ G deg ⁡ G deg ⁡ F = N
25 18 24 breqtrd ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ T ∧ deg ⁡ G = N ∧ N ∈ ℕ ∧ coeff ⁡ F ⁡ N = coeff ⁡ G ⁡ N → deg ⁡ F − f G ≤ N
26 eqid ⊢ coeff ⁡ F = coeff ⁡ F
27 eqid ⊢ coeff ⁡ G = coeff ⁡ G
28 26 27 coesub ⊢ F ∈ Poly ⁡ ℂ ∧ G ∈ Poly ⁡ ℂ → coeff ⁡ F − f G = coeff ⁡ F − f coeff ⁡ G
29 11 13 28 syl2an ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ T → coeff ⁡ F − f G = coeff ⁡ F − f coeff ⁡ G
30 29 adantr ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ T ∧ deg ⁡ G = N ∧ N ∈ ℕ ∧ coeff ⁡ F ⁡ N = coeff ⁡ G ⁡ N → coeff ⁡ F − f G = coeff ⁡ F − f coeff ⁡ G
31 30 fveq1d ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ T ∧ deg ⁡ G = N ∧ N ∈ ℕ ∧ coeff ⁡ F ⁡ N = coeff ⁡ G ⁡ N → coeff ⁡ F − f G ⁡ N = coeff ⁡ F − f coeff ⁡ G ⁡ N
32 2 nnnn0d ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ T ∧ deg ⁡ G = N ∧ N ∈ ℕ ∧ coeff ⁡ F ⁡ N = coeff ⁡ G ⁡ N → N ∈ ℕ 0
33 26 coef3 ⊢ F ∈ Poly ⁡ S → coeff ⁡ F : ℕ 0 ⟶ ℂ
34 33 ad2antrr ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ T ∧ deg ⁡ G = N ∧ N ∈ ℕ ∧ coeff ⁡ F ⁡ N = coeff ⁡ G ⁡ N → coeff ⁡ F : ℕ 0 ⟶ ℂ
35 34 ffnd ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ T ∧ deg ⁡ G = N ∧ N ∈ ℕ ∧ coeff ⁡ F ⁡ N = coeff ⁡ G ⁡ N → coeff ⁡ F Fn ℕ 0
36 27 coef3 ⊢ G ∈ Poly ⁡ T → coeff ⁡ G : ℕ 0 ⟶ ℂ
37 36 ad2antlr ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ T ∧ deg ⁡ G = N ∧ N ∈ ℕ ∧ coeff ⁡ F ⁡ N = coeff ⁡ G ⁡ N → coeff ⁡ G : ℕ 0 ⟶ ℂ
38 37 ffnd ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ T ∧ deg ⁡ G = N ∧ N ∈ ℕ ∧ coeff ⁡ F ⁡ N = coeff ⁡ G ⁡ N → coeff ⁡ G Fn ℕ 0
39 nn0ex ⊢ ℕ 0 ∈ V
40 39 a1i ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ T ∧ deg ⁡ G = N ∧ N ∈ ℕ ∧ coeff ⁡ F ⁡ N = coeff ⁡ G ⁡ N → ℕ 0 ∈ V
41 inidm ⊢ ℕ 0 ∩ ℕ 0 = ℕ 0
42 simplr3 ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ T ∧ deg ⁡ G = N ∧ N ∈ ℕ ∧ coeff ⁡ F ⁡ N = coeff ⁡ G ⁡ N ∧ N ∈ ℕ 0 → coeff ⁡ F ⁡ N = coeff ⁡ G ⁡ N
43 eqidd ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ T ∧ deg ⁡ G = N ∧ N ∈ ℕ ∧ coeff ⁡ F ⁡ N = coeff ⁡ G ⁡ N ∧ N ∈ ℕ 0 → coeff ⁡ G ⁡ N = coeff ⁡ G ⁡ N
44 35 38 40 40 41 42 43 ofval ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ T ∧ deg ⁡ G = N ∧ N ∈ ℕ ∧ coeff ⁡ F ⁡ N = coeff ⁡ G ⁡ N ∧ N ∈ ℕ 0 → coeff ⁡ F − f coeff ⁡ G ⁡ N = coeff ⁡ G ⁡ N − coeff ⁡ G ⁡ N
45 32 44 mpdan ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ T ∧ deg ⁡ G = N ∧ N ∈ ℕ ∧ coeff ⁡ F ⁡ N = coeff ⁡ G ⁡ N → coeff ⁡ F − f coeff ⁡ G ⁡ N = coeff ⁡ G ⁡ N − coeff ⁡ G ⁡ N
46 37 32 ffvelrnd ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ T ∧ deg ⁡ G = N ∧ N ∈ ℕ ∧ coeff ⁡ F ⁡ N = coeff ⁡ G ⁡ N → coeff ⁡ G ⁡ N ∈ ℂ
47 46 subidd ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ T ∧ deg ⁡ G = N ∧ N ∈ ℕ ∧ coeff ⁡ F ⁡ N = coeff ⁡ G ⁡ N → coeff ⁡ G ⁡ N − coeff ⁡ G ⁡ N = 0
48 31 45 47 3eqtrd ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ T ∧ deg ⁡ G = N ∧ N ∈ ℕ ∧ coeff ⁡ F ⁡ N = coeff ⁡ G ⁡ N → coeff ⁡ F − f G ⁡ N = 0
49 plysubcl ⊢ F ∈ Poly ⁡ ℂ ∧ G ∈ Poly ⁡ ℂ → F − f G ∈ Poly ⁡ ℂ
50 11 13 49 syl2an ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ T → F − f G ∈ Poly ⁡ ℂ
51 50 adantr ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ T ∧ deg ⁡ G = N ∧ N ∈ ℕ ∧ coeff ⁡ F ⁡ N = coeff ⁡ G ⁡ N → F − f G ∈ Poly ⁡ ℂ
52 eqid ⊢ deg ⁡ F − f G = deg ⁡ F − f G
53 eqid ⊢ coeff ⁡ F − f G = coeff ⁡ F − f G
54 52 53 dgrlt ⊢ F − f G ∈ Poly ⁡ ℂ ∧ N ∈ ℕ 0 → F − f G = 0 𝑝 ∨ deg ⁡ F − f G < N ↔ deg ⁡ F − f G ≤ N ∧ coeff ⁡ F − f G ⁡ N = 0
55 51 32 54 syl2anc ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ T ∧ deg ⁡ G = N ∧ N ∈ ℕ ∧ coeff ⁡ F ⁡ N = coeff ⁡ G ⁡ N → F − f G = 0 𝑝 ∨ deg ⁡ F − f G < N ↔ deg ⁡ F − f G ≤ N ∧ coeff ⁡ F − f G ⁡ N = 0
56 25 48 55 mpbir2and ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ T ∧ deg ⁡ G = N ∧ N ∈ ℕ ∧ coeff ⁡ F ⁡ N = coeff ⁡ G ⁡ N → F − f G = 0 𝑝 ∨ deg ⁡ F − f G < N
57 56 ord ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ T ∧ deg ⁡ G = N ∧ N ∈ ℕ ∧ coeff ⁡ F ⁡ N = coeff ⁡ G ⁡ N → ¬ F − f G = 0 𝑝 → deg ⁡ F − f G < N
58 9 57 pm2.61d ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ T ∧ deg ⁡ G = N ∧ N ∈ ℕ ∧ coeff ⁡ F ⁡ N = coeff ⁡ G ⁡ N → deg ⁡ F − f G < N