Proof of Theorem dgrsub2
Step | Hyp | Ref
| Expression |
1 | | simpr2 1068 |
. . 3
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → 𝑁 ∈ ℕ) |
2 | | dgr0 24018 |
. . . . 5
⊢
(deg‘0𝑝) = 0 |
3 | | nngt0 11049 |
. . . . 5
⊢ (𝑁 ∈ ℕ → 0 <
𝑁) |
4 | 2, 3 | syl5eqbr 4688 |
. . . 4
⊢ (𝑁 ∈ ℕ →
(deg‘0𝑝) < 𝑁) |
5 | | fveq2 6191 |
. . . . 5
⊢ ((𝐹 ∘𝑓
− 𝐺) =
0𝑝 → (deg‘(𝐹 ∘𝑓 − 𝐺)) =
(deg‘0𝑝)) |
6 | 5 | breq1d 4663 |
. . . 4
⊢ ((𝐹 ∘𝑓
− 𝐺) =
0𝑝 → ((deg‘(𝐹 ∘𝑓 − 𝐺)) < 𝑁 ↔ (deg‘0𝑝)
< 𝑁)) |
7 | 4, 6 | syl5ibrcom 237 |
. . 3
⊢ (𝑁 ∈ ℕ → ((𝐹 ∘𝑓
− 𝐺) =
0𝑝 → (deg‘(𝐹 ∘𝑓 − 𝐺)) < 𝑁)) |
8 | 1, 7 | syl 17 |
. 2
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → ((𝐹 ∘𝑓 − 𝐺) = 0𝑝 →
(deg‘(𝐹
∘𝑓 − 𝐺)) < 𝑁)) |
9 | | plyssc 23956 |
. . . . . . . 8
⊢
(Poly‘𝑆)
⊆ (Poly‘ℂ) |
10 | 9 | sseli 3599 |
. . . . . . 7
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹 ∈
(Poly‘ℂ)) |
11 | | plyssc 23956 |
. . . . . . . 8
⊢
(Poly‘𝑇)
⊆ (Poly‘ℂ) |
12 | 11 | sseli 3599 |
. . . . . . 7
⊢ (𝐺 ∈ (Poly‘𝑇) → 𝐺 ∈
(Poly‘ℂ)) |
13 | | eqid 2622 |
. . . . . . . 8
⊢
(deg‘𝐹) =
(deg‘𝐹) |
14 | | eqid 2622 |
. . . . . . . 8
⊢
(deg‘𝐺) =
(deg‘𝐺) |
15 | 13, 14 | dgrsub 24028 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ 𝐺 ∈
(Poly‘ℂ)) → (deg‘(𝐹 ∘𝑓 − 𝐺)) ≤ if((deg‘𝐹) ≤ (deg‘𝐺), (deg‘𝐺), (deg‘𝐹))) |
16 | 10, 12, 15 | syl2an 494 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) → (deg‘(𝐹 ∘𝑓 − 𝐺)) ≤ if((deg‘𝐹) ≤ (deg‘𝐺), (deg‘𝐺), (deg‘𝐹))) |
17 | 16 | adantr 481 |
. . . . 5
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → (deg‘(𝐹 ∘𝑓 − 𝐺)) ≤ if((deg‘𝐹) ≤ (deg‘𝐺), (deg‘𝐺), (deg‘𝐹))) |
18 | | simpr1 1067 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → (deg‘𝐺) = 𝑁) |
19 | | dgrsub2.a |
. . . . . . . . 9
⊢ 𝑁 = (deg‘𝐹) |
20 | 19 | eqcomi 2631 |
. . . . . . . 8
⊢
(deg‘𝐹) =
𝑁 |
21 | 20 | a1i 11 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → (deg‘𝐹) = 𝑁) |
22 | 18, 21 | ifeq12d 4106 |
. . . . . 6
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → if((deg‘𝐹) ≤ (deg‘𝐺), (deg‘𝐺), (deg‘𝐹)) = if((deg‘𝐹) ≤ (deg‘𝐺), 𝑁, 𝑁)) |
23 | | ifid 4125 |
. . . . . 6
⊢
if((deg‘𝐹)
≤ (deg‘𝐺), 𝑁, 𝑁) = 𝑁 |
24 | 22, 23 | syl6eq 2672 |
. . . . 5
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → if((deg‘𝐹) ≤ (deg‘𝐺), (deg‘𝐺), (deg‘𝐹)) = 𝑁) |
25 | 17, 24 | breqtrd 4679 |
. . . 4
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → (deg‘(𝐹 ∘𝑓 − 𝐺)) ≤ 𝑁) |
26 | | eqid 2622 |
. . . . . . . . 9
⊢
(coeff‘𝐹) =
(coeff‘𝐹) |
27 | | eqid 2622 |
. . . . . . . . 9
⊢
(coeff‘𝐺) =
(coeff‘𝐺) |
28 | 26, 27 | coesub 24013 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ 𝐺 ∈
(Poly‘ℂ)) → (coeff‘(𝐹 ∘𝑓 − 𝐺)) = ((coeff‘𝐹) ∘𝑓
− (coeff‘𝐺))) |
29 | 10, 12, 28 | syl2an 494 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) → (coeff‘(𝐹 ∘𝑓 − 𝐺)) = ((coeff‘𝐹) ∘𝑓
− (coeff‘𝐺))) |
30 | 29 | adantr 481 |
. . . . . 6
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → (coeff‘(𝐹 ∘𝑓 − 𝐺)) = ((coeff‘𝐹) ∘𝑓
− (coeff‘𝐺))) |
31 | 30 | fveq1d 6193 |
. . . . 5
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → ((coeff‘(𝐹 ∘𝑓 − 𝐺))‘𝑁) = (((coeff‘𝐹) ∘𝑓 −
(coeff‘𝐺))‘𝑁)) |
32 | 1 | nnnn0d 11351 |
. . . . . 6
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → 𝑁 ∈
ℕ0) |
33 | 26 | coef3 23988 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Poly‘𝑆) → (coeff‘𝐹):ℕ0⟶ℂ) |
34 | 33 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → (coeff‘𝐹):ℕ0⟶ℂ) |
35 | | ffn 6045 |
. . . . . . . 8
⊢
((coeff‘𝐹):ℕ0⟶ℂ →
(coeff‘𝐹) Fn
ℕ0) |
36 | 34, 35 | syl 17 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → (coeff‘𝐹) Fn ℕ0) |
37 | 27 | coef3 23988 |
. . . . . . . . 9
⊢ (𝐺 ∈ (Poly‘𝑇) → (coeff‘𝐺):ℕ0⟶ℂ) |
38 | 37 | ad2antlr 763 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → (coeff‘𝐺):ℕ0⟶ℂ) |
39 | | ffn 6045 |
. . . . . . . 8
⊢
((coeff‘𝐺):ℕ0⟶ℂ →
(coeff‘𝐺) Fn
ℕ0) |
40 | 38, 39 | syl 17 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → (coeff‘𝐺) Fn ℕ0) |
41 | | nn0ex 11298 |
. . . . . . . 8
⊢
ℕ0 ∈ V |
42 | 41 | a1i 11 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → ℕ0 ∈
V) |
43 | | inidm 3822 |
. . . . . . 7
⊢
(ℕ0 ∩ ℕ0) =
ℕ0 |
44 | | simplr3 1105 |
. . . . . . 7
⊢ ((((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) ∧ 𝑁 ∈ ℕ0) →
((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁)) |
45 | | eqidd 2623 |
. . . . . . 7
⊢ ((((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) ∧ 𝑁 ∈ ℕ0) →
((coeff‘𝐺)‘𝑁) = ((coeff‘𝐺)‘𝑁)) |
46 | 36, 40, 42, 42, 43, 44, 45 | ofval 6906 |
. . . . . 6
⊢ ((((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) ∧ 𝑁 ∈ ℕ0) →
(((coeff‘𝐹)
∘𝑓 − (coeff‘𝐺))‘𝑁) = (((coeff‘𝐺)‘𝑁) − ((coeff‘𝐺)‘𝑁))) |
47 | 32, 46 | mpdan 702 |
. . . . 5
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → (((coeff‘𝐹) ∘𝑓 −
(coeff‘𝐺))‘𝑁) = (((coeff‘𝐺)‘𝑁) − ((coeff‘𝐺)‘𝑁))) |
48 | 38, 32 | ffvelrnd 6360 |
. . . . . 6
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → ((coeff‘𝐺)‘𝑁) ∈ ℂ) |
49 | 48 | subidd 10380 |
. . . . 5
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → (((coeff‘𝐺)‘𝑁) − ((coeff‘𝐺)‘𝑁)) = 0) |
50 | 31, 47, 49 | 3eqtrd 2660 |
. . . 4
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → ((coeff‘(𝐹 ∘𝑓 − 𝐺))‘𝑁) = 0) |
51 | | plysubcl 23978 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ 𝐺 ∈
(Poly‘ℂ)) → (𝐹 ∘𝑓 − 𝐺) ∈
(Poly‘ℂ)) |
52 | 10, 12, 51 | syl2an 494 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) → (𝐹 ∘𝑓 − 𝐺) ∈
(Poly‘ℂ)) |
53 | 52 | adantr 481 |
. . . . 5
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → (𝐹 ∘𝑓 − 𝐺) ∈
(Poly‘ℂ)) |
54 | | eqid 2622 |
. . . . . 6
⊢
(deg‘(𝐹
∘𝑓 − 𝐺)) = (deg‘(𝐹 ∘𝑓 − 𝐺)) |
55 | | eqid 2622 |
. . . . . 6
⊢
(coeff‘(𝐹
∘𝑓 − 𝐺)) = (coeff‘(𝐹 ∘𝑓 − 𝐺)) |
56 | 54, 55 | dgrlt 24022 |
. . . . 5
⊢ (((𝐹 ∘𝑓
− 𝐺) ∈
(Poly‘ℂ) ∧ 𝑁 ∈ ℕ0) → (((𝐹 ∘𝑓
− 𝐺) =
0𝑝 ∨ (deg‘(𝐹 ∘𝑓 − 𝐺)) < 𝑁) ↔ ((deg‘(𝐹 ∘𝑓 − 𝐺)) ≤ 𝑁 ∧ ((coeff‘(𝐹 ∘𝑓 − 𝐺))‘𝑁) = 0))) |
57 | 53, 32, 56 | syl2anc 693 |
. . . 4
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → (((𝐹 ∘𝑓 − 𝐺) = 0𝑝 ∨
(deg‘(𝐹
∘𝑓 − 𝐺)) < 𝑁) ↔ ((deg‘(𝐹 ∘𝑓 − 𝐺)) ≤ 𝑁 ∧ ((coeff‘(𝐹 ∘𝑓 − 𝐺))‘𝑁) = 0))) |
58 | 25, 50, 57 | mpbir2and 957 |
. . 3
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → ((𝐹 ∘𝑓 − 𝐺) = 0𝑝 ∨
(deg‘(𝐹
∘𝑓 − 𝐺)) < 𝑁)) |
59 | 58 | ord 392 |
. 2
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → (¬ (𝐹 ∘𝑓 − 𝐺) = 0𝑝 →
(deg‘(𝐹
∘𝑓 − 𝐺)) < 𝑁)) |
60 | 8, 59 | pm2.61d 170 |
1
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑇)) ∧ ((deg‘𝐺) = 𝑁 ∧ 𝑁 ∈ ℕ ∧ ((coeff‘𝐹)‘𝑁) = ((coeff‘𝐺)‘𝑁))) → (deg‘(𝐹 ∘𝑓 − 𝐺)) < 𝑁) |