| Step | Hyp | Ref
| Expression |
| 1 | | plyf 26237 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘ℝ)
→ 𝐹:ℂ⟶ℂ) |
| 2 | 1 | ffnd 6737 |
. . . 4
⊢ (𝐹 ∈ (Poly‘ℝ)
→ 𝐹 Fn
ℂ) |
| 3 | | ovex 7464 |
. . . . . 6
⊢ (𝑥↑𝐷) ∈ V |
| 4 | 3 | rgenw 3065 |
. . . . 5
⊢
∀𝑥 ∈
ℝ+ (𝑥↑𝐷) ∈ V |
| 5 | | signsplypnf.g |
. . . . . 6
⊢ 𝐺 = (𝑥 ∈ ℝ+ ↦ (𝑥↑𝐷)) |
| 6 | 5 | fnmpt 6708 |
. . . . 5
⊢
(∀𝑥 ∈
ℝ+ (𝑥↑𝐷) ∈ V → 𝐺 Fn ℝ+) |
| 7 | 4, 6 | mp1i 13 |
. . . 4
⊢ (𝐹 ∈ (Poly‘ℝ)
→ 𝐺 Fn
ℝ+) |
| 8 | | cnex 11236 |
. . . . 5
⊢ ℂ
∈ V |
| 9 | 8 | a1i 11 |
. . . 4
⊢ (𝐹 ∈ (Poly‘ℝ)
→ ℂ ∈ V) |
| 10 | | reex 11246 |
. . . . . 6
⊢ ℝ
∈ V |
| 11 | | rpssre 13042 |
. . . . . 6
⊢
ℝ+ ⊆ ℝ |
| 12 | 10, 11 | ssexi 5322 |
. . . . 5
⊢
ℝ+ ∈ V |
| 13 | 12 | a1i 11 |
. . . 4
⊢ (𝐹 ∈ (Poly‘ℝ)
→ ℝ+ ∈ V) |
| 14 | | ax-resscn 11212 |
. . . . . 6
⊢ ℝ
⊆ ℂ |
| 15 | 11, 14 | sstri 3993 |
. . . . 5
⊢
ℝ+ ⊆ ℂ |
| 16 | | sseqin2 4223 |
. . . . 5
⊢
(ℝ+ ⊆ ℂ ↔ (ℂ ∩
ℝ+) = ℝ+) |
| 17 | 15, 16 | mpbi 230 |
. . . 4
⊢ (ℂ
∩ ℝ+) = ℝ+ |
| 18 | | signsply0.c |
. . . . 5
⊢ 𝐶 = (coeff‘𝐹) |
| 19 | | signsply0.d |
. . . . 5
⊢ 𝐷 = (deg‘𝐹) |
| 20 | 18, 19 | coeid2 26278 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈ ℂ)
→ (𝐹‘𝑥) = Σ𝑘 ∈ (0...𝐷)((𝐶‘𝑘) · (𝑥↑𝑘))) |
| 21 | 5 | fvmpt2 7027 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ+
∧ (𝑥↑𝐷) ∈ V) → (𝐺‘𝑥) = (𝑥↑𝐷)) |
| 22 | 3, 21 | mpan2 691 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ (𝐺‘𝑥) = (𝑥↑𝐷)) |
| 23 | 22 | adantl 481 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → (𝐺‘𝑥) = (𝑥↑𝐷)) |
| 24 | 2, 7, 9, 13, 17, 20, 23 | offval 7706 |
. . 3
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝐹
∘f / 𝐺) =
(𝑥 ∈
ℝ+ ↦ (Σ𝑘 ∈ (0...𝐷)((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)))) |
| 25 | | fzfid 14014 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → (0...𝐷) ∈ Fin) |
| 26 | 15 | a1i 11 |
. . . . . . . 8
⊢ (𝐹 ∈ (Poly‘ℝ)
→ ℝ+ ⊆ ℂ) |
| 27 | 26 | sselda 3983 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → 𝑥 ∈ ℂ) |
| 28 | | dgrcl 26272 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (deg‘𝐹) ∈
ℕ0) |
| 29 | 19, 28 | eqeltrid 2845 |
. . . . . . . 8
⊢ (𝐹 ∈ (Poly‘ℝ)
→ 𝐷 ∈
ℕ0) |
| 30 | 29 | adantr 480 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → 𝐷 ∈
ℕ0) |
| 31 | 27, 30 | expcld 14186 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → (𝑥↑𝐷) ∈ ℂ) |
| 32 | 18 | coef3 26271 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Poly‘ℝ)
→ 𝐶:ℕ0⟶ℂ) |
| 33 | 32 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝐷)) → 𝐶:ℕ0⟶ℂ) |
| 34 | | elfznn0 13660 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...𝐷) → 𝑘 ∈ ℕ0) |
| 35 | 34 | adantl 481 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝐷)) → 𝑘 ∈ ℕ0) |
| 36 | 33, 35 | ffvelcdmd 7105 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝐷)) → (𝐶‘𝑘) ∈ ℂ) |
| 37 | 27 | adantr 480 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝐷)) → 𝑥 ∈ ℂ) |
| 38 | 37, 35 | expcld 14186 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝐷)) → (𝑥↑𝑘) ∈ ℂ) |
| 39 | 36, 38 | mulcld 11281 |
. . . . . 6
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝐷)) → ((𝐶‘𝑘) · (𝑥↑𝑘)) ∈ ℂ) |
| 40 | | rpne0 13051 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ≠
0) |
| 41 | 40 | adantl 481 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → 𝑥 ≠ 0) |
| 42 | 29 | nn0zd 12639 |
. . . . . . . 8
⊢ (𝐹 ∈ (Poly‘ℝ)
→ 𝐷 ∈
ℤ) |
| 43 | 42 | adantr 480 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → 𝐷 ∈ ℤ) |
| 44 | 27, 41, 43 | expne0d 14192 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → (𝑥↑𝐷) ≠ 0) |
| 45 | 25, 31, 39, 44 | fsumdivc 15822 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → (Σ𝑘 ∈ (0...𝐷)((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) = Σ𝑘 ∈ (0...𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷))) |
| 46 | | fzosn 13775 |
. . . . . . . . 9
⊢ (𝐷 ∈ ℤ → (𝐷..^(𝐷 + 1)) = {𝐷}) |
| 47 | 46 | ineq2d 4220 |
. . . . . . . 8
⊢ (𝐷 ∈ ℤ →
((0..^𝐷) ∩ (𝐷..^(𝐷 + 1))) = ((0..^𝐷) ∩ {𝐷})) |
| 48 | | fzodisj 13733 |
. . . . . . . 8
⊢
((0..^𝐷) ∩
(𝐷..^(𝐷 + 1))) = ∅ |
| 49 | 47, 48 | eqtr3di 2792 |
. . . . . . 7
⊢ (𝐷 ∈ ℤ →
((0..^𝐷) ∩ {𝐷}) = ∅) |
| 50 | 43, 49 | syl 17 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → ((0..^𝐷) ∩ {𝐷}) = ∅) |
| 51 | | fzval3 13773 |
. . . . . . . . 9
⊢ (𝐷 ∈ ℤ →
(0...𝐷) = (0..^(𝐷 + 1))) |
| 52 | 42, 51 | syl 17 |
. . . . . . . 8
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (0...𝐷) =
(0..^(𝐷 +
1))) |
| 53 | | nn0uz 12920 |
. . . . . . . . . 10
⊢
ℕ0 = (ℤ≥‘0) |
| 54 | 29, 53 | eleqtrdi 2851 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Poly‘ℝ)
→ 𝐷 ∈
(ℤ≥‘0)) |
| 55 | | fzosplitsn 13814 |
. . . . . . . . 9
⊢ (𝐷 ∈
(ℤ≥‘0) → (0..^(𝐷 + 1)) = ((0..^𝐷) ∪ {𝐷})) |
| 56 | 54, 55 | syl 17 |
. . . . . . . 8
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (0..^(𝐷 + 1)) =
((0..^𝐷) ∪ {𝐷})) |
| 57 | 52, 56 | eqtrd 2777 |
. . . . . . 7
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (0...𝐷) =
((0..^𝐷) ∪ {𝐷})) |
| 58 | 57 | adantr 480 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → (0...𝐷) = ((0..^𝐷) ∪ {𝐷})) |
| 59 | 31 | adantr 480 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝐷)) → (𝑥↑𝐷) ∈ ℂ) |
| 60 | 41 | adantr 480 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝐷)) → 𝑥 ≠ 0) |
| 61 | 43 | adantr 480 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝐷)) → 𝐷 ∈ ℤ) |
| 62 | 37, 60, 61 | expne0d 14192 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝐷)) → (𝑥↑𝐷) ≠ 0) |
| 63 | 39, 59, 62 | divcld 12043 |
. . . . . 6
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝐷)) → (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) ∈ ℂ) |
| 64 | 50, 58, 25, 63 | fsumsplit 15777 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → Σ𝑘 ∈ (0...𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) = (Σ𝑘 ∈ (0..^𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) + Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)))) |
| 65 | 45, 64 | eqtrd 2777 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → (Σ𝑘 ∈ (0...𝐷)((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) = (Σ𝑘 ∈ (0..^𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) + Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)))) |
| 66 | 65 | mpteq2dva 5242 |
. . 3
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑘 ∈ (0...𝐷)((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑘 ∈ (0..^𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) + Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷))))) |
| 67 | 24, 66 | eqtrd 2777 |
. 2
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝐹
∘f / 𝐺) =
(𝑥 ∈
ℝ+ ↦ (Σ𝑘 ∈ (0..^𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) + Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷))))) |
| 68 | | sumex 15724 |
. . . . 5
⊢
Σ𝑘 ∈
(0..^𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) ∈ V |
| 69 | 68 | a1i 11 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → Σ𝑘 ∈ (0..^𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) ∈ V) |
| 70 | | sumex 15724 |
. . . . 5
⊢
Σ𝑘 ∈
{𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) ∈ V |
| 71 | 70 | a1i 11 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) ∈ V) |
| 72 | 11 | a1i 11 |
. . . . . 6
⊢ (𝐹 ∈ (Poly‘ℝ)
→ ℝ+ ⊆ ℝ) |
| 73 | | fzofi 14015 |
. . . . . . 7
⊢
(0..^𝐷) ∈
Fin |
| 74 | 73 | a1i 11 |
. . . . . 6
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (0..^𝐷) ∈
Fin) |
| 75 | | ovexd 7466 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ (𝑥 ∈
ℝ+ ∧ 𝑘
∈ (0..^𝐷))) →
(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) ∈ V) |
| 76 | 32 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → 𝐶:ℕ0⟶ℂ) |
| 77 | | elfzonn0 13747 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (0..^𝐷) → 𝑘 ∈ ℕ0) |
| 78 | 77 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → 𝑘 ∈
ℕ0) |
| 79 | 76, 78 | ffvelcdmd 7105 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (𝐶‘𝑘) ∈ ℂ) |
| 80 | 27 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℂ) |
| 81 | 80, 78 | expcld 14186 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (𝑥↑𝑘) ∈ ℂ) |
| 82 | 31 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (𝑥↑𝐷) ∈ ℂ) |
| 83 | 40 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → 𝑥 ≠ 0) |
| 84 | 43 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → 𝐷 ∈
ℤ) |
| 85 | 80, 83, 84 | expne0d 14192 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (𝑥↑𝐷) ≠ 0) |
| 86 | 79, 81, 82, 85 | divassd 12078 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) = ((𝐶‘𝑘) · ((𝑥↑𝑘) / (𝑥↑𝐷)))) |
| 87 | 86 | mpteq2dva 5242 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) → (𝑥 ∈ ℝ+ ↦ (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷))) = (𝑥 ∈ ℝ+ ↦ ((𝐶‘𝑘) · ((𝑥↑𝑘) / (𝑥↑𝐷))))) |
| 88 | | fvexd 6921 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (𝐶‘𝑘) ∈ V) |
| 89 | | ovexd 7466 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → ((𝑥↑𝑘) / (𝑥↑𝐷)) ∈ V) |
| 90 | 32 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) → 𝐶:ℕ0⟶ℂ) |
| 91 | 77 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) → 𝑘 ∈ ℕ0) |
| 92 | 90, 91 | ffvelcdmd 7105 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) → (𝐶‘𝑘) ∈ ℂ) |
| 93 | | rlimconst 15580 |
. . . . . . . . . 10
⊢
((ℝ+ ⊆ ℝ ∧ (𝐶‘𝑘) ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ (𝐶‘𝑘)) ⇝𝑟 (𝐶‘𝑘)) |
| 94 | 11, 92, 93 | sylancr 587 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) → (𝑥 ∈ ℝ+ ↦ (𝐶‘𝑘)) ⇝𝑟 (𝐶‘𝑘)) |
| 95 | 78 | nn0zd 12639 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → 𝑘 ∈
ℤ) |
| 96 | 84, 95 | zsubcld 12727 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (𝐷 − 𝑘) ∈ ℤ) |
| 97 | 80, 83, 96 | cxpexpzd 26753 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (𝑥↑𝑐(𝐷 − 𝑘)) = (𝑥↑(𝐷 − 𝑘))) |
| 98 | 97 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (1 /
(𝑥↑𝑐(𝐷 − 𝑘))) = (1 / (𝑥↑(𝐷 − 𝑘)))) |
| 99 | 80, 83, 96 | expnegd 14193 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (𝑥↑-(𝐷 − 𝑘)) = (1 / (𝑥↑(𝐷 − 𝑘)))) |
| 100 | 84 | zcnd 12723 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → 𝐷 ∈
ℂ) |
| 101 | 78 | nn0cnd 12589 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → 𝑘 ∈
ℂ) |
| 102 | 100, 101 | negsubdi2d 11636 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → -(𝐷 − 𝑘) = (𝑘 − 𝐷)) |
| 103 | 102 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (𝑥↑-(𝐷 − 𝑘)) = (𝑥↑(𝑘 − 𝐷))) |
| 104 | 98, 99, 103 | 3eqtr2d 2783 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (1 /
(𝑥↑𝑐(𝐷 − 𝑘))) = (𝑥↑(𝑘 − 𝐷))) |
| 105 | 80, 83, 84, 95 | expsubd 14197 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (𝑥↑(𝑘 − 𝐷)) = ((𝑥↑𝑘) / (𝑥↑𝐷))) |
| 106 | 104, 105 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (1 /
(𝑥↑𝑐(𝐷 − 𝑘))) = ((𝑥↑𝑘) / (𝑥↑𝐷))) |
| 107 | 106 | mpteq2dva 5242 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) → (𝑥 ∈ ℝ+ ↦ (1 /
(𝑥↑𝑐(𝐷 − 𝑘)))) = (𝑥 ∈ ℝ+ ↦ ((𝑥↑𝑘) / (𝑥↑𝐷)))) |
| 108 | 91 | nn0red 12588 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) → 𝑘 ∈ ℝ) |
| 109 | 29 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) → 𝐷 ∈
ℕ0) |
| 110 | 109 | nn0red 12588 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) → 𝐷 ∈ ℝ) |
| 111 | | elfzolt2 13708 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0..^𝐷) → 𝑘 < 𝐷) |
| 112 | 111 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) → 𝑘 < 𝐷) |
| 113 | | difrp 13073 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℝ ∧ 𝐷 ∈ ℝ) → (𝑘 < 𝐷 ↔ (𝐷 − 𝑘) ∈
ℝ+)) |
| 114 | 113 | biimpa 476 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ 𝑘 < 𝐷) → (𝐷 − 𝑘) ∈
ℝ+) |
| 115 | 108, 110,
112, 114 | syl21anc 838 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) → (𝐷 − 𝑘) ∈
ℝ+) |
| 116 | | cxplim 27015 |
. . . . . . . . . . 11
⊢ ((𝐷 − 𝑘) ∈ ℝ+ → (𝑥 ∈ ℝ+
↦ (1 / (𝑥↑𝑐(𝐷 − 𝑘)))) ⇝𝑟
0) |
| 117 | 115, 116 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) → (𝑥 ∈ ℝ+ ↦ (1 /
(𝑥↑𝑐(𝐷 − 𝑘)))) ⇝𝑟
0) |
| 118 | 107, 117 | eqbrtrrd 5167 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) → (𝑥 ∈ ℝ+ ↦ ((𝑥↑𝑘) / (𝑥↑𝐷))) ⇝𝑟
0) |
| 119 | 88, 89, 94, 118 | rlimmul 15681 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) → (𝑥 ∈ ℝ+ ↦ ((𝐶‘𝑘) · ((𝑥↑𝑘) / (𝑥↑𝐷)))) ⇝𝑟 ((𝐶‘𝑘) · 0)) |
| 120 | 92 | mul01d 11460 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) → ((𝐶‘𝑘) · 0) = 0) |
| 121 | 119, 120 | breqtrd 5169 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) → (𝑥 ∈ ℝ+ ↦ ((𝐶‘𝑘) · ((𝑥↑𝑘) / (𝑥↑𝐷)))) ⇝𝑟
0) |
| 122 | 87, 121 | eqbrtrd 5165 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑘 ∈ (0..^𝐷)) → (𝑥 ∈ ℝ+ ↦ (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷))) ⇝𝑟
0) |
| 123 | 72, 74, 75, 122 | fsumrlim 15847 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝑥 ∈
ℝ+ ↦ Σ𝑘 ∈ (0..^𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷))) ⇝𝑟 Σ𝑘 ∈ (0..^𝐷)0) |
| 124 | 74 | olcd 875 |
. . . . . 6
⊢ (𝐹 ∈ (Poly‘ℝ)
→ ((0..^𝐷) ⊆
(ℤ≥‘0) ∨ (0..^𝐷) ∈ Fin)) |
| 125 | | sumz 15758 |
. . . . . 6
⊢
(((0..^𝐷) ⊆
(ℤ≥‘0) ∨ (0..^𝐷) ∈ Fin) → Σ𝑘 ∈ (0..^𝐷)0 = 0) |
| 126 | 124, 125 | syl 17 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘ℝ)
→ Σ𝑘 ∈
(0..^𝐷)0 =
0) |
| 127 | 123, 126 | breqtrd 5169 |
. . . 4
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝑥 ∈
ℝ+ ↦ Σ𝑘 ∈ (0..^𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷))) ⇝𝑟
0) |
| 128 | 32, 29 | ffvelcdmd 7105 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝐶‘𝐷) ∈
ℂ) |
| 129 | 128 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → (𝐶‘𝐷) ∈ ℂ) |
| 130 | 129, 31 | mulcld 11281 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → ((𝐶‘𝐷) · (𝑥↑𝐷)) ∈ ℂ) |
| 131 | 130, 31, 44 | divcld 12043 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → (((𝐶‘𝐷) · (𝑥↑𝐷)) / (𝑥↑𝐷)) ∈ ℂ) |
| 132 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐷 → (𝐶‘𝑘) = (𝐶‘𝐷)) |
| 133 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐷 → (𝑥↑𝑘) = (𝑥↑𝐷)) |
| 134 | 132, 133 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐷 → ((𝐶‘𝑘) · (𝑥↑𝑘)) = ((𝐶‘𝐷) · (𝑥↑𝐷))) |
| 135 | 134 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝑘 = 𝐷 → (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) = (((𝐶‘𝐷) · (𝑥↑𝐷)) / (𝑥↑𝐷))) |
| 136 | 135 | sumsn 15782 |
. . . . . . . 8
⊢ ((𝐷 ∈ ℕ0
∧ (((𝐶‘𝐷) · (𝑥↑𝐷)) / (𝑥↑𝐷)) ∈ ℂ) → Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) = (((𝐶‘𝐷) · (𝑥↑𝐷)) / (𝑥↑𝐷))) |
| 137 | 30, 131, 136 | syl2anc 584 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) = (((𝐶‘𝐷) · (𝑥↑𝐷)) / (𝑥↑𝐷))) |
| 138 | 129, 31, 44 | divcan4d 12049 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → (((𝐶‘𝐷) · (𝑥↑𝐷)) / (𝑥↑𝐷)) = (𝐶‘𝐷)) |
| 139 | 137, 138 | eqtrd 2777 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝑥 ∈
ℝ+) → Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) = (𝐶‘𝐷)) |
| 140 | 139 | mpteq2dva 5242 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝑥 ∈
ℝ+ ↦ Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷))) = (𝑥 ∈ ℝ+ ↦ (𝐶‘𝐷))) |
| 141 | | rlimconst 15580 |
. . . . . 6
⊢
((ℝ+ ⊆ ℝ ∧ (𝐶‘𝐷) ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ (𝐶‘𝐷)) ⇝𝑟 (𝐶‘𝐷)) |
| 142 | 11, 128, 141 | sylancr 587 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝑥 ∈
ℝ+ ↦ (𝐶‘𝐷)) ⇝𝑟 (𝐶‘𝐷)) |
| 143 | 140, 142 | eqbrtrd 5165 |
. . . 4
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝑥 ∈
ℝ+ ↦ Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷))) ⇝𝑟 (𝐶‘𝐷)) |
| 144 | 69, 71, 127, 143 | rlimadd 15679 |
. . 3
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑘 ∈ (0..^𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) + Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)))) ⇝𝑟 (0 + (𝐶‘𝐷))) |
| 145 | 128 | addlidd 11462 |
. . . 4
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (0 + (𝐶‘𝐷)) = (𝐶‘𝐷)) |
| 146 | | signsply0.b |
. . . 4
⊢ 𝐵 = (𝐶‘𝐷) |
| 147 | 145, 146 | eqtr4di 2795 |
. . 3
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (0 + (𝐶‘𝐷)) = 𝐵) |
| 148 | 144, 147 | breqtrd 5169 |
. 2
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑘 ∈ (0..^𝐷)(((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)) + Σ𝑘 ∈ {𝐷} (((𝐶‘𝑘) · (𝑥↑𝑘)) / (𝑥↑𝐷)))) ⇝𝑟 𝐵) |
| 149 | 67, 148 | eqbrtrd 5165 |
1
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝐹
∘f / 𝐺)
⇝𝑟 𝐵) |