proposition: Lemma derivable_pt_finite_sum : forall (An:nat -> R) (N:nat) (x:R), derivable_pt (fun y:R => sum_f_R0 (fun k:nat => An k * y ^ k) N) x.
proof: Proof. intros. unfold derivable_pt. assert (H := derivable_pt_lim_finite_sum An x N). induction N as [| N HrecN]. - exists 0; apply H. - exists (sum_f_R0 (fun k:nat => INR (S k) * An (S k) * x ^ k) (pred (S N))); apply H. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Ranalysis3 Exp_prop MVT Lra Lia