proposition: Theorem alternated_series_ineq : forall (Un:nat -> R) (l:R) (N:nat), Un_decreasing Un -> Un_cv Un 0 -> Un_cv (fun N:nat => sum_f_R0 (tg_alt Un) N) l -> sum_f_R0 (tg_alt Un) (S (2 * N)) <= l <= sum_f_R0 (tg_alt Un) (2 * N).
proof: Proof. intros. assert (Un_cv (fun N:nat => sum_f_R0 (tg_alt Un) (2 * N)) l). { unfold Un_cv; unfold Rdist; unfold Un_cv in H1; unfold Rdist in H1; intros. elim (H1 eps H2); intros. exists x; intros. apply H3. apply Nat.le_trans with n; [ assumption | ]. rewrite <- Nat.double_twice; apply Nat.le_add_r. } assert (Un_cv (fun N:nat => sum_f_R0 (tg_alt Un) (S (2 * N))) l). { unfold Un_cv; unfold Rdist; unfold Un_cv in H1; unfold Rdist in H1; intros. elim (H1 eps H3); intros. exists x; intros. apply H4. apply Nat.le_trans with n; [ assumption | ]. apply Nat.le_le_succ_r. rewrite <- Nat.double_twice; apply Nat.le_add_r. } intros; split. - apply (growing_ineq (fun N:nat => sum_f_R0 (tg_alt Un) (S (2 * N)))). + apply CV_ALT_step0; assumption. + assumption. - apply (decreasing_ineq (fun N:nat => sum_f_R0 (tg_alt Un) (2 * N))). + apply CV_ALT_step1; assumption. + assumption. Qed.
imports: Rbase Rfunctions Rseries SeqProp PartSum Lra