proposition: Lemma AlembertC3_step1 : forall (An:nat -> R) (x:R), x <> 0 -> (forall n:nat, An n <> 0) -> Un_cv (fun n:nat => Rabs (An (S n) / An n)) 0 -> { l:R | Pser An x l }.
proof: Proof. intros; set (Bn := fun i:nat => An i * x ^ i). assert (forall n:nat, Bn n <> 0). { intro; unfold Bn; apply prod_neq_R0; [ apply H0 | apply pow_nonzero; assumption ]. } cut (Un_cv (fun n:nat => Rabs (Bn (S n) / Bn n)) 0). { intro; destruct (Alembert_C2 Bn H2 H3) as (x0,H4). exists x0; unfold Bn in H4; apply tech12; assumption. } unfold Un_cv; intros; unfold Un_cv in H1; cut (0 < eps / Rabs x). 2:{ unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption ]. } intro; elim (H1 (eps / Rabs x) H4); intros. exists x0; intros; unfold Rdist; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; rewrite Rabs_Rabsolu; unfold Bn; replace (An (S n) * x ^ S n / (An n * x ^ n)) with (An (S n) / An n * x). 2:{ replace (S n) with (n + 1)%nat by ring; rewrite pow_add; unfold Rdiv; rewrite Rinv_mult. replace (An (n + 1)%nat * (x ^ n * x ^ 1) * (/ An n * / x ^ n)) with (An (n + 1)%nat * x ^ 1 * / An n * (x ^ n * / x ^ n)) by ring; rewrite Rinv_r. - simpl; ring. - apply pow_nonzero; assumption. } rewrite Rabs_mult; apply Rmult_lt_reg_l with (/ Rabs x). { apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption. } rewrite <- (Rmult_comm (Rabs x)); rewrite <- Rmult_assoc; rewrite Rinv_l. 2:{ apply Rabs_no_R0; assumption. } rewrite Rmult_1_l; rewrite <- (Rmult_comm eps); unfold Rdiv in H5; replace (Rabs (An (S n) / An n)) with (Rdist (Rabs (An (S n) * / An n)) 0). { apply H5; assumption. } unfold Rdist; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; rewrite Rabs_Rabsolu; unfold Rdiv; reflexivity. Qed.
imports: Rbase Rfunctions Rseries SeqProp PartSum Lra