proposition: Lemma CV_mult : forall (An Bn:nat -> R) (l1 l2:R), Un_cv An l1 -> Un_cv Bn l2 -> Un_cv (fun i:nat => An i * Bn i) (l1 * l2).
proof: Proof. intros. assert (X:{ l:R | Un_cv An l }) by (exists l1; assumption). assert (H1 := maj_by_pos An X). elim H1; intros M H2. elim H2; intros. unfold Un_cv; unfold Rdist; intros. cut (0 < eps / (2 * M)). - intro. case (Req_dec l2 0); intro. + unfold Un_cv in H0; unfold Rdist in H0. elim (H0 (eps / (2 * M)) H6); intros. exists x; intros. apply Rle_lt_trans with (Rabs (An n * Bn n - An n * l2) + Rabs (An n * l2 - l1 * l2)). { replace (An n * Bn n - l1 * l2) with (An n * Bn n - An n * l2 + (An n * l2 - l1 * l2)); [ apply Rabs_triang | ring ]. } replace (Rabs (An n * Bn n - An n * l2)) with (Rabs (An n) * Rabs (Bn n - l2)). { replace (Rabs (An n * l2 - l1 * l2)) with 0. - rewrite Rplus_0_r. apply Rle_lt_trans with (M * Rabs (Bn n - l2)). + do 2 rewrite <- (Rmult_comm (Rabs (Bn n - l2))). apply Rmult_le_compat_l. * apply Rabs_pos. * apply H4. + apply Rmult_lt_reg_l with (/ M). { apply Rinv_0_lt_compat; apply H3. } rewrite <- Rmult_assoc; rewrite Rinv_l. * rewrite Rmult_1_l; rewrite (Rmult_comm (/ M)). apply Rlt_trans with (eps / (2 * M)). { apply H8; assumption. } unfold Rdiv; rewrite Rinv_mult. apply Rmult_lt_reg_l with 2. { prove_sup0. } replace (2 * (eps * (/ 2 * / M))) with (2 * / 2 * (eps * / M)); [ idtac | ring ]. rewrite Rinv_r. -- rewrite Rmult_1_l; rewrite <-Rplus_diag. pattern (eps * / M) at 1; rewrite <- Rplus_0_r. apply Rplus_lt_compat_l; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; assumption ]. -- discrR. * red; intro; rewrite H10 in H3; elim (Rlt_irrefl _ H3). - rewrite H7; do 2 rewrite Rmult_0_r; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; reflexivity. } replace (An n * Bn n - An n * l2) with (An n * (Bn n - l2)) by ring. symmetry ; apply Rabs_mult. + assert (0 < eps / (2 * Rabs l2)). { unfold Rdiv; apply Rmult_lt_0_compat. { assumption. } apply Rinv_0_lt_compat; apply Rmult_lt_0_compat; [ prove_sup0 | apply Rabs_pos_lt; assumption ]. } unfold Un_cv in H; unfold Rdist in H; unfold Un_cv in H0; unfold Rdist in H0. elim (H (eps / (2 * Rabs l2)) H8); intros N1 H9. elim (H0 (eps / (2 * M)) H6); intros N2 H10. set (N := max N1 N2). exists N; intros. apply Rle_lt_trans with (Rabs (An n * Bn n - An n * l2) + Rabs (An n * l2 - l1 * l2)). { replace (An n * Bn n - l1 * l2) with (An n * Bn n - An n * l2 + (An n * l2 - l1 * l2)) by ring; apply Rabs_triang. } replace (Rabs (An n * Bn n - An n * l2)) with (Rabs (An n) * Rabs (Bn n - l2)). 1:replace (Rabs (An n * l2 - l1 * l2)) with (Rabs l2 * Rabs (An n - l1)). * rewrite <-(Rplus_half_diag eps); apply Rplus_lt_compat. -- apply Rle_lt_trans with (M * Rabs (Bn n - l2)). { do 2 rewrite <- (Rmult_comm (Rabs (Bn n - l2))). apply Rmult_le_compat_l. - apply Rabs_pos. - apply H4. } apply Rmult_lt_reg_l with (/ M). { apply Rinv_0_lt_compat; apply H3. } rewrite <- Rmult_assoc; rewrite Rinv_l. ++ rewrite Rmult_1_l; rewrite (Rmult_comm (/ M)). apply Rlt_le_trans with (eps / (2 * M)). ** apply H10. unfold ge; apply Nat.le_trans with N. { unfold N; apply Nat.le_max_r. } assumption. ** unfold Rdiv; rewrite Rinv_mult. right; ring. ++ red; intro; rewrite H12 in H3; elim (Rlt_irrefl _ H3). -- apply Rmult_lt_reg_l with (/ Rabs l2). { apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption. } rewrite <- Rmult_assoc; rewrite Rinv_l. ++ rewrite Rmult_1_l; apply Rlt_le_trans with (eps / (2 * Rabs l2)). ** apply H9. unfold ge; apply Nat.le_trans with N. { unfold N; apply Nat.le_max_l. } assumption. ** unfold Rdiv; right; rewrite Rinv_mult. ring. ++ apply Rabs_no_R0; assumption. * replace (An n * l2 - l1 * l2) with (l2 * (An n - l1)); [ symmetry ; apply Rabs_mult | ring ]. * replace (An n * Bn n - An n * l2) with (An n * (Bn n - l2)); [ symmetry ; apply Rabs_mult | ring ]. - unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; apply Rmult_lt_0_compat; [ prove_sup0 | assumption ] ]. Qed.
imports: Rbase Rfunctions Rseries Lia