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