let Z be open Subset of REAL ; :: thesis: for f being PartFunc of REAL ,REAL st Z c= dom ((- 2) (#) ((#R (1 / 2)) * (f + cos ))) & ( for x being Real st x in Z holds
( f . x = 1 & sin . x > 0 & cos . x < 1 & cos . x > - 1 ) ) holds
( (- 2) (#) ((#R (1 / 2)) * (f + cos )) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- 2) (#) ((#R (1 / 2)) * (f + cos ))) `| Z) . x = (1 - (cos . x)) #R (1 / 2) ) )
let f be PartFunc of REAL ,REAL ; :: thesis: ( Z c= dom ((- 2) (#) ((#R (1 / 2)) * (f + cos ))) & ( for x being Real st x in Z holds
( f . x = 1 & sin . x > 0 & cos . x < 1 & cos . x > - 1 ) ) implies ( (- 2) (#) ((#R (1 / 2)) * (f + cos )) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- 2) (#) ((#R (1 / 2)) * (f + cos ))) `| Z) . x = (1 - (cos . x)) #R (1 / 2) ) ) )
assume that
A1:
Z c= dom ((- 2) (#) ((#R (1 / 2)) * (f + cos )))
and
A2:
for x being Real st x in Z holds
( f . x = 1 & sin . x > 0 & cos . x < 1 & cos . x > - 1 )
; :: thesis: ( (- 2) (#) ((#R (1 / 2)) * (f + cos )) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- 2) (#) ((#R (1 / 2)) * (f + cos ))) `| Z) . x = (1 - (cos . x)) #R (1 / 2) ) )
A3:
Z c= dom ((#R (1 / 2)) * (f + cos ))
by A1, VALUED_1:def 5;
then
for y being set st y in Z holds
y in dom (f + cos )
by FUNCT_1:21;
then A4:
Z c= dom (f + cos )
by TARSKI:def 3;
then
Z c= (dom cos ) /\ (dom f)
by VALUED_1:def 1;
then A5:
Z c= dom f
by XBOOLE_1:18;
A6:
for x being Real st x in Z holds
f . x = (0 * x) + 1
by A2;
then A7:
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 0 ) )
by A5, FDIFF_1:31;
A8:
cos is_differentiable_on Z
by FDIFF_1:34, SIN_COS:72;
then A9:
f + cos is_differentiable_on Z
by A4, A7, FDIFF_1:26;
A10:
for x being Real st x in Z holds
(f + cos ) . x > 0
then A15:
(#R (1 / 2)) * (f + cos ) is_differentiable_on Z
by A3, FDIFF_1:16;
for x being Real st x in Z holds
(((- 2) (#) ((#R (1 / 2)) * (f + cos ))) `| Z) . x = (1 - (cos . x)) #R (1 / 2)
proof
let x be
Real;
:: thesis: ( x in Z implies (((- 2) (#) ((#R (1 / 2)) * (f + cos ))) `| Z) . x = (1 - (cos . x)) #R (1 / 2) )
assume A16:
x in Z
;
:: thesis: (((- 2) (#) ((#R (1 / 2)) * (f + cos ))) `| Z) . x = (1 - (cos . x)) #R (1 / 2)
then A17:
f + cos is_differentiable_in x
by A9, FDIFF_1:16;
A18:
(f + cos ) . x > 0
by A10, A16;
A19:
(f + cos ) . x =
(f . x) + (cos . x)
by A4, A16, VALUED_1:def 1
.=
1
+ (cos . x)
by A2, A16
;
A20:
diff (f + cos ),
x =
((f + cos ) `| Z) . x
by A9, A16, FDIFF_1:def 8
.=
(diff f,x) + (diff cos ,x)
by A4, A7, A8, A16, FDIFF_1:26
.=
((f `| Z) . x) + (diff cos ,x)
by A7, A16, FDIFF_1:def 8
.=
0 + (diff cos ,x)
by A5, A6, A16, FDIFF_1:31
.=
- (sin . x)
by SIN_COS:68
;
A21:
(
sin . x > 0 &
cos . x < 1 &
cos . x > - 1 )
by A2, A16;
(((- 2) (#) ((#R (1 / 2)) * (f + cos ))) `| Z) . x =
(- 2) * (diff ((#R (1 / 2)) * (f + cos )),x)
by A1, A15, A16, FDIFF_1:28
.=
(- 2) * (((1 / 2) * (((f + cos ) . x) #R ((1 / 2) - 1))) * (diff (f + cos ),x))
by A17, A18, TAYLOR_1:22
.=
- (- ((sin . x) * ((1 + (cos . x)) #R (- (1 / 2)))))
by A19, A20
.=
(sin . x) * (1 / ((1 + (cos . x)) #R (1 / 2)))
by A10, A16, A19, PREPOWER:90
.=
(sin . x) / ((1 + (cos . x)) #R (1 / 2))
by XCMPLX_1:100
.=
(1 - (cos . x)) #R (1 / 2)
by A21, Lm5
;
hence
(((- 2) (#) ((#R (1 / 2)) * (f + cos ))) `| Z) . x = (1 - (cos . x)) #R (1 / 2)
;
:: thesis: verum
end;
hence
( (- 2) (#) ((#R (1 / 2)) * (f + cos )) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- 2) (#) ((#R (1 / 2)) * (f + cos ))) `| Z) . x = (1 - (cos . x)) #R (1 / 2) ) )
by A1, A15, FDIFF_1:28; :: thesis: verum