proposition: Lemma Alembert_C6 : forall (An:nat -> R) (x k:R), 0 < k -> (forall n:nat, An n <> 0) -> Un_cv (fun n:nat => Rabs (An (S n) / An n)) k -> Rabs x < / k -> { l:R | Pser An x l }.
proof: Proof. intros. cut { l:R | Un_cv (fun N:nat => sum_f_R0 (fun i:nat => An i * x ^ i) N) l }. { intro X. elim X; intros. exists x0. apply tech12; assumption. } destruct (total_order_T x 0) as [[Hlt|Heq]|Hgt]. - eapply Alembert_C5 with (k * Rabs x). + split. * unfold Rdiv; apply Rmult_le_pos. { lra. } left; apply Rabs_pos_lt. lra. * apply Rmult_lt_reg_l with (/ k). { apply Rinv_0_lt_compat; assumption. } rewrite <- Rmult_assoc. rewrite Rinv_l. 2:{ lra. } rewrite Rmult_1_l. rewrite Rmult_1_r; assumption. + intro; apply prod_neq_R0. { apply H0. } apply pow_nonzero. lra. + unfold Un_cv; unfold Un_cv in H1. intros. assert (0 < eps / Rabs x). { unfold Rdiv; apply Rmult_lt_0_compat. - assumption. - apply Rinv_0_lt_compat; apply Rabs_pos_lt. lra. } elim (H1 (eps / Rabs x) H4); intros. exists x0. intros. replace (An (S n) * x ^ S n / (An n * x ^ n)) with (An (S n) / An n * x). 2:{ unfold Rdiv; replace (S n) with (n + 1)%nat by ring. rewrite pow_add. simpl. rewrite Rmult_1_r. rewrite Rinv_mult. replace (An (n + 1)%nat * (x ^ n * x) * (/ An n * / x ^ n)) with (An (n + 1)%nat * / An n * x * (x ^ n * / x ^ n)) by ring. rewrite Rinv_r. { lra. } apply pow_nonzero;lra. } unfold Rdist. rewrite Rabs_mult. replace (Rabs (An (S n) / An n) * Rabs x - k * Rabs x) with (Rabs x * (Rabs (An (S n) / An n) - k)) by ring. rewrite Rabs_mult. rewrite Rabs_Rabsolu. apply Rmult_lt_reg_l with (/ Rabs x). { apply Rinv_0_lt_compat; apply Rabs_pos_lt. lra. } rewrite <- Rmult_assoc. rewrite Rinv_l. 2:{ apply Rabs_no_R0; lra. } rewrite Rmult_1_l. rewrite <- (Rmult_comm eps). unfold Rdist in H5. unfold Rdiv; unfold Rdiv in H5; apply H5; assumption. - exists (An 0%nat). unfold Un_cv. intros. exists 0%nat. intros. unfold Rdist. replace (sum_f_R0 (fun i:nat => An i * x ^ i) n) with (An 0%nat). { unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption. } induction n as [| n Hrecn]. + simpl; ring. + rewrite tech5. rewrite <- Hrecn,Heq;simpl. * ring. * unfold ge; apply Nat.le_0_l. - eapply Alembert_C5 with (k * Rabs x). + split. * unfold Rdiv; apply Rmult_le_pos. { left; assumption. } left; apply Rabs_pos_lt. lra. * apply Rmult_lt_reg_l with (/ k). { apply Rinv_0_lt_compat; assumption. } rewrite <- Rmult_assoc. rewrite Rinv_l. 2:{ lra. } rewrite Rmult_1_l. rewrite Rmult_1_r; assumption. + intro; apply prod_neq_R0. * apply H0. * apply pow_nonzero. lra. + unfold Un_cv; unfold Un_cv in H1. intros. assert (0 < eps / Rabs x). { unfold Rdiv; apply Rmult_lt_0_compat. - assumption. - apply Rinv_0_lt_compat; apply Rabs_pos_lt. lra. } elim (H1 (eps / Rabs x) H4); intros. exists x0. intros. replace (An (S n) * x ^ S n / (An n * x ^ n)) with (An (S n) / An n * x). 2:{ unfold Rdiv; replace (S n) with (n + 1)%nat by ring. rewrite pow_add. simpl. rewrite Rmult_1_r. rewrite Rinv_mult. replace (An (n + 1)%nat * (x ^ n * x) * (/ An n * / x ^ n)) with (An (n + 1)%nat * / An n * x * (x ^ n * / x ^ n)) by ring. rewrite Rinv_r. { lra. } apply pow_nonzero;lra. } unfold Rdist. rewrite Rabs_mult. replace (Rabs (An (S n) / An n) * Rabs x - k * Rabs x) with (Rabs x * (Rabs (An (S n) / An n) - k)); [ idtac | ring ]. rewrite Rabs_mult. rewrite Rabs_Rabsolu. apply Rmult_lt_reg_l with (/ Rabs x). { apply Rinv_0_lt_compat; apply Rabs_pos_lt. lra. } rewrite <- Rmult_assoc. rewrite Rinv_l. 2:{ apply Rabs_no_R0. lra. } rewrite Rmult_1_l. rewrite <- (Rmult_comm eps). unfold Rdist in H5. unfold Rdiv; unfold Rdiv in H5; apply H5; assumption. Qed.
imports: Rbase Rfunctions Rseries SeqProp PartSum Lra