Step | Hyp | Ref
| Expression |
1 | | dgrco.4 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆)) |
2 | | plyf 23954 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ (Poly‘𝑆) → 𝐺:ℂ⟶ℂ) |
3 | 1, 2 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺:ℂ⟶ℂ) |
4 | 3 | ffvelrnda 6359 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝐺‘𝑥) ∈ ℂ) |
5 | | dgrco.3 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) |
6 | | plyf 23954 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ) |
7 | 5, 6 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:ℂ⟶ℂ) |
8 | 7 | ffvelrnda 6359 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐺‘𝑥) ∈ ℂ) → (𝐹‘(𝐺‘𝑥)) ∈ ℂ) |
9 | 4, 8 | syldan 487 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝐹‘(𝐺‘𝑥)) ∈ ℂ) |
10 | | dgrco.5 |
. . . . . . . . . . . . 13
⊢ 𝐴 = (coeff‘𝐹) |
11 | 10 | coef3 23988 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶ℂ) |
12 | 5, 11 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) |
13 | | dgrco.1 |
. . . . . . . . . . . 12
⊢ 𝑀 = (deg‘𝐹) |
14 | | dgrcl 23989 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) ∈
ℕ0) |
15 | 5, 14 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (deg‘𝐹) ∈
ℕ0) |
16 | 13, 15 | syl5eqel 2705 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
17 | 12, 16 | ffvelrnd 6360 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴‘𝑀) ∈ ℂ) |
18 | 17 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝐴‘𝑀) ∈ ℂ) |
19 | 16 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝑀 ∈
ℕ0) |
20 | 4, 19 | expcld 13008 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((𝐺‘𝑥)↑𝑀) ∈ ℂ) |
21 | 18, 20 | mulcld 10060 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀)) ∈ ℂ) |
22 | 9, 21 | npcand 10396 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (((𝐹‘(𝐺‘𝑥)) − ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀))) + ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀))) = (𝐹‘(𝐺‘𝑥))) |
23 | 22 | mpteq2dva 4744 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (((𝐹‘(𝐺‘𝑥)) − ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀))) + ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀)))) = (𝑥 ∈ ℂ ↦ (𝐹‘(𝐺‘𝑥)))) |
24 | | cnex 10017 |
. . . . . . . 8
⊢ ℂ
∈ V |
25 | 24 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℂ ∈
V) |
26 | 9, 21 | subcld 10392 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((𝐹‘(𝐺‘𝑥)) − ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀))) ∈ ℂ) |
27 | | eqidd 2623 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺‘𝑥)) − ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀)))) = (𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺‘𝑥)) − ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀))))) |
28 | | eqidd 2623 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀))) = (𝑥 ∈ ℂ ↦ ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀)))) |
29 | 25, 26, 21, 27, 28 | offval2 6914 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺‘𝑥)) − ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀)))) ∘𝑓 + (𝑥 ∈ ℂ ↦ ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀)))) = (𝑥 ∈ ℂ ↦ (((𝐹‘(𝐺‘𝑥)) − ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀))) + ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀))))) |
30 | 3 | feqmptd 6249 |
. . . . . . 7
⊢ (𝜑 → 𝐺 = (𝑥 ∈ ℂ ↦ (𝐺‘𝑥))) |
31 | 7 | feqmptd 6249 |
. . . . . . 7
⊢ (𝜑 → 𝐹 = (𝑦 ∈ ℂ ↦ (𝐹‘𝑦))) |
32 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑦 = (𝐺‘𝑥) → (𝐹‘𝑦) = (𝐹‘(𝐺‘𝑥))) |
33 | 4, 30, 31, 32 | fmptco 6396 |
. . . . . 6
⊢ (𝜑 → (𝐹 ∘ 𝐺) = (𝑥 ∈ ℂ ↦ (𝐹‘(𝐺‘𝑥)))) |
34 | 23, 29, 33 | 3eqtr4rd 2667 |
. . . . 5
⊢ (𝜑 → (𝐹 ∘ 𝐺) = ((𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺‘𝑥)) − ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀)))) ∘𝑓 + (𝑥 ∈ ℂ ↦ ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀))))) |
35 | 34 | fveq2d 6195 |
. . . 4
⊢ (𝜑 → (deg‘(𝐹 ∘ 𝐺)) = (deg‘((𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺‘𝑥)) − ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀)))) ∘𝑓 + (𝑥 ∈ ℂ ↦ ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀)))))) |
36 | 35 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (deg‘(𝐹 ∘ 𝐺)) = (deg‘((𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺‘𝑥)) − ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀)))) ∘𝑓 + (𝑥 ∈ ℂ ↦ ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀)))))) |
37 | 25, 9, 21, 33, 28 | offval2 6914 |
. . . . . 6
⊢ (𝜑 → ((𝐹 ∘ 𝐺) ∘𝑓 − (𝑥 ∈ ℂ ↦ ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀)))) = (𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺‘𝑥)) − ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀))))) |
38 | | plyssc 23956 |
. . . . . . . . 9
⊢
(Poly‘𝑆)
⊆ (Poly‘ℂ) |
39 | 38, 5 | sseldi 3601 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈
(Poly‘ℂ)) |
40 | 38, 1 | sseldi 3601 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈
(Poly‘ℂ)) |
41 | | addcl 10018 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝑧 + 𝑤) ∈ ℂ) |
42 | 41 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ)) → (𝑧 + 𝑤) ∈ ℂ) |
43 | | mulcl 10020 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝑧 · 𝑤) ∈ ℂ) |
44 | 43 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ)) → (𝑧 · 𝑤) ∈ ℂ) |
45 | 39, 40, 42, 44 | plyco 23997 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ∘ 𝐺) ∈
(Poly‘ℂ)) |
46 | | eqidd 2623 |
. . . . . . . . 9
⊢ (𝜑 → (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))) = (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) |
47 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐺‘𝑥) → (𝑦↑𝑀) = ((𝐺‘𝑥)↑𝑀)) |
48 | 47 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝑦 = (𝐺‘𝑥) → ((𝐴‘𝑀) · (𝑦↑𝑀)) = ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀))) |
49 | 4, 30, 46, 48 | fmptco 6396 |
. . . . . . . 8
⊢ (𝜑 → ((𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))) ∘ 𝐺) = (𝑥 ∈ ℂ ↦ ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀)))) |
50 | | ssid 3624 |
. . . . . . . . . . 11
⊢ ℂ
⊆ ℂ |
51 | 50 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℂ ⊆
ℂ) |
52 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))) = (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))) |
53 | 52 | ply1term 23960 |
. . . . . . . . . 10
⊢ ((ℂ
⊆ ℂ ∧ (𝐴‘𝑀) ∈ ℂ ∧ 𝑀 ∈ ℕ0) → (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))) ∈
(Poly‘ℂ)) |
54 | 51, 17, 16, 53 | syl3anc 1326 |
. . . . . . . . 9
⊢ (𝜑 → (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))) ∈
(Poly‘ℂ)) |
55 | 54, 40, 42, 44 | plyco 23997 |
. . . . . . . 8
⊢ (𝜑 → ((𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))) ∘ 𝐺) ∈
(Poly‘ℂ)) |
56 | 49, 55 | eqeltrrd 2702 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀))) ∈
(Poly‘ℂ)) |
57 | | plysubcl 23978 |
. . . . . . 7
⊢ (((𝐹 ∘ 𝐺) ∈ (Poly‘ℂ) ∧ (𝑥 ∈ ℂ ↦ ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀))) ∈ (Poly‘ℂ)) →
((𝐹 ∘ 𝐺) ∘𝑓
− (𝑥 ∈ ℂ
↦ ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀)))) ∈
(Poly‘ℂ)) |
58 | 45, 56, 57 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → ((𝐹 ∘ 𝐺) ∘𝑓 − (𝑥 ∈ ℂ ↦ ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀)))) ∈
(Poly‘ℂ)) |
59 | 37, 58 | eqeltrrd 2702 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺‘𝑥)) − ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀)))) ∈
(Poly‘ℂ)) |
60 | 59 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺‘𝑥)) − ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀)))) ∈
(Poly‘ℂ)) |
61 | 56 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (𝑥 ∈ ℂ ↦ ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀))) ∈
(Poly‘ℂ)) |
62 | | dgrco.7 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 = (𝐷 + 1)) |
63 | | dgrco.6 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐷 ∈
ℕ0) |
64 | | nn0p1nn 11332 |
. . . . . . . . . . . 12
⊢ (𝐷 ∈ ℕ0
→ (𝐷 + 1) ∈
ℕ) |
65 | 63, 64 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐷 + 1) ∈ ℕ) |
66 | 62, 65 | eqeltrd 2701 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℕ) |
67 | 66 | nngt0d 11064 |
. . . . . . . . 9
⊢ (𝜑 → 0 < 𝑀) |
68 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ ((𝐹 ∘𝑓
− (𝑦 ∈ ℂ
↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) = 0𝑝 →
(deg‘(𝐹
∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) =
(deg‘0𝑝)) |
69 | | dgr0 24018 |
. . . . . . . . . . 11
⊢
(deg‘0𝑝) = 0 |
70 | 68, 69 | syl6eq 2672 |
. . . . . . . . . 10
⊢ ((𝐹 ∘𝑓
− (𝑦 ∈ ℂ
↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) = 0𝑝 →
(deg‘(𝐹
∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) = 0) |
71 | 70 | breq1d 4663 |
. . . . . . . . 9
⊢ ((𝐹 ∘𝑓
− (𝑦 ∈ ℂ
↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) = 0𝑝 →
((deg‘(𝐹
∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) < 𝑀 ↔ 0 < 𝑀)) |
72 | 67, 71 | syl5ibrcom 237 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) = 0𝑝 →
(deg‘(𝐹
∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) < 𝑀)) |
73 | | idd 24 |
. . . . . . . 8
⊢ (𝜑 → ((deg‘(𝐹 ∘𝑓
− (𝑦 ∈ ℂ
↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) < 𝑀 → (deg‘(𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) < 𝑀)) |
74 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(deg‘(𝑦 ∈
ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) = (deg‘(𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) |
75 | 13, 74 | dgrsub 24028 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ (𝑦 ∈ ℂ
↦ ((𝐴‘𝑀) · (𝑦↑𝑀))) ∈ (Poly‘ℂ)) →
(deg‘(𝐹
∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) ≤ if(𝑀 ≤ (deg‘(𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))), (deg‘(𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))), 𝑀)) |
76 | 39, 54, 75 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝜑 → (deg‘(𝐹 ∘𝑓
− (𝑦 ∈ ℂ
↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) ≤ if(𝑀 ≤ (deg‘(𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))), (deg‘(𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))), 𝑀)) |
77 | 66 | nnne0d 11065 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ≠ 0) |
78 | 13, 10 | dgreq0 24021 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0𝑝 ↔ (𝐴‘𝑀) = 0)) |
79 | 5, 78 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐹 = 0𝑝 ↔ (𝐴‘𝑀) = 0)) |
80 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 = 0𝑝 →
(deg‘𝐹) =
(deg‘0𝑝)) |
81 | 80, 69 | syl6eq 2672 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 = 0𝑝 →
(deg‘𝐹) =
0) |
82 | 13, 81 | syl5eq 2668 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 = 0𝑝 →
𝑀 = 0) |
83 | 79, 82 | syl6bir 244 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐴‘𝑀) = 0 → 𝑀 = 0)) |
84 | 83 | necon3d 2815 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀 ≠ 0 → (𝐴‘𝑀) ≠ 0)) |
85 | 77, 84 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴‘𝑀) ≠ 0) |
86 | 52 | dgr1term 24016 |
. . . . . . . . . . . . 13
⊢ (((𝐴‘𝑀) ∈ ℂ ∧ (𝐴‘𝑀) ≠ 0 ∧ 𝑀 ∈ ℕ0) →
(deg‘(𝑦 ∈
ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) = 𝑀) |
87 | 17, 85, 16, 86 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢ (𝜑 → (deg‘(𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) = 𝑀) |
88 | 87 | ifeq1d 4104 |
. . . . . . . . . . 11
⊢ (𝜑 → if(𝑀 ≤ (deg‘(𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))), (deg‘(𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))), 𝑀) = if(𝑀 ≤ (deg‘(𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))), 𝑀, 𝑀)) |
89 | | ifid 4125 |
. . . . . . . . . . 11
⊢ if(𝑀 ≤ (deg‘(𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))), 𝑀, 𝑀) = 𝑀 |
90 | 88, 89 | syl6eq 2672 |
. . . . . . . . . 10
⊢ (𝜑 → if(𝑀 ≤ (deg‘(𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))), (deg‘(𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))), 𝑀) = 𝑀) |
91 | 76, 90 | breqtrd 4679 |
. . . . . . . . 9
⊢ (𝜑 → (deg‘(𝐹 ∘𝑓
− (𝑦 ∈ ℂ
↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) ≤ 𝑀) |
92 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
(coeff‘(𝑦
∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) = (coeff‘(𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) |
93 | 10, 92 | coesub 24013 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ (𝑦 ∈ ℂ
↦ ((𝐴‘𝑀) · (𝑦↑𝑀))) ∈ (Poly‘ℂ)) →
(coeff‘(𝐹
∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) = (𝐴 ∘𝑓 −
(coeff‘(𝑦 ∈
ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))))) |
94 | 39, 54, 93 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝜑 → (coeff‘(𝐹 ∘𝑓
− (𝑦 ∈ ℂ
↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) = (𝐴 ∘𝑓 −
(coeff‘(𝑦 ∈
ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))))) |
95 | 94 | fveq1d 6193 |
. . . . . . . . . 10
⊢ (𝜑 → ((coeff‘(𝐹 ∘𝑓
− (𝑦 ∈ ℂ
↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))))‘𝑀) = ((𝐴 ∘𝑓 −
(coeff‘(𝑦 ∈
ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))))‘𝑀)) |
96 | | ffn 6045 |
. . . . . . . . . . . . 13
⊢ (𝐴:ℕ0⟶ℂ →
𝐴 Fn
ℕ0) |
97 | 12, 96 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 Fn ℕ0) |
98 | 92 | coef3 23988 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))) ∈ (Poly‘ℂ) →
(coeff‘(𝑦 ∈
ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))):ℕ0⟶ℂ) |
99 | 54, 98 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (coeff‘(𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))):ℕ0⟶ℂ) |
100 | | ffn 6045 |
. . . . . . . . . . . . 13
⊢
((coeff‘(𝑦
∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))):ℕ0⟶ℂ
→ (coeff‘(𝑦
∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) Fn
ℕ0) |
101 | 99, 100 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (coeff‘(𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) Fn
ℕ0) |
102 | | nn0ex 11298 |
. . . . . . . . . . . . 13
⊢
ℕ0 ∈ V |
103 | 102 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℕ0 ∈
V) |
104 | | inidm 3822 |
. . . . . . . . . . . 12
⊢
(ℕ0 ∩ ℕ0) =
ℕ0 |
105 | | eqidd 2623 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ0) → (𝐴‘𝑀) = (𝐴‘𝑀)) |
106 | 52 | coe1term 24015 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴‘𝑀) ∈ ℂ ∧ 𝑀 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
→ ((coeff‘(𝑦
∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))‘𝑀) = if(𝑀 = 𝑀, (𝐴‘𝑀), 0)) |
107 | 17, 16, 16, 106 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((coeff‘(𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))‘𝑀) = if(𝑀 = 𝑀, (𝐴‘𝑀), 0)) |
108 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢ 𝑀 = 𝑀 |
109 | 108 | iftruei 4093 |
. . . . . . . . . . . . . 14
⊢ if(𝑀 = 𝑀, (𝐴‘𝑀), 0) = (𝐴‘𝑀) |
110 | 107, 109 | syl6eq 2672 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((coeff‘(𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))‘𝑀) = (𝐴‘𝑀)) |
111 | 110 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ0) →
((coeff‘(𝑦 ∈
ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))‘𝑀) = (𝐴‘𝑀)) |
112 | 97, 101, 103, 103, 104, 105, 111 | ofval 6906 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ0) → ((𝐴 ∘𝑓
− (coeff‘(𝑦
∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))))‘𝑀) = ((𝐴‘𝑀) − (𝐴‘𝑀))) |
113 | 16, 112 | mpdan 702 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴 ∘𝑓 −
(coeff‘(𝑦 ∈
ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))))‘𝑀) = ((𝐴‘𝑀) − (𝐴‘𝑀))) |
114 | 17 | subidd 10380 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴‘𝑀) − (𝐴‘𝑀)) = 0) |
115 | 95, 113, 114 | 3eqtrd 2660 |
. . . . . . . . 9
⊢ (𝜑 → ((coeff‘(𝐹 ∘𝑓
− (𝑦 ∈ ℂ
↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))))‘𝑀) = 0) |
116 | | plysubcl 23978 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ (𝑦 ∈ ℂ
↦ ((𝐴‘𝑀) · (𝑦↑𝑀))) ∈ (Poly‘ℂ)) →
(𝐹
∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) ∈
(Poly‘ℂ)) |
117 | 39, 54, 116 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) ∈
(Poly‘ℂ)) |
118 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(deg‘(𝐹
∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) = (deg‘(𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) |
119 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(coeff‘(𝐹
∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) = (coeff‘(𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) |
120 | 118, 119 | dgrlt 24022 |
. . . . . . . . . 10
⊢ (((𝐹 ∘𝑓
− (𝑦 ∈ ℂ
↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) ∈ (Poly‘ℂ) ∧ 𝑀 ∈ ℕ0)
→ (((𝐹
∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) = 0𝑝 ∨
(deg‘(𝐹
∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) < 𝑀) ↔ ((deg‘(𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) ≤ 𝑀 ∧ ((coeff‘(𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))))‘𝑀) = 0))) |
121 | 117, 16, 120 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) = 0𝑝 ∨
(deg‘(𝐹
∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) < 𝑀) ↔ ((deg‘(𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) ≤ 𝑀 ∧ ((coeff‘(𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))))‘𝑀) = 0))) |
122 | 91, 115, 121 | mpbir2and 957 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) = 0𝑝 ∨
(deg‘(𝐹
∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) < 𝑀)) |
123 | 72, 73, 122 | mpjaod 396 |
. . . . . . 7
⊢ (𝜑 → (deg‘(𝐹 ∘𝑓
− (𝑦 ∈ ℂ
↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) < 𝑀) |
124 | 123 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (deg‘(𝐹 ∘𝑓
− (𝑦 ∈ ℂ
↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) < 𝑀) |
125 | | dgrcl 23989 |
. . . . . . . . . 10
⊢ ((𝐹 ∘𝑓
− (𝑦 ∈ ℂ
↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) ∈ (Poly‘ℂ) →
(deg‘(𝐹
∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) ∈
ℕ0) |
126 | 117, 125 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (deg‘(𝐹 ∘𝑓
− (𝑦 ∈ ℂ
↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) ∈
ℕ0) |
127 | 126 | nn0red 11352 |
. . . . . . . 8
⊢ (𝜑 → (deg‘(𝐹 ∘𝑓
− (𝑦 ∈ ℂ
↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) ∈ ℝ) |
128 | 127 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (deg‘(𝐹 ∘𝑓
− (𝑦 ∈ ℂ
↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) ∈ ℝ) |
129 | 16 | nn0red 11352 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℝ) |
130 | 129 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → 𝑀 ∈ ℝ) |
131 | | nnre 11027 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
132 | 131 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℝ) |
133 | | nngt0 11049 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 0 <
𝑁) |
134 | 133 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → 0 < 𝑁) |
135 | | ltmul1 10873 |
. . . . . . 7
⊢
(((deg‘(𝐹
∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((deg‘(𝐹 ∘𝑓
− (𝑦 ∈ ℂ
↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) < 𝑀 ↔ ((deg‘(𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) · 𝑁) < (𝑀 · 𝑁))) |
136 | 128, 130,
132, 134, 135 | syl112anc 1330 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → ((deg‘(𝐹 ∘𝑓
− (𝑦 ∈ ℂ
↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) < 𝑀 ↔ ((deg‘(𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) · 𝑁) < (𝑀 · 𝑁))) |
137 | 124, 136 | mpbid 222 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → ((deg‘(𝐹 ∘𝑓
− (𝑦 ∈ ℂ
↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) · 𝑁) < (𝑀 · 𝑁)) |
138 | 7 | ffvelrnda 6359 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝐹‘𝑦) ∈ ℂ) |
139 | 17 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝐴‘𝑀) ∈ ℂ) |
140 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℂ → 𝑦 ∈
ℂ) |
141 | | expcl 12878 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℂ ∧ 𝑀 ∈ ℕ0)
→ (𝑦↑𝑀) ∈
ℂ) |
142 | 140, 16, 141 | syl2anr 495 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝑦↑𝑀) ∈ ℂ) |
143 | 139, 142 | mulcld 10060 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((𝐴‘𝑀) · (𝑦↑𝑀)) ∈ ℂ) |
144 | 25, 138, 143, 31, 46 | offval2 6914 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) = (𝑦 ∈ ℂ ↦ ((𝐹‘𝑦) − ((𝐴‘𝑀) · (𝑦↑𝑀))))) |
145 | 32, 48 | oveq12d 6668 |
. . . . . . . . 9
⊢ (𝑦 = (𝐺‘𝑥) → ((𝐹‘𝑦) − ((𝐴‘𝑀) · (𝑦↑𝑀))) = ((𝐹‘(𝐺‘𝑥)) − ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀)))) |
146 | 4, 30, 144, 145 | fmptco 6396 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) ∘ 𝐺) = (𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺‘𝑥)) − ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀))))) |
147 | 146 | fveq2d 6195 |
. . . . . . 7
⊢ (𝜑 → (deg‘((𝐹 ∘𝑓
− (𝑦 ∈ ℂ
↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) ∘ 𝐺)) = (deg‘(𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺‘𝑥)) − ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀)))))) |
148 | | dgrco.8 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑓 ∈ (Poly‘ℂ)((deg‘𝑓) ≤ 𝐷 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁))) |
149 | 123, 62 | breqtrd 4679 |
. . . . . . . . 9
⊢ (𝜑 → (deg‘(𝐹 ∘𝑓
− (𝑦 ∈ ℂ
↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) < (𝐷 + 1)) |
150 | | nn0leltp1 11436 |
. . . . . . . . . 10
⊢
(((deg‘(𝐹
∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) ∈ ℕ0 ∧ 𝐷 ∈ ℕ0)
→ ((deg‘(𝐹
∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) ≤ 𝐷 ↔ (deg‘(𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) < (𝐷 + 1))) |
151 | 126, 63, 150 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → ((deg‘(𝐹 ∘𝑓
− (𝑦 ∈ ℂ
↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) ≤ 𝐷 ↔ (deg‘(𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) < (𝐷 + 1))) |
152 | 149, 151 | mpbird 247 |
. . . . . . . 8
⊢ (𝜑 → (deg‘(𝐹 ∘𝑓
− (𝑦 ∈ ℂ
↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) ≤ 𝐷) |
153 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) → (deg‘𝑓) = (deg‘(𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))))) |
154 | 153 | breq1d 4663 |
. . . . . . . . . 10
⊢ (𝑓 = (𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) → ((deg‘𝑓) ≤ 𝐷 ↔ (deg‘(𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) ≤ 𝐷)) |
155 | | coeq1 5279 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) → (𝑓 ∘ 𝐺) = ((𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) ∘ 𝐺)) |
156 | 155 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) → (deg‘(𝑓 ∘ 𝐺)) = (deg‘((𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) ∘ 𝐺))) |
157 | 153 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) → ((deg‘𝑓) · 𝑁) = ((deg‘(𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) · 𝑁)) |
158 | 156, 157 | eqeq12d 2637 |
. . . . . . . . . 10
⊢ (𝑓 = (𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) → ((deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁) ↔ (deg‘((𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) ∘ 𝐺)) = ((deg‘(𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) · 𝑁))) |
159 | 154, 158 | imbi12d 334 |
. . . . . . . . 9
⊢ (𝑓 = (𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) → (((deg‘𝑓) ≤ 𝐷 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁)) ↔ ((deg‘(𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) ≤ 𝐷 → (deg‘((𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) ∘ 𝐺)) = ((deg‘(𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) · 𝑁)))) |
160 | 159 | rspcv 3305 |
. . . . . . . 8
⊢ ((𝐹 ∘𝑓
− (𝑦 ∈ ℂ
↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) ∈ (Poly‘ℂ) →
(∀𝑓 ∈
(Poly‘ℂ)((deg‘𝑓) ≤ 𝐷 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁)) → ((deg‘(𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) ≤ 𝐷 → (deg‘((𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) ∘ 𝐺)) = ((deg‘(𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) · 𝑁)))) |
161 | 117, 148,
152, 160 | syl3c 66 |
. . . . . . 7
⊢ (𝜑 → (deg‘((𝐹 ∘𝑓
− (𝑦 ∈ ℂ
↦ ((𝐴‘𝑀) · (𝑦↑𝑀)))) ∘ 𝐺)) = ((deg‘(𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) · 𝑁)) |
162 | 147, 161 | eqtr3d 2658 |
. . . . . 6
⊢ (𝜑 → (deg‘(𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺‘𝑥)) − ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀))))) = ((deg‘(𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) · 𝑁)) |
163 | 162 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (deg‘(𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺‘𝑥)) − ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀))))) = ((deg‘(𝐹 ∘𝑓 − (𝑦 ∈ ℂ ↦ ((𝐴‘𝑀) · (𝑦↑𝑀))))) · 𝑁)) |
164 | | fconstmpt 5163 |
. . . . . . . . . . 11
⊢ (ℂ
× {(𝐴‘𝑀)}) = (𝑥 ∈ ℂ ↦ (𝐴‘𝑀)) |
165 | 164 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (ℂ × {(𝐴‘𝑀)}) = (𝑥 ∈ ℂ ↦ (𝐴‘𝑀))) |
166 | | eqidd 2623 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((𝐺‘𝑥)↑𝑀)) = (𝑥 ∈ ℂ ↦ ((𝐺‘𝑥)↑𝑀))) |
167 | 25, 18, 20, 165, 166 | offval2 6914 |
. . . . . . . . 9
⊢ (𝜑 → ((ℂ × {(𝐴‘𝑀)}) ∘𝑓 ·
(𝑥 ∈ ℂ ↦
((𝐺‘𝑥)↑𝑀))) = (𝑥 ∈ ℂ ↦ ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀)))) |
168 | 167 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝜑 → (deg‘((ℂ
× {(𝐴‘𝑀)}) ∘𝑓
· (𝑥 ∈ ℂ
↦ ((𝐺‘𝑥)↑𝑀)))) = (deg‘(𝑥 ∈ ℂ ↦ ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀))))) |
169 | | eqidd 2623 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑦 ∈ ℂ ↦ (𝑦↑𝑀)) = (𝑦 ∈ ℂ ↦ (𝑦↑𝑀))) |
170 | 4, 30, 169, 47 | fmptco 6396 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑦 ∈ ℂ ↦ (𝑦↑𝑀)) ∘ 𝐺) = (𝑥 ∈ ℂ ↦ ((𝐺‘𝑥)↑𝑀))) |
171 | | 1cnd 10056 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℂ) |
172 | | plypow 23961 |
. . . . . . . . . . . 12
⊢ ((ℂ
⊆ ℂ ∧ 1 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → (𝑦 ∈ ℂ ↦ (𝑦↑𝑀)) ∈
(Poly‘ℂ)) |
173 | 51, 171, 16, 172 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑦 ∈ ℂ ↦ (𝑦↑𝑀)) ∈
(Poly‘ℂ)) |
174 | 173, 40, 42, 44 | plyco 23997 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑦 ∈ ℂ ↦ (𝑦↑𝑀)) ∘ 𝐺) ∈
(Poly‘ℂ)) |
175 | 170, 174 | eqeltrrd 2702 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((𝐺‘𝑥)↑𝑀)) ∈
(Poly‘ℂ)) |
176 | | dgrmulc 24027 |
. . . . . . . . 9
⊢ (((𝐴‘𝑀) ∈ ℂ ∧ (𝐴‘𝑀) ≠ 0 ∧ (𝑥 ∈ ℂ ↦ ((𝐺‘𝑥)↑𝑀)) ∈ (Poly‘ℂ)) →
(deg‘((ℂ × {(𝐴‘𝑀)}) ∘𝑓 ·
(𝑥 ∈ ℂ ↦
((𝐺‘𝑥)↑𝑀)))) = (deg‘(𝑥 ∈ ℂ ↦ ((𝐺‘𝑥)↑𝑀)))) |
177 | 17, 85, 175, 176 | syl3anc 1326 |
. . . . . . . 8
⊢ (𝜑 → (deg‘((ℂ
× {(𝐴‘𝑀)}) ∘𝑓
· (𝑥 ∈ ℂ
↦ ((𝐺‘𝑥)↑𝑀)))) = (deg‘(𝑥 ∈ ℂ ↦ ((𝐺‘𝑥)↑𝑀)))) |
178 | 168, 177 | eqtr3d 2658 |
. . . . . . 7
⊢ (𝜑 → (deg‘(𝑥 ∈ ℂ ↦ ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀)))) = (deg‘(𝑥 ∈ ℂ ↦ ((𝐺‘𝑥)↑𝑀)))) |
179 | 178 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (deg‘(𝑥 ∈ ℂ ↦ ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀)))) = (deg‘(𝑥 ∈ ℂ ↦ ((𝐺‘𝑥)↑𝑀)))) |
180 | | dgrco.2 |
. . . . . . 7
⊢ 𝑁 = (deg‘𝐺) |
181 | 66 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → 𝑀 ∈ ℕ) |
182 | | simpr 477 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℕ) |
183 | 1 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → 𝐺 ∈ (Poly‘𝑆)) |
184 | 180, 181,
182, 183 | dgrcolem1 24029 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (deg‘(𝑥 ∈ ℂ ↦ ((𝐺‘𝑥)↑𝑀))) = (𝑀 · 𝑁)) |
185 | 179, 184 | eqtrd 2656 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (deg‘(𝑥 ∈ ℂ ↦ ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀)))) = (𝑀 · 𝑁)) |
186 | 137, 163,
185 | 3brtr4d 4685 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (deg‘(𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺‘𝑥)) − ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀))))) < (deg‘(𝑥 ∈ ℂ ↦ ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀))))) |
187 | | eqid 2622 |
. . . . 5
⊢
(deg‘(𝑥 ∈
ℂ ↦ ((𝐹‘(𝐺‘𝑥)) − ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀))))) = (deg‘(𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺‘𝑥)) − ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀))))) |
188 | | eqid 2622 |
. . . . 5
⊢
(deg‘(𝑥 ∈
ℂ ↦ ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀)))) = (deg‘(𝑥 ∈ ℂ ↦ ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀)))) |
189 | 187, 188 | dgradd2 24024 |
. . . 4
⊢ (((𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺‘𝑥)) − ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀)))) ∈ (Poly‘ℂ) ∧
(𝑥 ∈ ℂ ↦
((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀))) ∈ (Poly‘ℂ) ∧
(deg‘(𝑥 ∈
ℂ ↦ ((𝐹‘(𝐺‘𝑥)) − ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀))))) < (deg‘(𝑥 ∈ ℂ ↦ ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀))))) → (deg‘((𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺‘𝑥)) − ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀)))) ∘𝑓 + (𝑥 ∈ ℂ ↦ ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀))))) = (deg‘(𝑥 ∈ ℂ ↦ ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀))))) |
190 | 60, 61, 186, 189 | syl3anc 1326 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (deg‘((𝑥 ∈ ℂ ↦ ((𝐹‘(𝐺‘𝑥)) − ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀)))) ∘𝑓 + (𝑥 ∈ ℂ ↦ ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀))))) = (deg‘(𝑥 ∈ ℂ ↦ ((𝐴‘𝑀) · ((𝐺‘𝑥)↑𝑀))))) |
191 | 36, 190, 185 | 3eqtrd 2660 |
. 2
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (deg‘(𝐹 ∘ 𝐺)) = (𝑀 · 𝑁)) |
192 | | 0cn 10032 |
. . . . . . . 8
⊢ 0 ∈
ℂ |
193 | | ffvelrn 6357 |
. . . . . . . 8
⊢ ((𝐺:ℂ⟶ℂ ∧ 0
∈ ℂ) → (𝐺‘0) ∈ ℂ) |
194 | 3, 192, 193 | sylancl 694 |
. . . . . . 7
⊢ (𝜑 → (𝐺‘0) ∈ ℂ) |
195 | 7, 194 | ffvelrnd 6360 |
. . . . . 6
⊢ (𝜑 → (𝐹‘(𝐺‘0)) ∈ ℂ) |
196 | | 0dgr 24001 |
. . . . . 6
⊢ ((𝐹‘(𝐺‘0)) ∈ ℂ →
(deg‘(ℂ × {(𝐹‘(𝐺‘0))})) = 0) |
197 | 195, 196 | syl 17 |
. . . . 5
⊢ (𝜑 → (deg‘(ℂ
× {(𝐹‘(𝐺‘0))})) =
0) |
198 | 16 | nn0cnd 11353 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℂ) |
199 | 198 | mul01d 10235 |
. . . . 5
⊢ (𝜑 → (𝑀 · 0) = 0) |
200 | 197, 199 | eqtr4d 2659 |
. . . 4
⊢ (𝜑 → (deg‘(ℂ
× {(𝐹‘(𝐺‘0))})) = (𝑀 · 0)) |
201 | 200 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝑁 = 0) → (deg‘(ℂ ×
{(𝐹‘(𝐺‘0))})) = (𝑀 · 0)) |
202 | 194 | ad2antrr 762 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑁 = 0) ∧ 𝑥 ∈ ℂ) → (𝐺‘0) ∈ ℂ) |
203 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 = 0) → 𝑁 = 0) |
204 | 180, 203 | syl5eqr 2670 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 = 0) → (deg‘𝐺) = 0) |
205 | | 0dgrb 24002 |
. . . . . . . . . 10
⊢ (𝐺 ∈ (Poly‘𝑆) → ((deg‘𝐺) = 0 ↔ 𝐺 = (ℂ × {(𝐺‘0)}))) |
206 | 1, 205 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((deg‘𝐺) = 0 ↔ 𝐺 = (ℂ × {(𝐺‘0)}))) |
207 | 206 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 = 0) → ((deg‘𝐺) = 0 ↔ 𝐺 = (ℂ × {(𝐺‘0)}))) |
208 | 204, 207 | mpbid 222 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 = 0) → 𝐺 = (ℂ × {(𝐺‘0)})) |
209 | | fconstmpt 5163 |
. . . . . . 7
⊢ (ℂ
× {(𝐺‘0)}) =
(𝑥 ∈ ℂ ↦
(𝐺‘0)) |
210 | 208, 209 | syl6eq 2672 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 = 0) → 𝐺 = (𝑥 ∈ ℂ ↦ (𝐺‘0))) |
211 | 31 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 = 0) → 𝐹 = (𝑦 ∈ ℂ ↦ (𝐹‘𝑦))) |
212 | | fveq2 6191 |
. . . . . 6
⊢ (𝑦 = (𝐺‘0) → (𝐹‘𝑦) = (𝐹‘(𝐺‘0))) |
213 | 202, 210,
211, 212 | fmptco 6396 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 = 0) → (𝐹 ∘ 𝐺) = (𝑥 ∈ ℂ ↦ (𝐹‘(𝐺‘0)))) |
214 | | fconstmpt 5163 |
. . . . 5
⊢ (ℂ
× {(𝐹‘(𝐺‘0))}) = (𝑥 ∈ ℂ ↦ (𝐹‘(𝐺‘0))) |
215 | 213, 214 | syl6eqr 2674 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 = 0) → (𝐹 ∘ 𝐺) = (ℂ × {(𝐹‘(𝐺‘0))})) |
216 | 215 | fveq2d 6195 |
. . 3
⊢ ((𝜑 ∧ 𝑁 = 0) → (deg‘(𝐹 ∘ 𝐺)) = (deg‘(ℂ × {(𝐹‘(𝐺‘0))}))) |
217 | 203 | oveq2d 6666 |
. . 3
⊢ ((𝜑 ∧ 𝑁 = 0) → (𝑀 · 𝑁) = (𝑀 · 0)) |
218 | 201, 216,
217 | 3eqtr4d 2666 |
. 2
⊢ ((𝜑 ∧ 𝑁 = 0) → (deg‘(𝐹 ∘ 𝐺)) = (𝑀 · 𝑁)) |
219 | | dgrcl 23989 |
. . . . 5
⊢ (𝐺 ∈ (Poly‘𝑆) → (deg‘𝐺) ∈
ℕ0) |
220 | 1, 219 | syl 17 |
. . . 4
⊢ (𝜑 → (deg‘𝐺) ∈
ℕ0) |
221 | 180, 220 | syl5eqel 2705 |
. . 3
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
222 | | elnn0 11294 |
. . 3
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℕ
∨ 𝑁 =
0)) |
223 | 221, 222 | sylib 208 |
. 2
⊢ (𝜑 → (𝑁 ∈ ℕ ∨ 𝑁 = 0)) |
224 | 191, 218,
223 | mpjaodan 827 |
1
⊢ (𝜑 → (deg‘(𝐹 ∘ 𝐺)) = (𝑀 · 𝑁)) |