let a, b, c be Real; for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom (cosec * (f1 + (c (#) f2))) & f2 = #Z 2 & ( for x being Real st x in Z holds
f1 . x = a + (b * x) ) holds
( cosec * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * (f1 + (c (#) f2))) `| Z) . x = - (((b + ((2 * c) * x)) * (cos . ((a + (b * x)) + (c * (x ^2))))) / ((sin . ((a + (b * x)) + (c * (x ^2)))) ^2)) ) )
let Z be open Subset of REAL; for f1, f2 being PartFunc of REAL,REAL st Z c= dom (cosec * (f1 + (c (#) f2))) & f2 = #Z 2 & ( for x being Real st x in Z holds
f1 . x = a + (b * x) ) holds
( cosec * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * (f1 + (c (#) f2))) `| Z) . x = - (((b + ((2 * c) * x)) * (cos . ((a + (b * x)) + (c * (x ^2))))) / ((sin . ((a + (b * x)) + (c * (x ^2)))) ^2)) ) )
let f1, f2 be PartFunc of REAL,REAL; ( Z c= dom (cosec * (f1 + (c (#) f2))) & f2 = #Z 2 & ( for x being Real st x in Z holds
f1 . x = a + (b * x) ) implies ( cosec * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * (f1 + (c (#) f2))) `| Z) . x = - (((b + ((2 * c) * x)) * (cos . ((a + (b * x)) + (c * (x ^2))))) / ((sin . ((a + (b * x)) + (c * (x ^2)))) ^2)) ) ) )
assume that
A1:
Z c= dom (cosec * (f1 + (c (#) f2)))
and
A2:
f2 = #Z 2
and
A3:
for x being Real st x in Z holds
f1 . x = a + (b * x)
; ( cosec * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * (f1 + (c (#) f2))) `| Z) . x = - (((b + ((2 * c) * x)) * (cos . ((a + (b * x)) + (c * (x ^2))))) / ((sin . ((a + (b * x)) + (c * (x ^2)))) ^2)) ) )
dom (cosec * (f1 + (c (#) f2))) c= dom (f1 + (c (#) f2))
by RELAT_1:25;
then A4:
Z c= dom (f1 + (c (#) f2))
by A1, XBOOLE_1:1;
then A5:
f1 + (c (#) f2) is_differentiable_on Z
by A2, A3, FDIFF_4:12;
Z c= (dom f1) /\ (dom (c (#) f2))
by A4, VALUED_1:def 1;
then A6:
Z c= dom (c (#) f2)
by XBOOLE_1:18;
A7:
for x being Real st x in Z holds
sin . ((f1 + (c (#) f2)) . x) <> 0
A8:
for x being Real st x in Z holds
cosec * (f1 + (c (#) f2)) is_differentiable_in x
then A11:
cosec * (f1 + (c (#) f2)) is_differentiable_on Z
by A1, FDIFF_1:9;
for x being Real st x in Z holds
((cosec * (f1 + (c (#) f2))) `| Z) . x = - (((b + ((2 * c) * x)) * (cos . ((a + (b * x)) + (c * (x ^2))))) / ((sin . ((a + (b * x)) + (c * (x ^2)))) ^2))
proof
let x be
Real;
( x in Z implies ((cosec * (f1 + (c (#) f2))) `| Z) . x = - (((b + ((2 * c) * x)) * (cos . ((a + (b * x)) + (c * (x ^2))))) / ((sin . ((a + (b * x)) + (c * (x ^2)))) ^2)) )
assume A12:
x in Z
;
((cosec * (f1 + (c (#) f2))) `| Z) . x = - (((b + ((2 * c) * x)) * (cos . ((a + (b * x)) + (c * (x ^2))))) / ((sin . ((a + (b * x)) + (c * (x ^2)))) ^2))
then A13:
(f1 + (c (#) f2)) . x =
(f1 . x) + ((c (#) f2) . x)
by A4, VALUED_1:def 1
.=
(f1 . x) + (c * (f2 . x))
by A6, A12, VALUED_1:def 5
.=
(a + (b * x)) + (c * (f2 . x))
by A3, A12
.=
(a + (b * x)) + (c * (x #Z 2))
by A2, TAYLOR_1:def 1
.=
(a + (b * x)) + (c * (x |^ 2))
by PREPOWER:36
.=
(a + (b * x)) + (c * (x ^2))
by NEWTON:81
;
A14:
f1 + (c (#) f2) is_differentiable_in x
by A5, A12, FDIFF_1:9;
A15:
sin . ((f1 + (c (#) f2)) . x) <> 0
by A7, A12;
then
cosec is_differentiable_in (f1 + (c (#) f2)) . x
by Th2;
then diff (
(cosec * (f1 + (c (#) f2))),
x) =
(diff (cosec,((f1 + (c (#) f2)) . x))) * (diff ((f1 + (c (#) f2)),x))
by A14, FDIFF_2:13
.=
(- ((cos . ((f1 + (c (#) f2)) . x)) / ((sin . ((f1 + (c (#) f2)) . x)) ^2))) * (diff ((f1 + (c (#) f2)),x))
by A15, Th2
.=
(((f1 + (c (#) f2)) `| Z) . x) * (- ((cos . ((a + (b * x)) + (c * (x ^2)))) / ((sin . ((a + (b * x)) + (c * (x ^2)))) ^2)))
by A5, A12, A13, FDIFF_1:def 7
.=
(b + ((2 * c) * x)) * (- ((cos . ((a + (b * x)) + (c * (x ^2)))) / ((sin . ((a + (b * x)) + (c * (x ^2)))) ^2)))
by A2, A3, A4, A12, FDIFF_4:12
;
hence
((cosec * (f1 + (c (#) f2))) `| Z) . x = - (((b + ((2 * c) * x)) * (cos . ((a + (b * x)) + (c * (x ^2))))) / ((sin . ((a + (b * x)) + (c * (x ^2)))) ^2))
by A11, A12, FDIFF_1:def 7;
verum
end;
hence
( cosec * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * (f1 + (c (#) f2))) `| Z) . x = - (((b + ((2 * c) * x)) * (cos . ((a + (b * x)) + (c * (x ^2))))) / ((sin . ((a + (b * x)) + (c * (x ^2)))) ^2)) ) )
by A1, A8, FDIFF_1:9; verum