:: FDIFF_8 semantic presentation begin theorem Th1: :: FDIFF_8:1 for x being Real st x in dom tan holds cos . x <> 0 proof let x be Real; ::_thesis: ( x in dom tan implies cos . x <> 0 ) assume x in dom tan ; ::_thesis: cos . x <> 0 then x in (dom sin) /\ ((dom cos) \ (cos " {0})) by RFUNCT_1:def_1; then x in (dom cos) \ (cos " {0}) by XBOOLE_0:def_4; then x in dom (cos ^) by RFUNCT_1:def_2; hence cos . x <> 0 by RFUNCT_1:3; ::_thesis: verum end; theorem Th2: :: FDIFF_8:2 for x being Real st x in dom cot holds sin . x <> 0 proof let x be Real; ::_thesis: ( x in dom cot implies sin . x <> 0 ) assume x in dom cot ; ::_thesis: sin . x <> 0 then x in (dom cos) /\ ((dom sin) \ (sin " {0})) by RFUNCT_1:def_1; then x in (dom sin) \ (sin " {0}) by XBOOLE_0:def_4; then x in dom (sin ^) by RFUNCT_1:def_2; hence sin . x <> 0 by RFUNCT_1:3; ::_thesis: verum end; theorem Th3: :: FDIFF_8:3 for n being Nat for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 / f2) holds for x being Real st x in Z holds ((f1 / f2) . x) #Z n = ((f1 . x) #Z n) / ((f2 . x) #Z n) proof let n be Nat; ::_thesis: for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 / f2) holds for x being Real st x in Z holds ((f1 / f2) . x) #Z n = ((f1 . x) #Z n) / ((f2 . x) #Z n) let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 / f2) holds for x being Real st x in Z holds ((f1 / f2) . x) #Z n = ((f1 . x) #Z n) / ((f2 . x) #Z n) let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (f1 / f2) implies for x being Real st x in Z holds ((f1 / f2) . x) #Z n = ((f1 . x) #Z n) / ((f2 . x) #Z n) ) assume A1: Z c= dom (f1 / f2) ; ::_thesis: for x being Real st x in Z holds ((f1 / f2) . x) #Z n = ((f1 . x) #Z n) / ((f2 . x) #Z n) let x be Real; ::_thesis: ( x in Z implies ((f1 / f2) . x) #Z n = ((f1 . x) #Z n) / ((f2 . x) #Z n) ) assume x in Z ; ::_thesis: ((f1 / f2) . x) #Z n = ((f1 . x) #Z n) / ((f2 . x) #Z n) then ((f1 / f2) . x) #Z n = ((f1 . x) / (f2 . x)) #Z n by A1, RFUNCT_1:def_1 .= ((f1 . x) / (f2 . x)) |^ n by PREPOWER:36 .= ((f1 . x) |^ n) / ((f2 . x) |^ n) by PREPOWER:8 .= ((f1 . x) #Z n) / ((f2 . x) |^ n) by PREPOWER:36 .= ((f1 . x) #Z n) / ((f2 . x) #Z n) by PREPOWER:36 ; hence ((f1 / f2) . x) #Z n = ((f1 . x) #Z n) / ((f2 . x) #Z n) ; ::_thesis: verum end; theorem :: FDIFF_8:4 for a, b being Real for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 / f2) & ( for x being Real st x in Z holds ( f1 . x = x + a & f2 . x = x - b ) ) holds ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 / f2) `| Z) . x = ((- a) - b) / ((x - b) ^2) ) ) proof let a, b be Real; ::_thesis: for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 / f2) & ( for x being Real st x in Z holds ( f1 . x = x + a & f2 . x = x - b ) ) holds ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 / f2) `| Z) . x = ((- a) - b) / ((x - b) ^2) ) ) let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 / f2) & ( for x being Real st x in Z holds ( f1 . x = x + a & f2 . x = x - b ) ) holds ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 / f2) `| Z) . x = ((- a) - b) / ((x - b) ^2) ) ) let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (f1 / f2) & ( for x being Real st x in Z holds ( f1 . x = x + a & f2 . x = x - b ) ) implies ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 / f2) `| Z) . x = ((- a) - b) / ((x - b) ^2) ) ) ) assume that A1: Z c= dom (f1 / f2) and A2: for x being Real st x in Z holds ( f1 . x = x + a & f2 . x = x - b ) ; ::_thesis: ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 / f2) `| Z) . x = ((- a) - b) / ((x - b) ^2) ) ) Z c= (dom f1) /\ ((dom f2) \ (f2 " {0})) by A1, RFUNCT_1:def_1; then A3: Z c= (dom f2) \ (f2 " {0}) by XBOOLE_1:18; for x being Real st x in Z holds f2 . x <> 0 proof let x be Real; ::_thesis: ( x in Z implies f2 . x <> 0 ) assume x in Z ; ::_thesis: f2 . x <> 0 then x in (dom f2) \ (f2 " {0}) by A3; then x in dom (f2 ^) by RFUNCT_1:def_2; hence f2 . x <> 0 by RFUNCT_1:3; ::_thesis: verum end; then for x being Real st x in Z holds ( f1 . x = x - (- a) & f2 . x = x - b & f2 . x <> 0 ) by A2; hence ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 / f2) `| Z) . x = ((- a) - b) / ((x - b) ^2) ) ) by A1, FDIFF_5:3; ::_thesis: verum end; Lm1: right_open_halfline 0 = { g where g is Real : 0 < g } by XXREAL_1:230; theorem :: FDIFF_8:5 for Z being open Subset of REAL st not 0 in Z & Z c= dom (ln * ((id Z) ^)) holds ( ln * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * ((id Z) ^)) `| Z) . x = - (1 / x) ) ) proof let Z be open Subset of REAL; ::_thesis: ( not 0 in Z & Z c= dom (ln * ((id Z) ^)) implies ( ln * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * ((id Z) ^)) `| Z) . x = - (1 / x) ) ) ) set f = id Z; assume that A1: not 0 in Z and A2: Z c= dom (ln * ((id Z) ^)) ; ::_thesis: ( ln * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * ((id Z) ^)) `| Z) . x = - (1 / x) ) ) dom (ln * ((id Z) ^)) c= dom ((id Z) ^) by RELAT_1:25; then A3: Z c= dom ((id Z) ^) by A2, XBOOLE_1:1; A4: for x being Real st x in Z holds ((id Z) ^) . x > 0 proof let x be Real; ::_thesis: ( x in Z implies ((id Z) ^) . x > 0 ) assume A5: x in Z ; ::_thesis: ((id Z) ^) . x > 0 then A6: ((id Z) ^) . x = ((id Z) . x) " by A3, RFUNCT_1:def_2 .= 1 / x by A5, FUNCT_1:18 ; ((id Z) ^) . x in right_open_halfline 0 by A2, A5, FUNCT_1:11, TAYLOR_1:18; then ex g being Real st ( 1 / x = g & 0 < g ) by A6, Lm1; hence ((id Z) ^) . x > 0 by A6; ::_thesis: verum end; A7: for x being Real st x in Z holds (id Z) . x > 0 proof let x be Real; ::_thesis: ( x in Z implies (id Z) . x > 0 ) assume A8: x in Z ; ::_thesis: (id Z) . x > 0 then ((id Z) ^) . x > 0 by A4; then ((id Z) . x) " > 0 by A3, A8, RFUNCT_1:def_2; hence (id Z) . x > 0 by XREAL_1:122; ::_thesis: verum end; A9: (id Z) ^ is_differentiable_on Z by A1, FDIFF_5:4; A10: for x being Real st x in Z holds ( ln * ((id Z) ^) is_differentiable_in x & diff ((ln * ((id Z) ^)),x) = (diff (((id Z) ^),x)) / (((id Z) ^) . x) ) proof let x be Real; ::_thesis: ( x in Z implies ( ln * ((id Z) ^) is_differentiable_in x & diff ((ln * ((id Z) ^)),x) = (diff (((id Z) ^),x)) / (((id Z) ^) . x) ) ) assume x in Z ; ::_thesis: ( ln * ((id Z) ^) is_differentiable_in x & diff ((ln * ((id Z) ^)),x) = (diff (((id Z) ^),x)) / (((id Z) ^) . x) ) then ( (id Z) ^ is_differentiable_in x & ((id Z) ^) . x > 0 ) by A4, A9, FDIFF_1:9; hence ( ln * ((id Z) ^) is_differentiable_in x & diff ((ln * ((id Z) ^)),x) = (diff (((id Z) ^),x)) / (((id Z) ^) . x) ) by TAYLOR_1:20; ::_thesis: verum end; then A11: for x being Real st x in Z holds ln * ((id Z) ^) is_differentiable_in x ; then A12: ln * ((id Z) ^) is_differentiable_on Z by A2, FDIFF_1:9; for x being Real st x in Z holds ((ln * ((id Z) ^)) `| Z) . x = - (1 / x) proof let x be Real; ::_thesis: ( x in Z implies ((ln * ((id Z) ^)) `| Z) . x = - (1 / x) ) assume A13: x in Z ; ::_thesis: ((ln * ((id Z) ^)) `| Z) . x = - (1 / x) then (id Z) . x <> 0 by A7; then A14: x <> 0 by A13, FUNCT_1:18; diff ((ln * ((id Z) ^)),x) = (diff (((id Z) ^),x)) / (((id Z) ^) . x) by A10, A13 .= ((((id Z) ^) `| Z) . x) / (((id Z) ^) . x) by A9, A13, FDIFF_1:def_7 .= ((((id Z) ^) `| Z) . x) / (((id Z) . x) ") by A3, A13, RFUNCT_1:def_2 .= ((((id Z) ^) `| Z) . x) / (1 * (x ")) by A13, FUNCT_1:18 .= (- (1 / (x ^2))) / (1 * (x ")) by A1, A13, FDIFF_5:4 .= - (x / (x ^2)) .= - ((x / x) / x) by XCMPLX_1:78 .= - (1 / x) by A14, XCMPLX_1:60 ; hence ((ln * ((id Z) ^)) `| Z) . x = - (1 / x) by A12, A13, FDIFF_1:def_7; ::_thesis: verum end; hence ( ln * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * ((id Z) ^)) `| Z) . x = - (1 / x) ) ) by A2, A11, FDIFF_1:9; ::_thesis: verum end; theorem Th6: :: FDIFF_8:6 for a, b being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (tan * f) & ( for x being Real st x in Z holds f . x = (a * x) + b ) holds ( tan * f is_differentiable_on Z & ( for x being Real st x in Z holds ((tan * f) `| Z) . x = a / ((cos . ((a * x) + b)) ^2) ) ) proof let a, b be Real; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (tan * f) & ( for x being Real st x in Z holds f . x = (a * x) + b ) holds ( tan * f is_differentiable_on Z & ( for x being Real st x in Z holds ((tan * f) `| Z) . x = a / ((cos . ((a * x) + b)) ^2) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom (tan * f) & ( for x being Real st x in Z holds f . x = (a * x) + b ) holds ( tan * f is_differentiable_on Z & ( for x being Real st x in Z holds ((tan * f) `| Z) . x = a / ((cos . ((a * x) + b)) ^2) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (tan * f) & ( for x being Real st x in Z holds f . x = (a * x) + b ) implies ( tan * f is_differentiable_on Z & ( for x being Real st x in Z holds ((tan * f) `| Z) . x = a / ((cos . ((a * x) + b)) ^2) ) ) ) assume that A1: Z c= dom (tan * f) and A2: for x being Real st x in Z holds f . x = (a * x) + b ; ::_thesis: ( tan * f is_differentiable_on Z & ( for x being Real st x in Z holds ((tan * f) `| Z) . x = a / ((cos . ((a * x) + b)) ^2) ) ) dom (tan * f) c= dom f by RELAT_1:25; then A3: Z c= dom f by A1, XBOOLE_1:1; then A4: f is_differentiable_on Z by A2, FDIFF_1:23; A5: for x being Real st x in Z holds cos . (f . x) <> 0 proof let x be Real; ::_thesis: ( x in Z implies cos . (f . x) <> 0 ) assume x in Z ; ::_thesis: cos . (f . x) <> 0 then f . x in dom (sin / cos) by A1, FUNCT_1:11; hence cos . (f . x) <> 0 by Th1; ::_thesis: verum end; A6: for x being Real st x in Z holds tan * f is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies tan * f is_differentiable_in x ) assume A7: x in Z ; ::_thesis: tan * f is_differentiable_in x then cos . (f . x) <> 0 by A5; then A8: tan is_differentiable_in f . x by FDIFF_7:46; f is_differentiable_in x by A4, A7, FDIFF_1:9; hence tan * f is_differentiable_in x by A8, FDIFF_2:13; ::_thesis: verum end; then A9: tan * f is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((tan * f) `| Z) . x = a / ((cos . ((a * x) + b)) ^2) proof let x be Real; ::_thesis: ( x in Z implies ((tan * f) `| Z) . x = a / ((cos . ((a * x) + b)) ^2) ) assume A10: x in Z ; ::_thesis: ((tan * f) `| Z) . x = a / ((cos . ((a * x) + b)) ^2) then A11: f is_differentiable_in x by A4, FDIFF_1:9; A12: cos . (f . x) <> 0 by A5, A10; then tan is_differentiable_in f . x by FDIFF_7:46; then diff ((tan * f),x) = (diff (tan,(f . x))) * (diff (f,x)) by A11, FDIFF_2:13 .= (1 / ((cos . (f . x)) ^2)) * (diff (f,x)) by A12, FDIFF_7:46 .= (diff (f,x)) / ((cos . ((a * x) + b)) ^2) by A2, A10 .= ((f `| Z) . x) / ((cos . ((a * x) + b)) ^2) by A4, A10, FDIFF_1:def_7 .= a / ((cos . ((a * x) + b)) ^2) by A2, A3, A10, FDIFF_1:23 ; hence ((tan * f) `| Z) . x = a / ((cos . ((a * x) + b)) ^2) by A9, A10, FDIFF_1:def_7; ::_thesis: verum end; hence ( tan * f is_differentiable_on Z & ( for x being Real st x in Z holds ((tan * f) `| Z) . x = a / ((cos . ((a * x) + b)) ^2) ) ) by A1, A6, FDIFF_1:9; ::_thesis: verum end; theorem Th7: :: FDIFF_8:7 for a, b being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (cot * f) & ( for x being Real st x in Z holds f . x = (a * x) + b ) holds ( cot * f is_differentiable_on Z & ( for x being Real st x in Z holds ((cot * f) `| Z) . x = - (a / ((sin . ((a * x) + b)) ^2)) ) ) proof let a, b be Real; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (cot * f) & ( for x being Real st x in Z holds f . x = (a * x) + b ) holds ( cot * f is_differentiable_on Z & ( for x being Real st x in Z holds ((cot * f) `| Z) . x = - (a / ((sin . ((a * x) + b)) ^2)) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom (cot * f) & ( for x being Real st x in Z holds f . x = (a * x) + b ) holds ( cot * f is_differentiable_on Z & ( for x being Real st x in Z holds ((cot * f) `| Z) . x = - (a / ((sin . ((a * x) + b)) ^2)) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (cot * f) & ( for x being Real st x in Z holds f . x = (a * x) + b ) implies ( cot * f is_differentiable_on Z & ( for x being Real st x in Z holds ((cot * f) `| Z) . x = - (a / ((sin . ((a * x) + b)) ^2)) ) ) ) assume that A1: Z c= dom (cot * f) and A2: for x being Real st x in Z holds f . x = (a * x) + b ; ::_thesis: ( cot * f is_differentiable_on Z & ( for x being Real st x in Z holds ((cot * f) `| Z) . x = - (a / ((sin . ((a * x) + b)) ^2)) ) ) dom (cot * f) c= dom f by RELAT_1:25; then A3: Z c= dom f by A1, XBOOLE_1:1; then A4: f is_differentiable_on Z by A2, FDIFF_1:23; A5: for x being Real st x in Z holds sin . (f . x) <> 0 proof let x be Real; ::_thesis: ( x in Z implies sin . (f . x) <> 0 ) assume x in Z ; ::_thesis: sin . (f . x) <> 0 then f . x in dom (cos / sin) by A1, FUNCT_1:11; hence sin . (f . x) <> 0 by Th2; ::_thesis: verum end; A6: for x being Real st x in Z holds cot * f is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies cot * f is_differentiable_in x ) assume A7: x in Z ; ::_thesis: cot * f is_differentiable_in x then sin . (f . x) <> 0 by A5; then A8: cot is_differentiable_in f . x by FDIFF_7:47; f is_differentiable_in x by A4, A7, FDIFF_1:9; hence cot * f is_differentiable_in x by A8, FDIFF_2:13; ::_thesis: verum end; then A9: cot * f is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((cot * f) `| Z) . x = - (a / ((sin . ((a * x) + b)) ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((cot * f) `| Z) . x = - (a / ((sin . ((a * x) + b)) ^2)) ) assume A10: x in Z ; ::_thesis: ((cot * f) `| Z) . x = - (a / ((sin . ((a * x) + b)) ^2)) then A11: f is_differentiable_in x by A4, FDIFF_1:9; A12: sin . (f . x) <> 0 by A5, A10; then cot is_differentiable_in f . x by FDIFF_7:47; then diff ((cot * f),x) = (diff (cot,(f . x))) * (diff (f,x)) by A11, FDIFF_2:13 .= (- (1 / ((sin . (f . x)) ^2))) * (diff (f,x)) by A12, FDIFF_7:47 .= - ((diff (f,x)) / ((sin . (f . x)) ^2)) .= - ((diff (f,x)) / ((sin . ((a * x) + b)) ^2)) by A2, A10 .= - (((f `| Z) . x) / ((sin . ((a * x) + b)) ^2)) by A4, A10, FDIFF_1:def_7 .= - (a / ((sin . ((a * x) + b)) ^2)) by A2, A3, A10, FDIFF_1:23 ; hence ((cot * f) `| Z) . x = - (a / ((sin . ((a * x) + b)) ^2)) by A9, A10, FDIFF_1:def_7; ::_thesis: verum end; hence ( cot * f is_differentiable_on Z & ( for x being Real st x in Z holds ((cot * f) `| Z) . x = - (a / ((sin . ((a * x) + b)) ^2)) ) ) by A1, A6, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_8:8 for Z being open Subset of REAL st not 0 in Z & Z c= dom (tan * ((id Z) ^)) holds ( tan * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds ((tan * ((id Z) ^)) `| Z) . x = - (1 / ((x ^2) * ((cos . (1 / x)) ^2))) ) ) proof let Z be open Subset of REAL; ::_thesis: ( not 0 in Z & Z c= dom (tan * ((id Z) ^)) implies ( tan * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds ((tan * ((id Z) ^)) `| Z) . x = - (1 / ((x ^2) * ((cos . (1 / x)) ^2))) ) ) ) set f = id Z; assume that A1: not 0 in Z and A2: Z c= dom (tan * ((id Z) ^)) ; ::_thesis: ( tan * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds ((tan * ((id Z) ^)) `| Z) . x = - (1 / ((x ^2) * ((cos . (1 / x)) ^2))) ) ) A3: (id Z) ^ is_differentiable_on Z by A1, FDIFF_5:4; dom (tan * ((id Z) ^)) c= dom ((id Z) ^) by RELAT_1:25; then A4: Z c= dom ((id Z) ^) by A2, XBOOLE_1:1; A5: for x being Real st x in Z holds cos . (((id Z) ^) . x) <> 0 proof let x be Real; ::_thesis: ( x in Z implies cos . (((id Z) ^) . x) <> 0 ) assume x in Z ; ::_thesis: cos . (((id Z) ^) . x) <> 0 then ((id Z) ^) . x in dom (sin / cos) by A2, FUNCT_1:11; hence cos . (((id Z) ^) . x) <> 0 by Th1; ::_thesis: verum end; A6: for x being Real st x in Z holds tan * ((id Z) ^) is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies tan * ((id Z) ^) is_differentiable_in x ) assume A7: x in Z ; ::_thesis: tan * ((id Z) ^) is_differentiable_in x then cos . (((id Z) ^) . x) <> 0 by A5; then A8: tan is_differentiable_in ((id Z) ^) . x by FDIFF_7:46; (id Z) ^ is_differentiable_in x by A3, A7, FDIFF_1:9; hence tan * ((id Z) ^) is_differentiable_in x by A8, FDIFF_2:13; ::_thesis: verum end; then A9: tan * ((id Z) ^) is_differentiable_on Z by A2, FDIFF_1:9; for x being Real st x in Z holds ((tan * ((id Z) ^)) `| Z) . x = - (1 / ((x ^2) * ((cos . (1 / x)) ^2))) proof let x be Real; ::_thesis: ( x in Z implies ((tan * ((id Z) ^)) `| Z) . x = - (1 / ((x ^2) * ((cos . (1 / x)) ^2))) ) assume A10: x in Z ; ::_thesis: ((tan * ((id Z) ^)) `| Z) . x = - (1 / ((x ^2) * ((cos . (1 / x)) ^2))) then A11: (id Z) ^ is_differentiable_in x by A3, FDIFF_1:9; A12: cos . (((id Z) ^) . x) <> 0 by A5, A10; then tan is_differentiable_in ((id Z) ^) . x by FDIFF_7:46; then diff ((tan * ((id Z) ^)),x) = (diff (tan,(((id Z) ^) . x))) * (diff (((id Z) ^),x)) by A11, FDIFF_2:13 .= (1 / ((cos . (((id Z) ^) . x)) ^2)) * (diff (((id Z) ^),x)) by A12, FDIFF_7:46 .= (diff (((id Z) ^),x)) / ((cos . (((id Z) . x) ")) ^2) by A4, A10, RFUNCT_1:def_2 .= (diff (((id Z) ^),x)) / ((cos . (1 * (x "))) ^2) by A10, FUNCT_1:18 .= ((((id Z) ^) `| Z) . x) / ((cos . (1 * (x "))) ^2) by A3, A10, FDIFF_1:def_7 .= (- (1 / (x ^2))) / ((cos . (1 * (x "))) ^2) by A1, A10, FDIFF_5:4 .= ((- 1) / (x ^2)) / ((cos . (1 / x)) ^2) .= (- 1) / ((x ^2) * ((cos . (1 / x)) ^2)) by XCMPLX_1:78 .= - (1 / ((x ^2) * ((cos . (1 / x)) ^2))) ; hence ((tan * ((id Z) ^)) `| Z) . x = - (1 / ((x ^2) * ((cos . (1 / x)) ^2))) by A9, A10, FDIFF_1:def_7; ::_thesis: verum end; hence ( tan * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds ((tan * ((id Z) ^)) `| Z) . x = - (1 / ((x ^2) * ((cos . (1 / x)) ^2))) ) ) by A2, A6, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_8:9 for Z being open Subset of REAL st not 0 in Z & Z c= dom (cot * ((id Z) ^)) holds ( cot * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds ((cot * ((id Z) ^)) `| Z) . x = 1 / ((x ^2) * ((sin . (1 / x)) ^2)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( not 0 in Z & Z c= dom (cot * ((id Z) ^)) implies ( cot * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds ((cot * ((id Z) ^)) `| Z) . x = 1 / ((x ^2) * ((sin . (1 / x)) ^2)) ) ) ) set f = id Z; assume that A1: not 0 in Z and A2: Z c= dom (cot * ((id Z) ^)) ; ::_thesis: ( cot * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds ((cot * ((id Z) ^)) `| Z) . x = 1 / ((x ^2) * ((sin . (1 / x)) ^2)) ) ) A3: (id Z) ^ is_differentiable_on Z by A1, FDIFF_5:4; dom (cot * ((id Z) ^)) c= dom ((id Z) ^) by RELAT_1:25; then A4: Z c= dom ((id Z) ^) by A2, XBOOLE_1:1; A5: for x being Real st x in Z holds sin . (((id Z) ^) . x) <> 0 proof let x be Real; ::_thesis: ( x in Z implies sin . (((id Z) ^) . x) <> 0 ) assume x in Z ; ::_thesis: sin . (((id Z) ^) . x) <> 0 then ((id Z) ^) . x in dom (cos / sin) by A2, FUNCT_1:11; hence sin . (((id Z) ^) . x) <> 0 by Th2; ::_thesis: verum end; A6: for x being Real st x in Z holds cot * ((id Z) ^) is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies cot * ((id Z) ^) is_differentiable_in x ) assume A7: x in Z ; ::_thesis: cot * ((id Z) ^) is_differentiable_in x then sin . (((id Z) ^) . x) <> 0 by A5; then A8: cot is_differentiable_in ((id Z) ^) . x by FDIFF_7:47; (id Z) ^ is_differentiable_in x by A3, A7, FDIFF_1:9; hence cot * ((id Z) ^) is_differentiable_in x by A8, FDIFF_2:13; ::_thesis: verum end; then A9: cot * ((id Z) ^) is_differentiable_on Z by A2, FDIFF_1:9; for x being Real st x in Z holds ((cot * ((id Z) ^)) `| Z) . x = 1 / ((x ^2) * ((sin . (1 / x)) ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((cot * ((id Z) ^)) `| Z) . x = 1 / ((x ^2) * ((sin . (1 / x)) ^2)) ) assume A10: x in Z ; ::_thesis: ((cot * ((id Z) ^)) `| Z) . x = 1 / ((x ^2) * ((sin . (1 / x)) ^2)) then A11: (id Z) ^ is_differentiable_in x by A3, FDIFF_1:9; A12: sin . (((id Z) ^) . x) <> 0 by A5, A10; then cot is_differentiable_in ((id Z) ^) . x by FDIFF_7:47; then diff ((cot * ((id Z) ^)),x) = (diff (cot,(((id Z) ^) . x))) * (diff (((id Z) ^),x)) by A11, FDIFF_2:13 .= (- (1 / ((sin . (((id Z) ^) . x)) ^2))) * (diff (((id Z) ^),x)) by A12, FDIFF_7:47 .= - ((diff (((id Z) ^),x)) / ((sin . (((id Z) ^) . x)) ^2)) .= - ((diff (((id Z) ^),x)) / ((sin . (((id Z) . x) ")) ^2)) by A4, A10, RFUNCT_1:def_2 .= - ((diff (((id Z) ^),x)) / ((sin . (1 * (x "))) ^2)) by A10, FUNCT_1:18 .= - (((((id Z) ^) `| Z) . x) / ((sin . (1 * (x "))) ^2)) by A3, A10, FDIFF_1:def_7 .= - ((- (1 / (x ^2))) / ((sin . (1 * (x "))) ^2)) by A1, A10, FDIFF_5:4 .= - (((- 1) / (x ^2)) / ((sin . (1 / x)) ^2)) .= - ((- 1) / ((x ^2) * ((sin . (1 / x)) ^2))) by XCMPLX_1:78 .= 1 / ((x ^2) * ((sin . (1 / x)) ^2)) ; hence ((cot * ((id Z) ^)) `| Z) . x = 1 / ((x ^2) * ((sin . (1 / x)) ^2)) by A9, A10, FDIFF_1:def_7; ::_thesis: verum end; hence ( cot * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds ((cot * ((id Z) ^)) `| Z) . x = 1 / ((x ^2) * ((sin . (1 / x)) ^2)) ) ) by A2, A6, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_8:10 for c, a, b being Real for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (tan * (f1 + (c (#) f2))) & f2 = #Z 2 & ( for x being Real st x in Z holds f1 . x = a + (b * x) ) holds ( tan * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((tan * (f1 + (c (#) f2))) `| Z) . x = (b + ((2 * c) * x)) / ((cos . ((a + (b * x)) + (c * (x ^2)))) ^2) ) ) proof let c, a, b be Real; ::_thesis: for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (tan * (f1 + (c (#) f2))) & f2 = #Z 2 & ( for x being Real st x in Z holds f1 . x = a + (b * x) ) holds ( tan * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((tan * (f1 + (c (#) f2))) `| Z) . x = (b + ((2 * c) * x)) / ((cos . ((a + (b * x)) + (c * (x ^2)))) ^2) ) ) let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st Z c= dom (tan * (f1 + (c (#) f2))) & f2 = #Z 2 & ( for x being Real st x in Z holds f1 . x = a + (b * x) ) holds ( tan * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((tan * (f1 + (c (#) f2))) `| Z) . x = (b + ((2 * c) * x)) / ((cos . ((a + (b * x)) + (c * (x ^2)))) ^2) ) ) let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (tan * (f1 + (c (#) f2))) & f2 = #Z 2 & ( for x being Real st x in Z holds f1 . x = a + (b * x) ) implies ( tan * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((tan * (f1 + (c (#) f2))) `| Z) . x = (b + ((2 * c) * x)) / ((cos . ((a + (b * x)) + (c * (x ^2)))) ^2) ) ) ) assume that A1: Z c= dom (tan * (f1 + (c (#) f2))) and A2: f2 = #Z 2 and A3: for x being Real st x in Z holds f1 . x = a + (b * x) ; ::_thesis: ( tan * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((tan * (f1 + (c (#) f2))) `| Z) . x = (b + ((2 * c) * x)) / ((cos . ((a + (b * x)) + (c * (x ^2)))) ^2) ) ) dom (tan * (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 cos . ((f1 + (c (#) f2)) . x) <> 0 proof let x be Real; ::_thesis: ( x in Z implies cos . ((f1 + (c (#) f2)) . x) <> 0 ) assume x in Z ; ::_thesis: cos . ((f1 + (c (#) f2)) . x) <> 0 then (f1 + (c (#) f2)) . x in dom (sin / cos) by A1, FUNCT_1:11; hence cos . ((f1 + (c (#) f2)) . x) <> 0 by Th1; ::_thesis: verum end; A8: for x being Real st x in Z holds tan * (f1 + (c (#) f2)) is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies tan * (f1 + (c (#) f2)) is_differentiable_in x ) assume A9: x in Z ; ::_thesis: tan * (f1 + (c (#) f2)) is_differentiable_in x then cos . ((f1 + (c (#) f2)) . x) <> 0 by A7; then A10: tan is_differentiable_in (f1 + (c (#) f2)) . x by FDIFF_7:46; f1 + (c (#) f2) is_differentiable_in x by A5, A9, FDIFF_1:9; hence tan * (f1 + (c (#) f2)) is_differentiable_in x by A10, FDIFF_2:13; ::_thesis: verum end; then A11: tan * (f1 + (c (#) f2)) is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((tan * (f1 + (c (#) f2))) `| Z) . x = (b + ((2 * c) * x)) / ((cos . ((a + (b * x)) + (c * (x ^2)))) ^2) proof let x be Real; ::_thesis: ( x in Z implies ((tan * (f1 + (c (#) f2))) `| Z) . x = (b + ((2 * c) * x)) / ((cos . ((a + (b * x)) + (c * (x ^2)))) ^2) ) assume A12: x in Z ; ::_thesis: ((tan * (f1 + (c (#) f2))) `| Z) . x = (b + ((2 * c) * x)) / ((cos . ((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: cos . ((f1 + (c (#) f2)) . x) <> 0 by A7, A12; then tan is_differentiable_in (f1 + (c (#) f2)) . x by FDIFF_7:46; then diff ((tan * (f1 + (c (#) f2))),x) = (diff (tan,((f1 + (c (#) f2)) . x))) * (diff ((f1 + (c (#) f2)),x)) by A14, FDIFF_2:13 .= (1 / ((cos . ((f1 + (c (#) f2)) . x)) ^2)) * (diff ((f1 + (c (#) f2)),x)) by A15, FDIFF_7:46 .= (((f1 + (c (#) f2)) `| Z) . x) / ((cos . ((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)))) ^2) by A2, A3, A4, A12, FDIFF_4:12 ; hence ((tan * (f1 + (c (#) f2))) `| Z) . x = (b + ((2 * c) * x)) / ((cos . ((a + (b * x)) + (c * (x ^2)))) ^2) by A11, A12, FDIFF_1:def_7; ::_thesis: verum end; hence ( tan * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((tan * (f1 + (c (#) f2))) `| Z) . x = (b + ((2 * c) * x)) / ((cos . ((a + (b * x)) + (c * (x ^2)))) ^2) ) ) by A1, A8, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_8:11 for c, a, b being Real for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (cot * (f1 + (c (#) f2))) & f2 = #Z 2 & ( for x being Real st x in Z holds f1 . x = a + (b * x) ) holds ( cot * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((cot * (f1 + (c (#) f2))) `| Z) . x = - ((b + ((2 * c) * x)) / ((sin . ((a + (b * x)) + (c * (x ^2)))) ^2)) ) ) proof let c, a, b be Real; ::_thesis: for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (cot * (f1 + (c (#) f2))) & f2 = #Z 2 & ( for x being Real st x in Z holds f1 . x = a + (b * x) ) holds ( cot * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((cot * (f1 + (c (#) f2))) `| Z) . x = - ((b + ((2 * c) * x)) / ((sin . ((a + (b * x)) + (c * (x ^2)))) ^2)) ) ) let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st Z c= dom (cot * (f1 + (c (#) f2))) & f2 = #Z 2 & ( for x being Real st x in Z holds f1 . x = a + (b * x) ) holds ( cot * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((cot * (f1 + (c (#) f2))) `| Z) . x = - ((b + ((2 * c) * x)) / ((sin . ((a + (b * x)) + (c * (x ^2)))) ^2)) ) ) let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (cot * (f1 + (c (#) f2))) & f2 = #Z 2 & ( for x being Real st x in Z holds f1 . x = a + (b * x) ) implies ( cot * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((cot * (f1 + (c (#) f2))) `| Z) . x = - ((b + ((2 * c) * x)) / ((sin . ((a + (b * x)) + (c * (x ^2)))) ^2)) ) ) ) assume that A1: Z c= dom (cot * (f1 + (c (#) f2))) and A2: f2 = #Z 2 and A3: for x being Real st x in Z holds f1 . x = a + (b * x) ; ::_thesis: ( cot * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((cot * (f1 + (c (#) f2))) `| Z) . x = - ((b + ((2 * c) * x)) / ((sin . ((a + (b * x)) + (c * (x ^2)))) ^2)) ) ) dom (cot * (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 proof let x be Real; ::_thesis: ( x in Z implies sin . ((f1 + (c (#) f2)) . x) <> 0 ) assume x in Z ; ::_thesis: sin . ((f1 + (c (#) f2)) . x) <> 0 then (f1 + (c (#) f2)) . x in dom (cos / sin) by A1, FUNCT_1:11; hence sin . ((f1 + (c (#) f2)) . x) <> 0 by Th2; ::_thesis: verum end; A8: for x being Real st x in Z holds cot * (f1 + (c (#) f2)) is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies cot * (f1 + (c (#) f2)) is_differentiable_in x ) assume A9: x in Z ; ::_thesis: cot * (f1 + (c (#) f2)) is_differentiable_in x then sin . ((f1 + (c (#) f2)) . x) <> 0 by A7; then A10: cot is_differentiable_in (f1 + (c (#) f2)) . x by FDIFF_7:47; f1 + (c (#) f2) is_differentiable_in x by A5, A9, FDIFF_1:9; hence cot * (f1 + (c (#) f2)) is_differentiable_in x by A10, FDIFF_2:13; ::_thesis: verum end; then A11: cot * (f1 + (c (#) f2)) is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((cot * (f1 + (c (#) f2))) `| Z) . x = - ((b + ((2 * c) * x)) / ((sin . ((a + (b * x)) + (c * (x ^2)))) ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((cot * (f1 + (c (#) f2))) `| Z) . x = - ((b + ((2 * c) * x)) / ((sin . ((a + (b * x)) + (c * (x ^2)))) ^2)) ) assume A12: x in Z ; ::_thesis: ((cot * (f1 + (c (#) f2))) `| Z) . x = - ((b + ((2 * c) * x)) / ((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 cot is_differentiable_in (f1 + (c (#) f2)) . x by FDIFF_7:47; then diff ((cot * (f1 + (c (#) f2))),x) = (diff (cot,((f1 + (c (#) f2)) . x))) * (diff ((f1 + (c (#) f2)),x)) by A14, FDIFF_2:13 .= (- (1 / ((sin . ((f1 + (c (#) f2)) . x)) ^2))) * (diff ((f1 + (c (#) f2)),x)) by A15, FDIFF_7:47 .= - ((diff ((f1 + (c (#) f2)),x)) / ((sin . ((a + (b * x)) + (c * (x ^2)))) ^2)) by A13 .= - ((((f1 + (c (#) f2)) `| Z) . x) / ((sin . ((a + (b * x)) + (c * (x ^2)))) ^2)) by A5, A12, FDIFF_1:def_7 .= - ((b + ((2 * c) * x)) / ((sin . ((a + (b * x)) + (c * (x ^2)))) ^2)) by A2, A3, A4, A12, FDIFF_4:12 ; hence ((cot * (f1 + (c (#) f2))) `| Z) . x = - ((b + ((2 * c) * x)) / ((sin . ((a + (b * x)) + (c * (x ^2)))) ^2)) by A11, A12, FDIFF_1:def_7; ::_thesis: verum end; hence ( cot * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((cot * (f1 + (c (#) f2))) `| Z) . x = - ((b + ((2 * c) * x)) / ((sin . ((a + (b * x)) + (c * (x ^2)))) ^2)) ) ) by A1, A8, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_8:12 for Z being open Subset of REAL st Z c= dom (tan * exp_R) holds ( tan * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds ((tan * exp_R) `| Z) . x = (exp_R . x) / ((cos . (exp_R . x)) ^2) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (tan * exp_R) implies ( tan * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds ((tan * exp_R) `| Z) . x = (exp_R . x) / ((cos . (exp_R . x)) ^2) ) ) ) assume A1: Z c= dom (tan * exp_R) ; ::_thesis: ( tan * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds ((tan * exp_R) `| Z) . x = (exp_R . x) / ((cos . (exp_R . x)) ^2) ) ) A2: for x being Real st x in Z holds cos . (exp_R . x) <> 0 proof let x be Real; ::_thesis: ( x in Z implies cos . (exp_R . x) <> 0 ) assume x in Z ; ::_thesis: cos . (exp_R . x) <> 0 then exp_R . x in dom (sin / cos) by A1, FUNCT_1:11; hence cos . (exp_R . x) <> 0 by Th1; ::_thesis: verum end; A3: for x being Real st x in Z holds tan * exp_R is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies tan * exp_R is_differentiable_in x ) assume x in Z ; ::_thesis: tan * exp_R is_differentiable_in x then cos . (exp_R . x) <> 0 by A2; then ( exp_R is_differentiable_in x & tan is_differentiable_in exp_R . x ) by FDIFF_7:46, SIN_COS:65; hence tan * exp_R is_differentiable_in x by FDIFF_2:13; ::_thesis: verum end; then A4: tan * exp_R is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((tan * exp_R) `| Z) . x = (exp_R . x) / ((cos . (exp_R . x)) ^2) proof let x be Real; ::_thesis: ( x in Z implies ((tan * exp_R) `| Z) . x = (exp_R . x) / ((cos . (exp_R . x)) ^2) ) assume A5: x in Z ; ::_thesis: ((tan * exp_R) `| Z) . x = (exp_R . x) / ((cos . (exp_R . x)) ^2) then A6: cos . (exp_R . x) <> 0 by A2; then ( exp_R is_differentiable_in x & tan is_differentiable_in exp_R . x ) by FDIFF_7:46, SIN_COS:65; then diff ((tan * exp_R),x) = (diff (tan,(exp_R . x))) * (diff (exp_R,x)) by FDIFF_2:13 .= (1 / ((cos . (exp_R . x)) ^2)) * (diff (exp_R,x)) by A6, FDIFF_7:46 .= (exp_R . x) / ((cos . (exp_R . x)) ^2) by SIN_COS:65 ; hence ((tan * exp_R) `| Z) . x = (exp_R . x) / ((cos . (exp_R . x)) ^2) by A4, A5, FDIFF_1:def_7; ::_thesis: verum end; hence ( tan * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds ((tan * exp_R) `| Z) . x = (exp_R . x) / ((cos . (exp_R . x)) ^2) ) ) by A1, A3, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_8:13 for Z being open Subset of REAL st Z c= dom (cot * exp_R) holds ( cot * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds ((cot * exp_R) `| Z) . x = - ((exp_R . x) / ((sin . (exp_R . x)) ^2)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cot * exp_R) implies ( cot * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds ((cot * exp_R) `| Z) . x = - ((exp_R . x) / ((sin . (exp_R . x)) ^2)) ) ) ) assume A1: Z c= dom (cot * exp_R) ; ::_thesis: ( cot * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds ((cot * exp_R) `| Z) . x = - ((exp_R . x) / ((sin . (exp_R . x)) ^2)) ) ) A2: for x being Real st x in Z holds sin . (exp_R . x) <> 0 proof let x be Real; ::_thesis: ( x in Z implies sin . (exp_R . x) <> 0 ) assume x in Z ; ::_thesis: sin . (exp_R . x) <> 0 then exp_R . x in dom (cos / sin) by A1, FUNCT_1:11; hence sin . (exp_R . x) <> 0 by Th2; ::_thesis: verum end; A3: for x being Real st x in Z holds cot * exp_R is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies cot * exp_R is_differentiable_in x ) assume x in Z ; ::_thesis: cot * exp_R is_differentiable_in x then sin . (exp_R . x) <> 0 by A2; then ( exp_R is_differentiable_in x & cot is_differentiable_in exp_R . x ) by FDIFF_7:47, SIN_COS:65; hence cot * exp_R is_differentiable_in x by FDIFF_2:13; ::_thesis: verum end; then A4: cot * exp_R is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((cot * exp_R) `| Z) . x = - ((exp_R . x) / ((sin . (exp_R . x)) ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((cot * exp_R) `| Z) . x = - ((exp_R . x) / ((sin . (exp_R . x)) ^2)) ) assume A5: x in Z ; ::_thesis: ((cot * exp_R) `| Z) . x = - ((exp_R . x) / ((sin . (exp_R . x)) ^2)) then A6: sin . (exp_R . x) <> 0 by A2; then ( exp_R is_differentiable_in x & cot is_differentiable_in exp_R . x ) by FDIFF_7:47, SIN_COS:65; then diff ((cot * exp_R),x) = (diff (cot,(exp_R . x))) * (diff (exp_R,x)) by FDIFF_2:13 .= (- (1 / ((sin . (exp_R . x)) ^2))) * (diff (exp_R,x)) by A6, FDIFF_7:47 .= - ((diff (exp_R,x)) / ((sin . (exp_R . x)) ^2)) .= - ((exp_R . x) / ((sin . (exp_R . x)) ^2)) by SIN_COS:65 ; hence ((cot * exp_R) `| Z) . x = - ((exp_R . x) / ((sin . (exp_R . x)) ^2)) by A4, A5, FDIFF_1:def_7; ::_thesis: verum end; hence ( cot * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds ((cot * exp_R) `| Z) . x = - ((exp_R . x) / ((sin . (exp_R . x)) ^2)) ) ) by A1, A3, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_8:14 for Z being open Subset of REAL st Z c= dom (tan * ln) holds ( tan * ln is_differentiable_on Z & ( for x being Real st x in Z holds ((tan * ln) `| Z) . x = 1 / (x * ((cos . (ln . x)) ^2)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (tan * ln) implies ( tan * ln is_differentiable_on Z & ( for x being Real st x in Z holds ((tan * ln) `| Z) . x = 1 / (x * ((cos . (ln . x)) ^2)) ) ) ) assume A1: Z c= dom (tan * ln) ; ::_thesis: ( tan * ln is_differentiable_on Z & ( for x being Real st x in Z holds ((tan * ln) `| Z) . x = 1 / (x * ((cos . (ln . x)) ^2)) ) ) dom (tan * ln) c= dom ln by RELAT_1:25; then A2: Z c= dom ln by A1, XBOOLE_1:1; A3: for x being Real st x in Z holds x > 0 proof let x be Real; ::_thesis: ( x in Z implies x > 0 ) assume x in Z ; ::_thesis: x > 0 then x in right_open_halfline 0 by A2, TAYLOR_1:18; then ex g being Real st ( x = g & 0 < g ) by Lm1; hence x > 0 ; ::_thesis: verum end; A4: for x being Real st x in Z holds diff (ln,x) = 1 / x proof let x be Real; ::_thesis: ( x in Z implies diff (ln,x) = 1 / x ) assume x in Z ; ::_thesis: diff (ln,x) = 1 / x then x > 0 by A3; then x in right_open_halfline 0 by Lm1; hence diff (ln,x) = 1 / x by TAYLOR_1:18; ::_thesis: verum end; A5: for x being Real st x in Z holds cos . (ln . x) <> 0 proof let x be Real; ::_thesis: ( x in Z implies cos . (ln . x) <> 0 ) assume x in Z ; ::_thesis: cos . (ln . x) <> 0 then ln . x in dom (sin / cos) by A1, FUNCT_1:11; hence cos . (ln . x) <> 0 by Th1; ::_thesis: verum end; A6: for x being Real st x in Z holds tan * ln is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies tan * ln is_differentiable_in x ) assume A7: x in Z ; ::_thesis: tan * ln is_differentiable_in x then cos . (ln . x) <> 0 by A5; then A8: tan is_differentiable_in ln . x by FDIFF_7:46; ln is_differentiable_in x by A3, A7, TAYLOR_1:18; hence tan * ln is_differentiable_in x by A8, FDIFF_2:13; ::_thesis: verum end; then A9: tan * ln is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((tan * ln) `| Z) . x = 1 / (x * ((cos . (ln . x)) ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((tan * ln) `| Z) . x = 1 / (x * ((cos . (ln . x)) ^2)) ) assume A10: x in Z ; ::_thesis: ((tan * ln) `| Z) . x = 1 / (x * ((cos . (ln . x)) ^2)) then A11: ln is_differentiable_in x by A3, TAYLOR_1:18; A12: cos . (ln . x) <> 0 by A5, A10; then tan is_differentiable_in ln . x by FDIFF_7:46; then diff ((tan * ln),x) = (diff (tan,(ln . x))) * (diff (ln,x)) by A11, FDIFF_2:13 .= (1 / ((cos . (ln . x)) ^2)) * (diff (ln,x)) by A12, FDIFF_7:46 .= (1 / x) / ((cos . (ln . x)) ^2) by A4, A10 .= 1 / (x * ((cos . (ln . x)) ^2)) by XCMPLX_1:78 ; hence ((tan * ln) `| Z) . x = 1 / (x * ((cos . (ln . x)) ^2)) by A9, A10, FDIFF_1:def_7; ::_thesis: verum end; hence ( tan * ln is_differentiable_on Z & ( for x being Real st x in Z holds ((tan * ln) `| Z) . x = 1 / (x * ((cos . (ln . x)) ^2)) ) ) by A1, A6, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_8:15 for Z being open Subset of REAL st Z c= dom (cot * ln) holds ( cot * ln is_differentiable_on Z & ( for x being Real st x in Z holds ((cot * ln) `| Z) . x = - (1 / (x * ((sin . (ln . x)) ^2))) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cot * ln) implies ( cot * ln is_differentiable_on Z & ( for x being Real st x in Z holds ((cot * ln) `| Z) . x = - (1 / (x * ((sin . (ln . x)) ^2))) ) ) ) assume A1: Z c= dom (cot * ln) ; ::_thesis: ( cot * ln is_differentiable_on Z & ( for x being Real st x in Z holds ((cot * ln) `| Z) . x = - (1 / (x * ((sin . (ln . x)) ^2))) ) ) dom (cot * ln) c= dom ln by RELAT_1:25; then A2: Z c= dom ln by A1, XBOOLE_1:1; A3: for x being Real st x in Z holds x > 0 proof let x be Real; ::_thesis: ( x in Z implies x > 0 ) assume x in Z ; ::_thesis: x > 0 then x in right_open_halfline 0 by A2, TAYLOR_1:18; then ex g being Real st ( x = g & 0 < g ) by Lm1; hence x > 0 ; ::_thesis: verum end; A4: for x being Real st x in Z holds diff (ln,x) = 1 / x proof let x be Real; ::_thesis: ( x in Z implies diff (ln,x) = 1 / x ) assume x in Z ; ::_thesis: diff (ln,x) = 1 / x then x > 0 by A3; then x in right_open_halfline 0 by Lm1; hence diff (ln,x) = 1 / x by TAYLOR_1:18; ::_thesis: verum end; A5: for x being Real st x in Z holds sin . (ln . x) <> 0 proof let x be Real; ::_thesis: ( x in Z implies sin . (ln . x) <> 0 ) assume x in Z ; ::_thesis: sin . (ln . x) <> 0 then ln . x in dom (cos / sin) by A1, FUNCT_1:11; hence sin . (ln . x) <> 0 by Th2; ::_thesis: verum end; A6: for x being Real st x in Z holds cot * ln is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies cot * ln is_differentiable_in x ) assume A7: x in Z ; ::_thesis: cot * ln is_differentiable_in x then sin . (ln . x) <> 0 by A5; then A8: cot is_differentiable_in ln . x by FDIFF_7:47; ln is_differentiable_in x by A3, A7, TAYLOR_1:18; hence cot * ln is_differentiable_in x by A8, FDIFF_2:13; ::_thesis: verum end; then A9: cot * ln is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((cot * ln) `| Z) . x = - (1 / (x * ((sin . (ln . x)) ^2))) proof let x be Real; ::_thesis: ( x in Z implies ((cot * ln) `| Z) . x = - (1 / (x * ((sin . (ln . x)) ^2))) ) assume A10: x in Z ; ::_thesis: ((cot * ln) `| Z) . x = - (1 / (x * ((sin . (ln . x)) ^2))) then A11: ln is_differentiable_in x by A3, TAYLOR_1:18; A12: sin . (ln . x) <> 0 by A5, A10; then cot is_differentiable_in ln . x by FDIFF_7:47; then diff ((cot * ln),x) = (diff (cot,(ln . x))) * (diff (ln,x)) by A11, FDIFF_2:13 .= (- (1 / ((sin . (ln . x)) ^2))) * (diff (ln,x)) by A12, FDIFF_7:47 .= - ((diff (ln,x)) / ((sin . (ln . x)) ^2)) .= - ((1 / x) / ((sin . (ln . x)) ^2)) by A4, A10 .= - (1 / (x * ((sin . (ln . x)) ^2))) by XCMPLX_1:78 ; hence ((cot * ln) `| Z) . x = - (1 / (x * ((sin . (ln . x)) ^2))) by A9, A10, FDIFF_1:def_7; ::_thesis: verum end; hence ( cot * ln is_differentiable_on Z & ( for x being Real st x in Z holds ((cot * ln) `| Z) . x = - (1 / (x * ((sin . (ln . x)) ^2))) ) ) by A1, A6, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_8:16 for Z being open Subset of REAL st Z c= dom (exp_R * tan) holds ( exp_R * tan is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R * tan) `| Z) . x = (exp_R . (tan . x)) / ((cos . x) ^2) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (exp_R * tan) implies ( exp_R * tan is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R * tan) `| Z) . x = (exp_R . (tan . x)) / ((cos . x) ^2) ) ) ) assume A1: Z c= dom (exp_R * tan) ; ::_thesis: ( exp_R * tan is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R * tan) `| Z) . x = (exp_R . (tan . x)) / ((cos . x) ^2) ) ) A2: for x being Real st x in Z holds cos . x <> 0 proof let x be Real; ::_thesis: ( x in Z implies cos . x <> 0 ) assume x in Z ; ::_thesis: cos . x <> 0 then x in dom (sin / cos) by A1, FUNCT_1:11; hence cos . x <> 0 by Th1; ::_thesis: verum end; A3: for x being Real st x in Z holds exp_R * tan is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies exp_R * tan is_differentiable_in x ) assume x in Z ; ::_thesis: exp_R * tan is_differentiable_in x then cos . x <> 0 by A2; then A4: tan is_differentiable_in x by FDIFF_7:46; exp_R is_differentiable_in tan . x by SIN_COS:65; hence exp_R * tan is_differentiable_in x by A4, FDIFF_2:13; ::_thesis: verum end; then A5: exp_R * tan is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((exp_R * tan) `| Z) . x = (exp_R . (tan . x)) / ((cos . x) ^2) proof let x be Real; ::_thesis: ( x in Z implies ((exp_R * tan) `| Z) . x = (exp_R . (tan . x)) / ((cos . x) ^2) ) A6: exp_R is_differentiable_in tan . x by SIN_COS:65; assume A7: x in Z ; ::_thesis: ((exp_R * tan) `| Z) . x = (exp_R . (tan . x)) / ((cos . x) ^2) then A8: cos . x <> 0 by A2; then tan is_differentiable_in x by FDIFF_7:46; then diff ((exp_R * tan),x) = (diff (exp_R,(tan . x))) * (diff (tan,x)) by A6, FDIFF_2:13 .= (diff (exp_R,(tan . x))) * (1 / ((cos . x) ^2)) by A8, FDIFF_7:46 .= (exp_R . (tan . x)) / ((cos . x) ^2) by SIN_COS:65 ; hence ((exp_R * tan) `| Z) . x = (exp_R . (tan . x)) / ((cos . x) ^2) by A5, A7, FDIFF_1:def_7; ::_thesis: verum end; hence ( exp_R * tan is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R * tan) `| Z) . x = (exp_R . (tan . x)) / ((cos . x) ^2) ) ) by A1, A3, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_8:17 for Z being open Subset of REAL st Z c= dom (exp_R * cot) holds ( exp_R * cot is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R * cot) `| Z) . x = - ((exp_R . (cot . x)) / ((sin . x) ^2)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (exp_R * cot) implies ( exp_R * cot is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R * cot) `| Z) . x = - ((exp_R . (cot . x)) / ((sin . x) ^2)) ) ) ) assume A1: Z c= dom (exp_R * cot) ; ::_thesis: ( exp_R * cot is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R * cot) `| Z) . x = - ((exp_R . (cot . x)) / ((sin . x) ^2)) ) ) A2: for x being Real st x in Z holds sin . x <> 0 proof let x be Real; ::_thesis: ( x in Z implies sin . x <> 0 ) assume x in Z ; ::_thesis: sin . x <> 0 then x in dom (cos / sin) by A1, FUNCT_1:11; hence sin . x <> 0 by Th2; ::_thesis: verum end; A3: for x being Real st x in Z holds exp_R * cot is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies exp_R * cot is_differentiable_in x ) assume x in Z ; ::_thesis: exp_R * cot is_differentiable_in x then sin . x <> 0 by A2; then A4: cot is_differentiable_in x by FDIFF_7:47; exp_R is_differentiable_in cot . x by SIN_COS:65; hence exp_R * cot is_differentiable_in x by A4, FDIFF_2:13; ::_thesis: verum end; then A5: exp_R * cot is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((exp_R * cot) `| Z) . x = - ((exp_R . (cot . x)) / ((sin . x) ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((exp_R * cot) `| Z) . x = - ((exp_R . (cot . x)) / ((sin . x) ^2)) ) A6: exp_R is_differentiable_in cot . x by SIN_COS:65; assume A7: x in Z ; ::_thesis: ((exp_R * cot) `| Z) . x = - ((exp_R . (cot . x)) / ((sin . x) ^2)) then A8: sin . x <> 0 by A2; then cot is_differentiable_in x by FDIFF_7:47; then diff ((exp_R * cot),x) = (diff (exp_R,(cot . x))) * (diff (cot,x)) by A6, FDIFF_2:13 .= (diff (exp_R,(cot . x))) * (- (1 / ((sin . x) ^2))) by A8, FDIFF_7:47 .= (exp_R . (cot . x)) * (- (1 / ((sin . x) ^2))) by SIN_COS:65 .= - ((exp_R . (cot . x)) / ((sin . x) ^2)) ; hence ((exp_R * cot) `| Z) . x = - ((exp_R . (cot . x)) / ((sin . x) ^2)) by A5, A7, FDIFF_1:def_7; ::_thesis: verum end; hence ( exp_R * cot is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R * cot) `| Z) . x = - ((exp_R . (cot . x)) / ((sin . x) ^2)) ) ) by A1, A3, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_8:18 for Z being open Subset of REAL st Z c= dom (ln * tan) holds ( ln * tan is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * tan) `| Z) . x = 1 / ((cos . x) * (sin . x)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (ln * tan) implies ( ln * tan is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * tan) `| Z) . x = 1 / ((cos . x) * (sin . x)) ) ) ) assume A1: Z c= dom (ln * tan) ; ::_thesis: ( ln * tan is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * tan) `| Z) . x = 1 / ((cos . x) * (sin . x)) ) ) A2: for x being Real st x in Z holds tan . x > 0 proof let x be Real; ::_thesis: ( x in Z implies tan . x > 0 ) assume x in Z ; ::_thesis: tan . x > 0 then tan . x in right_open_halfline 0 by A1, FUNCT_1:11, TAYLOR_1:18; then ex g being Real st ( tan . x = g & 0 < g ) by Lm1; hence tan . x > 0 ; ::_thesis: verum end; dom (ln * tan) c= dom tan by RELAT_1:25; then A3: Z c= dom tan by A1, XBOOLE_1:1; A4: for x being Real st x in Z holds cos . x <> 0 proof let x be Real; ::_thesis: ( x in Z implies cos . x <> 0 ) assume x in Z ; ::_thesis: cos . x <> 0 then x in dom (sin / cos) by A1, FUNCT_1:11; hence cos . x <> 0 by Th1; ::_thesis: verum end; A5: for x being Real st x in Z holds tan is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies tan is_differentiable_in x ) assume x in Z ; ::_thesis: tan is_differentiable_in x then cos . x <> 0 by A4; hence tan is_differentiable_in x by FDIFF_7:46; ::_thesis: verum end; A6: for x being Real st x in Z holds ln * tan is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies ln * tan is_differentiable_in x ) assume x in Z ; ::_thesis: ln * tan is_differentiable_in x then ( tan is_differentiable_in x & tan . x > 0 ) by A2, A5; hence ln * tan is_differentiable_in x by TAYLOR_1:20; ::_thesis: verum end; then A7: ln * tan is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((ln * tan) `| Z) . x = 1 / ((cos . x) * (sin . x)) proof let x be Real; ::_thesis: ( x in Z implies ((ln * tan) `| Z) . x = 1 / ((cos . x) * (sin . x)) ) assume A8: x in Z ; ::_thesis: ((ln * tan) `| Z) . x = 1 / ((cos . x) * (sin . x)) then A9: cos . x <> 0 by A4; ( tan is_differentiable_in x & tan . x > 0 ) by A2, A5, A8; then diff ((ln * tan),x) = (diff (tan,x)) / (tan . x) by TAYLOR_1:20 .= (1 / ((cos . x) ^2)) / (tan . x) by A9, FDIFF_7:46 .= 1 / (((cos . x) ^2) * (tan . x)) by XCMPLX_1:78 .= 1 / (((cos . x) ^2) * ((sin . x) / (cos . x))) by A3, A8, RFUNCT_1:def_1 .= 1 / ((((cos . x) ^2) * (sin . x)) / (cos . x)) .= (cos . x) / (((cos . x) ^2) * (sin . x)) by XCMPLX_1:57 .= ((cos . x) / ((cos . x) ^2)) / (sin . x) by XCMPLX_1:78 .= (((cos . x) / (cos . x)) / (cos . x)) / (sin . x) by XCMPLX_1:78 .= (1 / (cos . x)) / (sin . x) by A4, A8, XCMPLX_1:60 .= 1 / ((cos . x) * (sin . x)) by XCMPLX_1:78 ; hence ((ln * tan) `| Z) . x = 1 / ((cos . x) * (sin . x)) by A7, A8, FDIFF_1:def_7; ::_thesis: verum end; hence ( ln * tan is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * tan) `| Z) . x = 1 / ((cos . x) * (sin . x)) ) ) by A1, A6, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_8:19 for Z being open Subset of REAL st Z c= dom (ln * cot) holds ( ln * cot is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * cot) `| Z) . x = - (1 / ((sin . x) * (cos . x))) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (ln * cot) implies ( ln * cot is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * cot) `| Z) . x = - (1 / ((sin . x) * (cos . x))) ) ) ) assume A1: Z c= dom (ln * cot) ; ::_thesis: ( ln * cot is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * cot) `| Z) . x = - (1 / ((sin . x) * (cos . x))) ) ) A2: for x being Real st x in Z holds cot . x > 0 proof let x be Real; ::_thesis: ( x in Z implies cot . x > 0 ) assume x in Z ; ::_thesis: cot . x > 0 then cot . x in right_open_halfline 0 by A1, FUNCT_1:11, TAYLOR_1:18; then ex g being Real st ( cot . x = g & 0 < g ) by Lm1; hence cot . x > 0 ; ::_thesis: verum end; dom (ln * cot) c= dom cot by RELAT_1:25; then A3: Z c= dom cot by A1, XBOOLE_1:1; A4: for x being Real st x in Z holds sin . x <> 0 proof let x be Real; ::_thesis: ( x in Z implies sin . x <> 0 ) assume x in Z ; ::_thesis: sin . x <> 0 then x in dom (cos / sin) by A1, FUNCT_1:11; hence sin . x <> 0 by Th2; ::_thesis: verum end; A5: for x being Real st x in Z holds cot is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies cot is_differentiable_in x ) assume x in Z ; ::_thesis: cot is_differentiable_in x then sin . x <> 0 by A4; hence cot is_differentiable_in x by FDIFF_7:47; ::_thesis: verum end; A6: for x being Real st x in Z holds ln * cot is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies ln * cot is_differentiable_in x ) assume x in Z ; ::_thesis: ln * cot is_differentiable_in x then ( cot is_differentiable_in x & cot . x > 0 ) by A2, A5; hence ln * cot is_differentiable_in x by TAYLOR_1:20; ::_thesis: verum end; then A7: ln * cot is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((ln * cot) `| Z) . x = - (1 / ((sin . x) * (cos . x))) proof let x be Real; ::_thesis: ( x in Z implies ((ln * cot) `| Z) . x = - (1 / ((sin . x) * (cos . x))) ) assume A8: x in Z ; ::_thesis: ((ln * cot) `| Z) . x = - (1 / ((sin . x) * (cos . x))) then A9: sin . x <> 0 by A4; ( cot is_differentiable_in x & cot . x > 0 ) by A2, A5, A8; then diff ((ln * cot),x) = (diff (cot,x)) / (cot . x) by TAYLOR_1:20 .= (- (1 / ((sin . x) ^2))) / (cot . x) by A9, FDIFF_7:47 .= - ((1 / ((sin . x) ^2)) / (cot . x)) .= - (1 / (((sin . x) ^2) * (cot . x))) by XCMPLX_1:78 .= - (1 / (((sin . x) ^2) * ((cos . x) / (sin . x)))) by A3, A8, RFUNCT_1:def_1 .= - (1 / ((((sin . x) ^2) * (cos . x)) / (sin . x))) .= - ((sin . x) / (((sin . x) ^2) * (cos . x))) by XCMPLX_1:57 .= - (((sin . x) / ((sin . x) ^2)) / (cos . x)) by XCMPLX_1:78 .= - ((((sin . x) / (sin . x)) / (sin . x)) / (cos . x)) by XCMPLX_1:78 .= - ((1 / (sin . x)) / (cos . x)) by A4, A8, XCMPLX_1:60 .= - (1 / ((sin . x) * (cos . x))) by XCMPLX_1:78 ; hence ((ln * cot) `| Z) . x = - (1 / ((sin . x) * (cos . x))) by A7, A8, FDIFF_1:def_7; ::_thesis: verum end; hence ( ln * cot is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * cot) `| Z) . x = - (1 / ((sin . x) * (cos . x))) ) ) by A1, A6, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_8:20 for n being Nat for Z being open Subset of REAL st Z c= dom ((#Z n) * tan) & 1 <= n holds ( (#Z n) * tan is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z n) * tan) `| Z) . x = (n * ((sin . x) #Z (n - 1))) / ((cos . x) #Z (n + 1)) ) ) proof let n be Nat; ::_thesis: for Z being open Subset of REAL st Z c= dom ((#Z n) * tan) & 1 <= n holds ( (#Z n) * tan is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z n) * tan) `| Z) . x = (n * ((sin . x) #Z (n - 1))) / ((cos . x) #Z (n + 1)) ) ) let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((#Z n) * tan) & 1 <= n implies ( (#Z n) * tan is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z n) * tan) `| Z) . x = (n * ((sin . x) #Z (n - 1))) / ((cos . x) #Z (n + 1)) ) ) ) assume that A1: Z c= dom ((#Z n) * tan) and A2: 1 <= n ; ::_thesis: ( (#Z n) * tan is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z n) * tan) `| Z) . x = (n * ((sin . x) #Z (n - 1))) / ((cos . x) #Z (n + 1)) ) ) A3: dom ((#Z n) * tan) c= dom tan by RELAT_1:25; A4: for x being Real st x in Z holds cos . x <> 0 proof let x be Real; ::_thesis: ( x in Z implies cos . x <> 0 ) assume x in Z ; ::_thesis: cos . x <> 0 then x in dom (sin / cos) by A1, FUNCT_1:11; hence cos . x <> 0 by Th1; ::_thesis: verum end; A5: for x being Real st x in Z holds (#Z n) * tan is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies (#Z n) * tan is_differentiable_in x ) assume x in Z ; ::_thesis: (#Z n) * tan is_differentiable_in x then cos . x <> 0 by A4; then tan is_differentiable_in x by FDIFF_7:46; hence (#Z n) * tan is_differentiable_in x by TAYLOR_1:3; ::_thesis: verum end; then A6: (#Z n) * tan is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds (((#Z n) * tan) `| Z) . x = (n * ((sin . x) #Z (n - 1))) / ((cos . x) #Z (n + 1)) proof set m = n - 1; let x be Real; ::_thesis: ( x in Z implies (((#Z n) * tan) `| Z) . x = (n * ((sin . x) #Z (n - 1))) / ((cos . x) #Z (n + 1)) ) A7: ex m being Nat st n = m + 1 by A2, NAT_1:6; assume A8: x in Z ; ::_thesis: (((#Z n) * tan) `| Z) . x = (n * ((sin . x) #Z (n - 1))) / ((cos . x) #Z (n + 1)) then A9: cos . x <> 0 by A4; then A10: tan is_differentiable_in x by FDIFF_7:46; (((#Z n) * tan) `| Z) . x = diff (((#Z n) * tan),x) by A6, A8, FDIFF_1:def_7 .= (n * ((tan . x) #Z (n - 1))) * (diff (tan,x)) by A10, TAYLOR_1:3 .= (n * ((tan . x) #Z (n - 1))) * (1 / ((cos . x) ^2)) by A9, FDIFF_7:46 .= (n * (((sin . x) #Z (n - 1)) / ((cos . x) #Z (n - 1)))) / ((cos . x) ^2) by A1, A3, A8, A7, Th3, XBOOLE_1:1 .= ((n * ((sin . x) #Z (n - 1))) / ((cos . x) #Z (n - 1))) / ((cos . x) ^2) .= (n * ((sin . x) #Z (n - 1))) / (((cos . x) #Z (n - 1)) * ((cos . x) ^2)) by XCMPLX_1:78 .= (n * ((sin . x) #Z (n - 1))) / (((cos . x) #Z (n - 1)) * ((cos . x) #Z 2)) by FDIFF_7:1 .= (n * ((sin . x) #Z (n - 1))) / ((cos . x) #Z ((n - 1) + 2)) by A4, A8, PREPOWER:44 .= (n * ((sin . x) #Z (n - 1))) / ((cos . x) #Z (n + 1)) ; hence (((#Z n) * tan) `| Z) . x = (n * ((sin . x) #Z (n - 1))) / ((cos . x) #Z (n + 1)) ; ::_thesis: verum end; hence ( (#Z n) * tan is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z n) * tan) `| Z) . x = (n * ((sin . x) #Z (n - 1))) / ((cos . x) #Z (n + 1)) ) ) by A1, A5, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_8:21 for n being Nat for Z being open Subset of REAL st Z c= dom ((#Z n) * cot) & 1 <= n holds ( (#Z n) * cot is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z n) * cot) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) / ((sin . x) #Z (n + 1))) ) ) proof let n be Nat; ::_thesis: for Z being open Subset of REAL st Z c= dom ((#Z n) * cot) & 1 <= n holds ( (#Z n) * cot is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z n) * cot) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) / ((sin . x) #Z (n + 1))) ) ) let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((#Z n) * cot) & 1 <= n implies ( (#Z n) * cot is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z n) * cot) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) / ((sin . x) #Z (n + 1))) ) ) ) assume that A1: Z c= dom ((#Z n) * cot) and A2: 1 <= n ; ::_thesis: ( (#Z n) * cot is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z n) * cot) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) / ((sin . x) #Z (n + 1))) ) ) A3: dom ((#Z n) * cot) c= dom cot by RELAT_1:25; A4: for x being Real st x in Z holds sin . x <> 0 proof let x be Real; ::_thesis: ( x in Z implies sin . x <> 0 ) assume x in Z ; ::_thesis: sin . x <> 0 then x in dom (cos / sin) by A1, FUNCT_1:11; hence sin . x <> 0 by Th2; ::_thesis: verum end; A5: for x being Real st x in Z holds (#Z n) * cot is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies (#Z n) * cot is_differentiable_in x ) assume x in Z ; ::_thesis: (#Z n) * cot is_differentiable_in x then sin . x <> 0 by A4; then cot is_differentiable_in x by FDIFF_7:47; hence (#Z n) * cot is_differentiable_in x by TAYLOR_1:3; ::_thesis: verum end; then A6: (#Z n) * cot is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds (((#Z n) * cot) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) / ((sin . x) #Z (n + 1))) proof set m = n - 1; let x be Real; ::_thesis: ( x in Z implies (((#Z n) * cot) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) / ((sin . x) #Z (n + 1))) ) A7: ex m being Nat st n = m + 1 by A2, NAT_1:6; assume A8: x in Z ; ::_thesis: (((#Z n) * cot) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) / ((sin . x) #Z (n + 1))) then A9: sin . x <> 0 by A4; then A10: cot is_differentiable_in x by FDIFF_7:47; (((#Z n) * cot) `| Z) . x = diff (((#Z n) * cot),x) by A6, A8, FDIFF_1:def_7 .= (n * ((cot . x) #Z (n - 1))) * (diff (cot,x)) by A10, TAYLOR_1:3 .= (n * ((cot . x) #Z (n - 1))) * (- (1 / ((sin . x) ^2))) by A9, FDIFF_7:47 .= - ((n * ((cot . x) #Z (n - 1))) / ((sin . x) ^2)) .= - ((n * (((cos . x) #Z (n - 1)) / ((sin . x) #Z (n - 1)))) / ((sin . x) ^2)) by A1, A3, A8, A7, Th3, XBOOLE_1:1 .= - (((n * ((cos . x) #Z (n - 1))) / ((sin . x) #Z (n - 1))) / ((sin . x) ^2)) .= - ((n * ((cos . x) #Z (n - 1))) / (((sin . x) #Z (n - 1)) * ((sin . x) ^2))) by XCMPLX_1:78 .= - ((n * ((cos . x) #Z (n - 1))) / (((sin . x) #Z (n - 1)) * ((sin . x) #Z 2))) by FDIFF_7:1 .= - ((n * ((cos . x) #Z (n - 1))) / ((sin . x) #Z ((n - 1) + 2))) by A4, A8, PREPOWER:44 .= - ((n * ((cos . x) #Z (n - 1))) / ((sin . x) #Z (n + 1))) ; hence (((#Z n) * cot) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) / ((sin . x) #Z (n + 1))) ; ::_thesis: verum end; hence ( (#Z n) * cot is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z n) * cot) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) / ((sin . x) #Z (n + 1))) ) ) by A1, A5, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_8:22 for Z being open Subset of REAL st Z c= dom (tan + (cos ^)) & ( for x being Real st x in Z holds ( 1 + (sin . x) <> 0 & 1 - (sin . x) <> 0 ) ) holds ( tan + (cos ^) is_differentiable_on Z & ( for x being Real st x in Z holds ((tan + (cos ^)) `| Z) . x = 1 / (1 - (sin . x)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (tan + (cos ^)) & ( for x being Real st x in Z holds ( 1 + (sin . x) <> 0 & 1 - (sin . x) <> 0 ) ) implies ( tan + (cos ^) is_differentiable_on Z & ( for x being Real st x in Z holds ((tan + (cos ^)) `| Z) . x = 1 / (1 - (sin . x)) ) ) ) assume that A1: Z c= dom (tan + (cos ^)) and A2: for x being Real st x in Z holds ( 1 + (sin . x) <> 0 & 1 - (sin . x) <> 0 ) ; ::_thesis: ( tan + (cos ^) is_differentiable_on Z & ( for x being Real st x in Z holds ((tan + (cos ^)) `| Z) . x = 1 / (1 - (sin . x)) ) ) Z c= (dom tan) /\ (dom (cos ^)) by A1, VALUED_1:def_1; then A3: Z c= dom tan by XBOOLE_1:18; then A4: for x being Real st x in Z holds cos . x <> 0 by Th1; then A5: cos ^ is_differentiable_on Z by FDIFF_4:39; for x being Real st x in Z holds tan is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies tan is_differentiable_in x ) assume x in Z ; ::_thesis: tan is_differentiable_in x then cos . x <> 0 by A3, Th1; hence tan is_differentiable_in x by FDIFF_7:46; ::_thesis: verum end; then A6: tan is_differentiable_on Z by A3, FDIFF_1:9; for x being Real st x in Z holds ((tan + (cos ^)) `| Z) . x = 1 / (1 - (sin . x)) proof let x be Real; ::_thesis: ( x in Z implies ((tan + (cos ^)) `| Z) . x = 1 / (1 - (sin . x)) ) assume A7: x in Z ; ::_thesis: ((tan + (cos ^)) `| Z) . x = 1 / (1 - (sin . x)) then A8: 1 + (sin . x) <> 0 by A2; A9: cos . x <> 0 by A3, A7, Th1; ((tan + (cos ^)) `| Z) . x = (diff (tan,x)) + (diff ((cos ^),x)) by A1, A5, A6, A7, FDIFF_1:18 .= (1 / ((cos . x) ^2)) + (diff ((cos ^),x)) by A9, FDIFF_7:46 .= (1 / ((cos . x) ^2)) + (((cos ^) `| Z) . x) by A5, A7, FDIFF_1:def_7 .= (1 / ((cos . x) ^2)) + ((sin . x) / ((cos . x) ^2)) by A4, A7, FDIFF_4:39 .= (1 + (sin . x)) / ((((cos . x) ^2) + ((sin . x) ^2)) - ((sin . x) ^2)) .= (1 + (sin . x)) / (1 - ((sin . x) ^2)) by SIN_COS:28 .= (1 + (sin . x)) / ((1 + (sin . x)) * (1 - (sin . x))) .= ((1 + (sin . x)) / (1 + (sin . x))) / (1 - (sin . x)) by XCMPLX_1:78 .= 1 / (1 - (sin . x)) by A8, XCMPLX_1:60 ; hence ((tan + (cos ^)) `| Z) . x = 1 / (1 - (sin . x)) ; ::_thesis: verum end; hence ( tan + (cos ^) is_differentiable_on Z & ( for x being Real st x in Z holds ((tan + (cos ^)) `| Z) . x = 1 / (1 - (sin . x)) ) ) by A1, A5, A6, FDIFF_1:18; ::_thesis: verum end; theorem :: FDIFF_8:23 for Z being open Subset of REAL st Z c= dom (tan - (cos ^)) & ( for x being Real st x in Z holds ( 1 - (sin . x) <> 0 & 1 + (sin . x) <> 0 ) ) holds ( tan - (cos ^) is_differentiable_on Z & ( for x being Real st x in Z holds ((tan - (cos ^)) `| Z) . x = 1 / (1 + (sin . x)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (tan - (cos ^)) & ( for x being Real st x in Z holds ( 1 - (sin . x) <> 0 & 1 + (sin . x) <> 0 ) ) implies ( tan - (cos ^) is_differentiable_on Z & ( for x being Real st x in Z holds ((tan - (cos ^)) `| Z) . x = 1 / (1 + (sin . x)) ) ) ) assume that A1: Z c= dom (tan - (cos ^)) and A2: for x being Real st x in Z holds ( 1 - (sin . x) <> 0 & 1 + (sin . x) <> 0 ) ; ::_thesis: ( tan - (cos ^) is_differentiable_on Z & ( for x being Real st x in Z holds ((tan - (cos ^)) `| Z) . x = 1 / (1 + (sin . x)) ) ) Z c= (dom tan) /\ (dom (cos ^)) by A1, VALUED_1:12; then A3: Z c= dom tan by XBOOLE_1:18; then A4: for x being Real st x in Z holds cos . x <> 0 by Th1; then A5: cos ^ is_differentiable_on Z by FDIFF_4:39; for x being Real st x in Z holds tan is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies tan is_differentiable_in x ) assume x in Z ; ::_thesis: tan is_differentiable_in x then cos . x <> 0 by A3, Th1; hence tan is_differentiable_in x by FDIFF_7:46; ::_thesis: verum end; then A6: tan is_differentiable_on Z by A3, FDIFF_1:9; for x being Real st x in Z holds ((tan - (cos ^)) `| Z) . x = 1 / (1 + (sin . x)) proof let x be Real; ::_thesis: ( x in Z implies ((tan - (cos ^)) `| Z) . x = 1 / (1 + (sin . x)) ) assume A7: x in Z ; ::_thesis: ((tan - (cos ^)) `| Z) . x = 1 / (1 + (sin . x)) then A8: 1 - (sin . x) <> 0 by A2; A9: cos . x <> 0 by A3, A7, Th1; ((tan - (cos ^)) `| Z) . x = (diff (tan,x)) - (diff ((cos ^),x)) by A1, A5, A6, A7, FDIFF_1:19 .= (1 / ((cos . x) ^2)) - (diff ((cos ^),x)) by A9, FDIFF_7:46 .= (1 / ((cos . x) ^2)) - (((cos ^) `| Z) . x) by A5, A7, FDIFF_1:def_7 .= (1 / ((cos . x) ^2)) - ((sin . x) / ((cos . x) ^2)) by A4, A7, FDIFF_4:39 .= (1 - (sin . x)) / ((((cos . x) ^2) + ((sin . x) ^2)) - ((sin . x) ^2)) .= (1 - (sin . x)) / (1 - ((sin . x) ^2)) by SIN_COS:28 .= (1 - (sin . x)) / ((1 - (sin . x)) * (1 + (sin . x))) .= ((1 - (sin . x)) / (1 - (sin . x))) / (1 + (sin . x)) by XCMPLX_1:78 .= 1 / (1 + (sin . x)) by A8, XCMPLX_1:60 ; hence ((tan - (cos ^)) `| Z) . x = 1 / (1 + (sin . x)) ; ::_thesis: verum end; hence ( tan - (cos ^) is_differentiable_on Z & ( for x being Real st x in Z holds ((tan - (cos ^)) `| Z) . x = 1 / (1 + (sin . x)) ) ) by A1, A5, A6, FDIFF_1:19; ::_thesis: verum end; theorem :: FDIFF_8:24 for Z being open Subset of REAL st Z c= dom (tan - (id Z)) holds ( tan - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds ((tan - (id Z)) `| Z) . x = ((sin . x) ^2) / ((cos . x) ^2) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (tan - (id Z)) implies ( tan - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds ((tan - (id Z)) `| Z) . x = ((sin . x) ^2) / ((cos . x) ^2) ) ) ) A1: for x being Real st x in Z holds (id Z) . x = (1 * x) + 0 by FUNCT_1:18; assume A2: Z c= dom (tan - (id Z)) ; ::_thesis: ( tan - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds ((tan - (id Z)) `| Z) . x = ((sin . x) ^2) / ((cos . x) ^2) ) ) then A3: Z c= (dom tan) /\ (dom (id Z)) by VALUED_1:12; then A4: Z c= dom tan by XBOOLE_1:18; A5: Z c= dom (id Z) by A3, XBOOLE_1:18; then A6: id Z is_differentiable_on Z by A1, FDIFF_1:23; for x being Real st x in Z holds tan is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies tan is_differentiable_in x ) assume x in Z ; ::_thesis: tan is_differentiable_in x then cos . x <> 0 by A4, Th1; hence tan is_differentiable_in x by FDIFF_7:46; ::_thesis: verum end; then A7: tan is_differentiable_on Z by A4, FDIFF_1:9; for x being Real st x in Z holds ((tan - (id Z)) `| Z) . x = ((sin . x) ^2) / ((cos . x) ^2) proof let x be Real; ::_thesis: ( x in Z implies ((tan - (id Z)) `| Z) . x = ((sin . x) ^2) / ((cos . x) ^2) ) assume A8: x in Z ; ::_thesis: ((tan - (id Z)) `| Z) . x = ((sin . x) ^2) / ((cos . x) ^2) then A9: cos . x <> 0 by A4, Th1; then A10: (cos . x) ^2 > 0 by SQUARE_1:12; ((tan - (id Z)) `| Z) . x = (diff (tan,x)) - (diff ((id Z),x)) by A2, A6, A7, A8, FDIFF_1:19 .= (1 / ((cos . x) ^2)) - (diff ((id Z),x)) by A9, FDIFF_7:46 .= (1 / ((cos . x) ^2)) - (((id Z) `| Z) . x) by A6, A8, FDIFF_1:def_7 .= (1 / ((cos . x) ^2)) - 1 by A5, A1, A8, FDIFF_1:23 .= (1 / ((cos . x) ^2)) - (((cos . x) ^2) / ((cos . x) ^2)) by A10, XCMPLX_1:60 .= (1 - ((cos . x) ^2)) / ((cos . x) ^2) .= ((((sin . x) ^2) + ((cos . x) ^2)) - ((cos . x) ^2)) / ((cos . x) ^2) by SIN_COS:28 .= ((sin . x) ^2) / ((cos . x) ^2) ; hence ((tan - (id Z)) `| Z) . x = ((sin . x) ^2) / ((cos . x) ^2) ; ::_thesis: verum end; hence ( tan - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds ((tan - (id Z)) `| Z) . x = ((sin . x) ^2) / ((cos . x) ^2) ) ) by A2, A6, A7, FDIFF_1:19; ::_thesis: verum end; theorem :: FDIFF_8:25 for Z being open Subset of REAL st Z c= dom ((- cot) - (id Z)) holds ( (- cot) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds (((- cot) - (id Z)) `| Z) . x = ((cos . x) ^2) / ((sin . x) ^2) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((- cot) - (id Z)) implies ( (- cot) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds (((- cot) - (id Z)) `| Z) . x = ((cos . x) ^2) / ((sin . x) ^2) ) ) ) set f = - cot; A1: for x being Real st x in Z holds (id Z) . x = (1 * x) + 0 by FUNCT_1:18; assume A2: Z c= dom ((- cot) - (id Z)) ; ::_thesis: ( (- cot) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds (((- cot) - (id Z)) `| Z) . x = ((cos . x) ^2) / ((sin . x) ^2) ) ) then A3: Z c= (dom (- cot)) /\ (dom (id Z)) by VALUED_1:12; then A4: Z c= dom (- cot) by XBOOLE_1:18; then A5: Z c= dom cot by VALUED_1:8; for x being Real st x in Z holds cot is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies cot is_differentiable_in x ) assume x in Z ; ::_thesis: cot is_differentiable_in x then sin . x <> 0 by A5, Th2; hence cot is_differentiable_in x by FDIFF_7:47; ::_thesis: verum end; then A6: cot is_differentiable_on Z by A5, FDIFF_1:9; then A7: (- 1) (#) cot is_differentiable_on Z by A4, FDIFF_1:20; A8: Z c= dom (id Z) by A3, XBOOLE_1:18; then A9: id Z is_differentiable_on Z by A1, FDIFF_1:23; for x being Real st x in Z holds (((- cot) - (id Z)) `| Z) . x = ((cos . x) ^2) / ((sin . x) ^2) proof let x be Real; ::_thesis: ( x in Z implies (((- cot) - (id Z)) `| Z) . x = ((cos . x) ^2) / ((sin . x) ^2) ) assume A10: x in Z ; ::_thesis: (((- cot) - (id Z)) `| Z) . x = ((cos . x) ^2) / ((sin . x) ^2) then A11: sin . x <> 0 by A5, Th2; then A12: (sin . x) ^2 > 0 by SQUARE_1:12; (((- cot) - (id Z)) `| Z) . x = (diff ((- cot),x)) - (diff ((id Z),x)) by A2, A9, A7, A10, FDIFF_1:19 .= ((((- 1) (#) cot) `| Z) . x) - (diff ((id Z),x)) by A7, A10, FDIFF_1:def_7 .= ((- 1) * (diff (cot,x))) - (diff ((id Z),x)) by A4, A6, A10, FDIFF_1:20 .= ((- 1) * (- (1 / ((sin . x) ^2)))) - (diff ((id Z),x)) by A11, FDIFF_7:47 .= (1 / ((sin . x) ^2)) - (((id Z) `| Z) . x) by A9, A10, FDIFF_1:def_7 .= (1 / ((sin . x) ^2)) - 1 by A8, A1, A10, FDIFF_1:23 .= (1 / ((sin . x) ^2)) - (((sin . x) ^2) / ((sin . x) ^2)) by A12, XCMPLX_1:60 .= (1 - ((sin . x) ^2)) / ((sin . x) ^2) .= ((((cos . x) ^2) + ((sin . x) ^2)) - ((sin . x) ^2)) / ((sin . x) ^2) by SIN_COS:28 .= ((cos . x) ^2) / ((sin . x) ^2) ; hence (((- cot) - (id Z)) `| Z) . x = ((cos . x) ^2) / ((sin . x) ^2) ; ::_thesis: verum end; hence ( (- cot) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds (((- cot) - (id Z)) `| Z) . x = ((cos . x) ^2) / ((sin . x) ^2) ) ) by A2, A9, A7, FDIFF_1:19; ::_thesis: verum end; theorem :: FDIFF_8:26 for a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (((1 / a) (#) (tan * f)) - (id Z)) & ( for x being Real st x in Z holds ( f . x = a * x & a <> 0 ) ) holds ( ((1 / a) (#) (tan * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds ((((1 / a) (#) (tan * f)) - (id Z)) `| Z) . x = ((sin . (a * x)) ^2) / ((cos . (a * x)) ^2) ) ) proof let a be Real; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (((1 / a) (#) (tan * f)) - (id Z)) & ( for x being Real st x in Z holds ( f . x = a * x & a <> 0 ) ) holds ( ((1 / a) (#) (tan * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds ((((1 / a) (#) (tan * f)) - (id Z)) `| Z) . x = ((sin . (a * x)) ^2) / ((cos . (a * x)) ^2) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom (((1 / a) (#) (tan * f)) - (id Z)) & ( for x being Real st x in Z holds ( f . x = a * x & a <> 0 ) ) holds ( ((1 / a) (#) (tan * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds ((((1 / a) (#) (tan * f)) - (id Z)) `| Z) . x = ((sin . (a * x)) ^2) / ((cos . (a * x)) ^2) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (((1 / a) (#) (tan * f)) - (id Z)) & ( for x being Real st x in Z holds ( f . x = a * x & a <> 0 ) ) implies ( ((1 / a) (#) (tan * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds ((((1 / a) (#) (tan * f)) - (id Z)) `| Z) . x = ((sin . (a * x)) ^2) / ((cos . (a * x)) ^2) ) ) ) assume that A1: Z c= dom (((1 / a) (#) (tan * f)) - (id Z)) and A2: for x being Real st x in Z holds ( f . x = a * x & a <> 0 ) ; ::_thesis: ( ((1 / a) (#) (tan * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds ((((1 / a) (#) (tan * f)) - (id Z)) `| Z) . x = ((sin . (a * x)) ^2) / ((cos . (a * x)) ^2) ) ) A3: Z c= (dom ((1 / a) (#) (tan * f))) /\ (dom (id Z)) by A1, VALUED_1:12; then A4: Z c= dom ((1 / a) (#) (tan * f)) by XBOOLE_1:18; then A5: Z c= dom (tan * f) by VALUED_1:def_5; A6: for x being Real st x in Z holds f . x = (a * x) + 0 by A2; then A7: tan * f is_differentiable_on Z by A5, Th6; then A8: (1 / a) (#) (tan * f) is_differentiable_on Z by A4, FDIFF_1:20; set g = (1 / a) (#) (tan * f); A9: for x being Real st x in Z holds (id Z) . x = (1 * x) + 0 by FUNCT_1:18; A10: Z c= dom (id Z) by A3, XBOOLE_1:18; then A11: id Z is_differentiable_on Z by A9, FDIFF_1:23; A12: for x being Real st x in Z holds cos . (f . x) <> 0 proof let x be Real; ::_thesis: ( x in Z implies cos . (f . x) <> 0 ) assume x in Z ; ::_thesis: cos . (f . x) <> 0 then f . x in dom (sin / cos) by A5, FUNCT_1:11; hence cos . (f . x) <> 0 by Th1; ::_thesis: verum end; for x being Real st x in Z holds ((((1 / a) (#) (tan * f)) - (id Z)) `| Z) . x = ((sin . (a * x)) ^2) / ((cos . (a * x)) ^2) proof let x be Real; ::_thesis: ( x in Z implies ((((1 / a) (#) (tan * f)) - (id Z)) `| Z) . x = ((sin . (a * x)) ^2) / ((cos . (a * x)) ^2) ) assume A13: x in Z ; ::_thesis: ((((1 / a) (#) (tan * f)) - (id Z)) `| Z) . x = ((sin . (a * x)) ^2) / ((cos . (a * x)) ^2) then A14: f . x = (a * x) + 0 by A2; cos . (f . x) <> 0 by A12, A13; then A15: (cos . (a * x)) ^2 > 0 by A14, SQUARE_1:12; ((((1 / a) (#) (tan * f)) - (id Z)) `| Z) . x = (diff (((1 / a) (#) (tan * f)),x)) - (diff ((id Z),x)) by A1, A8, A11, A13, FDIFF_1:19 .= ((((1 / a) (#) (tan * f)) `| Z) . x) - (diff ((id Z),x)) by A8, A13, FDIFF_1:def_7 .= ((1 / a) * (diff ((tan * f),x))) - (diff ((id Z),x)) by A4, A7, A13, FDIFF_1:20 .= ((1 / a) * (((tan * f) `| Z) . x)) - (diff ((id Z),x)) by A7, A13, FDIFF_1:def_7 .= ((1 / a) * (((tan * f) `| Z) . x)) - (((id Z) `| Z) . x) by A11, A13, FDIFF_1:def_7 .= ((1 / a) * (a / ((cos . (a * x)) ^2))) - (((id Z) `| Z) . x) by A5, A6, A13, A14, Th6 .= ((1 / ((cos . (a * x)) ^2)) * (a / a)) - 1 by A10, A9, A13, FDIFF_1:23 .= ((1 / ((cos . (a * x)) ^2)) * 1) - 1 by A2, A13, XCMPLX_1:60 .= (1 / ((cos . (a * x)) ^2)) - (((cos . (a * x)) ^2) / ((cos . (a * x)) ^2)) by A15, XCMPLX_1:60 .= (1 - ((cos . (a * x)) ^2)) / ((cos . (a * x)) ^2) .= ((((sin . (a * x)) ^2) + ((cos . (a * x)) ^2)) - ((cos . (a * x)) ^2)) / ((cos . (a * x)) ^2) by SIN_COS:28 .= ((sin . (a * x)) ^2) / ((cos . (a * x)) ^2) ; hence ((((1 / a) (#) (tan * f)) - (id Z)) `| Z) . x = ((sin . (a * x)) ^2) / ((cos . (a * x)) ^2) ; ::_thesis: verum end; hence ( ((1 / a) (#) (tan * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds ((((1 / a) (#) (tan * f)) - (id Z)) `| Z) . x = ((sin . (a * x)) ^2) / ((cos . (a * x)) ^2) ) ) by A1, A8, A11, FDIFF_1:19; ::_thesis: verum end; theorem :: FDIFF_8:27 for a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (((- (1 / a)) (#) (cot * f)) - (id Z)) & ( for x being Real st x in Z holds ( f . x = a * x & a <> 0 ) ) holds ( ((- (1 / a)) (#) (cot * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds ((((- (1 / a)) (#) (cot * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) ^2) / ((sin . (a * x)) ^2) ) ) proof let a be Real; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (((- (1 / a)) (#) (cot * f)) - (id Z)) & ( for x being Real st x in Z holds ( f . x = a * x & a <> 0 ) ) holds ( ((- (1 / a)) (#) (cot * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds ((((- (1 / a)) (#) (cot * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) ^2) / ((sin . (a * x)) ^2) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom (((- (1 / a)) (#) (cot * f)) - (id Z)) & ( for x being Real st x in Z holds ( f . x = a * x & a <> 0 ) ) holds ( ((- (1 / a)) (#) (cot * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds ((((- (1 / a)) (#) (cot * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) ^2) / ((sin . (a * x)) ^2) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (((- (1 / a)) (#) (cot * f)) - (id Z)) & ( for x being Real st x in Z holds ( f . x = a * x & a <> 0 ) ) implies ( ((- (1 / a)) (#) (cot * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds ((((- (1 / a)) (#) (cot * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) ^2) / ((sin . (a * x)) ^2) ) ) ) assume that A1: Z c= dom (((- (1 / a)) (#) (cot * f)) - (id Z)) and A2: for x being Real st x in Z holds ( f . x = a * x & a <> 0 ) ; ::_thesis: ( ((- (1 / a)) (#) (cot * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds ((((- (1 / a)) (#) (cot * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) ^2) / ((sin . (a * x)) ^2) ) ) A3: Z c= (dom ((- (1 / a)) (#) (cot * f))) /\ (dom (id Z)) by A1, VALUED_1:12; then A4: Z c= dom ((- (1 / a)) (#) (cot * f)) by XBOOLE_1:18; then A5: Z c= dom (cot * f) by VALUED_1:def_5; A6: for x being Real st x in Z holds f . x = (a * x) + 0 by A2; then A7: cot * f is_differentiable_on Z by A5, Th7; then A8: (- (1 / a)) (#) (cot * f) is_differentiable_on Z by A4, FDIFF_1:20; set g = (- (1 / a)) (#) (cot * f); A9: for x being Real st x in Z holds (id Z) . x = (1 * x) + 0 by FUNCT_1:18; A10: Z c= dom (id Z) by A3, XBOOLE_1:18; then A11: id Z is_differentiable_on Z by A9, FDIFF_1:23; A12: for x being Real st x in Z holds sin . (f . x) <> 0 proof let x be Real; ::_thesis: ( x in Z implies sin . (f . x) <> 0 ) assume x in Z ; ::_thesis: sin . (f . x) <> 0 then f . x in dom (cos / sin) by A5, FUNCT_1:11; hence sin . (f . x) <> 0 by Th2; ::_thesis: verum end; for x being Real st x in Z holds ((((- (1 / a)) (#) (cot * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) ^2) / ((sin . (a * x)) ^2) proof let x be Real; ::_thesis: ( x in Z implies ((((- (1 / a)) (#) (cot * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) ^2) / ((sin . (a * x)) ^2) ) assume A13: x in Z ; ::_thesis: ((((- (1 / a)) (#) (cot * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) ^2) / ((sin . (a * x)) ^2) then A14: f . x = (a * x) + 0 by A2; sin . (f . x) <> 0 by A12, A13; then A15: (sin . (a * x)) ^2 > 0 by A14, SQUARE_1:12; ((((- (1 / a)) (#) (cot * f)) - (id Z)) `| Z) . x = (diff (((- (1 / a)) (#) (cot * f)),x)) - (diff ((id Z),x)) by A1, A8, A11, A13, FDIFF_1:19 .= ((((- (1 / a)) (#) (cot * f)) `| Z) . x) - (diff ((id Z),x)) by A8, A13, FDIFF_1:def_7 .= ((- (1 / a)) * (diff ((cot * f),x))) - (diff ((id Z),x)) by A4, A7, A13, FDIFF_1:20 .= ((- (1 / a)) * (((cot * f) `| Z) . x)) - (diff ((id Z),x)) by A7, A13, FDIFF_1:def_7 .= ((- (1 / a)) * (((cot * f) `| Z) . x)) - (((id Z) `| Z) . x) by A11, A13, FDIFF_1:def_7 .= ((- (1 / a)) * (- (a / ((sin . (a * x)) ^2)))) - (((id Z) `| Z) . x) by A5, A6, A13, A14, Th7 .= ((1 / ((sin . (a * x)) ^2)) * (a / a)) - 1 by A10, A9, A13, FDIFF_1:23 .= ((1 / ((sin . (a * x)) ^2)) * 1) - 1 by A2, A13, XCMPLX_1:60 .= (1 / ((sin . (a * x)) ^2)) - (((sin . (a * x)) ^2) / ((sin . (a * x)) ^2)) by A15, XCMPLX_1:60 .= (1 - ((sin . (a * x)) ^2)) / ((sin . (a * x)) ^2) .= ((((cos . (a * x)) ^2) + ((sin . (a * x)) ^2)) - ((sin . (a * x)) ^2)) / ((sin . (a * x)) ^2) by SIN_COS:28 .= ((cos . (a * x)) ^2) / ((sin . (a * x)) ^2) ; hence ((((- (1 / a)) (#) (cot * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) ^2) / ((sin . (a * x)) ^2) ; ::_thesis: verum end; hence ( ((- (1 / a)) (#) (cot * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds ((((- (1 / a)) (#) (cot * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) ^2) / ((sin . (a * x)) ^2) ) ) by A1, A8, A11, FDIFF_1:19; ::_thesis: verum end; theorem :: FDIFF_8:28 for a, b being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (f (#) tan) & ( for x being Real st x in Z holds f . x = (a * x) + b ) holds ( f (#) tan is_differentiable_on Z & ( for x being Real st x in Z holds ((f (#) tan) `| Z) . x = ((a * (sin . x)) / (cos . x)) + (((a * x) + b) / ((cos . x) ^2)) ) ) proof let a, b be Real; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (f (#) tan) & ( for x being Real st x in Z holds f . x = (a * x) + b ) holds ( f (#) tan is_differentiable_on Z & ( for x being Real st x in Z holds ((f (#) tan) `| Z) . x = ((a * (sin . x)) / (cos . x)) + (((a * x) + b) / ((cos . x) ^2)) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom (f (#) tan) & ( for x being Real st x in Z holds f . x = (a * x) + b ) holds ( f (#) tan is_differentiable_on Z & ( for x being Real st x in Z holds ((f (#) tan) `| Z) . x = ((a * (sin . x)) / (cos . x)) + (((a * x) + b) / ((cos . x) ^2)) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (f (#) tan) & ( for x being Real st x in Z holds f . x = (a * x) + b ) implies ( f (#) tan is_differentiable_on Z & ( for x being Real st x in Z holds ((f (#) tan) `| Z) . x = ((a * (sin . x)) / (cos . x)) + (((a * x) + b) / ((cos . x) ^2)) ) ) ) assume that A1: Z c= dom (f (#) tan) and A2: for x being Real st x in Z holds f . x = (a * x) + b ; ::_thesis: ( f (#) tan is_differentiable_on Z & ( for x being Real st x in Z holds ((f (#) tan) `| Z) . x = ((a * (sin . x)) / (cos . x)) + (((a * x) + b) / ((cos . x) ^2)) ) ) A3: Z c= (dom f) /\ (dom tan) by A1, VALUED_1:def_4; then A4: Z c= dom tan by XBOOLE_1:18; A5: Z c= dom f by A3, XBOOLE_1:18; then A6: f is_differentiable_on Z by A2, FDIFF_1:23; A7: for x being Real st x in Z holds ( tan is_differentiable_in x & diff (tan,x) = 1 / ((cos . x) ^2) ) proof let x be Real; ::_thesis: ( x in Z implies ( tan is_differentiable_in x & diff (tan,x) = 1 / ((cos . x) ^2) ) ) assume x in Z ; ::_thesis: ( tan is_differentiable_in x & diff (tan,x) = 1 / ((cos . x) ^2) ) then cos . x <> 0 by A4, Th1; hence ( tan is_differentiable_in x & diff (tan,x) = 1 / ((cos . x) ^2) ) by FDIFF_7:46; ::_thesis: verum end; then for x being Real st x in Z holds tan is_differentiable_in x ; then A8: tan is_differentiable_on Z by A4, FDIFF_1:9; for x being Real st x in Z holds ((f (#) tan) `| Z) . x = ((a * (sin . x)) / (cos . x)) + (((a * x) + b) / ((cos . x) ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((f (#) tan) `| Z) . x = ((a * (sin . x)) / (cos . x)) + (((a * x) + b) / ((cos . x) ^2)) ) assume A9: x in Z ; ::_thesis: ((f (#) tan) `| Z) . x = ((a * (sin . x)) / (cos . x)) + (((a * x) + b) / ((cos . x) ^2)) then ((f (#) tan) `| Z) . x = ((tan . x) * (diff (f,x))) + ((f . x) * (diff (tan,x))) by A1, A6, A8, FDIFF_1:21 .= ((tan . x) * ((f `| Z) . x)) + ((f . x) * (diff (tan,x))) by A6, A9, FDIFF_1:def_7 .= ((tan . x) * a) + ((f . x) * (diff (tan,x))) by A2, A5, A9, FDIFF_1:23 .= ((tan . x) * a) + (((a * x) + b) * (diff (tan,x))) by A2, A9 .= ((tan . x) * a) + (((a * x) + b) * (1 / ((cos . x) ^2))) by A7, A9 .= (((sin . x) / (cos . x)) * (a / 1)) + (((a * x) + b) / ((cos . x) ^2)) by A4, A9, RFUNCT_1:def_1 .= ((a * (sin . x)) / (cos . x)) + (((a * x) + b) / ((cos . x) ^2)) ; hence ((f (#) tan) `| Z) . x = ((a * (sin . x)) / (cos . x)) + (((a * x) + b) / ((cos . x) ^2)) ; ::_thesis: verum end; hence ( f (#) tan is_differentiable_on Z & ( for x being Real st x in Z holds ((f (#) tan) `| Z) . x = ((a * (sin . x)) / (cos . x)) + (((a * x) + b) / ((cos . x) ^2)) ) ) by A1, A6, A8, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_8:29 for a, b being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (f (#) cot) & ( for x being Real st x in Z holds f . x = (a * x) + b ) holds ( f (#) cot is_differentiable_on Z & ( for x being Real st x in Z holds ((f (#) cot) `| Z) . x = ((a * (cos . x)) / (sin . x)) - (((a * x) + b) / ((sin . x) ^2)) ) ) proof let a, b be Real; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (f (#) cot) & ( for x being Real st x in Z holds f . x = (a * x) + b ) holds ( f (#) cot is_differentiable_on Z & ( for x being Real st x in Z holds ((f (#) cot) `| Z) . x = ((a * (cos . x)) / (sin . x)) - (((a * x) + b) / ((sin . x) ^2)) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom (f (#) cot) & ( for x being Real st x in Z holds f . x = (a * x) + b ) holds ( f (#) cot is_differentiable_on Z & ( for x being Real st x in Z holds ((f (#) cot) `| Z) . x = ((a * (cos . x)) / (sin . x)) - (((a * x) + b) / ((sin . x) ^2)) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (f (#) cot) & ( for x being Real st x in Z holds f . x = (a * x) + b ) implies ( f (#) cot is_differentiable_on Z & ( for x being Real st x in Z holds ((f (#) cot) `| Z) . x = ((a * (cos . x)) / (sin . x)) - (((a * x) + b) / ((sin . x) ^2)) ) ) ) assume that A1: Z c= dom (f (#) cot) and A2: for x being Real st x in Z holds f . x = (a * x) + b ; ::_thesis: ( f (#) cot is_differentiable_on Z & ( for x being Real st x in Z holds ((f (#) cot) `| Z) . x = ((a * (cos . x)) / (sin . x)) - (((a * x) + b) / ((sin . x) ^2)) ) ) A3: Z c= (dom f) /\ (dom cot) by A1, VALUED_1:def_4; then A4: Z c= dom cot by XBOOLE_1:18; A5: Z c= dom f by A3, XBOOLE_1:18; then A6: f is_differentiable_on Z by A2, FDIFF_1:23; A7: for x being Real st x in Z holds ( cot is_differentiable_in x & diff (cot,x) = - (1 / ((sin . x) ^2)) ) proof let x be Real; ::_thesis: ( x in Z implies ( cot is_differentiable_in x & diff (cot,x) = - (1 / ((sin . x) ^2)) ) ) assume x in Z ; ::_thesis: ( cot is_differentiable_in x & diff (cot,x) = - (1 / ((sin . x) ^2)) ) then sin . x <> 0 by A4, Th2; hence ( cot is_differentiable_in x & diff (cot,x) = - (1 / ((sin . x) ^2)) ) by FDIFF_7:47; ::_thesis: verum end; then for x being Real st x in Z holds cot is_differentiable_in x ; then A8: cot is_differentiable_on Z by A4, FDIFF_1:9; for x being Real st x in Z holds ((f (#) cot) `| Z) . x = ((a * (cos . x)) / (sin . x)) - (((a * x) + b) / ((sin . x) ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((f (#) cot) `| Z) . x = ((a * (cos . x)) / (sin . x)) - (((a * x) + b) / ((sin . x) ^2)) ) assume A9: x in Z ; ::_thesis: ((f (#) cot) `| Z) . x = ((a * (cos . x)) / (sin . x)) - (((a * x) + b) / ((sin . x) ^2)) then ((f (#) cot) `| Z) . x = ((cot . x) * (diff (f,x))) + ((f . x) * (diff (cot,x))) by A1, A6, A8, FDIFF_1:21 .= ((cot . x) * ((f `| Z) . x)) + ((f . x) * (diff (cot,x))) by A6, A9, FDIFF_1:def_7 .= ((cot . x) * a) + ((f . x) * (diff (cot,x))) by A2, A5, A9, FDIFF_1:23 .= ((cot . x) * a) + (((a * x) + b) * (diff (cot,x))) by A2, A9 .= ((cot . x) * a) + (((a * x) + b) * (- (1 / ((sin . x) ^2)))) by A7, A9 .= (((cos . x) / (sin . x)) * (a / 1)) - (((a * x) + b) / ((sin . x) ^2)) by A4, A9, RFUNCT_1:def_1 .= ((a * (cos . x)) / (sin . x)) - (((a * x) + b) / ((sin . x) ^2)) ; hence ((f (#) cot) `| Z) . x = ((a * (cos . x)) / (sin . x)) - (((a * x) + b) / ((sin . x) ^2)) ; ::_thesis: verum end; hence ( f (#) cot is_differentiable_on Z & ( for x being Real st x in Z holds ((f (#) cot) `| Z) . x = ((a * (cos . x)) / (sin . x)) - (((a * x) + b) / ((sin . x) ^2)) ) ) by A1, A6, A8, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_8:30 for Z being open Subset of REAL st Z c= dom (exp_R (#) tan) holds ( exp_R (#) tan is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) tan) `| Z) . x = (((exp_R . x) * (sin . x)) / (cos . x)) + ((exp_R . x) / ((cos . x) ^2)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (exp_R (#) tan) implies ( exp_R (#) tan is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) tan) `| Z) . x = (((exp_R . x) * (sin . x)) / (cos . x)) + ((exp_R . x) / ((cos . x) ^2)) ) ) ) A1: for x being Real st x in Z holds exp_R is_differentiable_in x by SIN_COS:65; assume A2: Z c= dom (exp_R (#) tan) ; ::_thesis: ( exp_R (#) tan is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) tan) `| Z) . x = (((exp_R . x) * (sin . x)) / (cos . x)) + ((exp_R . x) / ((cos . x) ^2)) ) ) then A3: Z c= (dom exp_R) /\ (dom tan) by VALUED_1:def_4; then A4: Z c= dom tan by XBOOLE_1:18; Z c= dom exp_R by A3, XBOOLE_1:18; then A5: exp_R is_differentiable_on Z by A1, FDIFF_1:9; A6: for x being Real st x in Z holds ( tan is_differentiable_in x & diff (tan,x) = 1 / ((cos . x) ^2) ) proof let x be Real; ::_thesis: ( x in Z implies ( tan is_differentiable_in x & diff (tan,x) = 1 / ((cos . x) ^2) ) ) assume x in Z ; ::_thesis: ( tan is_differentiable_in x & diff (tan,x) = 1 / ((cos . x) ^2) ) then cos . x <> 0 by A4, Th1; hence ( tan is_differentiable_in x & diff (tan,x) = 1 / ((cos . x) ^2) ) by FDIFF_7:46; ::_thesis: verum end; then for x being Real st x in Z holds tan is_differentiable_in x ; then A7: tan is_differentiable_on Z by A4, FDIFF_1:9; for x being Real st x in Z holds ((exp_R (#) tan) `| Z) . x = (((exp_R . x) * (sin . x)) / (cos . x)) + ((exp_R . x) / ((cos . x) ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((exp_R (#) tan) `| Z) . x = (((exp_R . x) * (sin . x)) / (cos . x)) + ((exp_R . x) / ((cos . x) ^2)) ) assume A8: x in Z ; ::_thesis: ((exp_R (#) tan) `| Z) . x = (((exp_R . x) * (sin . x)) / (cos . x)) + ((exp_R . x) / ((cos . x) ^2)) then ((exp_R (#) tan) `| Z) . x = ((tan . x) * (diff (exp_R,x))) + ((exp_R . x) * (diff (tan,x))) by A2, A5, A7, FDIFF_1:21 .= ((tan . x) * (exp_R . x)) + ((exp_R . x) * (diff (tan,x))) by SIN_COS:65 .= ((tan . x) * (exp_R . x)) + ((exp_R . x) * (1 / ((cos . x) ^2))) by A6, A8 .= (((sin . x) / (cos . x)) * ((exp_R . x) / 1)) + ((exp_R . x) / ((cos . x) ^2)) by A4, A8, RFUNCT_1:def_1 .= (((exp_R . x) * (sin . x)) / (cos . x)) + ((exp_R . x) / ((cos . x) ^2)) ; hence ((exp_R (#) tan) `| Z) . x = (((exp_R . x) * (sin . x)) / (cos . x)) + ((exp_R . x) / ((cos . x) ^2)) ; ::_thesis: verum end; hence ( exp_R (#) tan is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) tan) `| Z) . x = (((exp_R . x) * (sin . x)) / (cos . x)) + ((exp_R . x) / ((cos . x) ^2)) ) ) by A2, A5, A7, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_8:31 for Z being open Subset of REAL st Z c= dom (exp_R (#) cot) holds ( exp_R (#) cot is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) cot) `| Z) . x = (((exp_R . x) * (cos . x)) / (sin . x)) - ((exp_R . x) / ((sin . x) ^2)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (exp_R (#) cot) implies ( exp_R (#) cot is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) cot) `| Z) . x = (((exp_R . x) * (cos . x)) / (sin . x)) - ((exp_R . x) / ((sin . x) ^2)) ) ) ) A1: for x being Real st x in Z holds exp_R is_differentiable_in x by SIN_COS:65; assume A2: Z c= dom (exp_R (#) cot) ; ::_thesis: ( exp_R (#) cot is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) cot) `| Z) . x = (((exp_R . x) * (cos . x)) / (sin . x)) - ((exp_R . x) / ((sin . x) ^2)) ) ) then A3: Z c= (dom exp_R) /\ (dom cot) by VALUED_1:def_4; then A4: Z c= dom cot by XBOOLE_1:18; Z c= dom exp_R by A3, XBOOLE_1:18; then A5: exp_R is_differentiable_on Z by A1, FDIFF_1:9; A6: for x being Real st x in Z holds ( cot is_differentiable_in x & diff (cot,x) = - (1 / ((sin . x) ^2)) ) proof let x be Real; ::_thesis: ( x in Z implies ( cot is_differentiable_in x & diff (cot,x) = - (1 / ((sin . x) ^2)) ) ) assume x in Z ; ::_thesis: ( cot is_differentiable_in x & diff (cot,x) = - (1 / ((sin . x) ^2)) ) then sin . x <> 0 by A4, Th2; hence ( cot is_differentiable_in x & diff (cot,x) = - (1 / ((sin . x) ^2)) ) by FDIFF_7:47; ::_thesis: verum end; then for x being Real st x in Z holds cot is_differentiable_in x ; then A7: cot is_differentiable_on Z by A4, FDIFF_1:9; for x being Real st x in Z holds ((exp_R (#) cot) `| Z) . x = (((exp_R . x) * (cos . x)) / (sin . x)) - ((exp_R . x) / ((sin . x) ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((exp_R (#) cot) `| Z) . x = (((exp_R . x) * (cos . x)) / (sin . x)) - ((exp_R . x) / ((sin . x) ^2)) ) assume A8: x in Z ; ::_thesis: ((exp_R (#) cot) `| Z) . x = (((exp_R . x) * (cos . x)) / (sin . x)) - ((exp_R . x) / ((sin . x) ^2)) then ((exp_R (#) cot) `| Z) . x = ((cot . x) * (diff (exp_R,x))) + ((exp_R . x) * (diff (cot,x))) by A2, A5, A7, FDIFF_1:21 .= ((cot . x) * (exp_R . x)) + ((exp_R . x) * (diff (cot,x))) by SIN_COS:65 .= ((cot . x) * (exp_R . x)) + ((exp_R . x) * (- (1 / ((sin . x) ^2)))) by A6, A8 .= (((cos . x) / (sin . x)) * ((exp_R . x) / 1)) - ((exp_R . x) / ((sin . x) ^2)) by A4, A8, RFUNCT_1:def_1 .= (((exp_R . x) * (cos . x)) / (sin . x)) - ((exp_R . x) / ((sin . x) ^2)) ; hence ((exp_R (#) cot) `| Z) . x = (((exp_R . x) * (cos . x)) / (sin . x)) - ((exp_R . x) / ((sin . x) ^2)) ; ::_thesis: verum end; hence ( exp_R (#) cot is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) cot) `| Z) . x = (((exp_R . x) * (cos . x)) / (sin . x)) - ((exp_R . x) / ((sin . x) ^2)) ) ) by A2, A5, A7, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_8:32 for Z being open Subset of REAL st Z c= dom (ln (#) tan) holds ( ln (#) tan is_differentiable_on Z & ( for x being Real st x in Z holds ((ln (#) tan) `| Z) . x = (((sin . x) / (cos . x)) / x) + ((ln . x) / ((cos . x) ^2)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (ln (#) tan) implies ( ln (#) tan is_differentiable_on Z & ( for x being Real st x in Z holds ((ln (#) tan) `| Z) . x = (((sin . x) / (cos . x)) / x) + ((ln . x) / ((cos . x) ^2)) ) ) ) assume A1: Z c= dom (ln (#) tan) ; ::_thesis: ( ln (#) tan is_differentiable_on Z & ( for x being Real st x in Z holds ((ln (#) tan) `| Z) . x = (((sin . x) / (cos . x)) / x) + ((ln . x) / ((cos . x) ^2)) ) ) then A2: Z c= (dom ln) /\ (dom tan) by VALUED_1:def_4; then A3: Z c= dom tan by XBOOLE_1:18; A4: for x being Real st x in Z holds ( tan is_differentiable_in x & diff (tan,x) = 1 / ((cos . x) ^2) ) proof let x be Real; ::_thesis: ( x in Z implies ( tan is_differentiable_in x & diff (tan,x) = 1 / ((cos . x) ^2) ) ) assume x in Z ; ::_thesis: ( tan is_differentiable_in x & diff (tan,x) = 1 / ((cos . x) ^2) ) then cos . x <> 0 by A3, Th1; hence ( tan is_differentiable_in x & diff (tan,x) = 1 / ((cos . x) ^2) ) by FDIFF_7:46; ::_thesis: verum end; then for x being Real st x in Z holds tan is_differentiable_in x ; then A5: tan is_differentiable_on Z by A3, FDIFF_1:9; A6: Z c= dom ln by A2, XBOOLE_1:18; A7: for x being Real st x in Z holds x > 0 proof let x be Real; ::_thesis: ( x in Z implies x > 0 ) assume x in Z ; ::_thesis: x > 0 then x in right_open_halfline 0 by A6, TAYLOR_1:18; then ex g being Real st ( x = g & 0 < g ) by Lm1; hence x > 0 ; ::_thesis: verum end; then for x being Real st x in Z holds ln is_differentiable_in x by TAYLOR_1:18; then A8: ln is_differentiable_on Z by A6, FDIFF_1:9; A9: for x being Real st x in Z holds diff (ln,x) = 1 / x proof let x be Real; ::_thesis: ( x in Z implies diff (ln,x) = 1 / x ) assume x in Z ; ::_thesis: diff (ln,x) = 1 / x then x > 0 by A7; then x in right_open_halfline 0 by Lm1; hence diff (ln,x) = 1 / x by TAYLOR_1:18; ::_thesis: verum end; for x being Real st x in Z holds ((ln (#) tan) `| Z) . x = (((sin . x) / (cos . x)) / x) + ((ln . x) / ((cos . x) ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((ln (#) tan) `| Z) . x = (((sin . x) / (cos . x)) / x) + ((ln . x) / ((cos . x) ^2)) ) assume A10: x in Z ; ::_thesis: ((ln (#) tan) `| Z) . x = (((sin . x) / (cos . x)) / x) + ((ln . x) / ((cos . x) ^2)) then ((ln (#) tan) `| Z) . x = ((tan . x) * (diff (ln,x))) + ((ln . x) * (diff (tan,x))) by A1, A8, A5, FDIFF_1:21 .= ((tan . x) * (1 / x)) + ((ln . x) * (diff (tan,x))) by A9, A10 .= ((tan . x) * (1 / x)) + ((ln . x) * (1 / ((cos . x) ^2))) by A4, A10 .= (((sin . x) / (cos . x)) / x) + ((ln . x) / ((cos . x) ^2)) by A3, A10, RFUNCT_1:def_1 ; hence ((ln (#) tan) `| Z) . x = (((sin . x) / (cos . x)) / x) + ((ln . x) / ((cos . x) ^2)) ; ::_thesis: verum end; hence ( ln (#) tan is_differentiable_on Z & ( for x being Real st x in Z holds ((ln (#) tan) `| Z) . x = (((sin . x) / (cos . x)) / x) + ((ln . x) / ((cos . x) ^2)) ) ) by A1, A8, A5, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_8:33 for Z being open Subset of REAL st Z c= dom (ln (#) cot) holds ( ln (#) cot is_differentiable_on Z & ( for x being Real st x in Z holds ((ln (#) cot) `| Z) . x = (((cos . x) / (sin . x)) / x) - ((ln . x) / ((sin . x) ^2)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (ln (#) cot) implies ( ln (#) cot is_differentiable_on Z & ( for x being Real st x in Z holds ((ln (#) cot) `| Z) . x = (((cos . x) / (sin . x)) / x) - ((ln . x) / ((sin . x) ^2)) ) ) ) assume A1: Z c= dom (ln (#) cot) ; ::_thesis: ( ln (#) cot is_differentiable_on Z & ( for x being Real st x in Z holds ((ln (#) cot) `| Z) . x = (((cos . x) / (sin . x)) / x) - ((ln . x) / ((sin . x) ^2)) ) ) then A2: Z c= (dom ln) /\ (dom cot) by VALUED_1:def_4; then A3: Z c= dom cot by XBOOLE_1:18; A4: for x being Real st x in Z holds ( cot is_differentiable_in x & diff (cot,x) = - (1 / ((sin . x) ^2)) ) proof let x be Real; ::_thesis: ( x in Z implies ( cot is_differentiable_in x & diff (cot,x) = - (1 / ((sin . x) ^2)) ) ) assume x in Z ; ::_thesis: ( cot is_differentiable_in x & diff (cot,x) = - (1 / ((sin . x) ^2)) ) then sin . x <> 0 by A3, Th2; hence ( cot is_differentiable_in x & diff (cot,x) = - (1 / ((sin . x) ^2)) ) by FDIFF_7:47; ::_thesis: verum end; then for x being Real st x in Z holds cot is_differentiable_in x ; then A5: cot is_differentiable_on Z by A3, FDIFF_1:9; A6: Z c= dom ln by A2, XBOOLE_1:18; A7: for x being Real st x in Z holds x > 0 proof let x be Real; ::_thesis: ( x in Z implies x > 0 ) assume x in Z ; ::_thesis: x > 0 then x in right_open_halfline 0 by A6, TAYLOR_1:18; then ex g being Real st ( x = g & 0 < g ) by Lm1; hence x > 0 ; ::_thesis: verum end; then for x being Real st x in Z holds ln is_differentiable_in x by TAYLOR_1:18; then A8: ln is_differentiable_on Z by A6, FDIFF_1:9; A9: for x being Real st x in Z holds diff (ln,x) = 1 / x proof let x be Real; ::_thesis: ( x in Z implies diff (ln,x) = 1 / x ) assume x in Z ; ::_thesis: diff (ln,x) = 1 / x then x > 0 by A7; then x in right_open_halfline 0 by Lm1; hence diff (ln,x) = 1 / x by TAYLOR_1:18; ::_thesis: verum end; for x being Real st x in Z holds ((ln (#) cot) `| Z) . x = (((cos . x) / (sin . x)) / x) - ((ln . x) / ((sin . x) ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((ln (#) cot) `| Z) . x = (((cos . x) / (sin . x)) / x) - ((ln . x) / ((sin . x) ^2)) ) assume A10: x in Z ; ::_thesis: ((ln (#) cot) `| Z) . x = (((cos . x) / (sin . x)) / x) - ((ln . x) / ((sin . x) ^2)) then ((ln (#) cot) `| Z) . x = ((cot . x) * (diff (ln,x))) + ((ln . x) * (diff (cot,x))) by A1, A8, A5, FDIFF_1:21 .= ((cot . x) * (1 / x)) + ((ln . x) * (diff (cot,x))) by A9, A10 .= ((cot . x) * (1 / x)) + ((ln . x) * (- (1 / ((sin . x) ^2)))) by A4, A10 .= (((cos . x) / (sin . x)) / x) - ((ln . x) / ((sin . x) ^2)) by A3, A10, RFUNCT_1:def_1 ; hence ((ln (#) cot) `| Z) . x = (((cos . x) / (sin . x)) / x) - ((ln . x) / ((sin . x) ^2)) ; ::_thesis: verum end; hence ( ln (#) cot is_differentiable_on Z & ( for x being Real st x in Z holds ((ln (#) cot) `| Z) . x = (((cos . x) / (sin . x)) / x) - ((ln . x) / ((sin . x) ^2)) ) ) by A1, A8, A5, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_8:34 for Z being open Subset of REAL st not 0 in Z & Z c= dom (((id Z) ^) (#) tan) holds ( ((id Z) ^) (#) tan is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) ^) (#) tan) `| Z) . x = (- (((sin . x) / (cos . x)) / (x ^2))) + ((1 / x) / ((cos . x) ^2)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( not 0 in Z & Z c= dom (((id Z) ^) (#) tan) implies ( ((id Z) ^) (#) tan is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) ^) (#) tan) `| Z) . x = (- (((sin . x) / (cos . x)) / (x ^2))) + ((1 / x) / ((cos . x) ^2)) ) ) ) set f = id Z; assume that A1: not 0 in Z and A2: Z c= dom (((id Z) ^) (#) tan) ; ::_thesis: ( ((id Z) ^) (#) tan is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) ^) (#) tan) `| Z) . x = (- (((sin . x) / (cos . x)) / (x ^2))) + ((1 / x) / ((cos . x) ^2)) ) ) A3: (id Z) ^ is_differentiable_on Z by A1, FDIFF_5:4; A4: Z c= (dom ((id Z) ^)) /\ (dom tan) by A2, VALUED_1:def_4; then A5: Z c= dom tan by XBOOLE_1:18; A6: for x being Real st x in Z holds ( tan is_differentiable_in x & diff (tan,x) = 1 / ((cos . x) ^2) ) proof let x be Real; ::_thesis: ( x in Z implies ( tan is_differentiable_in x & diff (tan,x) = 1 / ((cos . x) ^2) ) ) assume x in Z ; ::_thesis: ( tan is_differentiable_in x & diff (tan,x) = 1 / ((cos . x) ^2) ) then cos . x <> 0 by A5, Th1; hence ( tan is_differentiable_in x & diff (tan,x) = 1 / ((cos . x) ^2) ) by FDIFF_7:46; ::_thesis: verum end; then for x being Real st x in Z holds tan is_differentiable_in x ; then A7: tan is_differentiable_on Z by A5, FDIFF_1:9; A8: Z c= dom ((id Z) ^) by A4, XBOOLE_1:18; for x being Real st x in Z holds ((((id Z) ^) (#) tan) `| Z) . x = (- (((sin . x) / (cos . x)) / (x ^2))) + ((1 / x) / ((cos . x) ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((((id Z) ^) (#) tan) `| Z) . x = (- (((sin . x) / (cos . x)) / (x ^2))) + ((1 / x) / ((cos . x) ^2)) ) assume A9: x in Z ; ::_thesis: ((((id Z) ^) (#) tan) `| Z) . x = (- (((sin . x) / (cos . x)) / (x ^2))) + ((1 / x) / ((cos . x) ^2)) then ((((id Z) ^) (#) tan) `| Z) . x = ((tan . x) * (diff (((id Z) ^),x))) + ((((id Z) ^) . x) * (diff (tan,x))) by A2, A3, A7, FDIFF_1:21 .= ((tan . x) * ((((id Z) ^) `| Z) . x)) + ((((id Z) ^) . x) * (diff (tan,x))) by A3, A9, FDIFF_1:def_7 .= ((tan . x) * (- (1 / (x ^2)))) + ((((id Z) ^) . x) * (diff (tan,x))) by A1, A9, FDIFF_5:4 .= (- ((tan . x) * (1 / (x ^2)))) + ((((id Z) ^) . x) * (1 / ((cos . x) ^2))) by A6, A9 .= (- (((sin . x) / (cos . x)) * (1 / (x ^2)))) + ((((id Z) ^) . x) / ((cos . x) ^2)) by A5, A9, RFUNCT_1:def_1 .= (- (((sin . x) / (cos . x)) / (x ^2))) + ((((id Z) . x) ") / ((cos . x) ^2)) by A8, A9, RFUNCT_1:def_2 .= (- (((sin . x) / (cos . x)) / (x ^2))) + ((1 / x) / ((cos . x) ^2)) by A9, FUNCT_1:18 ; hence ((((id Z) ^) (#) tan) `| Z) . x = (- (((sin . x) / (cos . x)) / (x ^2))) + ((1 / x) / ((cos . x) ^2)) ; ::_thesis: verum end; hence ( ((id Z) ^) (#) tan is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) ^) (#) tan) `| Z) . x = (- (((sin . x) / (cos . x)) / (x ^2))) + ((1 / x) / ((cos . x) ^2)) ) ) by A2, A3, A7, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_8:35 for Z being open Subset of REAL st not 0 in Z & Z c= dom (((id Z) ^) (#) cot) holds ( ((id Z) ^) (#) cot is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) ^) (#) cot) `| Z) . x = (- (((cos . x) / (sin . x)) / (x ^2))) - ((1 / x) / ((sin . x) ^2)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( not 0 in Z & Z c= dom (((id Z) ^) (#) cot) implies ( ((id Z) ^) (#) cot is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) ^) (#) cot) `| Z) . x = (- (((cos . x) / (sin . x)) / (x ^2))) - ((1 / x) / ((sin . x) ^2)) ) ) ) set f = id Z; assume that A1: not 0 in Z and A2: Z c= dom (((id Z) ^) (#) cot) ; ::_thesis: ( ((id Z) ^) (#) cot is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) ^) (#) cot) `| Z) . x = (- (((cos . x) / (sin . x)) / (x ^2))) - ((1 / x) / ((sin . x) ^2)) ) ) A3: (id Z) ^ is_differentiable_on Z by A1, FDIFF_5:4; A4: Z c= (dom ((id Z) ^)) /\ (dom cot) by A2, VALUED_1:def_4; then A5: Z c= dom cot by XBOOLE_1:18; A6: for x being Real st x in Z holds ( cot is_differentiable_in x & diff (cot,x) = - (1 / ((sin . x) ^2)) ) proof let x be Real; ::_thesis: ( x in Z implies ( cot is_differentiable_in x & diff (cot,x) = - (1 / ((sin . x) ^2)) ) ) assume x in Z ; ::_thesis: ( cot is_differentiable_in x & diff (cot,x) = - (1 / ((sin . x) ^2)) ) then sin . x <> 0 by A5, Th2; hence ( cot is_differentiable_in x & diff (cot,x) = - (1 / ((sin . x) ^2)) ) by FDIFF_7:47; ::_thesis: verum end; then for x being Real st x in Z holds cot is_differentiable_in x ; then A7: cot is_differentiable_on Z by A5, FDIFF_1:9; A8: Z c= dom ((id Z) ^) by A4, XBOOLE_1:18; for x being Real st x in Z holds ((((id Z) ^) (#) cot) `| Z) . x = (- (((cos . x) / (sin . x)) / (x ^2))) - ((1 / x) / ((sin . x) ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((((id Z) ^) (#) cot) `| Z) . x = (- (((cos . x) / (sin . x)) / (x ^2))) - ((1 / x) / ((sin . x) ^2)) ) assume A9: x in Z ; ::_thesis: ((((id Z) ^) (#) cot) `| Z) . x = (- (((cos . x) / (sin . x)) / (x ^2))) - ((1 / x) / ((sin . x) ^2)) then ((((id Z) ^) (#) cot) `| Z) . x = ((cot . x) * (diff (((id Z) ^),x))) + ((((id Z) ^) . x) * (diff (cot,x))) by A2, A3, A7, FDIFF_1:21 .= ((cot . x) * ((((id Z) ^) `| Z) . x)) + ((((id Z) ^) . x) * (diff (cot,x))) by A3, A9, FDIFF_1:def_7 .= ((cot . x) * (- (1 / (x ^2)))) + ((((id Z) ^) . x) * (diff (cot,x))) by A1, A9, FDIFF_5:4 .= (- ((cot . x) * (1 / (x ^2)))) + ((((id Z) ^) . x) * (- (1 / ((sin . x) ^2)))) by A6, A9 .= (- (((cos . x) / (sin . x)) * (1 / (x ^2)))) - ((((id Z) ^) . x) / ((sin . x) ^2)) by A5, A9, RFUNCT_1:def_1 .= (- (((cos . x) / (sin . x)) / (x ^2))) - ((((id Z) . x) ") / ((sin . x) ^2)) by A8, A9, RFUNCT_1:def_2 .= (- (((cos . x) / (sin . x)) / (x ^2))) - ((1 / x) / ((sin . x) ^2)) by A9, FUNCT_1:18 ; hence ((((id Z) ^) (#) cot) `| Z) . x = (- (((cos . x) / (sin . x)) / (x ^2))) - ((1 / x) / ((sin . x) ^2)) ; ::_thesis: verum end; hence ( ((id Z) ^) (#) cot is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) ^) (#) cot) `| Z) . x = (- (((cos . x) / (sin . x)) / (x ^2))) - ((1 / x) / ((sin . x) ^2)) ) ) by A2, A3, A7, FDIFF_1:21; ::_thesis: verum end;