Proof of Theorem plydivlem4
Step | Hyp | Ref
| Expression |
1 | | plydiv.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) |
2 | | plybss 23950 |
. . . . . . . 8
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝑆 ⊆ ℂ) |
3 | 1, 2 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
4 | | plydiv.pl |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
5 | | plydiv.tm |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆) |
6 | | plydiv.rc |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0)) → (1 / 𝑥) ∈ 𝑆) |
7 | | plydiv.m1 |
. . . . . . . . . . . . 13
⊢ (𝜑 → -1 ∈ 𝑆) |
8 | 4, 5, 6, 7 | plydivlem1 24048 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈ 𝑆) |
9 | | plydiv.a |
. . . . . . . . . . . . 13
⊢ 𝐴 = (coeff‘𝐹) |
10 | 9 | coef2 23987 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 0 ∈ 𝑆) → 𝐴:ℕ0⟶𝑆) |
11 | 1, 8, 10 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴:ℕ0⟶𝑆) |
12 | | plydiv.m |
. . . . . . . . . . . 12
⊢ 𝑀 = (deg‘𝐹) |
13 | | dgrcl 23989 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) ∈
ℕ0) |
14 | 1, 13 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (deg‘𝐹) ∈
ℕ0) |
15 | 12, 14 | syl5eqel 2705 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
16 | 11, 15 | ffvelrnd 6360 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴‘𝑀) ∈ 𝑆) |
17 | 3, 16 | sseldd 3604 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴‘𝑀) ∈ ℂ) |
18 | | plydiv.g |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆)) |
19 | | plydiv.b |
. . . . . . . . . . . . 13
⊢ 𝐵 = (coeff‘𝐺) |
20 | 19 | coef2 23987 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ (Poly‘𝑆) ∧ 0 ∈ 𝑆) → 𝐵:ℕ0⟶𝑆) |
21 | 18, 8, 20 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵:ℕ0⟶𝑆) |
22 | | plydiv.n |
. . . . . . . . . . . 12
⊢ 𝑁 = (deg‘𝐺) |
23 | | dgrcl 23989 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ (Poly‘𝑆) → (deg‘𝐺) ∈
ℕ0) |
24 | 18, 23 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (deg‘𝐺) ∈
ℕ0) |
25 | 22, 24 | syl5eqel 2705 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
26 | 21, 25 | ffvelrnd 6360 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵‘𝑁) ∈ 𝑆) |
27 | 3, 26 | sseldd 3604 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵‘𝑁) ∈ ℂ) |
28 | | plydiv.z |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ≠
0𝑝) |
29 | 22, 19 | dgreq0 24021 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ (Poly‘𝑆) → (𝐺 = 0𝑝 ↔ (𝐵‘𝑁) = 0)) |
30 | 18, 29 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 = 0𝑝 ↔ (𝐵‘𝑁) = 0)) |
31 | 30 | necon3bid 2838 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺 ≠ 0𝑝 ↔ (𝐵‘𝑁) ≠ 0)) |
32 | 28, 31 | mpbid 222 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵‘𝑁) ≠ 0) |
33 | 17, 27, 32 | divrecd 10804 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴‘𝑀) / (𝐵‘𝑁)) = ((𝐴‘𝑀) · (1 / (𝐵‘𝑁)))) |
34 | | fvex 6201 |
. . . . . . . . . . . 12
⊢ (𝐵‘𝑁) ∈ V |
35 | | eleq1 2689 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝐵‘𝑁) → (𝑥 ∈ 𝑆 ↔ (𝐵‘𝑁) ∈ 𝑆)) |
36 | | neeq1 2856 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝐵‘𝑁) → (𝑥 ≠ 0 ↔ (𝐵‘𝑁) ≠ 0)) |
37 | 35, 36 | anbi12d 747 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝐵‘𝑁) → ((𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0) ↔ ((𝐵‘𝑁) ∈ 𝑆 ∧ (𝐵‘𝑁) ≠ 0))) |
38 | 37 | anbi2d 740 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝐵‘𝑁) → ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0)) ↔ (𝜑 ∧ ((𝐵‘𝑁) ∈ 𝑆 ∧ (𝐵‘𝑁) ≠ 0)))) |
39 | | oveq2 6658 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝐵‘𝑁) → (1 / 𝑥) = (1 / (𝐵‘𝑁))) |
40 | 39 | eleq1d 2686 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝐵‘𝑁) → ((1 / 𝑥) ∈ 𝑆 ↔ (1 / (𝐵‘𝑁)) ∈ 𝑆)) |
41 | 38, 40 | imbi12d 334 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝐵‘𝑁) → (((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0)) → (1 / 𝑥) ∈ 𝑆) ↔ ((𝜑 ∧ ((𝐵‘𝑁) ∈ 𝑆 ∧ (𝐵‘𝑁) ≠ 0)) → (1 / (𝐵‘𝑁)) ∈ 𝑆))) |
42 | 34, 41, 6 | vtocl 3259 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝐵‘𝑁) ∈ 𝑆 ∧ (𝐵‘𝑁) ≠ 0)) → (1 / (𝐵‘𝑁)) ∈ 𝑆) |
43 | 42 | ex 450 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐵‘𝑁) ∈ 𝑆 ∧ (𝐵‘𝑁) ≠ 0) → (1 / (𝐵‘𝑁)) ∈ 𝑆)) |
44 | 26, 32, 43 | mp2and 715 |
. . . . . . . . 9
⊢ (𝜑 → (1 / (𝐵‘𝑁)) ∈ 𝑆) |
45 | 5, 16, 44 | caovcld 6827 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴‘𝑀) · (1 / (𝐵‘𝑁))) ∈ 𝑆) |
46 | 33, 45 | eqeltrd 2701 |
. . . . . . 7
⊢ (𝜑 → ((𝐴‘𝑀) / (𝐵‘𝑁)) ∈ 𝑆) |
47 | | plydiv.d |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈
ℕ0) |
48 | | plydiv.h |
. . . . . . . 8
⊢ 𝐻 = (𝑧 ∈ ℂ ↦ (((𝐴‘𝑀) / (𝐵‘𝑁)) · (𝑧↑𝐷))) |
49 | 48 | ply1term 23960 |
. . . . . . 7
⊢ ((𝑆 ⊆ ℂ ∧ ((𝐴‘𝑀) / (𝐵‘𝑁)) ∈ 𝑆 ∧ 𝐷 ∈ ℕ0) → 𝐻 ∈ (Poly‘𝑆)) |
50 | 3, 46, 47, 49 | syl3anc 1326 |
. . . . . 6
⊢ (𝜑 → 𝐻 ∈ (Poly‘𝑆)) |
51 | 50 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → 𝐻 ∈ (Poly‘𝑆)) |
52 | | simpr 477 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → 𝑝 ∈ (Poly‘𝑆)) |
53 | 4 | adantlr 751 |
. . . . 5
⊢ (((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
54 | 51, 52, 53 | plyadd 23973 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → (𝐻 ∘𝑓 + 𝑝) ∈ (Poly‘𝑆)) |
55 | 54 | adantr 481 |
. . 3
⊢ (((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) ∧ (((𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺))
∘𝑓 − (𝐺 ∘𝑓 · 𝑝)) = 0𝑝 ∨
(deg‘((𝐹
∘𝑓 − (𝐻 ∘𝑓 · 𝐺)) ∘𝑓
− (𝐺
∘𝑓 · 𝑝))) < 𝑁)) → (𝐻 ∘𝑓 + 𝑝) ∈ (Poly‘𝑆)) |
56 | | cnex 10017 |
. . . . . . . . 9
⊢ ℂ
∈ V |
57 | 56 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → ℂ ∈ V) |
58 | 1 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → 𝐹 ∈ (Poly‘𝑆)) |
59 | | plyf 23954 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ) |
60 | 58, 59 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → 𝐹:ℂ⟶ℂ) |
61 | | mulcl 10020 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ) |
62 | 61 | adantl 482 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ) |
63 | | plyf 23954 |
. . . . . . . . . 10
⊢ (𝐻 ∈ (Poly‘𝑆) → 𝐻:ℂ⟶ℂ) |
64 | 51, 63 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → 𝐻:ℂ⟶ℂ) |
65 | 18 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → 𝐺 ∈ (Poly‘𝑆)) |
66 | | plyf 23954 |
. . . . . . . . . 10
⊢ (𝐺 ∈ (Poly‘𝑆) → 𝐺:ℂ⟶ℂ) |
67 | 65, 66 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → 𝐺:ℂ⟶ℂ) |
68 | | inidm 3822 |
. . . . . . . . 9
⊢ (ℂ
∩ ℂ) = ℂ |
69 | 62, 64, 67, 57, 57, 68 | off 6912 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → (𝐻 ∘𝑓 · 𝐺):ℂ⟶ℂ) |
70 | | plyf 23954 |
. . . . . . . . . 10
⊢ (𝑝 ∈ (Poly‘𝑆) → 𝑝:ℂ⟶ℂ) |
71 | 70 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → 𝑝:ℂ⟶ℂ) |
72 | 62, 67, 71, 57, 57, 68 | off 6912 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → (𝐺 ∘𝑓 · 𝑝):ℂ⟶ℂ) |
73 | | subsub4 10314 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥 − 𝑦) − 𝑧) = (𝑥 − (𝑦 + 𝑧))) |
74 | 73 | adantl 482 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → ((𝑥 − 𝑦) − 𝑧) = (𝑥 − (𝑦 + 𝑧))) |
75 | 57, 60, 69, 72, 74 | caofass 6931 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → ((𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺))
∘𝑓 − (𝐺 ∘𝑓 · 𝑝)) = (𝐹 ∘𝑓 − ((𝐻 ∘𝑓
· 𝐺)
∘𝑓 + (𝐺 ∘𝑓 · 𝑝)))) |
76 | | mulcom 10022 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) = (𝑦 · 𝑥)) |
77 | 76 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) = (𝑦 · 𝑥)) |
78 | 57, 64, 67, 77 | caofcom 6929 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → (𝐻 ∘𝑓 · 𝐺) = (𝐺 ∘𝑓 · 𝐻)) |
79 | 78 | oveq1d 6665 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → ((𝐻 ∘𝑓 · 𝐺) ∘𝑓 +
(𝐺
∘𝑓 · 𝑝)) = ((𝐺 ∘𝑓 · 𝐻) ∘𝑓 +
(𝐺
∘𝑓 · 𝑝))) |
80 | | adddi 10025 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧))) |
81 | 80 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧))) |
82 | 57, 67, 64, 71, 81 | caofdi 6933 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → (𝐺 ∘𝑓 · (𝐻 ∘𝑓 +
𝑝)) = ((𝐺 ∘𝑓 · 𝐻) ∘𝑓 +
(𝐺
∘𝑓 · 𝑝))) |
83 | 79, 82 | eqtr4d 2659 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → ((𝐻 ∘𝑓 · 𝐺) ∘𝑓 +
(𝐺
∘𝑓 · 𝑝)) = (𝐺 ∘𝑓 · (𝐻 ∘𝑓 +
𝑝))) |
84 | 83 | oveq2d 6666 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → (𝐹 ∘𝑓 − ((𝐻 ∘𝑓
· 𝐺)
∘𝑓 + (𝐺 ∘𝑓 · 𝑝))) = (𝐹 ∘𝑓 − (𝐺 ∘𝑓
· (𝐻
∘𝑓 + 𝑝)))) |
85 | 75, 84 | eqtrd 2656 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → ((𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺))
∘𝑓 − (𝐺 ∘𝑓 · 𝑝)) = (𝐹 ∘𝑓 − (𝐺 ∘𝑓
· (𝐻
∘𝑓 + 𝑝)))) |
86 | 85 | eqeq1d 2624 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → (((𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺))
∘𝑓 − (𝐺 ∘𝑓 · 𝑝)) = 0𝑝
↔ (𝐹
∘𝑓 − (𝐺 ∘𝑓 · (𝐻 ∘𝑓 +
𝑝))) =
0𝑝)) |
87 | 85 | fveq2d 6195 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → (deg‘((𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺))
∘𝑓 − (𝐺 ∘𝑓 · 𝑝))) = (deg‘(𝐹 ∘𝑓
− (𝐺
∘𝑓 · (𝐻 ∘𝑓 + 𝑝))))) |
88 | 87 | breq1d 4663 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → ((deg‘((𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺))
∘𝑓 − (𝐺 ∘𝑓 · 𝑝))) < 𝑁 ↔ (deg‘(𝐹 ∘𝑓 − (𝐺 ∘𝑓
· (𝐻
∘𝑓 + 𝑝)))) < 𝑁)) |
89 | 86, 88 | orbi12d 746 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) → ((((𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺))
∘𝑓 − (𝐺 ∘𝑓 · 𝑝)) = 0𝑝 ∨
(deg‘((𝐹
∘𝑓 − (𝐻 ∘𝑓 · 𝐺)) ∘𝑓
− (𝐺
∘𝑓 · 𝑝))) < 𝑁) ↔ ((𝐹 ∘𝑓 − (𝐺 ∘𝑓
· (𝐻
∘𝑓 + 𝑝))) = 0𝑝 ∨
(deg‘(𝐹
∘𝑓 − (𝐺 ∘𝑓 · (𝐻 ∘𝑓 +
𝑝)))) < 𝑁))) |
90 | 89 | biimpa 501 |
. . 3
⊢ (((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) ∧ (((𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺))
∘𝑓 − (𝐺 ∘𝑓 · 𝑝)) = 0𝑝 ∨
(deg‘((𝐹
∘𝑓 − (𝐻 ∘𝑓 · 𝐺)) ∘𝑓
− (𝐺
∘𝑓 · 𝑝))) < 𝑁)) → ((𝐹 ∘𝑓 − (𝐺 ∘𝑓
· (𝐻
∘𝑓 + 𝑝))) = 0𝑝 ∨
(deg‘(𝐹
∘𝑓 − (𝐺 ∘𝑓 · (𝐻 ∘𝑓 +
𝑝)))) < 𝑁)) |
91 | | plydiv.r |
. . . . . . 7
⊢ 𝑅 = (𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) |
92 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑞 = (𝐻 ∘𝑓 + 𝑝) → (𝐺 ∘𝑓 · 𝑞) = (𝐺 ∘𝑓 · (𝐻 ∘𝑓 +
𝑝))) |
93 | 92 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑞 = (𝐻 ∘𝑓 + 𝑝) → (𝐹 ∘𝑓 − (𝐺 ∘𝑓
· 𝑞)) = (𝐹 ∘𝑓
− (𝐺
∘𝑓 · (𝐻 ∘𝑓 + 𝑝)))) |
94 | 91, 93 | syl5eq 2668 |
. . . . . 6
⊢ (𝑞 = (𝐻 ∘𝑓 + 𝑝) → 𝑅 = (𝐹 ∘𝑓 − (𝐺 ∘𝑓
· (𝐻
∘𝑓 + 𝑝)))) |
95 | 94 | eqeq1d 2624 |
. . . . 5
⊢ (𝑞 = (𝐻 ∘𝑓 + 𝑝) → (𝑅 = 0𝑝 ↔ (𝐹 ∘𝑓
− (𝐺
∘𝑓 · (𝐻 ∘𝑓 + 𝑝))) =
0𝑝)) |
96 | 94 | fveq2d 6195 |
. . . . . 6
⊢ (𝑞 = (𝐻 ∘𝑓 + 𝑝) → (deg‘𝑅) = (deg‘(𝐹 ∘𝑓
− (𝐺
∘𝑓 · (𝐻 ∘𝑓 + 𝑝))))) |
97 | 96 | breq1d 4663 |
. . . . 5
⊢ (𝑞 = (𝐻 ∘𝑓 + 𝑝) → ((deg‘𝑅) < 𝑁 ↔ (deg‘(𝐹 ∘𝑓 − (𝐺 ∘𝑓
· (𝐻
∘𝑓 + 𝑝)))) < 𝑁)) |
98 | 95, 97 | orbi12d 746 |
. . . 4
⊢ (𝑞 = (𝐻 ∘𝑓 + 𝑝) → ((𝑅 = 0𝑝 ∨
(deg‘𝑅) < 𝑁) ↔ ((𝐹 ∘𝑓 − (𝐺 ∘𝑓
· (𝐻
∘𝑓 + 𝑝))) = 0𝑝 ∨
(deg‘(𝐹
∘𝑓 − (𝐺 ∘𝑓 · (𝐻 ∘𝑓 +
𝑝)))) < 𝑁))) |
99 | 98 | rspcev 3309 |
. . 3
⊢ (((𝐻 ∘𝑓 +
𝑝) ∈ (Poly‘𝑆) ∧ ((𝐹 ∘𝑓 − (𝐺 ∘𝑓
· (𝐻
∘𝑓 + 𝑝))) = 0𝑝 ∨
(deg‘(𝐹
∘𝑓 − (𝐺 ∘𝑓 · (𝐻 ∘𝑓 +
𝑝)))) < 𝑁)) → ∃𝑞 ∈ (Poly‘𝑆)(𝑅 = 0𝑝 ∨
(deg‘𝑅) < 𝑁)) |
100 | 55, 90, 99 | syl2anc 693 |
. 2
⊢ (((𝜑 ∧ 𝑝 ∈ (Poly‘𝑆)) ∧ (((𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺))
∘𝑓 − (𝐺 ∘𝑓 · 𝑝)) = 0𝑝 ∨
(deg‘((𝐹
∘𝑓 − (𝐻 ∘𝑓 · 𝐺)) ∘𝑓
− (𝐺
∘𝑓 · 𝑝))) < 𝑁)) → ∃𝑞 ∈ (Poly‘𝑆)(𝑅 = 0𝑝 ∨
(deg‘𝑅) < 𝑁)) |
101 | 50, 18, 4, 5 | plymul 23974 |
. . . 4
⊢ (𝜑 → (𝐻 ∘𝑓 · 𝐺) ∈ (Poly‘𝑆)) |
102 | 1, 101, 4, 5, 7 | plysub 23975 |
. . 3
⊢ (𝜑 → (𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺)) ∈
(Poly‘𝑆)) |
103 | | plydiv.al |
. . 3
⊢ (𝜑 → ∀𝑓 ∈ (Poly‘𝑆)((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
𝑁) < 𝐷) → ∃𝑝 ∈ (Poly‘𝑆)(𝑈 = 0𝑝 ∨
(deg‘𝑈) < 𝑁))) |
104 | | eqid 2622 |
. . . . . . 7
⊢
(deg‘(𝐻
∘𝑓 · 𝐺)) = (deg‘(𝐻 ∘𝑓 · 𝐺)) |
105 | 12, 104 | dgrsub 24028 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐻 ∘𝑓 · 𝐺) ∈ (Poly‘𝑆)) → (deg‘(𝐹 ∘𝑓
− (𝐻
∘𝑓 · 𝐺))) ≤ if(𝑀 ≤ (deg‘(𝐻 ∘𝑓 · 𝐺)), (deg‘(𝐻 ∘𝑓
· 𝐺)), 𝑀)) |
106 | 1, 101, 105 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (deg‘(𝐹 ∘𝑓
− (𝐻
∘𝑓 · 𝐺))) ≤ if(𝑀 ≤ (deg‘(𝐻 ∘𝑓 · 𝐺)), (deg‘(𝐻 ∘𝑓
· 𝐺)), 𝑀)) |
107 | | plydiv.fz |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ≠
0𝑝) |
108 | 12, 9 | dgreq0 24021 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0𝑝 ↔ (𝐴‘𝑀) = 0)) |
109 | 1, 108 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹 = 0𝑝 ↔ (𝐴‘𝑀) = 0)) |
110 | 109 | necon3bid 2838 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹 ≠ 0𝑝 ↔ (𝐴‘𝑀) ≠ 0)) |
111 | 107, 110 | mpbid 222 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴‘𝑀) ≠ 0) |
112 | 17, 27, 111, 32 | divne0d 10817 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴‘𝑀) / (𝐵‘𝑁)) ≠ 0) |
113 | 3, 46 | sseldd 3604 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐴‘𝑀) / (𝐵‘𝑁)) ∈ ℂ) |
114 | 48 | coe1term 24015 |
. . . . . . . . . . . . 13
⊢ ((((𝐴‘𝑀) / (𝐵‘𝑁)) ∈ ℂ ∧ 𝐷 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0)
→ ((coeff‘𝐻)‘𝐷) = if(𝐷 = 𝐷, ((𝐴‘𝑀) / (𝐵‘𝑁)), 0)) |
115 | 113, 47, 47, 114 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((coeff‘𝐻)‘𝐷) = if(𝐷 = 𝐷, ((𝐴‘𝑀) / (𝐵‘𝑁)), 0)) |
116 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ 𝐷 = 𝐷 |
117 | 116 | iftruei 4093 |
. . . . . . . . . . . 12
⊢ if(𝐷 = 𝐷, ((𝐴‘𝑀) / (𝐵‘𝑁)), 0) = ((𝐴‘𝑀) / (𝐵‘𝑁)) |
118 | 115, 117 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ (𝜑 → ((coeff‘𝐻)‘𝐷) = ((𝐴‘𝑀) / (𝐵‘𝑁))) |
119 | | c0ex 10034 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
120 | 119 | fvconst2 6469 |
. . . . . . . . . . . 12
⊢ (𝐷 ∈ ℕ0
→ ((ℕ0 × {0})‘𝐷) = 0) |
121 | 47, 120 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((ℕ0
× {0})‘𝐷) =
0) |
122 | 112, 118,
121 | 3netr4d 2871 |
. . . . . . . . . 10
⊢ (𝜑 → ((coeff‘𝐻)‘𝐷) ≠ ((ℕ0 ×
{0})‘𝐷)) |
123 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝐻 = 0𝑝 →
(coeff‘𝐻) =
(coeff‘0𝑝)) |
124 | | coe0 24012 |
. . . . . . . . . . . . 13
⊢
(coeff‘0𝑝) = (ℕ0 ×
{0}) |
125 | 123, 124 | syl6eq 2672 |
. . . . . . . . . . . 12
⊢ (𝐻 = 0𝑝 →
(coeff‘𝐻) =
(ℕ0 × {0})) |
126 | 125 | fveq1d 6193 |
. . . . . . . . . . 11
⊢ (𝐻 = 0𝑝 →
((coeff‘𝐻)‘𝐷) = ((ℕ0 ×
{0})‘𝐷)) |
127 | 126 | necon3i 2826 |
. . . . . . . . . 10
⊢
(((coeff‘𝐻)‘𝐷) ≠ ((ℕ0 ×
{0})‘𝐷) → 𝐻 ≠
0𝑝) |
128 | 122, 127 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐻 ≠
0𝑝) |
129 | | eqid 2622 |
. . . . . . . . . 10
⊢
(deg‘𝐻) =
(deg‘𝐻) |
130 | 129, 22 | dgrmul 24026 |
. . . . . . . . 9
⊢ (((𝐻 ∈ (Poly‘𝑆) ∧ 𝐻 ≠ 0𝑝) ∧ (𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝)) →
(deg‘(𝐻
∘𝑓 · 𝐺)) = ((deg‘𝐻) + 𝑁)) |
131 | 50, 128, 18, 28, 130 | syl22anc 1327 |
. . . . . . . 8
⊢ (𝜑 → (deg‘(𝐻 ∘𝑓
· 𝐺)) =
((deg‘𝐻) + 𝑁)) |
132 | 48 | dgr1term 24016 |
. . . . . . . . . . . 12
⊢ ((((𝐴‘𝑀) / (𝐵‘𝑁)) ∈ ℂ ∧ ((𝐴‘𝑀) / (𝐵‘𝑁)) ≠ 0 ∧ 𝐷 ∈ ℕ0) →
(deg‘𝐻) = 𝐷) |
133 | 113, 112,
47, 132 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (𝜑 → (deg‘𝐻) = 𝐷) |
134 | | plydiv.e |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑀 − 𝑁) = 𝐷) |
135 | 133, 134 | eqtr4d 2659 |
. . . . . . . . . 10
⊢ (𝜑 → (deg‘𝐻) = (𝑀 − 𝑁)) |
136 | 135 | oveq1d 6665 |
. . . . . . . . 9
⊢ (𝜑 → ((deg‘𝐻) + 𝑁) = ((𝑀 − 𝑁) + 𝑁)) |
137 | 15 | nn0cnd 11353 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℂ) |
138 | 25 | nn0cnd 11353 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℂ) |
139 | 137, 138 | npcand 10396 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑀 − 𝑁) + 𝑁) = 𝑀) |
140 | 136, 139 | eqtrd 2656 |
. . . . . . . 8
⊢ (𝜑 → ((deg‘𝐻) + 𝑁) = 𝑀) |
141 | 131, 140 | eqtrd 2656 |
. . . . . . 7
⊢ (𝜑 → (deg‘(𝐻 ∘𝑓
· 𝐺)) = 𝑀) |
142 | 141 | ifeq1d 4104 |
. . . . . 6
⊢ (𝜑 → if(𝑀 ≤ (deg‘(𝐻 ∘𝑓 · 𝐺)), (deg‘(𝐻 ∘𝑓
· 𝐺)), 𝑀) = if(𝑀 ≤ (deg‘(𝐻 ∘𝑓 · 𝐺)), 𝑀, 𝑀)) |
143 | | ifid 4125 |
. . . . . 6
⊢ if(𝑀 ≤ (deg‘(𝐻 ∘𝑓
· 𝐺)), 𝑀, 𝑀) = 𝑀 |
144 | 142, 143 | syl6eq 2672 |
. . . . 5
⊢ (𝜑 → if(𝑀 ≤ (deg‘(𝐻 ∘𝑓 · 𝐺)), (deg‘(𝐻 ∘𝑓
· 𝐺)), 𝑀) = 𝑀) |
145 | 106, 144 | breqtrd 4679 |
. . . 4
⊢ (𝜑 → (deg‘(𝐹 ∘𝑓
− (𝐻
∘𝑓 · 𝐺))) ≤ 𝑀) |
146 | | eqid 2622 |
. . . . . . . 8
⊢
(coeff‘(𝐻
∘𝑓 · 𝐺)) = (coeff‘(𝐻 ∘𝑓 · 𝐺)) |
147 | 9, 146 | coesub 24013 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐻 ∘𝑓 · 𝐺) ∈ (Poly‘𝑆)) → (coeff‘(𝐹 ∘𝑓
− (𝐻
∘𝑓 · 𝐺))) = (𝐴 ∘𝑓 −
(coeff‘(𝐻
∘𝑓 · 𝐺)))) |
148 | 1, 101, 147 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (coeff‘(𝐹 ∘𝑓
− (𝐻
∘𝑓 · 𝐺))) = (𝐴 ∘𝑓 −
(coeff‘(𝐻
∘𝑓 · 𝐺)))) |
149 | 148 | fveq1d 6193 |
. . . . 5
⊢ (𝜑 → ((coeff‘(𝐹 ∘𝑓
− (𝐻
∘𝑓 · 𝐺)))‘𝑀) = ((𝐴 ∘𝑓 −
(coeff‘(𝐻
∘𝑓 · 𝐺)))‘𝑀)) |
150 | 9 | coef3 23988 |
. . . . . . . 8
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶ℂ) |
151 | | ffn 6045 |
. . . . . . . 8
⊢ (𝐴:ℕ0⟶ℂ →
𝐴 Fn
ℕ0) |
152 | 1, 150, 151 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → 𝐴 Fn ℕ0) |
153 | 146 | coef3 23988 |
. . . . . . . 8
⊢ ((𝐻 ∘𝑓
· 𝐺) ∈
(Poly‘𝑆) →
(coeff‘(𝐻
∘𝑓 · 𝐺)):ℕ0⟶ℂ) |
154 | | ffn 6045 |
. . . . . . . 8
⊢
((coeff‘(𝐻
∘𝑓 · 𝐺)):ℕ0⟶ℂ →
(coeff‘(𝐻
∘𝑓 · 𝐺)) Fn ℕ0) |
155 | 101, 153,
154 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (coeff‘(𝐻 ∘𝑓
· 𝐺)) Fn
ℕ0) |
156 | | nn0ex 11298 |
. . . . . . . 8
⊢
ℕ0 ∈ V |
157 | 156 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℕ0 ∈
V) |
158 | | inidm 3822 |
. . . . . . 7
⊢
(ℕ0 ∩ ℕ0) =
ℕ0 |
159 | | eqidd 2623 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ0) → (𝐴‘𝑀) = (𝐴‘𝑀)) |
160 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(coeff‘𝐻) =
(coeff‘𝐻) |
161 | 160, 19, 129, 22 | coemulhi 24010 |
. . . . . . . . . 10
⊢ ((𝐻 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ((coeff‘(𝐻 ∘𝑓 · 𝐺))‘((deg‘𝐻) + 𝑁)) = (((coeff‘𝐻)‘(deg‘𝐻)) · (𝐵‘𝑁))) |
162 | 50, 18, 161 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → ((coeff‘(𝐻 ∘𝑓
· 𝐺))‘((deg‘𝐻) + 𝑁)) = (((coeff‘𝐻)‘(deg‘𝐻)) · (𝐵‘𝑁))) |
163 | 140 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝜑 → ((coeff‘(𝐻 ∘𝑓
· 𝐺))‘((deg‘𝐻) + 𝑁)) = ((coeff‘(𝐻 ∘𝑓 · 𝐺))‘𝑀)) |
164 | 133 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((coeff‘𝐻)‘(deg‘𝐻)) = ((coeff‘𝐻)‘𝐷)) |
165 | 164, 118 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ (𝜑 → ((coeff‘𝐻)‘(deg‘𝐻)) = ((𝐴‘𝑀) / (𝐵‘𝑁))) |
166 | 165 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (𝜑 → (((coeff‘𝐻)‘(deg‘𝐻)) · (𝐵‘𝑁)) = (((𝐴‘𝑀) / (𝐵‘𝑁)) · (𝐵‘𝑁))) |
167 | 17, 27, 32 | divcan1d 10802 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐴‘𝑀) / (𝐵‘𝑁)) · (𝐵‘𝑁)) = (𝐴‘𝑀)) |
168 | 166, 167 | eqtrd 2656 |
. . . . . . . . 9
⊢ (𝜑 → (((coeff‘𝐻)‘(deg‘𝐻)) · (𝐵‘𝑁)) = (𝐴‘𝑀)) |
169 | 162, 163,
168 | 3eqtr3d 2664 |
. . . . . . . 8
⊢ (𝜑 → ((coeff‘(𝐻 ∘𝑓
· 𝐺))‘𝑀) = (𝐴‘𝑀)) |
170 | 169 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ0) →
((coeff‘(𝐻
∘𝑓 · 𝐺))‘𝑀) = (𝐴‘𝑀)) |
171 | 152, 155,
157, 157, 158, 159, 170 | ofval 6906 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ0) → ((𝐴 ∘𝑓
− (coeff‘(𝐻
∘𝑓 · 𝐺)))‘𝑀) = ((𝐴‘𝑀) − (𝐴‘𝑀))) |
172 | 15, 171 | mpdan 702 |
. . . . 5
⊢ (𝜑 → ((𝐴 ∘𝑓 −
(coeff‘(𝐻
∘𝑓 · 𝐺)))‘𝑀) = ((𝐴‘𝑀) − (𝐴‘𝑀))) |
173 | 17 | subidd 10380 |
. . . . 5
⊢ (𝜑 → ((𝐴‘𝑀) − (𝐴‘𝑀)) = 0) |
174 | 149, 172,
173 | 3eqtrd 2660 |
. . . 4
⊢ (𝜑 → ((coeff‘(𝐹 ∘𝑓
− (𝐻
∘𝑓 · 𝐺)))‘𝑀) = 0) |
175 | | dgrcl 23989 |
. . . . . . . . . 10
⊢ ((𝐹 ∘𝑓
− (𝐻
∘𝑓 · 𝐺)) ∈ (Poly‘𝑆) → (deg‘(𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺))) ∈
ℕ0) |
176 | 102, 175 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (deg‘(𝐹 ∘𝑓
− (𝐻
∘𝑓 · 𝐺))) ∈
ℕ0) |
177 | 176 | nn0red 11352 |
. . . . . . . 8
⊢ (𝜑 → (deg‘(𝐹 ∘𝑓
− (𝐻
∘𝑓 · 𝐺))) ∈ ℝ) |
178 | 15 | nn0red 11352 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℝ) |
179 | 25 | nn0red 11352 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℝ) |
180 | 177, 178,
179 | ltsub1d 10636 |
. . . . . . 7
⊢ (𝜑 → ((deg‘(𝐹 ∘𝑓
− (𝐻
∘𝑓 · 𝐺))) < 𝑀 ↔ ((deg‘(𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺))) − 𝑁) < (𝑀 − 𝑁))) |
181 | 134 | breq2d 4665 |
. . . . . . 7
⊢ (𝜑 → (((deg‘(𝐹 ∘𝑓
− (𝐻
∘𝑓 · 𝐺))) − 𝑁) < (𝑀 − 𝑁) ↔ ((deg‘(𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺))) − 𝑁) < 𝐷)) |
182 | 180, 181 | bitrd 268 |
. . . . . 6
⊢ (𝜑 → ((deg‘(𝐹 ∘𝑓
− (𝐻
∘𝑓 · 𝐺))) < 𝑀 ↔ ((deg‘(𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺))) − 𝑁) < 𝐷)) |
183 | 182 | orbi2d 738 |
. . . . 5
⊢ (𝜑 → (((𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺)) =
0𝑝 ∨ (deg‘(𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺))) < 𝑀) ↔ ((𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺)) =
0𝑝 ∨ ((deg‘(𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺))) − 𝑁) < 𝐷))) |
184 | | eqid 2622 |
. . . . . . 7
⊢
(deg‘(𝐹
∘𝑓 − (𝐻 ∘𝑓 · 𝐺))) = (deg‘(𝐹 ∘𝑓
− (𝐻
∘𝑓 · 𝐺))) |
185 | | eqid 2622 |
. . . . . . 7
⊢
(coeff‘(𝐹
∘𝑓 − (𝐻 ∘𝑓 · 𝐺))) = (coeff‘(𝐹 ∘𝑓
− (𝐻
∘𝑓 · 𝐺))) |
186 | 184, 185 | dgrlt 24022 |
. . . . . 6
⊢ (((𝐹 ∘𝑓
− (𝐻
∘𝑓 · 𝐺)) ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0) → (((𝐹 ∘𝑓
− (𝐻
∘𝑓 · 𝐺)) = 0𝑝 ∨
(deg‘(𝐹
∘𝑓 − (𝐻 ∘𝑓 · 𝐺))) < 𝑀) ↔ ((deg‘(𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺))) ≤ 𝑀 ∧ ((coeff‘(𝐹 ∘𝑓
− (𝐻
∘𝑓 · 𝐺)))‘𝑀) = 0))) |
187 | 102, 15, 186 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (((𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺)) =
0𝑝 ∨ (deg‘(𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺))) < 𝑀) ↔ ((deg‘(𝐹 ∘𝑓
− (𝐻
∘𝑓 · 𝐺))) ≤ 𝑀 ∧ ((coeff‘(𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺)))‘𝑀) = 0))) |
188 | 183, 187 | bitr3d 270 |
. . . 4
⊢ (𝜑 → (((𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺)) =
0𝑝 ∨ ((deg‘(𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺))) − 𝑁) < 𝐷) ↔ ((deg‘(𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺))) ≤ 𝑀 ∧ ((coeff‘(𝐹 ∘𝑓
− (𝐻
∘𝑓 · 𝐺)))‘𝑀) = 0))) |
189 | 145, 174,
188 | mpbir2and 957 |
. . 3
⊢ (𝜑 → ((𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺)) =
0𝑝 ∨ ((deg‘(𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺))) − 𝑁) < 𝐷)) |
190 | | eqeq1 2626 |
. . . . . 6
⊢ (𝑓 = (𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺)) → (𝑓 = 0𝑝 ↔
(𝐹
∘𝑓 − (𝐻 ∘𝑓 · 𝐺)) =
0𝑝)) |
191 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑓 = (𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺)) →
(deg‘𝑓) =
(deg‘(𝐹
∘𝑓 − (𝐻 ∘𝑓 · 𝐺)))) |
192 | 191 | oveq1d 6665 |
. . . . . . 7
⊢ (𝑓 = (𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺)) →
((deg‘𝑓) −
𝑁) = ((deg‘(𝐹 ∘𝑓
− (𝐻
∘𝑓 · 𝐺))) − 𝑁)) |
193 | 192 | breq1d 4663 |
. . . . . 6
⊢ (𝑓 = (𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺)) →
(((deg‘𝑓) −
𝑁) < 𝐷 ↔ ((deg‘(𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺))) − 𝑁) < 𝐷)) |
194 | 190, 193 | orbi12d 746 |
. . . . 5
⊢ (𝑓 = (𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺)) → ((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
𝑁) < 𝐷) ↔ ((𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺)) =
0𝑝 ∨ ((deg‘(𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺))) − 𝑁) < 𝐷))) |
195 | | plydiv.u |
. . . . . . . . 9
⊢ 𝑈 = (𝑓 ∘𝑓 − (𝐺 ∘𝑓
· 𝑝)) |
196 | | oveq1 6657 |
. . . . . . . . 9
⊢ (𝑓 = (𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺)) → (𝑓 ∘𝑓
− (𝐺
∘𝑓 · 𝑝)) = ((𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺))
∘𝑓 − (𝐺 ∘𝑓 · 𝑝))) |
197 | 195, 196 | syl5eq 2668 |
. . . . . . . 8
⊢ (𝑓 = (𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺)) → 𝑈 = ((𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺))
∘𝑓 − (𝐺 ∘𝑓 · 𝑝))) |
198 | 197 | eqeq1d 2624 |
. . . . . . 7
⊢ (𝑓 = (𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺)) → (𝑈 = 0𝑝 ↔
((𝐹
∘𝑓 − (𝐻 ∘𝑓 · 𝐺)) ∘𝑓
− (𝐺
∘𝑓 · 𝑝)) = 0𝑝)) |
199 | 197 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑓 = (𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺)) →
(deg‘𝑈) =
(deg‘((𝐹
∘𝑓 − (𝐻 ∘𝑓 · 𝐺)) ∘𝑓
− (𝐺
∘𝑓 · 𝑝)))) |
200 | 199 | breq1d 4663 |
. . . . . . 7
⊢ (𝑓 = (𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺)) →
((deg‘𝑈) < 𝑁 ↔ (deg‘((𝐹 ∘𝑓
− (𝐻
∘𝑓 · 𝐺)) ∘𝑓 −
(𝐺
∘𝑓 · 𝑝))) < 𝑁)) |
201 | 198, 200 | orbi12d 746 |
. . . . . 6
⊢ (𝑓 = (𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺)) → ((𝑈 = 0𝑝 ∨
(deg‘𝑈) < 𝑁) ↔ (((𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺))
∘𝑓 − (𝐺 ∘𝑓 · 𝑝)) = 0𝑝 ∨
(deg‘((𝐹
∘𝑓 − (𝐻 ∘𝑓 · 𝐺)) ∘𝑓
− (𝐺
∘𝑓 · 𝑝))) < 𝑁))) |
202 | 201 | rexbidv 3052 |
. . . . 5
⊢ (𝑓 = (𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺)) →
(∃𝑝 ∈
(Poly‘𝑆)(𝑈 = 0𝑝 ∨
(deg‘𝑈) < 𝑁) ↔ ∃𝑝 ∈ (Poly‘𝑆)(((𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺))
∘𝑓 − (𝐺 ∘𝑓 · 𝑝)) = 0𝑝 ∨
(deg‘((𝐹
∘𝑓 − (𝐻 ∘𝑓 · 𝐺)) ∘𝑓
− (𝐺
∘𝑓 · 𝑝))) < 𝑁))) |
203 | 194, 202 | imbi12d 334 |
. . . 4
⊢ (𝑓 = (𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺)) →
(((𝑓 =
0𝑝 ∨ ((deg‘𝑓) − 𝑁) < 𝐷) → ∃𝑝 ∈ (Poly‘𝑆)(𝑈 = 0𝑝 ∨
(deg‘𝑈) < 𝑁)) ↔ (((𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺)) =
0𝑝 ∨ ((deg‘(𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺))) − 𝑁) < 𝐷) → ∃𝑝 ∈ (Poly‘𝑆)(((𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺))
∘𝑓 − (𝐺 ∘𝑓 · 𝑝)) = 0𝑝 ∨
(deg‘((𝐹
∘𝑓 − (𝐻 ∘𝑓 · 𝐺)) ∘𝑓
− (𝐺
∘𝑓 · 𝑝))) < 𝑁)))) |
204 | 203 | rspcv 3305 |
. . 3
⊢ ((𝐹 ∘𝑓
− (𝐻
∘𝑓 · 𝐺)) ∈ (Poly‘𝑆) → (∀𝑓 ∈ (Poly‘𝑆)((𝑓 = 0𝑝 ∨
((deg‘𝑓) −
𝑁) < 𝐷) → ∃𝑝 ∈ (Poly‘𝑆)(𝑈 = 0𝑝 ∨
(deg‘𝑈) < 𝑁)) → (((𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺)) =
0𝑝 ∨ ((deg‘(𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺))) − 𝑁) < 𝐷) → ∃𝑝 ∈ (Poly‘𝑆)(((𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺))
∘𝑓 − (𝐺 ∘𝑓 · 𝑝)) = 0𝑝 ∨
(deg‘((𝐹
∘𝑓 − (𝐻 ∘𝑓 · 𝐺)) ∘𝑓
− (𝐺
∘𝑓 · 𝑝))) < 𝑁)))) |
205 | 102, 103,
189, 204 | syl3c 66 |
. 2
⊢ (𝜑 → ∃𝑝 ∈ (Poly‘𝑆)(((𝐹 ∘𝑓 − (𝐻 ∘𝑓
· 𝐺))
∘𝑓 − (𝐺 ∘𝑓 · 𝑝)) = 0𝑝 ∨
(deg‘((𝐹
∘𝑓 − (𝐻 ∘𝑓 · 𝐺)) ∘𝑓
− (𝐺
∘𝑓 · 𝑝))) < 𝑁)) |
206 | 100, 205 | r19.29a 3078 |
1
⊢ (𝜑 → ∃𝑞 ∈ (Poly‘𝑆)(𝑅 = 0𝑝 ∨
(deg‘𝑅) < 𝑁)) |