proposition: Lemma Dmult : forall (D:R -> Prop) (df dg f g:R -> R) (x0:R), D_in f df D x0 -> D_in g dg D x0 -> D_in (fun x:R => f x * g x) (fun x:R => df x * g x + f x * dg x) D x0.
proof: Proof. intros; unfold D_in; generalize H H0; intros; unfold D_in in H, H0; generalize (cont_deriv f df D x0 H1); unfold continue_in; intro; generalize (limit_mul (fun x:R => (g x - g x0) * / (x - x0)) ( fun x:R => f x) (D_x D x0) (dg x0) (f x0) x0 H0 H3); intro; cut (limit1_in (fun x:R => g x0) (D_x D x0) (g x0) x0). - intro; generalize (limit_mul (fun x:R => (f x - f x0) * / (x - x0)) ( fun _:R => g x0) (D_x D x0) (df x0) (g x0) x0 H H5); clear H H0 H1 H2 H3 H5; intro; generalize (limit_plus (fun x:R => (f x - f x0) * / (x - x0) * g x0) (fun x:R => (g x - g x0) * / (x - x0) * f x) ( D_x D x0) (df x0 * g x0) (dg x0 * f x0) x0 H H4); clear H4 H; intro; unfold limit1_in in H; unfold limit_in in H; simpl in H; unfold limit1_in; unfold limit_in; simpl; intros; elim (H eps H0); clear H; intros; elim H; clear H; intros; split with x; split; auto; intros; generalize (H1 x1 H2); clear H1; intro; rewrite (Rmult_comm (f x1 - f x0) (/ (x1 - x0))) in H1; rewrite (Rmult_comm (g x1 - g x0) (/ (x1 - x0))) in H1; rewrite (Rmult_assoc (/ (x1 - x0)) (f x1 - f x0) (g x0)) in H1; rewrite (Rmult_assoc (/ (x1 - x0)) (g x1 - g x0) (f x1)) in H1; rewrite <- (Rmult_plus_distr_l (/ (x1 - x0)) ((f x1 - f x0) * g x0) ((g x1 - g x0) * f x1)) in H1; rewrite (Rmult_comm (/ (x1 - x0)) ((f x1 - f x0) * g x0 + (g x1 - g x0) * f x1)) in H1; rewrite (Rmult_comm (dg x0) (f x0)) in H1; cut ((f x1 - f x0) * g x0 + (g x1 - g x0) * f x1 = f x1 * g x1 - f x0 * g x0). + intro; rewrite H3 in H1; assumption. + ring. - unfold limit1_in; unfold limit_in; simpl; intros; split with eps; split; auto; intros; elim (Rdist_refl (g x0) (g x0)); intros a b; rewrite (b (eq_refl (g x0))); unfold Rgt in H; assumption. Qed.
imports: Rbase Rfunctions Rlimit Lra Lia