proposition: Lemma Alembert_C1 : forall An:nat -> R, (forall n:nat, 0 < An n) -> Un_cv (fun n:nat => Rabs (An (S n) / An n)) 0 -> { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l }.
proof: Proof. intros An H H0. assert (X:{ l:R | is_lub (EUn (fun N:nat => sum_f_R0 An N)) l } -> { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l }). { intros (x,H1). exists x; apply Un_cv_crit_lub; [ unfold Un_growing; intro; rewrite tech5; pattern (sum_f_R0 An n) at 1; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left; apply H | apply H1 ]. } apply X. apply completeness. 2:{ exists (sum_f_R0 An 0); unfold EUn; exists 0%nat; reflexivity. } unfold Un_cv in H0; unfold bound; cut (0 < / 2); [ intro | apply Rinv_0_lt_compat; prove_sup0 ]. elim (H0 (/ 2) H1); intros. exists (sum_f_R0 An x + 2 * An (S x)). unfold is_upper_bound; intros; unfold EUn in H3; destruct H3 as (x1,->). destruct (lt_eq_lt_dec x1 x) as [[| -> ]|]. - replace (sum_f_R0 An x) with (sum_f_R0 An x1 + sum_f_R0 (fun i:nat => An (S x1 + i)%nat) (x - S x1)). 2:{ symmetry; apply tech2; assumption. } pattern (sum_f_R0 An x1) at 1; rewrite <- Rplus_0_r; rewrite Rplus_assoc; apply Rplus_le_compat_l. left; apply Rplus_lt_0_compat. + apply tech1; intros; apply H. + apply Rmult_lt_0_compat; [ prove_sup0 | apply H ]. - pattern (sum_f_R0 An x) at 1; rewrite <- Rplus_0_r; apply Rplus_le_compat_l. left; apply Rmult_lt_0_compat; [ prove_sup0 | apply H ]. - replace (sum_f_R0 An x1) with (sum_f_R0 An x + sum_f_R0 (fun i:nat => An (S x + i)%nat) (x1 - S x)). 2:{ symmetry; apply tech2; assumption. } apply Rplus_le_compat_l. cut (sum_f_R0 (fun i:nat => An (S x + i)%nat) (x1 - S x) <= An (S x) * sum_f_R0 (fun i:nat => (/ 2) ^ i) (x1 - S x)). { intro; apply Rle_trans with (An (S x) * sum_f_R0 (fun i:nat => (/ 2) ^ i) (x1 - S x)). - assumption. - rewrite <- (Rmult_comm (An (S x))); apply Rmult_le_compat_l. + left; apply H. + rewrite tech3. * replace (1 - / 2) with (/ 2). -- unfold Rdiv; rewrite Rinv_inv. pattern 2 at 3; rewrite <- Rmult_1_r; rewrite <- (Rmult_comm 2); apply Rmult_le_compat_l. ++ left; prove_sup0. ++ left; apply Rplus_lt_reg_l with ((/ 2) ^ S (x1 - S x)). replace ((/ 2) ^ S (x1 - S x) + (1 - (/ 2) ^ S (x1 - S x))) with 1; [ idtac | ring ]. rewrite <- (Rplus_comm 1); pattern 1 at 1; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l. apply pow_lt; apply Rinv_0_lt_compat; prove_sup0. -- field. * replace 1 with (/ 1); [ apply tech7; discrR | apply Rinv_1 ]. } replace (An (S x)) with (An (S x + 0)%nat) by (f_equal; ring). apply (tech6 (fun i:nat => An (S x + i)%nat) (/ 2)). { left; apply Rinv_0_lt_compat; prove_sup0. } intro; cut (forall n:nat, (n >= x)%nat -> An (S n) < / 2 * An n). { intro H4; replace (S x + S i)%nat with (S (S x + i)) by auto with zarith. apply H4; unfold ge; apply tech8. } intros; unfold Rdist in H2; apply Rmult_lt_reg_l with (/ An n). { apply Rinv_0_lt_compat; apply H. } do 2 rewrite (Rmult_comm (/ An n)); rewrite Rmult_assoc; rewrite Rinv_r. 2:{ intro H5; assert (H8 := H n); rewrite H5 in H8; elim (Rlt_irrefl _ H8). } rewrite Rmult_1_r; replace (An (S n) * / An n) with (Rabs (Rabs (An (S n) / An n) - 0)). { apply H2; assumption. } unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; rewrite Rabs_Rabsolu; rewrite Rabs_right. { unfold Rdiv; reflexivity. } left; unfold Rdiv; change (0 < An (S n) * / An n); apply Rmult_lt_0_compat; [ apply H | apply Rinv_0_lt_compat; apply H ]. Qed.
imports: Rbase Rfunctions Rseries SeqProp PartSum Lra