Proof of Theorem dgrsub2
Step | Hyp | Ref
| Expression |
1 | | simpr2 1197 |
. . 3
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → 𝑁 ∈ ℕ) |
2 | | dgr0 25156 |
. . . . 5
⊢
(deg‘0𝑝) = 0 |
3 | | nngt0 11861 |
. . . . 5
⊢ (𝑁 ∈ ℕ → 0 <
𝑁) |
4 | 2, 3 | eqbrtrid 5088 |
. . . 4
⊢ (𝑁 ∈ ℕ →
(deg‘0𝑝) < 𝑁) |
5 | | fveq2 6717 |
. . . . 5
⊢ ((𝐹 ∘f −
𝐺) = 0𝑝
→ (deg‘(𝐹
∘f − 𝐺)) =
(deg‘0𝑝)) |
6 | 5 | breq1d 5063 |
. . . 4
⊢ ((𝐹 ∘f −
𝐺) = 0𝑝
→ ((deg‘(𝐹
∘f − 𝐺)) < 𝑁 ↔ (deg‘0𝑝)
< 𝑁)) |
7 | 4, 6 | syl5ibrcom 250 |
. . 3
⊢ (𝑁 ∈ ℕ → ((𝐹 ∘f −
𝐺) = 0𝑝
→ (deg‘(𝐹
∘f − 𝐺)) < 𝑁)) |
8 | 1, 7 | syl 17 |
. 2
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → ((𝐹 ∘f − 𝐺) = 0𝑝 →
(deg‘(𝐹
∘f − 𝐺)) < 𝑁)) |
9 | | plyssc 25094 |
. . . . . . . 8
⊢
(Poly‘𝑆)
⊆ (Poly‘ℂ) |
10 | 9 | sseli 3896 |
. . . . . . 7
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹 ∈
(Poly‘ℂ)) |
11 | | plyssc 25094 |
. . . . . . . 8
⊢
(Poly‘𝑇)
⊆ (Poly‘ℂ) |
12 | 11 | sseli 3896 |
. . . . . . 7
⊢ (𝐺 ∈ (Poly‘𝑇) → 𝐺 ∈
(Poly‘ℂ)) |
13 | | eqid 2737 |
. . . . . . . 8
⊢
(deg‘𝐹) =
(deg‘𝐹) |
14 | | eqid 2737 |
. . . . . . . 8
⊢
(deg‘𝐺) =
(deg‘𝐺) |
15 | 13, 14 | dgrsub 25166 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ 𝐺 ∈
(Poly‘ℂ)) → (deg‘(𝐹 ∘f − 𝐺)) ≤ if((deg‘𝐹) ≤ (deg‘𝐺), (deg‘𝐺), (deg‘𝐹))) |
16 | 10, 12, 15 | syl2an 599 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) → (deg‘(𝐹 ∘f − 𝐺)) ≤ if((deg‘𝐹) ≤ (deg‘𝐺), (deg‘𝐺), (deg‘𝐹))) |
17 | 16 | adantr 484 |
. . . . 5
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → (deg‘(𝐹 ∘f − 𝐺)) ≤ if((deg‘𝐹) ≤ (deg‘𝐺), (deg‘𝐺), (deg‘𝐹))) |
18 | | simpr1 1196 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → (deg‘𝐺) = 𝑁) |
19 | | dgrsub2.a |
. . . . . . . . 9
⊢ 𝑁 = (deg‘𝐹) |
20 | 19 | eqcomi 2746 |
. . . . . . . 8
⊢
(deg‘𝐹) =
𝑁 |
21 | 20 | a1i 11 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → (deg‘𝐹) = 𝑁) |
22 | 18, 21 | ifeq12d 4460 |
. . . . . 6
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → if((deg‘𝐹) ≤ (deg‘𝐺), (deg‘𝐺), (deg‘𝐹)) = if((deg‘𝐹) ≤ (deg‘𝐺), 𝑁, 𝑁)) |
23 | | ifid 4479 |
. . . . . 6
⊢
if((deg‘𝐹)
≤ (deg‘𝐺), 𝑁, 𝑁) = 𝑁 |
24 | 22, 23 | eqtrdi 2794 |
. . . . 5
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → if((deg‘𝐹) ≤ (deg‘𝐺), (deg‘𝐺), (deg‘𝐹)) = 𝑁) |
25 | 17, 24 | breqtrd 5079 |
. . . 4
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → (deg‘(𝐹 ∘f − 𝐺)) ≤ 𝑁) |
26 | | eqid 2737 |
. . . . . . . . 9
⊢
(coeff‘𝐹) =
(coeff‘𝐹) |
27 | | eqid 2737 |
. . . . . . . . 9
⊢
(coeff‘𝐺) =
(coeff‘𝐺) |
28 | 26, 27 | coesub 25151 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ 𝐺 ∈
(Poly‘ℂ)) → (coeff‘(𝐹 ∘f − 𝐺)) = ((coeff‘𝐹) ∘f −
(coeff‘𝐺))) |
29 | 10, 12, 28 | syl2an 599 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) → (coeff‘(𝐹 ∘f − 𝐺)) = ((coeff‘𝐹) ∘f −
(coeff‘𝐺))) |
30 | 29 | adantr 484 |
. . . . . 6
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → (coeff‘(𝐹 ∘f − 𝐺)) = ((coeff‘𝐹) ∘f −
(coeff‘𝐺))) |
31 | 30 | fveq1d 6719 |
. . . . 5
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → ((coeff‘(𝐹 ∘f − 𝐺))‘𝑁) = (((coeff‘𝐹) ∘f −
(coeff‘𝐺))‘𝑁)) |
32 | 1 | nnnn0d 12150 |
. . . . . 6
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → 𝑁 ∈
ℕ0) |
33 | 26 | coef3 25126 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Poly‘𝑆) → (coeff‘𝐹):ℕ0⟶ℂ) |
34 | 33 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → (coeff‘𝐹):ℕ0⟶ℂ) |
35 | 34 | ffnd 6546 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → (coeff‘𝐹) Fn ℕ0) |
36 | 27 | coef3 25126 |
. . . . . . . . 9
⊢ (𝐺 ∈ (Poly‘𝑇) → (coeff‘𝐺):ℕ0⟶ℂ) |
37 | 36 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → (coeff‘𝐺):ℕ0⟶ℂ) |
38 | 37 | ffnd 6546 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → (coeff‘𝐺) Fn ℕ0) |
39 | | nn0ex 12096 |
. . . . . . . 8
⊢
ℕ0 ∈ V |
40 | 39 | a1i 11 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → ℕ0 ∈
V) |
41 | | inidm 4133 |
. . . . . . 7
⊢
(ℕ0 ∩ ℕ0) =
ℕ0 |
42 | | simplr3 1219 |
. . . . . . 7
⊢ ((((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) ∧ 𝑁 ∈ ℕ0) →
((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁)) |
43 | | eqidd 2738 |
. . . . . . 7
⊢ ((((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) ∧ 𝑁 ∈ ℕ0) →
((coeff‘𝐺)‘𝑁) = ((coeff‘𝐺)‘𝑁)) |
44 | 35, 38, 40, 40, 41, 42, 43 | ofval 7479 |
. . . . . 6
⊢ ((((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) ∧ 𝑁 ∈ ℕ0) →
(((coeff‘𝐹)
∘f − (coeff‘𝐺))‘𝑁) = (((coeff‘𝐺)‘𝑁) − ((coeff‘𝐺)‘𝑁))) |
45 | 32, 44 | mpdan 687 |
. . . . 5
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → (((coeff‘𝐹) ∘f −
(coeff‘𝐺))‘𝑁) = (((coeff‘𝐺)‘𝑁) − ((coeff‘𝐺)‘𝑁))) |
46 | 37, 32 | ffvelrnd 6905 |
. . . . . 6
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → ((coeff‘𝐺)‘𝑁) ∈ ℂ) |
47 | 46 | subidd 11177 |
. . . . 5
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → (((coeff‘𝐺)‘𝑁) − ((coeff‘𝐺)‘𝑁)) = 0) |
48 | 31, 45, 47 | 3eqtrd 2781 |
. . . 4
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → ((coeff‘(𝐹 ∘f − 𝐺))‘𝑁) = 0) |
49 | | plysubcl 25116 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ 𝐺 ∈
(Poly‘ℂ)) → (𝐹 ∘f − 𝐺) ∈
(Poly‘ℂ)) |
50 | 10, 12, 49 | syl2an 599 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) → (𝐹 ∘f − 𝐺) ∈
(Poly‘ℂ)) |
51 | 50 | adantr 484 |
. . . . 5
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → (𝐹 ∘f − 𝐺) ∈
(Poly‘ℂ)) |
52 | | eqid 2737 |
. . . . . 6
⊢
(deg‘(𝐹
∘f − 𝐺)) = (deg‘(𝐹 ∘f − 𝐺)) |
53 | | eqid 2737 |
. . . . . 6
⊢
(coeff‘(𝐹
∘f − 𝐺)) = (coeff‘(𝐹 ∘f − 𝐺)) |
54 | 52, 53 | dgrlt 25160 |
. . . . 5
⊢ (((𝐹 ∘f −
𝐺) ∈
(Poly‘ℂ) ∧ 𝑁 ∈ ℕ0) → (((𝐹 ∘f −
𝐺) = 0𝑝
∨ (deg‘(𝐹
∘f − 𝐺)) < 𝑁) ↔ ((deg‘(𝐹 ∘f − 𝐺)) ≤ 𝑁 ∧ ((coeff‘(𝐹 ∘f − 𝐺))‘𝑁) = 0))) |
55 | 51, 32, 54 | syl2anc 587 |
. . . 4
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → (((𝐹 ∘f − 𝐺) = 0𝑝 ∨
(deg‘(𝐹
∘f − 𝐺)) < 𝑁) ↔ ((deg‘(𝐹 ∘f − 𝐺)) ≤ 𝑁 ∧ ((coeff‘(𝐹 ∘f − 𝐺))‘𝑁) = 0))) |
56 | 25, 48, 55 | mpbir2and 713 |
. . 3
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → ((𝐹 ∘f − 𝐺) = 0𝑝 ∨
(deg‘(𝐹
∘f − 𝐺)) < 𝑁)) |
57 | 56 | ord 864 |
. 2
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → (¬ (𝐹 ∘f − 𝐺) = 0𝑝 →
(deg‘(𝐹
∘f − 𝐺)) < 𝑁)) |
58 | 8, 57 | pm2.61d 182 |
1
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → (deg‘(𝐹 ∘f − 𝐺)) < 𝑁) |