proposition: Lemma null_derivative_loc : forall (f:R -> R) (a b:R) (pr:forall x:R, a < x < b -> derivable_pt f x), (forall x:R, a <= x <= b -> continuity_pt f x) -> (forall (x:R) (P:a < x < b), derive_pt f x (pr x P) = 0) -> constant_D_eq f (fun x:R => a <= x <= b) (f a).
proof: Proof. intros; unfold constant_D_eq; intros; destruct (total_order_T a b) as [[Hlt|Heq]|Hgt]. - assert (H2 : forall y:R, a < y < x -> derivable_pt id y). { intros; apply derivable_pt_id. } assert (H3 : forall y:R, a <= y <= x -> continuity_pt id y). { intros; apply derivable_continuous; apply derivable_id. } assert (H4 : forall y:R, a < y < x -> derivable_pt f y). { intros; apply pr; elim H4; intros; split. - assumption. - elim H1; intros; apply Rlt_le_trans with x; assumption. } assert (H5 : forall y:R, a <= y <= x -> continuity_pt f y). { intros; apply H; elim H5; intros; split. - assumption. - elim H1; intros; apply Rle_trans with x; assumption. } elim H1; clear H1; intros; elim H1; clear H1; intro. + assert (H7 := MVT f id a x H4 H2 H1 H5 H3). destruct H7 as (c & P & H9). assert (H10 : a < c < b). { split. - apply P. - apply Rlt_le_trans with x; [apply P|assumption]. } assert (H11 : derive_pt f c (H4 c P) = 0). { replace (derive_pt f c (H4 c P)) with (derive_pt f c (pr c H10)); [ apply H0 | apply pr_nu ]. } assert (H12 : derive_pt id c (H2 c P) = 1). { apply derive_pt_eq_0; apply derivable_pt_lim_id. } rewrite H11 in H9; rewrite H12 in H9; rewrite Rmult_0_r in H9; rewrite Rmult_1_r in H9; apply Rminus_diag_uniq; symmetry ; assumption. + rewrite H1; reflexivity. - assert (H2 : x = a). { rewrite <- Heq in H1; elim H1; intros; apply Rle_antisym; assumption. } rewrite H2; reflexivity. - elim H1; intros; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ (Rle_trans _ _ _ H2 H3) Hgt)). Qed.
imports: Rbase Rfunctions Ranalysis1 Rtopology Lra