Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  signsplypnf Structured version   Visualization version   GIF version

Theorem signsplypnf 29787
Description: The quotient of a polynomial 𝐹 by a monic monomial of same degree 𝐺 converges to the highest coefficient of 𝐹. (Contributed by Thierry Arnoux, 18-Sep-2018.)
Hypotheses
Ref Expression
signsply0.d 𝐷 = (deg‘𝐹)
signsply0.c 𝐶 = (coeff‘𝐹)
signsply0.b 𝐵 = (𝐶𝐷)
signsplypnf.g 𝐺 = (𝑥 ∈ ℝ+ ↦ (𝑥𝐷))
Assertion
Ref Expression
signsplypnf (𝐹 ∈ (Poly‘ℝ) → (𝐹𝑓 / 𝐺) ⇝𝑟 𝐵)
Distinct variable groups:   𝑥,𝐶   𝑥,𝐷   𝑥,𝐹   𝑥,𝐺
Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem signsplypnf
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 plyf 23703 . . . . 5 (𝐹 ∈ (Poly‘ℝ) → 𝐹:ℂ⟶ℂ)
2 ffn 5944 . . . . 5 (𝐹:ℂ⟶ℂ → 𝐹 Fn ℂ)
31, 2syl 17 . . . 4 (𝐹 ∈ (Poly‘ℝ) → 𝐹 Fn ℂ)
4 ovex 6555 . . . . . 6 (𝑥𝐷) ∈ V
54rgenw 2907 . . . . 5 𝑥 ∈ ℝ+ (𝑥𝐷) ∈ V
6 signsplypnf.g . . . . . 6 𝐺 = (𝑥 ∈ ℝ+ ↦ (𝑥𝐷))
76fnmpt 5919 . . . . 5 (∀𝑥 ∈ ℝ+ (𝑥𝐷) ∈ V → 𝐺 Fn ℝ+)
85, 7mp1i 13 . . . 4 (𝐹 ∈ (Poly‘ℝ) → 𝐺 Fn ℝ+)
9 cnex 9874 . . . . 5 ℂ ∈ V
109a1i 11 . . . 4 (𝐹 ∈ (Poly‘ℝ) → ℂ ∈ V)
11 reex 9884 . . . . . 6 ℝ ∈ V
12 rpssre 11678 . . . . . 6 + ⊆ ℝ
1311, 12ssexi 4726 . . . . 5 + ∈ V
1413a1i 11 . . . 4 (𝐹 ∈ (Poly‘ℝ) → ℝ+ ∈ V)
15 ax-resscn 9850 . . . . . 6 ℝ ⊆ ℂ
1612, 15sstri 3576 . . . . 5 + ⊆ ℂ
17 sseqin2 3778 . . . . 5 (ℝ+ ⊆ ℂ ↔ (ℂ ∩ ℝ+) = ℝ+)
1816, 17mpbi 218 . . . 4 (ℂ ∩ ℝ+) = ℝ+
19 signsply0.c . . . . 5 𝐶 = (coeff‘𝐹)
20 signsply0.d . . . . 5 𝐷 = (deg‘𝐹)
2119, 20coeid2 23744 . . . 4 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℂ) → (𝐹𝑥) = Σ𝑘 ∈ (0...𝐷)((𝐶𝑘) · (𝑥𝑘)))
226fvmpt2 6185 . . . . . 6 ((𝑥 ∈ ℝ+ ∧ (𝑥𝐷) ∈ V) → (𝐺𝑥) = (𝑥𝐷))
234, 22mpan2 702 . . . . 5 (𝑥 ∈ ℝ+ → (𝐺𝑥) = (𝑥𝐷))
2423adantl 480 . . . 4 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ+) → (𝐺𝑥) = (𝑥𝐷))
253, 8, 10, 14, 18, 21, 24offval 6780 . . 3 (𝐹 ∈ (Poly‘ℝ) → (𝐹𝑓 / 𝐺) = (𝑥 ∈ ℝ+ ↦ (Σ𝑘 ∈ (0...𝐷)((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷))))
26 fzfid 12592 . . . . . 6 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ+) → (0...𝐷) ∈ Fin)
2716a1i 11 . . . . . . . 8 (𝐹 ∈ (Poly‘ℝ) → ℝ+ ⊆ ℂ)
2827sselda 3567 . . . . . . 7 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
29 dgrcl 23738 . . . . . . . . 9 (𝐹 ∈ (Poly‘ℝ) → (deg‘𝐹) ∈ ℕ0)
3020, 29syl5eqel 2691 . . . . . . . 8 (𝐹 ∈ (Poly‘ℝ) → 𝐷 ∈ ℕ0)
3130adantr 479 . . . . . . 7 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ+) → 𝐷 ∈ ℕ0)
3228, 31expcld 12828 . . . . . 6 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ+) → (𝑥𝐷) ∈ ℂ)
3319coef3 23737 . . . . . . . . 9 (𝐹 ∈ (Poly‘ℝ) → 𝐶:ℕ0⟶ℂ)
3433ad2antrr 757 . . . . . . . 8 (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝐷)) → 𝐶:ℕ0⟶ℂ)
35 elfznn0 12260 . . . . . . . . 9 (𝑘 ∈ (0...𝐷) → 𝑘 ∈ ℕ0)
3635adantl 480 . . . . . . . 8 (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝐷)) → 𝑘 ∈ ℕ0)
3734, 36ffvelrnd 6253 . . . . . . 7 (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝐷)) → (𝐶𝑘) ∈ ℂ)
3828adantr 479 . . . . . . . 8 (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝐷)) → 𝑥 ∈ ℂ)
3938, 36expcld 12828 . . . . . . 7 (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝐷)) → (𝑥𝑘) ∈ ℂ)
4037, 39mulcld 9917 . . . . . 6 (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝐷)) → ((𝐶𝑘) · (𝑥𝑘)) ∈ ℂ)
41 rpne0 11683 . . . . . . . 8 (𝑥 ∈ ℝ+𝑥 ≠ 0)
4241adantl 480 . . . . . . 7 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ+) → 𝑥 ≠ 0)
4330nn0zd 11315 . . . . . . . 8 (𝐹 ∈ (Poly‘ℝ) → 𝐷 ∈ ℤ)
4443adantr 479 . . . . . . 7 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ+) → 𝐷 ∈ ℤ)
4528, 42, 44expne0d 12834 . . . . . 6 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ+) → (𝑥𝐷) ≠ 0)
4626, 32, 40, 45fsumdivc 14309 . . . . 5 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ+) → (Σ𝑘 ∈ (0...𝐷)((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷)) = Σ𝑘 ∈ (0...𝐷)(((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷)))
47 fzodisj 12329 . . . . . . . 8 ((0..^𝐷) ∩ (𝐷..^(𝐷 + 1))) = ∅
48 fzosn 12363 . . . . . . . . 9 (𝐷 ∈ ℤ → (𝐷..^(𝐷 + 1)) = {𝐷})
4948ineq2d 3775 . . . . . . . 8 (𝐷 ∈ ℤ → ((0..^𝐷) ∩ (𝐷..^(𝐷 + 1))) = ((0..^𝐷) ∩ {𝐷}))
5047, 49syl5reqr 2658 . . . . . . 7 (𝐷 ∈ ℤ → ((0..^𝐷) ∩ {𝐷}) = ∅)
5144, 50syl 17 . . . . . 6 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ+) → ((0..^𝐷) ∩ {𝐷}) = ∅)
52 fzval3 12362 . . . . . . . . 9 (𝐷 ∈ ℤ → (0...𝐷) = (0..^(𝐷 + 1)))
5343, 52syl 17 . . . . . . . 8 (𝐹 ∈ (Poly‘ℝ) → (0...𝐷) = (0..^(𝐷 + 1)))
54 nn0uz 11557 . . . . . . . . . 10 0 = (ℤ‘0)
5530, 54syl6eleq 2697 . . . . . . . . 9 (𝐹 ∈ (Poly‘ℝ) → 𝐷 ∈ (ℤ‘0))
56 fzosplitsn 12400 . . . . . . . . 9 (𝐷 ∈ (ℤ‘0) → (0..^(𝐷 + 1)) = ((0..^𝐷) ∪ {𝐷}))
5755, 56syl 17 . . . . . . . 8 (𝐹 ∈ (Poly‘ℝ) → (0..^(𝐷 + 1)) = ((0..^𝐷) ∪ {𝐷}))
5853, 57eqtrd 2643 . . . . . . 7 (𝐹 ∈ (Poly‘ℝ) → (0...𝐷) = ((0..^𝐷) ∪ {𝐷}))
5958adantr 479 . . . . . 6 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ+) → (0...𝐷) = ((0..^𝐷) ∪ {𝐷}))
6032adantr 479 . . . . . . 7 (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝐷)) → (𝑥𝐷) ∈ ℂ)
6142adantr 479 . . . . . . . 8 (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝐷)) → 𝑥 ≠ 0)
6244adantr 479 . . . . . . . 8 (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝐷)) → 𝐷 ∈ ℤ)
6338, 61, 62expne0d 12834 . . . . . . 7 (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝐷)) → (𝑥𝐷) ≠ 0)
6440, 60, 63divcld 10653 . . . . . 6 (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝐷)) → (((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷)) ∈ ℂ)
6551, 59, 26, 64fsumsplit 14267 . . . . 5 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ+) → Σ𝑘 ∈ (0...𝐷)(((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷)) = (Σ𝑘 ∈ (0..^𝐷)(((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷)) + Σ𝑘 ∈ {𝐷} (((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷))))
6646, 65eqtrd 2643 . . . 4 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ+) → (Σ𝑘 ∈ (0...𝐷)((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷)) = (Σ𝑘 ∈ (0..^𝐷)(((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷)) + Σ𝑘 ∈ {𝐷} (((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷))))
6766mpteq2dva 4666 . . 3 (𝐹 ∈ (Poly‘ℝ) → (𝑥 ∈ ℝ+ ↦ (Σ𝑘 ∈ (0...𝐷)((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷))) = (𝑥 ∈ ℝ+ ↦ (Σ𝑘 ∈ (0..^𝐷)(((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷)) + Σ𝑘 ∈ {𝐷} (((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷)))))
6825, 67eqtrd 2643 . 2 (𝐹 ∈ (Poly‘ℝ) → (𝐹𝑓 / 𝐺) = (𝑥 ∈ ℝ+ ↦ (Σ𝑘 ∈ (0..^𝐷)(((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷)) + Σ𝑘 ∈ {𝐷} (((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷)))))
69 sumex 14215 . . . . 5 Σ𝑘 ∈ (0..^𝐷)(((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷)) ∈ V
7069a1i 11 . . . 4 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ+) → Σ𝑘 ∈ (0..^𝐷)(((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷)) ∈ V)
71 sumex 14215 . . . . 5 Σ𝑘 ∈ {𝐷} (((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷)) ∈ V
7271a1i 11 . . . 4 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ+) → Σ𝑘 ∈ {𝐷} (((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷)) ∈ V)
7312a1i 11 . . . . . 6 (𝐹 ∈ (Poly‘ℝ) → ℝ+ ⊆ ℝ)
74 fzofi 12593 . . . . . . 7 (0..^𝐷) ∈ Fin
7574a1i 11 . . . . . 6 (𝐹 ∈ (Poly‘ℝ) → (0..^𝐷) ∈ Fin)
76 ovex 6555 . . . . . . 7 (((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷)) ∈ V
7776a1i 11 . . . . . 6 ((𝐹 ∈ (Poly‘ℝ) ∧ (𝑥 ∈ ℝ+𝑘 ∈ (0..^𝐷))) → (((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷)) ∈ V)
7833ad2antrr 757 . . . . . . . . . 10 (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → 𝐶:ℕ0⟶ℂ)
79 elfzonn0 12338 . . . . . . . . . . 11 (𝑘 ∈ (0..^𝐷) → 𝑘 ∈ ℕ0)
8079ad2antlr 758 . . . . . . . . . 10 (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → 𝑘 ∈ ℕ0)
8178, 80ffvelrnd 6253 . . . . . . . . 9 (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (𝐶𝑘) ∈ ℂ)
8228adantlr 746 . . . . . . . . . 10 (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
8382, 80expcld 12828 . . . . . . . . 9 (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (𝑥𝑘) ∈ ℂ)
8432adantlr 746 . . . . . . . . 9 (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (𝑥𝐷) ∈ ℂ)
8541adantl 480 . . . . . . . . . 10 (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → 𝑥 ≠ 0)
8644adantlr 746 . . . . . . . . . 10 (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → 𝐷 ∈ ℤ)
8782, 85, 86expne0d 12834 . . . . . . . . 9 (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (𝑥𝐷) ≠ 0)
8881, 83, 84, 87divassd 10688 . . . . . . . 8 (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷)) = ((𝐶𝑘) · ((𝑥𝑘) / (𝑥𝐷))))
8988mpteq2dva 4666 . . . . . . 7 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) → (𝑥 ∈ ℝ+ ↦ (((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷))) = (𝑥 ∈ ℝ+ ↦ ((𝐶𝑘) · ((𝑥𝑘) / (𝑥𝐷)))))
90 fvex 6098 . . . . . . . . . 10 (𝐶𝑘) ∈ V
9190a1i 11 . . . . . . . . 9 (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (𝐶𝑘) ∈ V)
92 ovex 6555 . . . . . . . . . 10 ((𝑥𝑘) / (𝑥𝐷)) ∈ V
9392a1i 11 . . . . . . . . 9 (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → ((𝑥𝑘) / (𝑥𝐷)) ∈ V)
9433adantr 479 . . . . . . . . . . 11 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) → 𝐶:ℕ0⟶ℂ)
9579adantl 480 . . . . . . . . . . 11 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) → 𝑘 ∈ ℕ0)
9694, 95ffvelrnd 6253 . . . . . . . . . 10 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) → (𝐶𝑘) ∈ ℂ)
97 rlimconst 14072 . . . . . . . . . 10 ((ℝ+ ⊆ ℝ ∧ (𝐶𝑘) ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ (𝐶𝑘)) ⇝𝑟 (𝐶𝑘))
9812, 96, 97sylancr 693 . . . . . . . . 9 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) → (𝑥 ∈ ℝ+ ↦ (𝐶𝑘)) ⇝𝑟 (𝐶𝑘))
9980nn0zd 11315 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → 𝑘 ∈ ℤ)
10086, 99zsubcld 11322 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (𝐷𝑘) ∈ ℤ)
10182, 85, 100cxpexpzd 24202 . . . . . . . . . . . . . 14 (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (𝑥𝑐(𝐷𝑘)) = (𝑥↑(𝐷𝑘)))
102101oveq2d 6543 . . . . . . . . . . . . 13 (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (1 / (𝑥𝑐(𝐷𝑘))) = (1 / (𝑥↑(𝐷𝑘))))
10382, 85, 100expnegd 12835 . . . . . . . . . . . . 13 (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (𝑥↑-(𝐷𝑘)) = (1 / (𝑥↑(𝐷𝑘))))
10486zcnd 11318 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → 𝐷 ∈ ℂ)
10580nn0cnd 11203 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → 𝑘 ∈ ℂ)
106104, 105negsubdi2d 10260 . . . . . . . . . . . . . 14 (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → -(𝐷𝑘) = (𝑘𝐷))
107106oveq2d 6543 . . . . . . . . . . . . 13 (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (𝑥↑-(𝐷𝑘)) = (𝑥↑(𝑘𝐷)))
108102, 103, 1073eqtr2d 2649 . . . . . . . . . . . 12 (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (1 / (𝑥𝑐(𝐷𝑘))) = (𝑥↑(𝑘𝐷)))
10982, 85, 86, 99expsubd 12839 . . . . . . . . . . . 12 (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (𝑥↑(𝑘𝐷)) = ((𝑥𝑘) / (𝑥𝐷)))
110108, 109eqtrd 2643 . . . . . . . . . . 11 (((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) ∧ 𝑥 ∈ ℝ+) → (1 / (𝑥𝑐(𝐷𝑘))) = ((𝑥𝑘) / (𝑥𝐷)))
111110mpteq2dva 4666 . . . . . . . . . 10 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) → (𝑥 ∈ ℝ+ ↦ (1 / (𝑥𝑐(𝐷𝑘)))) = (𝑥 ∈ ℝ+ ↦ ((𝑥𝑘) / (𝑥𝐷))))
11295nn0red 11202 . . . . . . . . . . . 12 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) → 𝑘 ∈ ℝ)
11330adantr 479 . . . . . . . . . . . . 13 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) → 𝐷 ∈ ℕ0)
114113nn0red 11202 . . . . . . . . . . . 12 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) → 𝐷 ∈ ℝ)
115 elfzolt2 12306 . . . . . . . . . . . . 13 (𝑘 ∈ (0..^𝐷) → 𝑘 < 𝐷)
116115adantl 480 . . . . . . . . . . . 12 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) → 𝑘 < 𝐷)
117 difrp 11703 . . . . . . . . . . . . 13 ((𝑘 ∈ ℝ ∧ 𝐷 ∈ ℝ) → (𝑘 < 𝐷 ↔ (𝐷𝑘) ∈ ℝ+))
118117biimpa 499 . . . . . . . . . . . 12 (((𝑘 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ 𝑘 < 𝐷) → (𝐷𝑘) ∈ ℝ+)
119112, 114, 116, 118syl21anc 1316 . . . . . . . . . . 11 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) → (𝐷𝑘) ∈ ℝ+)
120 cxplim 24443 . . . . . . . . . . 11 ((𝐷𝑘) ∈ ℝ+ → (𝑥 ∈ ℝ+ ↦ (1 / (𝑥𝑐(𝐷𝑘)))) ⇝𝑟 0)
121119, 120syl 17 . . . . . . . . . 10 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) → (𝑥 ∈ ℝ+ ↦ (1 / (𝑥𝑐(𝐷𝑘)))) ⇝𝑟 0)
122111, 121eqbrtrrd 4601 . . . . . . . . 9 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) → (𝑥 ∈ ℝ+ ↦ ((𝑥𝑘) / (𝑥𝐷))) ⇝𝑟 0)
12391, 93, 98, 122rlimmul 14172 . . . . . . . 8 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) → (𝑥 ∈ ℝ+ ↦ ((𝐶𝑘) · ((𝑥𝑘) / (𝑥𝐷)))) ⇝𝑟 ((𝐶𝑘) · 0))
12496mul01d 10087 . . . . . . . 8 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) → ((𝐶𝑘) · 0) = 0)
125123, 124breqtrd 4603 . . . . . . 7 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) → (𝑥 ∈ ℝ+ ↦ ((𝐶𝑘) · ((𝑥𝑘) / (𝑥𝐷)))) ⇝𝑟 0)
12689, 125eqbrtrd 4599 . . . . . 6 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑘 ∈ (0..^𝐷)) → (𝑥 ∈ ℝ+ ↦ (((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷))) ⇝𝑟 0)
12773, 75, 77, 126fsumrlim 14333 . . . . 5 (𝐹 ∈ (Poly‘ℝ) → (𝑥 ∈ ℝ+ ↦ Σ𝑘 ∈ (0..^𝐷)(((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷))) ⇝𝑟 Σ𝑘 ∈ (0..^𝐷)0)
12875olcd 406 . . . . . 6 (𝐹 ∈ (Poly‘ℝ) → ((0..^𝐷) ⊆ (ℤ‘0) ∨ (0..^𝐷) ∈ Fin))
129 sumz 14249 . . . . . 6 (((0..^𝐷) ⊆ (ℤ‘0) ∨ (0..^𝐷) ∈ Fin) → Σ𝑘 ∈ (0..^𝐷)0 = 0)
130128, 129syl 17 . . . . 5 (𝐹 ∈ (Poly‘ℝ) → Σ𝑘 ∈ (0..^𝐷)0 = 0)
131127, 130breqtrd 4603 . . . 4 (𝐹 ∈ (Poly‘ℝ) → (𝑥 ∈ ℝ+ ↦ Σ𝑘 ∈ (0..^𝐷)(((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷))) ⇝𝑟 0)
13233, 30ffvelrnd 6253 . . . . . . . . . . 11 (𝐹 ∈ (Poly‘ℝ) → (𝐶𝐷) ∈ ℂ)
133132adantr 479 . . . . . . . . . 10 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ+) → (𝐶𝐷) ∈ ℂ)
134133, 32mulcld 9917 . . . . . . . . 9 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ+) → ((𝐶𝐷) · (𝑥𝐷)) ∈ ℂ)
135134, 32, 45divcld 10653 . . . . . . . 8 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ+) → (((𝐶𝐷) · (𝑥𝐷)) / (𝑥𝐷)) ∈ ℂ)
136 fveq2 6088 . . . . . . . . . . 11 (𝑘 = 𝐷 → (𝐶𝑘) = (𝐶𝐷))
137 oveq2 6535 . . . . . . . . . . 11 (𝑘 = 𝐷 → (𝑥𝑘) = (𝑥𝐷))
138136, 137oveq12d 6545 . . . . . . . . . 10 (𝑘 = 𝐷 → ((𝐶𝑘) · (𝑥𝑘)) = ((𝐶𝐷) · (𝑥𝐷)))
139138oveq1d 6542 . . . . . . . . 9 (𝑘 = 𝐷 → (((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷)) = (((𝐶𝐷) · (𝑥𝐷)) / (𝑥𝐷)))
140139sumsn 14268 . . . . . . . 8 ((𝐷 ∈ ℕ0 ∧ (((𝐶𝐷) · (𝑥𝐷)) / (𝑥𝐷)) ∈ ℂ) → Σ𝑘 ∈ {𝐷} (((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷)) = (((𝐶𝐷) · (𝑥𝐷)) / (𝑥𝐷)))
14131, 135, 140syl2anc 690 . . . . . . 7 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ+) → Σ𝑘 ∈ {𝐷} (((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷)) = (((𝐶𝐷) · (𝑥𝐷)) / (𝑥𝐷)))
142133, 32, 45divcan4d 10659 . . . . . . 7 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ+) → (((𝐶𝐷) · (𝑥𝐷)) / (𝑥𝐷)) = (𝐶𝐷))
143141, 142eqtrd 2643 . . . . . 6 ((𝐹 ∈ (Poly‘ℝ) ∧ 𝑥 ∈ ℝ+) → Σ𝑘 ∈ {𝐷} (((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷)) = (𝐶𝐷))
144143mpteq2dva 4666 . . . . 5 (𝐹 ∈ (Poly‘ℝ) → (𝑥 ∈ ℝ+ ↦ Σ𝑘 ∈ {𝐷} (((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷))) = (𝑥 ∈ ℝ+ ↦ (𝐶𝐷)))
145 rlimconst 14072 . . . . . 6 ((ℝ+ ⊆ ℝ ∧ (𝐶𝐷) ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ (𝐶𝐷)) ⇝𝑟 (𝐶𝐷))
14612, 132, 145sylancr 693 . . . . 5 (𝐹 ∈ (Poly‘ℝ) → (𝑥 ∈ ℝ+ ↦ (𝐶𝐷)) ⇝𝑟 (𝐶𝐷))
147144, 146eqbrtrd 4599 . . . 4 (𝐹 ∈ (Poly‘ℝ) → (𝑥 ∈ ℝ+ ↦ Σ𝑘 ∈ {𝐷} (((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷))) ⇝𝑟 (𝐶𝐷))
14870, 72, 131, 147rlimadd 14170 . . 3 (𝐹 ∈ (Poly‘ℝ) → (𝑥 ∈ ℝ+ ↦ (Σ𝑘 ∈ (0..^𝐷)(((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷)) + Σ𝑘 ∈ {𝐷} (((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷)))) ⇝𝑟 (0 + (𝐶𝐷)))
149132addid2d 10089 . . . 4 (𝐹 ∈ (Poly‘ℝ) → (0 + (𝐶𝐷)) = (𝐶𝐷))
150 signsply0.b . . . 4 𝐵 = (𝐶𝐷)
151149, 150syl6eqr 2661 . . 3 (𝐹 ∈ (Poly‘ℝ) → (0 + (𝐶𝐷)) = 𝐵)
152148, 151breqtrd 4603 . 2 (𝐹 ∈ (Poly‘ℝ) → (𝑥 ∈ ℝ+ ↦ (Σ𝑘 ∈ (0..^𝐷)(((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷)) + Σ𝑘 ∈ {𝐷} (((𝐶𝑘) · (𝑥𝑘)) / (𝑥𝐷)))) ⇝𝑟 𝐵)
15368, 152eqbrtrd 4599 1 (𝐹 ∈ (Poly‘ℝ) → (𝐹𝑓 / 𝐺) ⇝𝑟 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 381  wa 382   = wceq 1474  wcel 1976  wne 2779  wral 2895  Vcvv 3172  cun 3537  cin 3538  wss 3539  c0 3873  {csn 4124   class class class wbr 4577  cmpt 4637   Fn wfn 5785  wf 5786  cfv 5790  (class class class)co 6527  𝑓 cof 6771  Fincfn 7819  cc 9791  cr 9792  0cc0 9793  1c1 9794   + caddc 9796   · cmul 9798   < clt 9931  cmin 10118  -cneg 10119   / cdiv 10536  0cn0 11142  cz 11213  cuz 11522  +crp 11667  ...cfz 12155  ..^cfzo 12292  cexp 12680  𝑟 crli 14013  Σcsu 14213  Polycply 23689  coeffccoe 23691  degcdgr 23692  𝑐ccxp 24051
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-inf2 8399  ax-cnex 9849  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-mulcom 9857  ax-addass 9858  ax-mulass 9859  ax-distr 9860  ax-i2m1 9861  ax-1ne0 9862  ax-1rid 9863  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866  ax-pre-lttri 9867  ax-pre-lttrn 9868  ax-pre-ltadd 9869  ax-pre-mulgt0 9870  ax-pre-sup 9871  ax-addf 9872  ax-mulf 9873
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-iin 4452  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-se 4988  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-isom 5799  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-of 6773  df-om 6936  df-1st 7037  df-2nd 7038  df-supp 7161  df-wrecs 7272  df-recs 7333  df-rdg 7371  df-1o 7425  df-2o 7426  df-oadd 7429  df-er 7607  df-map 7724  df-pm 7725  df-ixp 7773  df-en 7820  df-dom 7821  df-sdom 7822  df-fin 7823  df-fsupp 8137  df-fi 8178  df-sup 8209  df-inf 8210  df-oi 8276  df-card 8626  df-cda 8851  df-pnf 9933  df-mnf 9934  df-xr 9935  df-ltxr 9936  df-le 9937  df-sub 10120  df-neg 10121  df-div 10537  df-nn 10871  df-2 10929  df-3 10930  df-4 10931  df-5 10932  df-6 10933  df-7 10934  df-8 10935  df-9 10936  df-n0 11143  df-z 11214  df-dec 11329  df-uz 11523  df-q 11624  df-rp 11668  df-xneg 11781  df-xadd 11782  df-xmul 11783  df-ioo 12009  df-ioc 12010  df-ico 12011  df-icc 12012  df-fz 12156  df-fzo 12293  df-fl 12413  df-mod 12489  df-seq 12622  df-exp 12681  df-fac 12881  df-bc 12910  df-hash 12938  df-shft 13604  df-cj 13636  df-re 13637  df-im 13638  df-sqrt 13772  df-abs 13773  df-limsup 13999  df-clim 14016  df-rlim 14017  df-sum 14214  df-ef 14586  df-sin 14588  df-cos 14589  df-pi 14591  df-struct 15646  df-ndx 15647  df-slot 15648  df-base 15649  df-sets 15650  df-ress 15651  df-plusg 15730  df-mulr 15731  df-starv 15732  df-sca 15733  df-vsca 15734  df-ip 15735  df-tset 15736  df-ple 15737  df-ds 15740  df-unif 15741  df-hom 15742  df-cco 15743  df-rest 15855  df-topn 15856  df-0g 15874  df-gsum 15875  df-topgen 15876  df-pt 15877  df-prds 15880  df-xrs 15934  df-qtop 15939  df-imas 15940  df-xps 15942  df-mre 16018  df-mrc 16019  df-acs 16021  df-mgm 17014  df-sgrp 17056  df-mnd 17067  df-submnd 17108  df-mulg 17313  df-cntz 17522  df-cmn 17967  df-psmet 19508  df-xmet 19509  df-met 19510  df-bl 19511  df-mopn 19512  df-fbas 19513  df-fg 19514  df-cnfld 19517  df-top 20469  df-bases 20470  df-topon 20471  df-topsp 20472  df-cld 20581  df-ntr 20582  df-cls 20583  df-nei 20660  df-lp 20698  df-perf 20699  df-cn 20789  df-cnp 20790  df-haus 20877  df-tx 21123  df-hmeo 21316  df-fil 21408  df-fm 21500  df-flim 21501  df-flf 21502  df-xms 21883  df-ms 21884  df-tms 21885  df-cncf 22437  df-0p 23188  df-limc 23381  df-dv 23382  df-ply 23693  df-coe 23695  df-dgr 23696  df-log 24052  df-cxp 24053
This theorem is referenced by:  signsply0  29788
  Copyright terms: Public domain W3C validator