proposition: Lemma Alembert_C2_aux_Un_cv : forall Xn : nat -> R, let Yn i := (2 * Rabs (Xn i) + Xn i) / 2 in (forall n, Xn n <> 0) -> Un_cv (fun n:nat => Rabs (Xn (S n) / Xn n)) 0 -> Un_cv (fun n => Rabs (Yn (S n) / Yn n)) 0.
proof: Proof. intros An Vn H H0. pose proof (Alembert_C2_aux_positivity An H); fold Vn in H1. pose proof tt as H2. cut (forall n:nat, / 2 * Rabs (An n) <= Vn n <= 3 * / 2 * Rabs (An n)). 1:intro; cut (forall n:nat, / Vn n <= 2 * / Rabs (An n)). 1:intro; cut (forall n:nat, Vn (S n) / Vn n <= 3 * Rabs (An (S n) / An n)). + intro; unfold Un_cv; intros; unfold Un_cv in H1; assert (0 < eps / 3). { unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ]. } elim (H0 (eps / 3) H7); intros. exists x; intros. assert (H10 := H8 n H9). unfold Rdist; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; rewrite Rabs_Rabsolu; unfold Rdist in H10; unfold Rminus in H10; rewrite Ropp_0 in H10; rewrite Rplus_0_r in H10; rewrite Rabs_Rabsolu in H10; rewrite Rabs_right. 2:{ left; change (0 < Vn (S n) / Vn n); unfold Rdiv; apply Rmult_lt_0_compat. - apply H1. - apply Rinv_0_lt_compat; apply H1. } apply Rle_lt_trans with (3 * Rabs (An (S n) / An n)). { apply H5. } apply Rmult_lt_reg_l with (/ 3). { apply Rinv_0_lt_compat; prove_sup0. } rewrite <- Rmult_assoc; rewrite Rinv_l; [ idtac | discrR ]; rewrite Rmult_1_l; rewrite <- (Rmult_comm eps); unfold Rdiv in H10; exact H10. + intro; unfold Rdiv; rewrite Rabs_mult; rewrite <- Rmult_assoc; replace 3 with (2 * (3 * / 2)); [ idtac | rewrite <- Rmult_assoc; apply Rmult_inv_r_id_m; discrR ]; apply Rle_trans with (Vn (S n) * 2 * / Rabs (An n)). { rewrite Rmult_assoc; apply Rmult_le_compat_l. - left; apply H1. - apply H4. } rewrite Rabs_inv. replace (Vn (S n) * 2 * / Rabs (An n)) with (2 * / Rabs (An n) * Vn (S n)) by ring; replace (2 * (3 * / 2) * Rabs (An (S n)) * / Rabs (An n)) with (2 * / Rabs (An n) * (3 * / 2 * Rabs (An (S n)))) by ring; apply Rmult_le_compat_l. { left; apply Rmult_lt_0_compat. - prove_sup0. - apply Rinv_0_lt_compat; apply Rabs_pos_lt; apply H. } elim (H3 (S n)); intros; assumption. + intro; apply Rmult_le_reg_l with (Vn n). { apply H1. } rewrite Rinv_r. 2:{ red; intro; assert (H5 := H1 n); rewrite H4 in H5; elim (Rlt_irrefl _ H5). } apply Rmult_le_reg_l with (Rabs (An n)). { apply Rabs_pos_lt; apply H. } rewrite Rmult_1_r; replace (Rabs (An n) * (Vn n * (2 * / Rabs (An n)))) with (2 * Vn n * (Rabs (An n) * / Rabs (An n))); [ idtac | ring ]; rewrite Rinv_r. 2:{ apply Rabs_no_R0; apply H. } rewrite Rmult_1_r; apply Rmult_le_reg_l with (/ 2). { apply Rinv_0_lt_compat; prove_sup0. } rewrite <- Rmult_assoc; rewrite Rinv_l. * rewrite Rmult_1_l; elim (H3 n); intros; assumption. * discrR. + intro; split. * unfold Vn; unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); apply Rmult_le_compat_l. { left; apply Rinv_0_lt_compat; prove_sup0. } pattern (Rabs (An n)) at 1; rewrite <- Rplus_0_r; rewrite <-Rplus_diag; rewrite Rplus_assoc; apply Rplus_le_compat_l. apply Rplus_le_reg_l with (- An n); rewrite Rplus_0_r; rewrite <- (Rplus_comm (An n)); rewrite <- Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_l; rewrite <- Rabs_Ropp; apply RRle_abs. * unfold Vn; unfold Rdiv; repeat rewrite <- (Rmult_comm (/ 2)); repeat rewrite Rmult_assoc; apply Rmult_le_compat_l. { left; apply Rinv_0_lt_compat; prove_sup0. } unfold Rminus; rewrite <-Rplus_diag; replace (3 * Rabs (An n)) with (Rabs (An n) + Rabs (An n) + Rabs (An n)); [ idtac | ring ]; repeat rewrite Rplus_assoc; repeat apply Rplus_le_compat_l; apply RRle_abs. Qed.
imports: Rbase Rfunctions Rseries SeqProp PartSum Lra