Metamath Proof Explorer

Theorem signsplypnf

Description: The quotient of a polynomial F by a monic monomial of same degree G converges to the highest coefficient of F . (Contributed by Thierry Arnoux, 18-Sep-2018)

Ref Expression
Hypotheses signsply0.d ⊢ 𝐷 = ( deg ‘ 𝐹 )
signsply0.c ⊢ 𝐶 = ( coeff ‘ 𝐹 )
signsply0.b ⊢ 𝐵 = ( 𝐶 ‘ 𝐷 )
signsplypnf.g ⊢ 𝐺 = ( 𝑥 ∈ ℝ+ ↦ ( 𝑥 ↑ 𝐷 ) )
Assertion signsplypnf ( 𝐹 ∈ ( Poly ‘ ℝ ) → ( 𝐹 ∘f / 𝐺 ) ⇝𝑟 𝐵 )

Proof

Step Hyp Ref Expression
1 signsply0.d ⊢ 𝐷 = ( deg ‘ 𝐹 )
2 signsply0.c ⊢ 𝐶 = ( coeff ‘ 𝐹 )
3 signsply0.b ⊢ 𝐵 = ( 𝐶 ‘ 𝐷 )
4 signsplypnf.g ⊢ 𝐺 = ( 𝑥 ∈ ℝ+ ↦ ( 𝑥 ↑ 𝐷 ) )
5 plyf ⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → 𝐹 : ℂ ⟶ ℂ )
6 5 ffnd ⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → 𝐹 Fn ℂ )
7 ovex ⊢ ( 𝑥 ↑ 𝐷 ) ∈ V
8 7 rgenw ⊢ ∀ 𝑥 ∈ ℝ+ ( 𝑥 ↑ 𝐷 ) ∈ V
9 4 fnmpt ⊢ ( ∀ 𝑥 ∈ ℝ+ ( 𝑥 ↑ 𝐷 ) ∈ V → 𝐺 Fn ℝ+ )
10 8 9 mp1i ⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → 𝐺 Fn ℝ+ )
11 cnex ⊢ ℂ ∈ V
12 11 a1i ⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ℂ ∈ V )
13 reex ⊢ ℝ ∈ V
14 rpssre ⊢ ℝ+ ⊆ ℝ
15 13 14 ssexi ⊢ ℝ+ ∈ V
16 15 a1i ⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ℝ+ ∈ V )
17 ax-resscn ⊢ ℝ ⊆ ℂ
18 14 17 sstri ⊢ ℝ+ ⊆ ℂ
19 sseqin2 ⊢ ( ℝ+ ⊆ ℂ ↔ ( ℂ ∩ ℝ+ ) = ℝ+ )
20 18 19 mpbi ⊢ ( ℂ ∩ ℝ+ ) = ℝ+
21 2 1 coeid2 ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑥 ∈ ℂ ) → ( 𝐹 ‘ 𝑥 ) = Σ 𝑘 ∈ ( 0 ... 𝐷 ) ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) )
22 4 fvmpt2 ⊢ ( ( 𝑥 ∈ ℝ+ ∧ ( 𝑥 ↑ 𝐷 ) ∈ V ) → ( 𝐺 ‘ 𝑥 ) = ( 𝑥 ↑ 𝐷 ) )
23 7 22 mpan2 ⊢ ( 𝑥 ∈ ℝ+ → ( 𝐺 ‘ 𝑥 ) = ( 𝑥 ↑ 𝐷 ) )
24 23 adantl ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐺 ‘ 𝑥 ) = ( 𝑥 ↑ 𝐷 ) )
25 6 10 12 16 20 21 24 offval ⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ( 𝐹 ∘f / 𝐺 ) = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑘 ∈ ( 0 ... 𝐷 ) ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) / ( 𝑥 ↑ 𝐷 ) ) ) )
26 fzfid ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → ( 0 ... 𝐷 ) ∈ Fin )
27 18 a1i ⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ℝ+ ⊆ ℂ )
28 27 sselda ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℂ )
29 dgrcl ⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
30 1 29 eqeltrid ⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → 𝐷 ∈ ℕ0 )
31 30 adantr ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → 𝐷 ∈ ℕ0 )
32 28 31 expcld ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ↑ 𝐷 ) ∈ ℂ )
33 2 coef3 ⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → 𝐶 : ℕ0 ⟶ ℂ )
34 33 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 0 ... 𝐷 ) ) → 𝐶 : ℕ0 ⟶ ℂ )
35 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝐷 ) → 𝑘 ∈ ℕ0 )
36 35 adantl ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 0 ... 𝐷 ) ) → 𝑘 ∈ ℕ0 )
37 34 36 ffvelrnd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 0 ... 𝐷 ) ) → ( 𝐶 ‘ 𝑘 ) ∈ ℂ )
38 28 adantr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 0 ... 𝐷 ) ) → 𝑥 ∈ ℂ )
39 38 36 expcld ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 0 ... 𝐷 ) ) → ( 𝑥 ↑ 𝑘 ) ∈ ℂ )
40 37 39 mulcld ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 0 ... 𝐷 ) ) → ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ∈ ℂ )
41 rpne0 ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ≠ 0 )
42 41 adantl ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ≠ 0 )
43 30 nn0zd ⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → 𝐷 ∈ ℤ )
44 43 adantr ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → 𝐷 ∈ ℤ )
45 28 42 44 expne0d ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ↑ 𝐷 ) ≠ 0 )
46 26 32 40 45 fsumdivc ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑘 ∈ ( 0 ... 𝐷 ) ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) / ( 𝑥 ↑ 𝐷 ) ) = Σ 𝑘 ∈ ( 0 ... 𝐷 ) ( ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) / ( 𝑥 ↑ 𝐷 ) ) )
47 fzosn ⊢ ( 𝐷 ∈ ℤ → ( 𝐷 ..^ ( 𝐷 + 1 ) ) = { 𝐷 } )
48 47 ineq2d ⊢ ( 𝐷 ∈ ℤ → ( ( 0 ..^ 𝐷 ) ∩ ( 𝐷 ..^ ( 𝐷 + 1 ) ) ) = ( ( 0 ..^ 𝐷 ) ∩ { 𝐷 } ) )
49 fzodisj ⊢ ( ( 0 ..^ 𝐷 ) ∩ ( 𝐷 ..^ ( 𝐷 + 1 ) ) ) = ∅
50 48 49 eqtr3di ⊢ ( 𝐷 ∈ ℤ → ( ( 0 ..^ 𝐷 ) ∩ { 𝐷 } ) = ∅ )
51 44 50 syl ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → ( ( 0 ..^ 𝐷 ) ∩ { 𝐷 } ) = ∅ )
52 fzval3 ⊢ ( 𝐷 ∈ ℤ → ( 0 ... 𝐷 ) = ( 0 ..^ ( 𝐷 + 1 ) ) )
53 43 52 syl ⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ( 0 ... 𝐷 ) = ( 0 ..^ ( 𝐷 + 1 ) ) )
54 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
55 30 54 eleqtrdi ⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → 𝐷 ∈ ( ℤ≥ ‘ 0 ) )
56 fzosplitsn ⊢ ( 𝐷 ∈ ( ℤ≥ ‘ 0 ) → ( 0 ..^ ( 𝐷 + 1 ) ) = ( ( 0 ..^ 𝐷 ) ∪ { 𝐷 } ) )
57 55 56 syl ⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ( 0 ..^ ( 𝐷 + 1 ) ) = ( ( 0 ..^ 𝐷 ) ∪ { 𝐷 } ) )
58 53 57 eqtrd ⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ( 0 ... 𝐷 ) = ( ( 0 ..^ 𝐷 ) ∪ { 𝐷 } ) )
59 58 adantr ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → ( 0 ... 𝐷 ) = ( ( 0 ..^ 𝐷 ) ∪ { 𝐷 } ) )
60 32 adantr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 0 ... 𝐷 ) ) → ( 𝑥 ↑ 𝐷 ) ∈ ℂ )
61 42 adantr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 0 ... 𝐷 ) ) → 𝑥 ≠ 0 )
62 44 adantr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 0 ... 𝐷 ) ) → 𝐷 ∈ ℤ )
63 38 61 62 expne0d ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 0 ... 𝐷 ) ) → ( 𝑥 ↑ 𝐷 ) ≠ 0 )
64 40 60 63 divcld ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 0 ... 𝐷 ) ) → ( ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) / ( 𝑥 ↑ 𝐷 ) ) ∈ ℂ )
65 51 59 26 64 fsumsplit ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑘 ∈ ( 0 ... 𝐷 ) ( ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) / ( 𝑥 ↑ 𝐷 ) ) = ( Σ 𝑘 ∈ ( 0 ..^ 𝐷 ) ( ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) / ( 𝑥 ↑ 𝐷 ) ) + Σ 𝑘 ∈ { 𝐷 } ( ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) / ( 𝑥 ↑ 𝐷 ) ) ) )
66 46 65 eqtrd ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑘 ∈ ( 0 ... 𝐷 ) ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) / ( 𝑥 ↑ 𝐷 ) ) = ( Σ 𝑘 ∈ ( 0 ..^ 𝐷 ) ( ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) / ( 𝑥 ↑ 𝐷 ) ) + Σ 𝑘 ∈ { 𝐷 } ( ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) / ( 𝑥 ↑ 𝐷 ) ) ) )
67 66 mpteq2dva ⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑘 ∈ ( 0 ... 𝐷 ) ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) / ( 𝑥 ↑ 𝐷 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑘 ∈ ( 0 ..^ 𝐷 ) ( ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) / ( 𝑥 ↑ 𝐷 ) ) + Σ 𝑘 ∈ { 𝐷 } ( ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) / ( 𝑥 ↑ 𝐷 ) ) ) ) )
68 25 67 eqtrd ⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ( 𝐹 ∘f / 𝐺 ) = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑘 ∈ ( 0 ..^ 𝐷 ) ( ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) / ( 𝑥 ↑ 𝐷 ) ) + Σ 𝑘 ∈ { 𝐷 } ( ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) / ( 𝑥 ↑ 𝐷 ) ) ) ) )
69 sumex ⊢ Σ 𝑘 ∈ ( 0 ..^ 𝐷 ) ( ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) / ( 𝑥 ↑ 𝐷 ) ) ∈ V
70 69 a1i ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑘 ∈ ( 0 ..^ 𝐷 ) ( ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) / ( 𝑥 ↑ 𝐷 ) ) ∈ V )
71 sumex ⊢ Σ 𝑘 ∈ { 𝐷 } ( ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) / ( 𝑥 ↑ 𝐷 ) ) ∈ V
72 71 a1i ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑘 ∈ { 𝐷 } ( ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) / ( 𝑥 ↑ 𝐷 ) ) ∈ V )
73 14 a1i ⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ℝ+ ⊆ ℝ )
74 fzofi ⊢ ( 0 ..^ 𝐷 ) ∈ Fin
75 74 a1i ⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ( 0 ..^ 𝐷 ) ∈ Fin )
76 ovexd ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) ) → ( ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) / ( 𝑥 ↑ 𝐷 ) ) ∈ V )
77 33 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝐶 : ℕ0 ⟶ ℂ )
78 elfzonn0 ⊢ ( 𝑘 ∈ ( 0 ..^ 𝐷 ) → 𝑘 ∈ ℕ0 )
79 78 ad2antlr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝑘 ∈ ℕ0 )
80 77 79 ffvelrnd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐶 ‘ 𝑘 ) ∈ ℂ )
81 28 adantlr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℂ )
82 81 79 expcld ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ↑ 𝑘 ) ∈ ℂ )
83 32 adantlr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ↑ 𝐷 ) ∈ ℂ )
84 41 adantl ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ≠ 0 )
85 44 adantlr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝐷 ∈ ℤ )
86 81 84 85 expne0d ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ↑ 𝐷 ) ≠ 0 )
87 80 82 83 86 divassd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) / ( 𝑥 ↑ 𝐷 ) ) = ( ( 𝐶 ‘ 𝑘 ) · ( ( 𝑥 ↑ 𝑘 ) / ( 𝑥 ↑ 𝐷 ) ) ) )
88 87 mpteq2dva ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) → ( 𝑥 ∈ ℝ+ ↦ ( ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) / ( 𝑥 ↑ 𝐷 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( 𝐶 ‘ 𝑘 ) · ( ( 𝑥 ↑ 𝑘 ) / ( 𝑥 ↑ 𝐷 ) ) ) ) )
89 fvexd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐶 ‘ 𝑘 ) ∈ V )
90 ovexd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝑥 ↑ 𝑘 ) / ( 𝑥 ↑ 𝐷 ) ) ∈ V )
91 33 adantr ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) → 𝐶 : ℕ0 ⟶ ℂ )
92 78 adantl ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) → 𝑘 ∈ ℕ0 )
93 91 92 ffvelrnd ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) → ( 𝐶 ‘ 𝑘 ) ∈ ℂ )
94 rlimconst ⊢ ( ( ℝ+ ⊆ ℝ ∧ ( 𝐶 ‘ 𝑘 ) ∈ ℂ ) → ( 𝑥 ∈ ℝ+ ↦ ( 𝐶 ‘ 𝑘 ) ) ⇝𝑟 ( 𝐶 ‘ 𝑘 ) )
95 14 93 94 sylancr ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) → ( 𝑥 ∈ ℝ+ ↦ ( 𝐶 ‘ 𝑘 ) ) ⇝𝑟 ( 𝐶 ‘ 𝑘 ) )
96 79 nn0zd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝑘 ∈ ℤ )
97 85 96 zsubcld ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐷 − 𝑘 ) ∈ ℤ )
98 81 84 97 cxpexpzd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ↑𝑐 ( 𝐷 − 𝑘 ) ) = ( 𝑥 ↑ ( 𝐷 − 𝑘 ) ) )
99 98 oveq2d ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 1 / ( 𝑥 ↑𝑐 ( 𝐷 − 𝑘 ) ) ) = ( 1 / ( 𝑥 ↑ ( 𝐷 − 𝑘 ) ) ) )
100 81 84 97 expnegd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ↑ - ( 𝐷 − 𝑘 ) ) = ( 1 / ( 𝑥 ↑ ( 𝐷 − 𝑘 ) ) ) )
101 85 zcnd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝐷 ∈ ℂ )
102 79 nn0cnd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝑘 ∈ ℂ )
103 101 102 negsubdi2d ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) → - ( 𝐷 − 𝑘 ) = ( 𝑘 − 𝐷 ) )
104 103 oveq2d ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ↑ - ( 𝐷 − 𝑘 ) ) = ( 𝑥 ↑ ( 𝑘 − 𝐷 ) ) )
105 99 100 104 3eqtr2d ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 1 / ( 𝑥 ↑𝑐 ( 𝐷 − 𝑘 ) ) ) = ( 𝑥 ↑ ( 𝑘 − 𝐷 ) ) )
106 81 84 85 96 expsubd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ↑ ( 𝑘 − 𝐷 ) ) = ( ( 𝑥 ↑ 𝑘 ) / ( 𝑥 ↑ 𝐷 ) ) )
107 105 106 eqtrd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 1 / ( 𝑥 ↑𝑐 ( 𝐷 − 𝑘 ) ) ) = ( ( 𝑥 ↑ 𝑘 ) / ( 𝑥 ↑ 𝐷 ) ) )
108 107 mpteq2dva ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) → ( 𝑥 ∈ ℝ+ ↦ ( 1 / ( 𝑥 ↑𝑐 ( 𝐷 − 𝑘 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( 𝑥 ↑ 𝑘 ) / ( 𝑥 ↑ 𝐷 ) ) ) )
109 92 nn0red ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) → 𝑘 ∈ ℝ )
110 30 adantr ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) → 𝐷 ∈ ℕ0 )
111 110 nn0red ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) → 𝐷 ∈ ℝ )
112 elfzolt2 ⊢ ( 𝑘 ∈ ( 0 ..^ 𝐷 ) → 𝑘 < 𝐷 )
113 112 adantl ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) → 𝑘 < 𝐷 )
114 difrp ⊢ ( ( 𝑘 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( 𝑘 < 𝐷 ↔ ( 𝐷 − 𝑘 ) ∈ ℝ+ ) )
115 114 biimpa ⊢ ( ( ( 𝑘 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ∧ 𝑘 < 𝐷 ) → ( 𝐷 − 𝑘 ) ∈ ℝ+ )
116 109 111 113 115 syl21anc ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) → ( 𝐷 − 𝑘 ) ∈ ℝ+ )
117 cxplim ⊢ ( ( 𝐷 − 𝑘 ) ∈ ℝ+ → ( 𝑥 ∈ ℝ+ ↦ ( 1 / ( 𝑥 ↑𝑐 ( 𝐷 − 𝑘 ) ) ) ) ⇝𝑟 0 )
118 116 117 syl ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) → ( 𝑥 ∈ ℝ+ ↦ ( 1 / ( 𝑥 ↑𝑐 ( 𝐷 − 𝑘 ) ) ) ) ⇝𝑟 0 )
119 108 118 eqbrtrrd ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) → ( 𝑥 ∈ ℝ+ ↦ ( ( 𝑥 ↑ 𝑘 ) / ( 𝑥 ↑ 𝐷 ) ) ) ⇝𝑟 0 )
120 89 90 95 119 rlimmul ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) → ( 𝑥 ∈ ℝ+ ↦ ( ( 𝐶 ‘ 𝑘 ) · ( ( 𝑥 ↑ 𝑘 ) / ( 𝑥 ↑ 𝐷 ) ) ) ) ⇝𝑟 ( ( 𝐶 ‘ 𝑘 ) · 0 ) )
121 93 mul01d ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) → ( ( 𝐶 ‘ 𝑘 ) · 0 ) = 0 )
122 120 121 breqtrd ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) → ( 𝑥 ∈ ℝ+ ↦ ( ( 𝐶 ‘ 𝑘 ) · ( ( 𝑥 ↑ 𝑘 ) / ( 𝑥 ↑ 𝐷 ) ) ) ) ⇝𝑟 0 )
123 88 122 eqbrtrd ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑘 ∈ ( 0 ..^ 𝐷 ) ) → ( 𝑥 ∈ ℝ+ ↦ ( ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) / ( 𝑥 ↑ 𝐷 ) ) ) ⇝𝑟 0 )
124 73 75 76 123 fsumrlim ⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑘 ∈ ( 0 ..^ 𝐷 ) ( ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) / ( 𝑥 ↑ 𝐷 ) ) ) ⇝𝑟 Σ 𝑘 ∈ ( 0 ..^ 𝐷 ) 0 )
125 75 olcd ⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ( ( 0 ..^ 𝐷 ) ⊆ ( ℤ≥ ‘ 0 ) ∨ ( 0 ..^ 𝐷 ) ∈ Fin ) )
126 sumz ⊢ ( ( ( 0 ..^ 𝐷 ) ⊆ ( ℤ≥ ‘ 0 ) ∨ ( 0 ..^ 𝐷 ) ∈ Fin ) → Σ 𝑘 ∈ ( 0 ..^ 𝐷 ) 0 = 0 )
127 125 126 syl ⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → Σ 𝑘 ∈ ( 0 ..^ 𝐷 ) 0 = 0 )
128 124 127 breqtrd ⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑘 ∈ ( 0 ..^ 𝐷 ) ( ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) / ( 𝑥 ↑ 𝐷 ) ) ) ⇝𝑟 0 )
129 33 30 ffvelrnd ⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ( 𝐶 ‘ 𝐷 ) ∈ ℂ )
130 129 adantr ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐶 ‘ 𝐷 ) ∈ ℂ )
131 130 32 mulcld ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝐶 ‘ 𝐷 ) · ( 𝑥 ↑ 𝐷 ) ) ∈ ℂ )
132 131 32 45 divcld ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → ( ( ( 𝐶 ‘ 𝐷 ) · ( 𝑥 ↑ 𝐷 ) ) / ( 𝑥 ↑ 𝐷 ) ) ∈ ℂ )
133 fveq2 ⊢ ( 𝑘 = 𝐷 → ( 𝐶 ‘ 𝑘 ) = ( 𝐶 ‘ 𝐷 ) )
134 oveq2 ⊢ ( 𝑘 = 𝐷 → ( 𝑥 ↑ 𝑘 ) = ( 𝑥 ↑ 𝐷 ) )
135 133 134 oveq12d ⊢ ( 𝑘 = 𝐷 → ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) = ( ( 𝐶 ‘ 𝐷 ) · ( 𝑥 ↑ 𝐷 ) ) )
136 135 oveq1d ⊢ ( 𝑘 = 𝐷 → ( ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) / ( 𝑥 ↑ 𝐷 ) ) = ( ( ( 𝐶 ‘ 𝐷 ) · ( 𝑥 ↑ 𝐷 ) ) / ( 𝑥 ↑ 𝐷 ) ) )
137 136 sumsn ⊢ ( ( 𝐷 ∈ ℕ0 ∧ ( ( ( 𝐶 ‘ 𝐷 ) · ( 𝑥 ↑ 𝐷 ) ) / ( 𝑥 ↑ 𝐷 ) ) ∈ ℂ ) → Σ 𝑘 ∈ { 𝐷 } ( ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) / ( 𝑥 ↑ 𝐷 ) ) = ( ( ( 𝐶 ‘ 𝐷 ) · ( 𝑥 ↑ 𝐷 ) ) / ( 𝑥 ↑ 𝐷 ) ) )
138 31 132 137 syl2anc ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑘 ∈ { 𝐷 } ( ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) / ( 𝑥 ↑ 𝐷 ) ) = ( ( ( 𝐶 ‘ 𝐷 ) · ( 𝑥 ↑ 𝐷 ) ) / ( 𝑥 ↑ 𝐷 ) ) )
139 130 32 45 divcan4d ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → ( ( ( 𝐶 ‘ 𝐷 ) · ( 𝑥 ↑ 𝐷 ) ) / ( 𝑥 ↑ 𝐷 ) ) = ( 𝐶 ‘ 𝐷 ) )
140 138 139 eqtrd ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑘 ∈ { 𝐷 } ( ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) / ( 𝑥 ↑ 𝐷 ) ) = ( 𝐶 ‘ 𝐷 ) )
141 140 mpteq2dva ⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑘 ∈ { 𝐷 } ( ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) / ( 𝑥 ↑ 𝐷 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 𝐶 ‘ 𝐷 ) ) )
142 rlimconst ⊢ ( ( ℝ+ ⊆ ℝ ∧ ( 𝐶 ‘ 𝐷 ) ∈ ℂ ) → ( 𝑥 ∈ ℝ+ ↦ ( 𝐶 ‘ 𝐷 ) ) ⇝𝑟 ( 𝐶 ‘ 𝐷 ) )
143 14 129 142 sylancr ⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ( 𝑥 ∈ ℝ+ ↦ ( 𝐶 ‘ 𝐷 ) ) ⇝𝑟 ( 𝐶 ‘ 𝐷 ) )
144 141 143 eqbrtrd ⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑘 ∈ { 𝐷 } ( ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) / ( 𝑥 ↑ 𝐷 ) ) ) ⇝𝑟 ( 𝐶 ‘ 𝐷 ) )
145 70 72 128 144 rlimadd ⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑘 ∈ ( 0 ..^ 𝐷 ) ( ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) / ( 𝑥 ↑ 𝐷 ) ) + Σ 𝑘 ∈ { 𝐷 } ( ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) / ( 𝑥 ↑ 𝐷 ) ) ) ) ⇝𝑟 ( 0 + ( 𝐶 ‘ 𝐷 ) ) )
146 129 addid2d ⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ( 0 + ( 𝐶 ‘ 𝐷 ) ) = ( 𝐶 ‘ 𝐷 ) )
147 146 3 eqtr4di ⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ( 0 + ( 𝐶 ‘ 𝐷 ) ) = 𝐵 )
148 145 147 breqtrd ⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑘 ∈ ( 0 ..^ 𝐷 ) ( ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) / ( 𝑥 ↑ 𝐷 ) ) + Σ 𝑘 ∈ { 𝐷 } ( ( ( 𝐶 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) / ( 𝑥 ↑ 𝐷 ) ) ) ) ⇝𝑟 𝐵 )
149 68 148 eqbrtrd ⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ( 𝐹 ∘f / 𝐺 ) ⇝𝑟 𝐵 )