Step | Hyp | Ref
| Expression |
1 | | plyf 23758 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘ℝ)
→ 𝐹:ℂ⟶ℂ) |
2 | | ffn 5958 |
. . . . 5
⊢ (𝐹:ℂ⟶ℂ →
𝐹 Fn
ℂ) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝐹 ∈ (Poly‘ℝ)
→ 𝐹 Fn
ℂ) |
4 | | ovex 6577 |
. . . . . 6
⊢ (𝑥↑𝐷) ∈ V |
5 | 4 | rgenw 2908 |
. . . . 5
⊢
∀𝑥 ∈
ℝ+ (𝑥↑𝐷) ∈ V |
6 | | signsplypnf.g |
. . . . . 6
⊢ 𝐺 = (𝑥 ∈ ℝ+ ↦ (𝑥↑𝐷)) |
7 | 6 | fnmpt 5933 |
. . . . 5
⊢
(∀𝑥 ∈
ℝ+ (𝑥↑𝐷) ∈ V → 𝐺 Fn ℝ+) |
8 | 5, 7 | mp1i 13 |
. . . 4
⊢ (𝐹 ∈ (Poly‘ℝ)
→ 𝐺 Fn
ℝ+) |
9 | | cnex 9896 |
. . . . 5
⊢ ℂ
∈ V |
10 | 9 | a1i 11 |
. . . 4
⊢ (𝐹 ∈ (Poly‘ℝ)
→ ℂ ∈ V) |
11 | | reex 9906 |
. . . . . 6
⊢ ℝ
∈ V |
12 | | rpssre 11719 |
. . . . . 6
⊢
ℝ+ ⊆ ℝ |
13 | 11, 12 | ssexi 4731 |
. . . . 5
⊢
ℝ+ ∈ V |
14 | 13 | a1i 11 |
. . . 4
⊢ (𝐹 ∈ (Poly‘ℝ)
→ ℝ+ ∈ V) |
15 | | ax-resscn 9872 |
. . . . . 6
⊢ ℝ
⊆ ℂ |
16 | 12, 15 | sstri 3577 |
. . . . 5
⊢
ℝ+ ⊆ ℂ |
17 | | sseqin2 3779 |
. . . . 5
⊢
(ℝ+ ⊆ ℂ ↔ (ℂ ∩
ℝ+) = ℝ+) |
18 | 16, 17 | mpbi 219 |
. . . 4
⊢ (ℂ
∩ ℝ+) = ℝ+ |
19 | | signsply0.c |
. . . . 5
⊢ 𝐶 = (coeff‘𝐹) |
20 | | signsply0.d |
. . . . 5
⊢ 𝐷 = (deg‘𝐹) |
21 | 19, 20 | coeid2 23799 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈ ℂ)
→ (𝐹‘𝑥) = Σ𝑘 ∈ (0...𝐷)((𝐶‘𝑘) · (𝑥↑𝑘))) |
22 | 6 | fvmpt2 6200 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ+
∧ (𝑥↑𝐷) ∈ V) → (𝐺‘𝑥) = (𝑥↑𝐷)) |
23 | 4, 22 | mpan2 703 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ (𝐺‘𝑥) = (𝑥↑𝐷)) |
24 | 23 | adantl 481 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → (𝐺‘𝑥) = (𝑥↑𝐷)) |
25 | 3, 8, 10, 14, 18, 21, 24 | offval 6802 |
. . 3
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝐹
∘𝑓 / 𝐺) = (𝑥 ∈ ℝ+ ↦
(Σ𝑘 ∈ (0...𝐷)((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)))) |
26 | | fzfid 12634 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → (0...𝐷) ∈ Fin) |
27 | 16 | a1i 11 |
. . . . . . . 8
⊢ (𝐹 ∈ (Poly‘ℝ)
→ ℝ+ ⊆ ℂ) |
28 | 27 | sselda 3568 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → 𝑥 ∈ ℂ) |
29 | | dgrcl 23793 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (deg‘𝐹) ∈
ℕ0) |
30 | 20, 29 | syl5eqel 2692 |
. . . . . . . 8
⊢ (𝐹 ∈ (Poly‘ℝ)
→ 𝐷 ∈
ℕ0) |
31 | 30 | adantr 480 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → 𝐷 ∈
ℕ0) |
32 | 28, 31 | expcld 12870 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → (𝑥↑𝐷) ∈ ℂ) |
33 | 19 | coef3 23792 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Poly‘ℝ)
→ 𝐶:ℕ0⟶ℂ) |
34 | 33 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝐷)) → 𝐶:ℕ0⟶ℂ) |
35 | | elfznn0 12302 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...𝐷) → 𝑘 ∈ ℕ0) |
36 | 35 | adantl 481 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝐷)) → 𝑘 ∈ ℕ0) |
37 | 34, 36 | ffvelrnd 6268 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝐷)) → (𝐶‘𝑘) ∈ ℂ) |
38 | 28 | adantr 480 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝐷)) → 𝑥 ∈ ℂ) |
39 | 38, 36 | expcld 12870 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝐷)) → (𝑥↑𝑘) ∈ ℂ) |
40 | 37, 39 | mulcld 9939 |
. . . . . 6
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝐷)) → ((𝐶‘𝑘) · (𝑥↑𝑘)) ∈ ℂ) |
41 | | rpne0 11724 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ≠
0) |
42 | 41 | adantl 481 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → 𝑥 ≠ 0) |
43 | 30 | nn0zd 11356 |
. . . . . . . 8
⊢ (𝐹 ∈ (Poly‘ℝ)
→ 𝐷 ∈
ℤ) |
44 | 43 | adantr 480 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → 𝐷 ∈ ℤ) |
45 | 28, 42, 44 | expne0d 12876 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → (𝑥↑𝐷) ≠ 0) |
46 | 26, 32, 40, 45 | fsumdivc 14360 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → (Σ𝑘 ∈ (0...𝐷)((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) = Σ𝑘 ∈ (0...𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷))) |
47 | | fzodisj 12371 |
. . . . . . . 8
⊢
((0..^𝐷) ∩
(𝐷..^(𝐷 + 1))) = ∅ |
48 | | fzosn 12405 |
. . . . . . . . 9
⊢ (𝐷 ∈ ℤ → (𝐷..^(𝐷 + 1)) = {𝐷}) |
49 | 48 | ineq2d 3776 |
. . . . . . . 8
⊢ (𝐷 ∈ ℤ →
((0..^𝐷) ∩ (𝐷..^(𝐷 + 1))) = ((0..^𝐷) ∩ {𝐷})) |
50 | 47, 49 | syl5reqr 2659 |
. . . . . . 7
⊢ (𝐷 ∈ ℤ →
((0..^𝐷) ∩ {𝐷}) = ∅) |
51 | 44, 50 | syl 17 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → ((0..^𝐷) ∩ {𝐷}) = ∅) |
52 | | fzval3 12404 |
. . . . . . . . 9
⊢ (𝐷 ∈ ℤ →
(0...𝐷) = (0..^(𝐷 + 1))) |
53 | 43, 52 | syl 17 |
. . . . . . . 8
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (0...𝐷) =
(0..^(𝐷 +
1))) |
54 | | nn0uz 11598 |
. . . . . . . . . 10
⊢
ℕ0 = (ℤ≥‘0) |
55 | 30, 54 | syl6eleq 2698 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Poly‘ℝ)
→ 𝐷 ∈
(ℤ≥‘0)) |
56 | | fzosplitsn 12442 |
. . . . . . . . 9
⊢ (𝐷 ∈
(ℤ≥‘0) → (0..^(𝐷 + 1)) = ((0..^𝐷) ∪ {𝐷})) |
57 | 55, 56 | syl 17 |
. . . . . . . 8
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (0..^(𝐷 + 1)) =
((0..^𝐷) ∪ {𝐷})) |
58 | 53, 57 | eqtrd 2644 |
. . . . . . 7
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (0...𝐷) =
((0..^𝐷) ∪ {𝐷})) |
59 | 58 | adantr 480 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → (0...𝐷) = ((0..^𝐷) ∪ {𝐷})) |
60 | 32 | adantr 480 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝐷)) → (𝑥↑𝐷) ∈ ℂ) |
61 | 42 | adantr 480 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝐷)) → 𝑥 ≠ 0) |
62 | 44 | adantr 480 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝐷)) → 𝐷 ∈ ℤ) |
63 | 38, 61, 62 | expne0d 12876 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝐷)) → (𝑥↑𝐷) ≠ 0) |
64 | 40, 60, 63 | divcld 10680 |
. . . . . 6
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝐷)) → (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) ∈ ℂ) |
65 | 51, 59, 26, 64 | fsumsplit 14318 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → Σ𝑘 ∈ (0...𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) = (Σ𝑘 ∈ (0..^𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) + Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)))) |
66 | 46, 65 | eqtrd 2644 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → (Σ𝑘 ∈ (0...𝐷)((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) = (Σ𝑘 ∈ (0..^𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) + Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)))) |
67 | 66 | mpteq2dva 4672 |
. . 3
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑘 ∈ (0...𝐷)((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑘 ∈ (0..^𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) + Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷))))) |
68 | 25, 67 | eqtrd 2644 |
. 2
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝐹
∘𝑓 / 𝐺) = (𝑥 ∈ ℝ+ ↦
(Σ𝑘 ∈ (0..^𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) + Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷))))) |
69 | | sumex 14266 |
. . . . 5
⊢
Σ𝑘 ∈
(0..^𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) ∈ V |
70 | 69 | a1i 11 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → Σ𝑘 ∈ (0..^𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) ∈ V) |
71 | | sumex 14266 |
. . . . 5
⊢
Σ𝑘 ∈
{𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) ∈ V |
72 | 71 | a1i 11 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) ∈ V) |
73 | 12 | a1i 11 |
. . . . . 6
⊢ (𝐹 ∈ (Poly‘ℝ)
→ ℝ+ ⊆ ℝ) |
74 | | fzofi 12635 |
. . . . . . 7
⊢
(0..^𝐷) ∈
Fin |
75 | 74 | a1i 11 |
. . . . . 6
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (0..^𝐷) ∈
Fin) |
76 | | ovex 6577 |
. . . . . . 7
⊢ (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) ∈ V |
77 | 76 | a1i 11 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ (𝑥 ∈
ℝ+ ∧ 𝑘
∈ (0..^𝐷))) →
(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) ∈ V) |
78 | 33 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → 𝐶:ℕ0⟶ℂ) |
79 | | elfzonn0 12380 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (0..^𝐷) → 𝑘 ∈ ℕ0) |
80 | 79 | ad2antlr 759 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → 𝑘 ∈
ℕ0) |
81 | 78, 80 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (𝐶‘𝑘) ∈ ℂ) |
82 | 28 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℂ) |
83 | 82, 80 | expcld 12870 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (𝑥↑𝑘) ∈ ℂ) |
84 | 32 | adantlr 747 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (𝑥↑𝐷) ∈ ℂ) |
85 | 41 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → 𝑥 ≠ 0) |
86 | 44 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → 𝐷 ∈
ℤ) |
87 | 82, 85, 86 | expne0d 12876 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (𝑥↑𝐷) ≠ 0) |
88 | 81, 83, 84, 87 | divassd 10715 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) = ((𝐶‘𝑘) · ((𝑥↑𝑘) / (𝑥↑𝐷)))) |
89 | 88 | mpteq2dva 4672 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) → (𝑥 ∈ ℝ+ ↦ (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷))) = (𝑥 ∈ ℝ+ ↦ ((𝐶‘𝑘) · ((𝑥↑𝑘) / (𝑥↑𝐷))))) |
90 | | fvex 6113 |
. . . . . . . . . 10
⊢ (𝐶‘𝑘) ∈ V |
91 | 90 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (𝐶‘𝑘) ∈ V) |
92 | | ovex 6577 |
. . . . . . . . . 10
⊢ ((𝑥↑𝑘) / (𝑥↑𝐷)) ∈ V |
93 | 92 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → ((𝑥↑𝑘) / (𝑥↑𝐷)) ∈ V) |
94 | 33 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) → 𝐶:ℕ0⟶ℂ) |
95 | 79 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) → 𝑘 ∈ ℕ0) |
96 | 94, 95 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) → (𝐶‘𝑘) ∈ ℂ) |
97 | | rlimconst 14123 |
. . . . . . . . . 10
⊢
((ℝ+ ⊆ ℝ ∧ (𝐶‘𝑘) ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ (𝐶‘𝑘)) ⇝𝑟 (𝐶‘𝑘)) |
98 | 12, 96, 97 | sylancr 694 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) → (𝑥 ∈ ℝ+ ↦ (𝐶‘𝑘)) ⇝𝑟 (𝐶‘𝑘)) |
99 | 80 | nn0zd 11356 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → 𝑘 ∈
ℤ) |
100 | 86, 99 | zsubcld 11363 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (𝐷 − 𝑘) ∈ ℤ) |
101 | 82, 85, 100 | cxpexpzd 24257 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (𝑥↑𝑐(𝐷 − 𝑘)) = (𝑥↑(𝐷 − 𝑘))) |
102 | 101 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (1 /
(𝑥↑𝑐(𝐷 − 𝑘))) = (1 / (𝑥↑(𝐷 − 𝑘)))) |
103 | 82, 85, 100 | expnegd 12877 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (𝑥↑-(𝐷 − 𝑘)) = (1 / (𝑥↑(𝐷 − 𝑘)))) |
104 | 86 | zcnd 11359 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → 𝐷 ∈
ℂ) |
105 | 80 | nn0cnd 11230 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → 𝑘 ∈
ℂ) |
106 | 104, 105 | negsubdi2d 10287 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → -(𝐷 − 𝑘) = (𝑘 − 𝐷)) |
107 | 106 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (𝑥↑-(𝐷 − 𝑘)) = (𝑥↑(𝑘 − 𝐷))) |
108 | 102, 103,
107 | 3eqtr2d 2650 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (1 /
(𝑥↑𝑐(𝐷 − 𝑘))) = (𝑥↑(𝑘 − 𝐷))) |
109 | 82, 85, 86, 99 | expsubd 12881 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (𝑥↑(𝑘 − 𝐷)) = ((𝑥↑𝑘) / (𝑥↑𝐷))) |
110 | 108, 109 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (1 /
(𝑥↑𝑐(𝐷 − 𝑘))) = ((𝑥↑𝑘) / (𝑥↑𝐷))) |
111 | 110 | mpteq2dva 4672 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) → (𝑥 ∈ ℝ+ ↦ (1 /
(𝑥↑𝑐(𝐷 − 𝑘)))) = (𝑥 ∈ ℝ+ ↦ ((𝑥↑𝑘) / (𝑥↑𝐷)))) |
112 | 95 | nn0red 11229 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) → 𝑘 ∈ ℝ) |
113 | 30 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) → 𝐷 ∈
ℕ0) |
114 | 113 | nn0red 11229 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) → 𝐷 ∈ ℝ) |
115 | | elfzolt2 12348 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0..^𝐷) → 𝑘 < 𝐷) |
116 | 115 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) → 𝑘 < 𝐷) |
117 | | difrp 11744 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℝ ∧ 𝐷 ∈ ℝ) → (𝑘 < 𝐷 ↔ (𝐷 − 𝑘) ∈
ℝ+)) |
118 | 117 | biimpa 500 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ 𝑘 < 𝐷) → (𝐷 − 𝑘) ∈
ℝ+) |
119 | 112, 114,
116, 118 | syl21anc 1317 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) → (𝐷 − 𝑘) ∈
ℝ+) |
120 | | cxplim 24498 |
. . . . . . . . . . 11
⊢ ((𝐷 − 𝑘) ∈ ℝ+ → (𝑥 ∈ ℝ+
↦ (1 / (𝑥↑𝑐(𝐷 − 𝑘)))) ⇝𝑟
0) |
121 | 119, 120 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) → (𝑥 ∈ ℝ+ ↦ (1 /
(𝑥↑𝑐(𝐷 − 𝑘)))) ⇝𝑟
0) |
122 | 111, 121 | eqbrtrrd 4607 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) → (𝑥 ∈ ℝ+ ↦ ((𝑥↑𝑘) / (𝑥↑𝐷))) ⇝𝑟
0) |
123 | 91, 93, 98, 122 | rlimmul 14223 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) → (𝑥 ∈ ℝ+ ↦ ((𝐶‘𝑘) · ((𝑥↑𝑘) / (𝑥↑𝐷)))) ⇝𝑟 ((𝐶‘𝑘) · 0)) |
124 | 96 | mul01d 10114 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) → ((𝐶‘𝑘) · 0) = 0) |
125 | 123, 124 | breqtrd 4609 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) → (𝑥 ∈ ℝ+ ↦ ((𝐶‘𝑘) · ((𝑥↑𝑘) / (𝑥↑𝐷)))) ⇝𝑟
0) |
126 | 89, 125 | eqbrtrd 4605 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) → (𝑥 ∈ ℝ+ ↦ (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷))) ⇝𝑟
0) |
127 | 73, 75, 77, 126 | fsumrlim 14384 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝑥 ∈
ℝ+ ↦ Σ𝑘 ∈ (0..^𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷))) ⇝𝑟 Σ𝑘 ∈ (0..^𝐷)0) |
128 | 75 | olcd 407 |
. . . . . 6
⊢ (𝐹 ∈ (Poly‘ℝ)
→ ((0..^𝐷) ⊆
(ℤ≥‘0) ∨ (0..^𝐷) ∈ Fin)) |
129 | | sumz 14300 |
. . . . . 6
⊢
(((0..^𝐷) ⊆
(ℤ≥‘0) ∨ (0..^𝐷) ∈ Fin) → Σ𝑘 ∈ (0..^𝐷)0 = 0) |
130 | 128, 129 | syl 17 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘ℝ)
→ Σ𝑘 ∈
(0..^𝐷)0 =
0) |
131 | 127, 130 | breqtrd 4609 |
. . . 4
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝑥 ∈
ℝ+ ↦ Σ𝑘 ∈ (0..^𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷))) ⇝𝑟
0) |
132 | 33, 30 | ffvelrnd 6268 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝐶‘𝐷) ∈
ℂ) |
133 | 132 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → (𝐶‘𝐷) ∈ ℂ) |
134 | 133, 32 | mulcld 9939 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → ((𝐶‘𝐷) · (𝑥↑𝐷)) ∈ ℂ) |
135 | 134, 32, 45 | divcld 10680 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → (((𝐶‘𝐷) · (𝑥↑𝐷)) / (𝑥↑𝐷)) ∈ ℂ) |
136 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐷 → (𝐶‘𝑘) = (𝐶‘𝐷)) |
137 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐷 → (𝑥↑𝑘) = (𝑥↑𝐷)) |
138 | 136, 137 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐷 → ((𝐶‘𝑘) · (𝑥↑𝑘)) = ((𝐶‘𝐷) · (𝑥↑𝐷))) |
139 | 138 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑘 = 𝐷 → (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) = (((𝐶‘𝐷) · (𝑥↑𝐷)) / (𝑥↑𝐷))) |
140 | 139 | sumsn 14319 |
. . . . . . . 8
⊢ ((𝐷 ∈ ℕ0
∧ (((𝐶‘𝐷) · (𝑥↑𝐷)) / (𝑥↑𝐷)) ∈ ℂ) → Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) = (((𝐶‘𝐷) · (𝑥↑𝐷)) / (𝑥↑𝐷))) |
141 | 31, 135, 140 | syl2anc 691 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) = (((𝐶‘𝐷) · (𝑥↑𝐷)) / (𝑥↑𝐷))) |
142 | 133, 32, 45 | divcan4d 10686 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → (((𝐶‘𝐷) · (𝑥↑𝐷)) / (𝑥↑𝐷)) = (𝐶‘𝐷)) |
143 | 141, 142 | eqtrd 2644 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) = (𝐶‘𝐷)) |
144 | 143 | mpteq2dva 4672 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝑥 ∈
ℝ+ ↦ Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷))) = (𝑥 ∈ ℝ+ ↦ (𝐶‘𝐷))) |
145 | | rlimconst 14123 |
. . . . . 6
⊢
((ℝ+ ⊆ ℝ ∧ (𝐶‘𝐷) ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ (𝐶‘𝐷)) ⇝𝑟 (𝐶‘𝐷)) |
146 | 12, 132, 145 | sylancr 694 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝑥 ∈
ℝ+ ↦ (𝐶‘𝐷)) ⇝𝑟 (𝐶‘𝐷)) |
147 | 144, 146 | eqbrtrd 4605 |
. . . 4
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝑥 ∈
ℝ+ ↦ Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷))) ⇝𝑟 (𝐶‘𝐷)) |
148 | 70, 72, 131, 147 | rlimadd 14221 |
. . 3
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑘 ∈ (0..^𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) + Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)))) ⇝𝑟 (0 + (𝐶‘𝐷))) |
149 | 132 | addid2d 10116 |
. . . 4
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (0 + (𝐶‘𝐷)) = (𝐶‘𝐷)) |
150 | | signsply0.b |
. . . 4
⊢ 𝐵 = (𝐶‘𝐷) |
151 | 149, 150 | syl6eqr 2662 |
. . 3
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (0 + (𝐶‘𝐷)) = 𝐵) |
152 | 148, 151 | breqtrd 4609 |
. 2
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑘 ∈ (0..^𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) + Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)))) ⇝𝑟 𝐵) |
153 | 68, 152 | eqbrtrd 4605 |
1
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝐹
∘𝑓 / 𝐺) ⇝𝑟 𝐵) |