proposition: Theorem MVT_cor2 : forall (f f':R -> R) (a b:R), a < b -> (forall c:R, a <= c <= b -> derivable_pt_lim f c (f' c)) -> exists c : R, f b - f a = f' c * (b - a) /\ a < c < b.
proof: Proof. intros f f' a b H H0; cut (forall c:R, a <= c <= b -> derivable_pt f c). 1:intro X; cut (forall c:R, a < c < b -> derivable_pt f c). 1:intro X0; cut (forall c:R, a <= c <= b -> continuity_pt f c). 1:intro; cut (forall c:R, a <= c <= b -> derivable_pt id c). 1:intro X1; cut (forall c:R, a < c < b -> derivable_pt id c). 1:intro X2; cut (forall c:R, a <= c <= b -> continuity_pt id c). - intro; elim (MVT f id a b X0 X2 H H1 H2); intros x (P,H3). exists x; split. + cut (derive_pt id x (X2 x P) = 1). 1:cut (derive_pt f x (X0 x P) = f' x). * intros; rewrite H4 in H3; rewrite H5 in H3; unfold id in H3; rewrite Rmult_1_r in H3; rewrite Rmult_comm; symmetry ; assumption. * apply derive_pt_eq_0; apply H0; elim P; intros; split; left; assumption. * apply derive_pt_eq_0; apply derivable_pt_lim_id. + assumption. - intros; apply derivable_continuous_pt; apply X1; assumption. - intros; apply derivable_pt_id. - intros; apply derivable_pt_id. - intros; apply derivable_continuous_pt; apply X; assumption. - intros; elim H1; intros; apply X; split; left; assumption. - intros; unfold derivable_pt; exists (f' c); apply H0; apply H1. Qed.
imports: Rbase Rfunctions Ranalysis1 Rtopology Lra