let Z be open Subset of REAL; 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; ( 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 )
; ( (- 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:
for x being Real st x in Z holds
f . x = (0 * x) + 1
by A2;
A4:
Z c= dom ((#R (1 / 2)) * (f + cos))
by A1, VALUED_1:def 5;
then
for y being object st y in Z holds
y in dom (f + cos)
by FUNCT_1:11;
then A5:
Z c= dom (f + cos)
by TARSKI:def 3;
then
Z c= (dom cos) /\ (dom f)
by VALUED_1:def 1;
then A6:
Z c= dom f
by XBOOLE_1:18;
then A7:
f is_differentiable_on Z
by A3, FDIFF_1:23;
A8:
cos is_differentiable_on Z
by FDIFF_1:26, SIN_COS:67;
then A9:
f + cos is_differentiable_on Z
by A5, A7, FDIFF_1:18;
A10:
for x being Real st x in Z holds
(f + cos) . x > 0
then A13:
(#R (1 / 2)) * (f + cos) is_differentiable_on Z
by A4, FDIFF_1:9;
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;
( x in Z implies (((- 2) (#) ((#R (1 / 2)) * (f + cos))) `| Z) . x = (1 - (cos . x)) #R (1 / 2) )
assume A14:
x in Z
;
(((- 2) (#) ((#R (1 / 2)) * (f + cos))) `| Z) . x = (1 - (cos . x)) #R (1 / 2)
then A15:
diff (
(f + cos),
x) =
((f + cos) `| Z) . x
by A9, FDIFF_1:def 7
.=
(diff (f,x)) + (diff (cos,x))
by A5, A7, A8, A14, FDIFF_1:18
.=
((f `| Z) . x) + (diff (cos,x))
by A7, A14, FDIFF_1:def 7
.=
0 + (diff (cos,x))
by A6, A3, A14, FDIFF_1:23
.=
- (sin . x)
by SIN_COS:63
;
A16:
cos . x > - 1
by A2, A14;
A17:
(f + cos) . x =
(f . x) + (cos . x)
by A5, A14, VALUED_1:def 1
.=
1
+ (cos . x)
by A2, A14
;
A18:
(
f + cos is_differentiable_in x &
(f + cos) . x > 0 )
by A9, A10, A14, FDIFF_1:9;
A19:
(
sin . x > 0 &
cos . x < 1 )
by A2, A14;
(((- 2) (#) ((#R (1 / 2)) * (f + cos))) `| Z) . x =
(- 2) * (diff (((#R (1 / 2)) * (f + cos)),x))
by A1, A13, A14, FDIFF_1:20
.=
(- 2) * (((1 / 2) * (((f + cos) . x) #R ((1 / 2) - 1))) * (diff ((f + cos),x)))
by A18, TAYLOR_1:22
.=
- (- ((sin . x) * ((1 + (cos . x)) #R (- (1 / 2)))))
by A17, A15
.=
(sin . x) * (1 / ((1 + (cos . x)) #R (1 / 2)))
by A10, A14, A17, PREPOWER:76
.=
(sin . x) / ((1 + (cos . x)) #R (1 / 2))
by XCMPLX_1:99
.=
(1 - (cos . x)) #R (1 / 2)
by A19, A16, Lm5
;
hence
(((- 2) (#) ((#R (1 / 2)) * (f + cos))) `| Z) . x = (1 - (cos . x)) #R (1 / 2)
;
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, A13, FDIFF_1:20; verum