proposition: Lemma Rpser_alembert_prelim : forall (An : nat -> R) (M : R), 0 < M -> (forall n : nat, An n <> 0) -> Rseq_bound (fun n => (An (S n) / An n)) M -> forall r, Rabs r < / M -> Cv_radius_weak An r.
proof: Proof. intros An M M_pos An_neq An_frac_ub r r_bd. assert (r_lb := Rabs_pos r) ; case r_lb ; clear r_lb ; intro rabs_lb. assert (my_lam : 0 < /Rabs r - M). apply Rgt_minus ; rewrite <- Rinv_inv. apply Rinv_lt_contravar. apply Rmult_lt_0_compat ; [| apply Rlt_trans with (Rabs r)] ; assumption. assumption. exists (Rabs (An 0%nat)) ; intros x Hyp ; elim Hyp ; intros n Hn ; rewrite Hn ; unfold gt_abs_pser, gt_pser, Rseq_abs, Rseq_mult ; rewrite Rabs_mult. clear Hn ; induction n. simpl ; rewrite Rabs_R1 ; rewrite Rmult_1_r ; right ; reflexivity. apply Rle_trans with (Rabs (An (S n) / (An n)) * Rabs (An n) * Rabs (r ^ S n)). right ; repeat rewrite <- Rabs_mult ; apply Rabs_eq_compat ; field ; apply An_neq. apply Rle_trans with (M * Rabs (An n) * Rabs (r ^ S n)). repeat apply Rmult_le_compat_r ; [| | apply An_frac_ub] ; apply Rabs_pos. simpl ; rewrite Rabs_mult. apply Rle_trans with (M * Rabs (An n) * (/M * Rabs (r ^ n))). repeat rewrite <- Rmult_assoc ; apply Rmult_le_compat_r ; [apply Rabs_pos | repeat rewrite Rmult_assoc ; repeat apply Rmult_le_compat_l]. left ; assumption. apply Rabs_pos. left ; assumption. apply Rle_trans with (Rabs (An n) * Rabs (r ^ n))%R ; [right ; field ; apply Rgt_not_eq |] ; assumption. exists (Rabs (An 0%nat)). intros x Hx ; destruct Hx as (n,Hn) ; rewrite Hn ; destruct n. apply gt_abs_pser_0_ub. destruct (Req_dec r 0) as [Hr | Hf]. rewrite Hr ; apply gt_abs_pser_0_ub. apply False_ind ; assert (T := Rabs_no_R0 _ Hf) ; apply T ; symmetry ; assumption. Qed.
imports: Reals Rsequence_def Rpser_def Rpser_def_simpl Rpser_base_facts Rsequence_facts Rsequence_sums_facts Rsequence_rewrite_facts Rpow_facts Lra PeanoNat MyRIneq MyNeq Rinterval RFsequence RFsequence_facts Tactics