proposition: Theorem MVT : forall (f g:R -> R) (a b:R) (pr1:forall c:R, a < c < b -> derivable_pt f c) (pr2:forall c:R, a < c < b -> derivable_pt g c), a < b -> (forall c:R, a <= c <= b -> continuity_pt f c) -> (forall c:R, a <= c <= b -> continuity_pt g c) -> exists c : R, (exists P : a < c < b, (g b - g a) * derive_pt f c (pr1 c P) = (f b - f a) * derive_pt g c (pr2 c P)).
proof: Proof. intros; assert (H2 := Rlt_le _ _ H). set (h := fun y:R => (g b - g a) * f y - (f b - f a) * g y). assert (X:forall c:R, a < c < b -> derivable_pt h c). { intros; change (derivable_pt ((fct_cte (g b - g a) * f)%F - (fct_cte (f b - f a) * g)%F) c). apply derivable_pt_minus; apply derivable_pt_mult. - apply derivable_pt_const. - apply (pr1 _ H3). - apply derivable_pt_const. - apply (pr2 _ H3). } assert (forall c:R, a <= c <= b -> continuity_pt h c). { intros; unfold h; change (continuity_pt ((fct_cte (g b - g a) * f)%F - (fct_cte (f b - f a) * g)%F) c). apply continuity_pt_minus; apply continuity_pt_mult. - apply derivable_continuous_pt; apply derivable_const. - apply H0; apply H3. - apply derivable_continuous_pt; apply derivable_const. - apply H1; apply H3. } assert (H4 := continuity_ab_maj h a b H2 H3). assert (H5 := continuity_ab_min h a b H2 H3). elim H4; intros Mx H6. elim H5; intros mx H7. assert (h a = h b) by (unfold h;ring). set (M := h Mx); set (m := h mx). assert (forall (c:R) (P:a < c < b), derive_pt h c (X c P) = (g b - g a) * derive_pt f c (pr1 c P) - (f b - f a) * derive_pt g c (pr2 c P)). { intros; unfold h; replace (derive_pt (fun y:R => (g b - g a) * f y - (f b - f a) * g y) c (X c P)) with (derive_pt ((fct_cte (g b - g a) * f)%F - (fct_cte (f b - f a) * g)%F) c (derivable_pt_minus _ _ _ (derivable_pt_mult _ _ _ (derivable_pt_const (g b - g a) c) (pr1 c P)) (derivable_pt_mult _ _ _ (derivable_pt_const (f b - f a) c) (pr2 c P)))); [ idtac | apply pr_nu ]. rewrite derive_pt_minus; do 2 rewrite derive_pt_mult; do 2 rewrite derive_pt_const; do 2 rewrite Rmult_0_l; do 2 rewrite Rplus_0_l; reflexivity. } case (Req_dec (h a) M); intro. 1:case (Req_dec (h a) m); intro. - assert (forall c:R, a <= c <= b -> h c = M). { intros; elim H6; intros H13 _. elim H7; intros H14 _. apply Rle_antisym. - apply H13; apply H12. - rewrite H10 in H11; rewrite H11; apply H14; apply H12. } assert (a < (a + b) / 2 < b). { split. - apply Rmult_lt_reg_l with 2. + prove_sup0. + unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite Rinv_r. * rewrite Rmult_1_l; rewrite <-Rplus_diag; apply Rplus_lt_compat_l; apply H. * discrR. - apply Rmult_lt_reg_l with 2. + prove_sup0. + unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite Rinv_r. * rewrite Rmult_1_l; rewrite Rplus_comm; rewrite <-Rplus_diag; apply Rplus_lt_compat_l; apply H. * discrR. } exists ((a + b) / 2). exists H13. apply Rminus_diag_uniq; rewrite <- H9; apply deriv_constant2 with a b. + elim H13; intros; assumption. + elim H13; intros; assumption. + intros; rewrite (H12 ((a + b) / 2)). * apply H12; split; left; assumption. * elim H13; intros; split; left; assumption. - assert (a < mx < b). { elim H7; intros _ H12; elim H12; intros; split. - inversion H13. + apply H15. + rewrite H15 in H11; elim H11; reflexivity. - inversion H14. + apply H15. + rewrite H8 in H11; rewrite <- H15 in H11; elim H11; reflexivity. } exists mx. exists H12. apply Rminus_diag_uniq; rewrite <- H9; apply deriv_minimum with a b. + elim H12; intros; assumption. + elim H12; intros; assumption. + intros; elim H7; intros. apply H15; split; left; assumption. - assert (a < Mx < b). { elim H6; intros _ H11; elim H11; intros; split. - inversion H12. + apply H14. + rewrite H14 in H10; elim H10; reflexivity. - inversion H13. + apply H14. + rewrite H8 in H10; rewrite <- H14 in H10; elim H10; reflexivity. } exists Mx. exists H11. apply Rminus_diag_uniq; rewrite <- H9; apply deriv_maximum with a b. + elim H11; intros; assumption. + elim H11; intros; assumption. + intros; elim H6; intros; apply H14. split; left; assumption. Qed.
imports: Rbase Rfunctions Ranalysis1 Rtopology Lra