proposition: Lemma limit_mul : forall (f g:C -> C) (D:C -> Prop) (l l' x0:C), limit1_in f D l x0 -> limit1_in g D l' x0 -> limit1_in (fun x:C => f x * g x) D (l * l') x0.
proof: Proof. intros f g D l l' z Hf Hg eps eps_pos. elim (Hf (Rmin 1 (eps * mul_factor (Cnorm l) (Cnorm l'))) (mul_factor_gt_f eps (Cnorm l) (Cnorm l') eps_pos)) ; elim (Hg (eps * mul_factor (Cnorm l) (Cnorm l'))%R (mul_factor_gt eps (Cnorm l) (Cnorm l') eps_pos)) ; clear Hf Hg ; simpl ; intros x Hf y Hg ; elim Hf ; elim Hg ; clear Hf Hg ; intros y_pos Hx x_pos Hy ; split with (Rmin y x) ; split ; [apply Rmin_Rgt_r ; split ; assumption |]. intros z' [Dz' Hz'] ; unfold C_dist ; replace (f z' * g z' - l * l') with (f z' * (g z' - l') + l' * (f z' - l)). cut (Cnorm (f z' * (g z' - l')) + Cnorm (l' * (f z' - l)) < eps). cut (Cnorm (f z' * (g z' - l') + l' * (f z' - l)) <= Cnorm (f z' * (g z' - l')) + Cnorm (l' * (f z' - l))). apply Rle_lt_trans. apply Cnorm_triang. repeat (rewrite Cnorm_Cmult) ; cut ((1 + Cnorm l) * (eps * mul_factor (Cnorm l) (Cnorm l')) + Cnorm l' * (eps * mul_factor (Cnorm l) (Cnorm l')) <= eps). cut (Cnorm (f z') * Cnorm (g z' - l') + Cnorm l' * Cnorm (f z' - l) < (1 + Cnorm l) * (eps * mul_factor (Cnorm l) (Cnorm l')) + Cnorm l' * (eps * mul_factor (Cnorm l) (Cnorm l'))). apply Rlt_le_trans. elim (Rmin_Rgt_l y x (C_dist z' z) Hz'); intros Hx2 Hy2. apply Rplus_lt_le_compat. apply Rmult_ge_0_gt_0_lt_compat. apply Rle_ge ; apply Cnorm_pos. rewrite Rplus_comm ; unfold Rgt in |- *; apply Rle_lt_0_plus_1; apply Cnorm_pos. apply Rplus_lt_reg_l with (- Cnorm l)%R. rewrite <- Rplus_assoc ; rewrite (Rplus_comm (- Cnorm l) 1). rewrite (Rplus_assoc 1 (- Cnorm l) (Cnorm l)) ; rewrite Rplus_opp_l ; rewrite (proj1 (Rplus_ne 1)) ; rewrite (Rplus_comm (- Cnorm l) (Cnorm (f z'))) ; cut (Cnorm (f z' - l) < 1) ; cut (Cnorm (f z') - Cnorm l <= Cnorm (f z' - l)). apply Rle_lt_trans. apply Cnorm_triang_rev_l. intros _ ; apply Rlt_le_trans with (Rmin 1 (eps * mul_factor (Cnorm l) (Cnorm l'))) ; [apply Hx ; split ; assumption | apply Rmin_l]. apply Cnorm_triang_rev_l. apply Hy ; split ; assumption. apply Rmult_le_compat. apply Cnorm_pos. apply Cnorm_pos. right ; trivial. apply Rlt_le ; apply Rlt_le_trans with (Rmin 1 (eps * mul_factor (Cnorm l) (Cnorm l'))) ; [apply Hx | apply Rmin_r] ; split ; assumption. rewrite (Rmult_comm (1 + Cnorm l) (eps * mul_factor (Cnorm l) (Cnorm l'))); rewrite (Rmult_comm (Cnorm l') (eps * mul_factor (Cnorm l) (Cnorm l'))); rewrite <- (Rmult_plus_distr_l (eps * mul_factor (Cnorm l) (Cnorm l')) (1 + Cnorm l) (Cnorm l')) ; rewrite (Rmult_assoc eps (mul_factor (Cnorm l) (Cnorm l')) (1 + Cnorm l + Cnorm l')); rewrite (Rplus_assoc 1 (Cnorm l) (Cnorm l')). unfold mul_factor ; right. repeat rewrite Rabs_Cnorm. rewrite Rinv_l. field. apply Rgt_not_eq. rewrite Rplus_comm ; apply Rle_lt_0_plus_1 ; apply Rplus_le_le_0_compat ; apply Cnorm_pos. field. Qed.
imports: Rlimit Cbase Ctacfield Cnorm Cprop_base Rsequence_def Csequence Csequence_facts Cfunctions