let p, x be Real; ( x > 0 implies ( #R p is_differentiable_in x & diff ((#R p),x) = p * (x #R (p - 1)) ) )
set f = #R p;
A1:
for x being Real st 0 < x holds
( exp_R * (p (#) ln) is_differentiable_in x & diff ((exp_R * (p (#) ln)),x) = p * (x #R (p - 1)) )
proof
let x be
Real;
( 0 < x implies ( exp_R * (p (#) ln) is_differentiable_in x & diff ((exp_R * (p (#) ln)),x) = p * (x #R (p - 1)) ) )
assume A2:
x > 0
;
( exp_R * (p (#) ln) is_differentiable_in x & diff ((exp_R * (p (#) ln)),x) = p * (x #R (p - 1)) )
A3:
ln is_differentiable_in x
by A2, Th18;
then A4:
p (#) ln is_differentiable_in x
by FDIFF_1:15;
x in { g where g is Real : 0 < g }
by A2;
then A5:
x in right_open_halfline 0
by XXREAL_1:230;
then A6:
x in dom (p (#) ln)
by Th18, VALUED_1:def 5;
A7:
diff (
(p (#) ln),
x) =
p * (diff (ln,x))
by A3, FDIFF_1:15
.=
p * (1 / x)
by A5, Th18
;
A8:
exp_R is_differentiable_in (p (#) ln) . x
by SIN_COS:65;
hence
exp_R * (p (#) ln) is_differentiable_in x
by A4, FDIFF_2:13;
diff ((exp_R * (p (#) ln)),x) = p * (x #R (p - 1))
diff (
exp_R,
((p (#) ln) . x)) =
exp_R . ((p (#) ln) . x)
by Th16
.=
exp_R . (p * (ln . x))
by A6, VALUED_1:def 5
.=
exp_R . (p * (log (number_e,x)))
by A5, Def2
.=
exp_R . (log (number_e,(x to_power p)))
by A2, Lm4, POWER:55
.=
x to_power p
by A2, Th15, POWER:34
;
hence diff (
(exp_R * (p (#) ln)),
x) =
(x to_power p) * (p * (1 / x))
by A4, A8, A7, FDIFF_2:13
.=
p * ((x to_power p) * (1 / x))
.=
p * ((x to_power p) * (1 / (x to_power 1)))
by POWER:25
.=
p * ((x to_power p) * (x to_power (- 1)))
by A2, POWER:28
.=
p * (x to_power (p + (- 1)))
by A2, POWER:27
.=
p * (x #R (p - 1))
by A2, POWER:def 2
;
verum
end;
rng (p (#) ln) c= dom exp_R
by Th16;
then A9: dom (exp_R * (p (#) ln)) =
dom (p (#) ln)
by RELAT_1:27
.=
right_open_halfline 0
by Th18, VALUED_1:def 5
;
A10:
for d being Element of REAL st d in right_open_halfline 0 holds
(exp_R * (p (#) ln)) . d = (#R p) . d
proof
let d be
Element of
REAL ;
( d in right_open_halfline 0 implies (exp_R * (p (#) ln)) . d = (#R p) . d )
assume A11:
d in right_open_halfline 0
;
(exp_R * (p (#) ln)) . d = (#R p) . d
A12:
d in dom (p (#) ln)
by A11, Th18, VALUED_1:def 5;
d in { g where g is Real : 0 < g }
by A11, XXREAL_1:230;
then A13:
ex
g being
Real st
(
g = d &
g > 0 )
;
thus (exp_R * (p (#) ln)) . d =
(exp_R * (p (#) ln)) /. d
by A9, A11, PARTFUN1:def 6
.=
exp_R /. ((p (#) ln) /. d)
by A9, A11, PARTFUN2:3
.=
exp_R . ((p (#) ln) . d)
by A12, PARTFUN1:def 6
.=
exp_R . (p * (ln . d))
by A12, VALUED_1:def 5
.=
exp_R . (p * (log (number_e,d)))
by A11, Def2
.=
exp_R . (log (number_e,(d to_power p)))
by A13, Lm4, POWER:55
.=
d to_power p
by A13, Th15, POWER:34
.=
d #R p
by A13, POWER:def 2
.=
(#R p) . d
by A11, Def4
;
verum
end;
dom (#R p) = right_open_halfline 0
by Def4;
then
( x is Real & exp_R * (p (#) ln) = #R p )
by A9, A10, PARTFUN1:5;
hence
( x > 0 implies ( #R p is_differentiable_in x & diff ((#R p),x) = p * (x #R (p - 1)) ) )
by A1; verum