proposition: Theorem Dpower : forall y z:R, 0 < y -> D_in (fun x:R => Rpower x z) (fun x:R => z * Rpower x (z - 1)) ( fun x:R => 0 < x) y.
proof: Proof. intros y z H; apply D_in_imp with (D := Dgf (fun x:R => 0 < x) (fun x:R => True) ln). { intros x H0; repeat split. assumption. } apply D_in_ext with (f := fun x:R => / x * (z * exp (z * ln x))). { unfold Rminus; rewrite Rpower_plus; rewrite Rpower_Ropp; rewrite (Rpower_1 _ H); unfold Rpower; ring. } apply Dcomp with (f := ln) (g := fun x:R => exp (z * x)) (df := Rinv) (dg := fun x:R => z * exp (z * x)). { apply (Dln _ H). } apply D_in_imp with (D := Dgf (fun x:R => True) (fun x:R => True) (fun x:R => z * x)). { intros x H1; repeat split; auto. } apply (Dcomp (fun _:R => True) (fun _:R => True) (fun x => z) exp (fun x:R => z * x) exp); simpl. - apply D_in_ext with (f := fun x:R => z * 1). { apply Rmult_1_r. } apply (Dmult_const (fun x => True) (fun x => x) (fun x => 1)); apply Dx. - assert (H0 := derivable_pt_lim_D_in exp exp (z * ln y)); elim H0; clear H0; intros _ H0; apply H0; apply derivable_pt_lim_exp. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra