:: FDIFF_10 semantic presentation begin theorem :: FDIFF_10:1 for Z being open Subset of REAL st Z c= dom (tan * cot) holds ( tan * cot is_differentiable_on Z & ( for x being Real st x in Z holds ((tan * cot) `| Z) . x = (1 / ((cos . (cot . x)) ^2)) * (- (1 / ((sin . x) ^2))) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (tan * cot) implies ( tan * cot is_differentiable_on Z & ( for x being Real st x in Z holds ((tan * cot) `| Z) . x = (1 / ((cos . (cot . x)) ^2)) * (- (1 / ((sin . x) ^2))) ) ) ) assume A1: Z c= dom (tan * cot) ; ::_thesis: ( tan * cot is_differentiable_on Z & ( for x being Real st x in Z holds ((tan * cot) `| Z) . x = (1 / ((cos . (cot . x)) ^2)) * (- (1 / ((sin . 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 tan by A1, FUNCT_1:11; hence cos . (cot . x) <> 0 by FDIFF_8:1; ::_thesis: verum end; A3: for x being Real st x in Z holds sin . x <> 0 proof let x be Real; ::_thesis: ( x in Z implies sin . x <> 0 ) assume x in Z ; ::_thesis: sin . x <> 0 then x in dom (cos / sin) by A1, FUNCT_1:11; hence sin . x <> 0 by FDIFF_8:2; ::_thesis: verum end; A4: for x being Real st x in Z holds tan * cot is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies tan * cot is_differentiable_in x ) assume A5: x in Z ; ::_thesis: tan * cot is_differentiable_in x then cos . (cot . x) <> 0 by A2; then A6: tan is_differentiable_in cot . x by FDIFF_7:46; sin . x <> 0 by A3, A5; then cot is_differentiable_in x by FDIFF_7:47; hence tan * cot is_differentiable_in x by A6, FDIFF_2:13; ::_thesis: verum end; then A7: tan * cot is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((tan * cot) `| Z) . x = (1 / ((cos . (cot . x)) ^2)) * (- (1 / ((sin . x) ^2))) proof let x be Real; ::_thesis: ( x in Z implies ((tan * cot) `| Z) . x = (1 / ((cos . (cot . x)) ^2)) * (- (1 / ((sin . x) ^2))) ) assume A8: x in Z ; ::_thesis: ((tan * cot) `| Z) . x = (1 / ((cos . (cot . x)) ^2)) * (- (1 / ((sin . x) ^2))) then A9: cos . (cot . x) <> 0 by A2; then A10: tan is_differentiable_in cot . x by FDIFF_7:46; A11: sin . x <> 0 by A3, A8; then cot is_differentiable_in x by FDIFF_7:47; then diff ((tan * cot),x) = (diff (tan,(cot . x))) * (diff (cot,x)) by A10, FDIFF_2:13 .= (1 / ((cos . (cot . x)) ^2)) * (diff (cot,x)) by A9, FDIFF_7:46 .= (1 / ((cos . (cot . x)) ^2)) * (- (1 / ((sin . x) ^2))) by A11, FDIFF_7:47 ; hence ((tan * cot) `| Z) . x = (1 / ((cos . (cot . x)) ^2)) * (- (1 / ((sin . x) ^2))) by A7, A8, FDIFF_1:def_7; ::_thesis: verum end; hence ( tan * cot is_differentiable_on Z & ( for x being Real st x in Z holds ((tan * cot) `| Z) . x = (1 / ((cos . (cot . x)) ^2)) * (- (1 / ((sin . x) ^2))) ) ) by A1, A4, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_10:2 for Z being open Subset of REAL st Z c= dom (tan * tan) holds ( tan * tan is_differentiable_on Z & ( for x being Real st x in Z holds ((tan * tan) `| Z) . x = (1 / ((cos . (tan . x)) ^2)) * (1 / ((cos . x) ^2)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (tan * tan) implies ( tan * tan is_differentiable_on Z & ( for x being Real st x in Z holds ((tan * tan) `| Z) . x = (1 / ((cos . (tan . x)) ^2)) * (1 / ((cos . x) ^2)) ) ) ) assume A1: Z c= dom (tan * tan) ; ::_thesis: ( tan * tan is_differentiable_on Z & ( for x being Real st x in Z holds ((tan * tan) `| Z) . x = (1 / ((cos . (tan . x)) ^2)) * (1 / ((cos . 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 tan by A1, FUNCT_1:11; hence cos . (tan . x) <> 0 by FDIFF_8:1; ::_thesis: verum end; A3: for x being Real st x in Z holds cos . x <> 0 proof let x be Real; ::_thesis: ( x in Z implies cos . x <> 0 ) assume x in Z ; ::_thesis: cos . x <> 0 then x in dom (sin / cos) by A1, FUNCT_1:11; hence cos . x <> 0 by FDIFF_8:1; ::_thesis: verum end; A4: for x being Real st x in Z holds tan * tan is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies tan * tan is_differentiable_in x ) assume A5: x in Z ; ::_thesis: tan * tan is_differentiable_in x then cos . (tan . x) <> 0 by A2; then A6: tan is_differentiable_in tan . x by FDIFF_7:46; cos . x <> 0 by A3, A5; then tan is_differentiable_in x by FDIFF_7:46; hence tan * tan is_differentiable_in x by A6, FDIFF_2:13; ::_thesis: verum end; then A7: tan * tan is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((tan * tan) `| Z) . x = (1 / ((cos . (tan . x)) ^2)) * (1 / ((cos . x) ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((tan * tan) `| Z) . x = (1 / ((cos . (tan . x)) ^2)) * (1 / ((cos . x) ^2)) ) assume A8: x in Z ; ::_thesis: ((tan * tan) `| Z) . x = (1 / ((cos . (tan . x)) ^2)) * (1 / ((cos . x) ^2)) then A9: cos . (tan . x) <> 0 by A2; then A10: tan is_differentiable_in tan . x by FDIFF_7:46; A11: cos . x <> 0 by A3, A8; then tan is_differentiable_in x by FDIFF_7:46; then diff ((tan * tan),x) = (diff (tan,(tan . x))) * (diff (tan,x)) by A10, FDIFF_2:13 .= (1 / ((cos . (tan . x)) ^2)) * (diff (tan,x)) by A9, FDIFF_7:46 .= (1 / ((cos . (tan . x)) ^2)) * (1 / ((cos . x) ^2)) by A11, FDIFF_7:46 ; hence ((tan * tan) `| Z) . x = (1 / ((cos . (tan . x)) ^2)) * (1 / ((cos . x) ^2)) by A7, A8, FDIFF_1:def_7; ::_thesis: verum end; hence ( tan * tan is_differentiable_on Z & ( for x being Real st x in Z holds ((tan * tan) `| Z) . x = (1 / ((cos . (tan . x)) ^2)) * (1 / ((cos . x) ^2)) ) ) by A1, A4, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_10:3 for Z being open Subset of REAL st Z c= dom (cot * cot) holds ( cot * cot is_differentiable_on Z & ( for x being Real st x in Z holds ((cot * cot) `| Z) . x = (1 / ((sin . (cot . x)) ^2)) * (1 / ((sin . x) ^2)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cot * cot) implies ( cot * cot is_differentiable_on Z & ( for x being Real st x in Z holds ((cot * cot) `| Z) . x = (1 / ((sin . (cot . x)) ^2)) * (1 / ((sin . x) ^2)) ) ) ) assume A1: Z c= dom (cot * cot) ; ::_thesis: ( cot * cot is_differentiable_on Z & ( for x being Real st x in Z holds ((cot * cot) `| Z) . x = (1 / ((sin . (cot . x)) ^2)) * (1 / ((sin . 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 cot by A1, FUNCT_1:11; hence sin . (cot . x) <> 0 by FDIFF_8:2; ::_thesis: verum end; A3: for x being Real st x in Z holds sin . x <> 0 proof let x be Real; ::_thesis: ( x in Z implies sin . x <> 0 ) assume x in Z ; ::_thesis: sin . x <> 0 then x in dom (cos / sin) by A1, FUNCT_1:11; hence sin . x <> 0 by FDIFF_8:2; ::_thesis: verum end; A4: for x being Real st x in Z holds cot * cot is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies cot * cot is_differentiable_in x ) assume A5: x in Z ; ::_thesis: cot * cot is_differentiable_in x then sin . (cot . x) <> 0 by A2; then A6: cot is_differentiable_in cot . x by FDIFF_7:47; sin . x <> 0 by A3, A5; then cot is_differentiable_in x by FDIFF_7:47; hence cot * cot is_differentiable_in x by A6, FDIFF_2:13; ::_thesis: verum end; then A7: cot * cot is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((cot * cot) `| Z) . x = (1 / ((sin . (cot . x)) ^2)) * (1 / ((sin . x) ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((cot * cot) `| Z) . x = (1 / ((sin . (cot . x)) ^2)) * (1 / ((sin . x) ^2)) ) assume A8: x in Z ; ::_thesis: ((cot * cot) `| Z) . x = (1 / ((sin . (cot . x)) ^2)) * (1 / ((sin . x) ^2)) then A9: sin . (cot . x) <> 0 by A2; then A10: cot is_differentiable_in cot . x by FDIFF_7:47; A11: sin . x <> 0 by A3, A8; then cot is_differentiable_in x by FDIFF_7:47; then diff ((cot * cot),x) = (diff (cot,(cot . x))) * (diff (cot,x)) by A10, FDIFF_2:13 .= (- (1 / ((sin . (cot . x)) ^2))) * (diff (cot,x)) by A9, FDIFF_7:47 .= (- (1 / ((sin . (cot . x)) ^2))) * (- (1 / ((sin . x) ^2))) by A11, FDIFF_7:47 ; hence ((cot * cot) `| Z) . x = (1 / ((sin . (cot . x)) ^2)) * (1 / ((sin . x) ^2)) by A7, A8, FDIFF_1:def_7; ::_thesis: verum end; hence ( cot * cot is_differentiable_on Z & ( for x being Real st x in Z holds ((cot * cot) `| Z) . x = (1 / ((sin . (cot . x)) ^2)) * (1 / ((sin . x) ^2)) ) ) by A1, A4, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_10:4 for Z being open Subset of REAL st Z c= dom (cot * tan) holds ( cot * tan is_differentiable_on Z & ( for x being Real st x in Z holds ((cot * tan) `| Z) . x = (- (1 / ((sin . (tan . x)) ^2))) * (1 / ((cos . x) ^2)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cot * tan) implies ( cot * tan is_differentiable_on Z & ( for x being Real st x in Z holds ((cot * tan) `| Z) . x = (- (1 / ((sin . (tan . x)) ^2))) * (1 / ((cos . x) ^2)) ) ) ) assume A1: Z c= dom (cot * tan) ; ::_thesis: ( cot * tan is_differentiable_on Z & ( for x being Real st x in Z holds ((cot * tan) `| Z) . x = (- (1 / ((sin . (tan . x)) ^2))) * (1 / ((cos . 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 cot by A1, FUNCT_1:11; hence sin . (tan . x) <> 0 by FDIFF_8:2; ::_thesis: verum end; A3: for x being Real st x in Z holds cos . x <> 0 proof let x be Real; ::_thesis: ( x in Z implies cos . x <> 0 ) assume x in Z ; ::_thesis: cos . x <> 0 then x in dom (sin / cos) by A1, FUNCT_1:11; hence cos . x <> 0 by FDIFF_8:1; ::_thesis: verum end; A4: for x being Real st x in Z holds cot * tan is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies cot * tan is_differentiable_in x ) assume A5: x in Z ; ::_thesis: cot * tan is_differentiable_in x then sin . (tan . x) <> 0 by A2; then A6: cot is_differentiable_in tan . x by FDIFF_7:47; cos . x <> 0 by A3, A5; then tan is_differentiable_in x by FDIFF_7:46; hence cot * tan is_differentiable_in x by A6, FDIFF_2:13; ::_thesis: verum end; then A7: cot * tan is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((cot * tan) `| Z) . x = (- (1 / ((sin . (tan . x)) ^2))) * (1 / ((cos . x) ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((cot * tan) `| Z) . x = (- (1 / ((sin . (tan . x)) ^2))) * (1 / ((cos . x) ^2)) ) assume A8: x in Z ; ::_thesis: ((cot * tan) `| Z) . x = (- (1 / ((sin . (tan . x)) ^2))) * (1 / ((cos . x) ^2)) then A9: sin . (tan . x) <> 0 by A2; then A10: cot is_differentiable_in tan . x by FDIFF_7:47; A11: cos . x <> 0 by A3, A8; then tan is_differentiable_in x by FDIFF_7:46; then diff ((cot * tan),x) = (diff (cot,(tan . x))) * (diff (tan,x)) by A10, FDIFF_2:13 .= (- (1 / ((sin . (tan . x)) ^2))) * (diff (tan,x)) by A9, FDIFF_7:47 .= (- (1 / ((sin . (tan . x)) ^2))) * (1 / ((cos . x) ^2)) by A11, FDIFF_7:46 ; hence ((cot * tan) `| Z) . x = (- (1 / ((sin . (tan . x)) ^2))) * (1 / ((cos . x) ^2)) by A7, A8, FDIFF_1:def_7; ::_thesis: verum end; hence ( cot * tan is_differentiable_on Z & ( for x being Real st x in Z holds ((cot * tan) `| Z) . x = (- (1 / ((sin . (tan . x)) ^2))) * (1 / ((cos . x) ^2)) ) ) by A1, A4, FDIFF_1:9; ::_thesis: verum end; theorem Th5: :: FDIFF_10:5 for Z being open Subset of REAL st Z c= dom (tan - cot) holds ( tan - cot is_differentiable_on Z & ( for x being Real st x in Z holds ((tan - cot) `| Z) . x = (1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (tan - cot) implies ( tan - cot is_differentiable_on Z & ( for x being Real st x in Z holds ((tan - cot) `| Z) . x = (1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) ) ) ) assume A1: Z c= dom (tan - cot) ; ::_thesis: ( tan - cot is_differentiable_on Z & ( for x being Real st x in Z holds ((tan - cot) `| Z) . x = (1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) ) ) then A2: Z c= (dom tan) /\ (dom cot) by VALUED_1:12; 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 cot by A2, 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 A5, FDIFF_8:2; hence cot is_differentiable_in x by FDIFF_7:47; ::_thesis: verum end; then A6: cot is_differentiable_on Z by A5, FDIFF_1:9; for x being Real st x in Z holds ((tan - cot) `| Z) . x = (1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((tan - cot) `| Z) . x = (1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) ) assume A7: x in Z ; ::_thesis: ((tan - cot) `| Z) . x = (1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) then A8: sin . x <> 0 by A5, FDIFF_8:2; A9: cos . x <> 0 by A3, A7, FDIFF_8:1; ((tan - cot) `| Z) . x = (diff (tan,x)) - (diff (cot,x)) by A1, A6, A4, A7, FDIFF_1:19 .= (1 / ((cos . x) ^2)) - (diff (cot,x)) by A9, FDIFF_7:46 .= (1 / ((cos . x) ^2)) - (- (1 / ((sin . x) ^2))) by A8, FDIFF_7:47 .= (1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) ; hence ((tan - cot) `| Z) . x = (1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) ; ::_thesis: verum end; hence ( tan - cot is_differentiable_on Z & ( for x being Real st x in Z holds ((tan - cot) `| Z) . x = (1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) ) ) by A1, A6, A4, FDIFF_1:19; ::_thesis: verum end; theorem Th6: :: FDIFF_10:6 for Z being open Subset of REAL st Z c= dom (tan + cot) holds ( tan + cot is_differentiable_on Z & ( for x being Real st x in Z holds ((tan + cot) `| Z) . x = (1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (tan + cot) implies ( tan + cot is_differentiable_on Z & ( for x being Real st x in Z holds ((tan + cot) `| Z) . x = (1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) ) ) ) assume A1: Z c= dom (tan + cot) ; ::_thesis: ( tan + cot is_differentiable_on Z & ( for x being Real st x in Z holds ((tan + cot) `| Z) . x = (1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) ) ) then A2: Z c= (dom tan) /\ (dom cot) by VALUED_1:def_1; 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 cot by A2, 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 A5, FDIFF_8:2; hence cot is_differentiable_in x by FDIFF_7:47; ::_thesis: verum end; then A6: cot is_differentiable_on Z by A5, FDIFF_1:9; for x being Real st x in Z holds ((tan + cot) `| Z) . x = (1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((tan + cot) `| Z) . x = (1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) ) assume A7: x in Z ; ::_thesis: ((tan + cot) `| Z) . x = (1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) then A8: sin . x <> 0 by A5, FDIFF_8:2; A9: cos . x <> 0 by A3, A7, FDIFF_8:1; ((tan + cot) `| Z) . x = (diff (tan,x)) + (diff (cot,x)) by A1, A6, A4, A7, FDIFF_1:18 .= (1 / ((cos . x) ^2)) + (diff (cot,x)) by A9, FDIFF_7:46 .= (1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) by A8, FDIFF_7:47 ; hence ((tan + cot) `| Z) . x = (1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) ; ::_thesis: verum end; hence ( tan + cot is_differentiable_on Z & ( for x being Real st x in Z holds ((tan + cot) `| Z) . x = (1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) ) ) by A1, A6, A4, FDIFF_1:18; ::_thesis: verum end; theorem :: FDIFF_10:7 for Z being open Subset of REAL holds ( sin * sin is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * sin) `| Z) . x = (cos . (sin . x)) * (cos . x) ) ) proof let Z be open Subset of REAL; ::_thesis: ( sin * sin is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * sin) `| Z) . x = (cos . (sin . x)) * (cos . x) ) ) A1: for x being Real st x in Z holds sin * sin is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies sin * sin is_differentiable_in x ) assume x in Z ; ::_thesis: sin * sin is_differentiable_in x A2: sin is_differentiable_in sin . x by SIN_COS:64; sin is_differentiable_in x by SIN_COS:64; hence sin * sin is_differentiable_in x by A2, FDIFF_2:13; ::_thesis: verum end; rng sin c= REAL ; then A3: dom (sin * sin) = REAL by RELAT_1:27, SIN_COS:24; then A4: sin * sin is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((sin * sin) `| Z) . x = (cos . (sin . x)) * (cos . x) proof let x be Real; ::_thesis: ( x in Z implies ((sin * sin) `| Z) . x = (cos . (sin . x)) * (cos . x) ) assume A5: x in Z ; ::_thesis: ((sin * sin) `| Z) . x = (cos . (sin . x)) * (cos . x) A6: sin is_differentiable_in sin . x by SIN_COS:64; sin is_differentiable_in x by SIN_COS:64; then diff ((sin * sin),x) = (diff (sin,(sin . x))) * (diff (sin,x)) by A6, FDIFF_2:13 .= (cos . (sin . x)) * (diff (sin,x)) by SIN_COS:64 .= (cos . (sin . x)) * (cos . x) by SIN_COS:64 ; hence ((sin * sin) `| Z) . x = (cos . (sin . x)) * (cos . x) by A4, A5, FDIFF_1:def_7; ::_thesis: verum end; hence ( sin * sin is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * sin) `| Z) . x = (cos . (sin . x)) * (cos . x) ) ) by A3, A1, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_10:8 for Z being open Subset of REAL holds ( sin * cos is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * cos) `| Z) . x = - ((cos . (cos . x)) * (sin . x)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( sin * cos is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * cos) `| Z) . x = - ((cos . (cos . x)) * (sin . x)) ) ) A1: for x being Real st x in Z holds sin * cos is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies sin * cos is_differentiable_in x ) assume x in Z ; ::_thesis: sin * cos is_differentiable_in x A2: sin is_differentiable_in cos . x by SIN_COS:64; cos is_differentiable_in x by SIN_COS:63; hence sin * cos is_differentiable_in x by A2, FDIFF_2:13; ::_thesis: verum end; rng cos c= dom cos by SIN_COS:24; then A3: dom (sin * cos) = REAL by RELAT_1:27, SIN_COS:24; then A4: sin * cos is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((sin * cos) `| Z) . x = - ((cos . (cos . x)) * (sin . x)) proof let x be Real; ::_thesis: ( x in Z implies ((sin * cos) `| Z) . x = - ((cos . (cos . x)) * (sin . x)) ) assume A5: x in Z ; ::_thesis: ((sin * cos) `| Z) . x = - ((cos . (cos . x)) * (sin . x)) A6: sin is_differentiable_in cos . x by SIN_COS:64; cos is_differentiable_in x by SIN_COS:63; then diff ((sin * cos),x) = (diff (sin,(cos . x))) * (diff (cos,x)) by A6, FDIFF_2:13 .= (cos . (cos . x)) * (diff (cos,x)) by SIN_COS:64 .= (cos . (cos . x)) * (- (sin . x)) by SIN_COS:63 ; hence ((sin * cos) `| Z) . x = - ((cos . (cos . x)) * (sin . x)) by A4, A5, FDIFF_1:def_7; ::_thesis: verum end; hence ( sin * cos is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * cos) `| Z) . x = - ((cos . (cos . x)) * (sin . x)) ) ) by A3, A1, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_10:9 for Z being open Subset of REAL holds ( cos * sin is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * sin) `| Z) . x = - ((sin . (sin . x)) * (cos . x)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( cos * sin is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * sin) `| Z) . x = - ((sin . (sin . x)) * (cos . x)) ) ) A1: for x being Real st x in Z holds cos * sin is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies cos * sin is_differentiable_in x ) assume x in Z ; ::_thesis: cos * sin is_differentiable_in x A2: cos is_differentiable_in sin . x by SIN_COS:63; sin is_differentiable_in x by SIN_COS:64; hence cos * sin is_differentiable_in x by A2, FDIFF_2:13; ::_thesis: verum end; rng sin c= dom sin by SIN_COS:24; then A3: dom (cos * sin) = REAL by RELAT_1:27, SIN_COS:24; then A4: cos * sin is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((cos * sin) `| Z) . x = - ((sin . (sin . x)) * (cos . x)) proof let x be Real; ::_thesis: ( x in Z implies ((cos * sin) `| Z) . x = - ((sin . (sin . x)) * (cos . x)) ) assume A5: x in Z ; ::_thesis: ((cos * sin) `| Z) . x = - ((sin . (sin . x)) * (cos . x)) A6: cos is_differentiable_in sin . x by SIN_COS:63; sin is_differentiable_in x by SIN_COS:64; then diff ((cos * sin),x) = (diff (cos,(sin . x))) * (diff (sin,x)) by A6, FDIFF_2:13 .= (- (sin . (sin . x))) * (diff (sin,x)) by SIN_COS:63 .= (- (sin . (sin . x))) * (cos . x) by SIN_COS:64 ; hence ((cos * sin) `| Z) . x = - ((sin . (sin . x)) * (cos . x)) by A4, A5, FDIFF_1:def_7; ::_thesis: verum end; hence ( cos * sin is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * sin) `| Z) . x = - ((sin . (sin . x)) * (cos . x)) ) ) by A3, A1, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_10:10 for Z being open Subset of REAL holds ( cos * cos is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * cos) `| Z) . x = (sin . (cos . x)) * (sin . x) ) ) proof let Z be open Subset of REAL; ::_thesis: ( cos * cos is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * cos) `| Z) . x = (sin . (cos . x)) * (sin . x) ) ) A1: for x being Real st x in Z holds cos * cos is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies cos * cos is_differentiable_in x ) assume x in Z ; ::_thesis: cos * cos is_differentiable_in x A2: cos is_differentiable_in cos . x by SIN_COS:63; cos is_differentiable_in x by SIN_COS:63; hence cos * cos is_differentiable_in x by A2, FDIFF_2:13; ::_thesis: verum end; rng cos c= REAL ; then A3: dom (cos * cos) = REAL by RELAT_1:27, SIN_COS:24; then A4: cos * cos is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((cos * cos) `| Z) . x = (sin . (cos . x)) * (sin . x) proof let x be Real; ::_thesis: ( x in Z implies ((cos * cos) `| Z) . x = (sin . (cos . x)) * (sin . x) ) assume A5: x in Z ; ::_thesis: ((cos * cos) `| Z) . x = (sin . (cos . x)) * (sin . x) A6: cos is_differentiable_in cos . x by SIN_COS:63; cos is_differentiable_in x by SIN_COS:63; then diff ((cos * cos),x) = (diff (cos,(cos . x))) * (diff (cos,x)) by A6, FDIFF_2:13 .= (- (sin . (cos . x))) * (diff (cos,x)) by SIN_COS:63 .= (- (sin . (cos . x))) * (- (sin . x)) by SIN_COS:63 ; hence ((cos * cos) `| Z) . x = (sin . (cos . x)) * (sin . x) by A4, A5, FDIFF_1:def_7; ::_thesis: verum end; hence ( cos * cos is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * cos) `| Z) . x = (sin . (cos . x)) * (sin . x) ) ) by A3, A1, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_10:11 for Z being open Subset of REAL st Z c= dom (cos (#) cot) holds ( cos (#) cot is_differentiable_on Z & ( for x being Real st x in Z holds ((cos (#) cot) `| Z) . x = (- (cos . x)) - ((cos . x) / ((sin . x) ^2)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cos (#) cot) implies ( cos (#) cot is_differentiable_on Z & ( for x being Real st x in Z holds ((cos (#) cot) `| Z) . x = (- (cos . x)) - ((cos . x) / ((sin . x) ^2)) ) ) ) A1: for x being Real st x in Z holds cos is_differentiable_in x by SIN_COS:63; assume A2: Z c= dom (cos (#) cot) ; ::_thesis: ( cos (#) cot is_differentiable_on Z & ( for x being Real st x in Z holds ((cos (#) cot) `| Z) . x = (- (cos . x)) - ((cos . x) / ((sin . x) ^2)) ) ) then A3: Z c= (dom cos) /\ (dom cot) by VALUED_1:def_4; then A4: 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 A4, FDIFF_8:2; hence cot is_differentiable_in x by FDIFF_7:47; ::_thesis: verum end; then A5: cot is_differentiable_on Z by A4, FDIFF_1:9; Z c= dom cos by A3, XBOOLE_1:18; then A6: cos is_differentiable_on Z by A1, FDIFF_1:9; A7: for x being Real st x in Z holds diff (cot,x) = - (1 / ((sin . x) ^2)) proof let x be Real; ::_thesis: ( x in Z implies diff (cot,x) = - (1 / ((sin . x) ^2)) ) assume x in Z ; ::_thesis: diff (cot,x) = - (1 / ((sin . x) ^2)) then sin . x <> 0 by A4, FDIFF_8:2; hence diff (cot,x) = - (1 / ((sin . x) ^2)) by FDIFF_7:47; ::_thesis: verum end; for x being Real st x in Z holds ((cos (#) cot) `| Z) . x = (- (cos . x)) - ((cos . x) / ((sin . x) ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((cos (#) cot) `| Z) . x = (- (cos . x)) - ((cos . x) / ((sin . x) ^2)) ) assume A8: x in Z ; ::_thesis: ((cos (#) cot) `| Z) . x = (- (cos . x)) - ((cos . x) / ((sin . x) ^2)) then ((cos (#) cot) `| Z) . x = ((diff (cos,x)) * (cot . x)) + ((cos . x) * (diff (cot,x))) by A2, A5, A6, FDIFF_1:21 .= ((cot . x) * (- (sin . x))) + ((cos . x) * (diff (cot,x))) by SIN_COS:63 .= ((cot . x) * (- (sin . x))) + ((cos . x) * (- (1 / ((sin . x) ^2)))) by A7, A8 .= (((cos . x) / (sin . x)) * (- ((sin . x) / 1))) - ((cos . x) / ((sin . x) ^2)) by A4, A8, RFUNCT_1:def_1 .= (- ((cos . x) * ((sin . x) / (sin . x)))) - ((cos . x) / ((sin . x) ^2)) .= (- ((cos . x) * 1)) - ((cos . x) / ((sin . x) ^2)) by A4, A8, FDIFF_8:2, XCMPLX_1:60 .= (- (cos . x)) - ((cos . x) / ((sin . x) ^2)) ; hence ((cos (#) cot) `| Z) . x = (- (cos . x)) - ((cos . x) / ((sin . x) ^2)) ; ::_thesis: verum end; hence ( cos (#) cot is_differentiable_on Z & ( for x being Real st x in Z holds ((cos (#) cot) `| Z) . x = (- (cos . x)) - ((cos . x) / ((sin . x) ^2)) ) ) by A2, A5, A6, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_10:12 for Z being open Subset of REAL st Z c= dom (sin (#) tan) holds ( sin (#) tan is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) tan) `| Z) . x = (sin . x) + ((sin . x) / ((cos . x) ^2)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sin (#) tan) implies ( sin (#) tan is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) tan) `| Z) . x = (sin . x) + ((sin . x) / ((cos . x) ^2)) ) ) ) A1: for x being Real st x in Z holds sin is_differentiable_in x by SIN_COS:64; assume A2: Z c= dom (sin (#) tan) ; ::_thesis: ( sin (#) tan is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) tan) `| Z) . x = (sin . x) + ((sin . x) / ((cos . x) ^2)) ) ) then A3: Z c= (dom sin) /\ (dom tan) by VALUED_1:def_4; then A4: 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 A4, FDIFF_8:1; hence tan is_differentiable_in x by FDIFF_7:46; ::_thesis: verum end; then A5: tan is_differentiable_on Z by A4, FDIFF_1:9; Z c= dom sin by A3, XBOOLE_1:18; then A6: sin is_differentiable_on Z by A1, FDIFF_1:9; A7: for x being Real st x in Z holds diff (tan,x) = 1 / ((cos . x) ^2) proof let x be Real; ::_thesis: ( x in Z implies diff (tan,x) = 1 / ((cos . x) ^2) ) assume x in Z ; ::_thesis: diff (tan,x) = 1 / ((cos . x) ^2) then cos . x <> 0 by A4, FDIFF_8:1; hence diff (tan,x) = 1 / ((cos . x) ^2) by FDIFF_7:46; ::_thesis: verum end; for x being Real st x in Z holds ((sin (#) tan) `| Z) . x = (sin . x) + ((sin . x) / ((cos . x) ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((sin (#) tan) `| Z) . x = (sin . x) + ((sin . x) / ((cos . x) ^2)) ) assume A8: x in Z ; ::_thesis: ((sin (#) tan) `| Z) . x = (sin . x) + ((sin . x) / ((cos . x) ^2)) then ((sin (#) tan) `| Z) . x = ((diff (sin,x)) * (tan . x)) + ((sin . x) * (diff (tan,x))) by A2, A5, A6, FDIFF_1:21 .= ((cos . x) * (tan . x)) + ((sin . x) * (diff (tan,x))) by SIN_COS:64 .= ((cos . x) * (tan . x)) + ((sin . x) * (1 / ((cos . x) ^2))) by A7, A8 .= (((sin . x) / (cos . x)) * ((cos . x) / 1)) + ((sin . x) / ((cos . x) ^2)) by A4, A8, RFUNCT_1:def_1 .= ((sin . x) * ((cos . x) / (cos . x))) + ((sin . x) / ((cos . x) ^2)) .= ((sin . x) * 1) + ((sin . x) / ((cos . x) ^2)) by A4, A8, FDIFF_8:1, XCMPLX_1:60 .= (sin . x) + ((sin . x) / ((cos . x) ^2)) ; hence ((sin (#) tan) `| Z) . x = (sin . x) + ((sin . x) / ((cos . x) ^2)) ; ::_thesis: verum end; hence ( sin (#) tan is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) tan) `| Z) . x = (sin . x) + ((sin . x) / ((cos . x) ^2)) ) ) by A2, A5, A6, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_10:13 for Z being open Subset of REAL st Z c= dom (sin (#) cot) holds ( sin (#) cot is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) cot) `| Z) . x = ((cos . x) * (cot . x)) - (1 / (sin . x)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sin (#) cot) implies ( sin (#) cot is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) cot) `| Z) . x = ((cos . x) * (cot . x)) - (1 / (sin . x)) ) ) ) A1: for x being Real st x in Z holds sin is_differentiable_in x by SIN_COS:64; assume A2: Z c= dom (sin (#) cot) ; ::_thesis: ( sin (#) cot is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) cot) `| Z) . x = ((cos . x) * (cot . x)) - (1 / (sin . x)) ) ) then A3: Z c= (dom sin) /\ (dom cot) by VALUED_1:def_4; then A4: 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 A4, FDIFF_8:2; hence cot is_differentiable_in x by FDIFF_7:47; ::_thesis: verum end; then A5: cot is_differentiable_on Z by A4, FDIFF_1:9; Z c= dom sin by A3, XBOOLE_1:18; then A6: sin is_differentiable_on Z by A1, FDIFF_1:9; A7: for x being Real st x in Z holds diff (cot,x) = - (1 / ((sin . x) ^2)) proof let x be Real; ::_thesis: ( x in Z implies diff (cot,x) = - (1 / ((sin . x) ^2)) ) assume x in Z ; ::_thesis: diff (cot,x) = - (1 / ((sin . x) ^2)) then sin . x <> 0 by A4, FDIFF_8:2; hence diff (cot,x) = - (1 / ((sin . x) ^2)) by FDIFF_7:47; ::_thesis: verum end; for x being Real st x in Z holds ((sin (#) cot) `| Z) . x = ((cos . x) * (cot . x)) - (1 / (sin . x)) proof let x be Real; ::_thesis: ( x in Z implies ((sin (#) cot) `| Z) . x = ((cos . x) * (cot . x)) - (1 / (sin . x)) ) assume A8: x in Z ; ::_thesis: ((sin (#) cot) `| Z) . x = ((cos . x) * (cot . x)) - (1 / (sin . x)) then ((sin (#) cot) `| Z) . x = ((diff (sin,x)) * (cot . x)) + ((sin . x) * (diff (cot,x))) by A2, A5, A6, FDIFF_1:21 .= ((cos . x) * (cot . x)) + ((sin . x) * (diff (cot,x))) by SIN_COS:64 .= ((cos . x) * (cot . x)) + ((sin . x) * (- (1 / ((sin . x) ^2)))) by A7, A8 .= ((cos . x) * (cot . x)) - ((sin . x) / ((sin . x) ^2)) .= ((cos . x) * (cot . x)) - (((sin . x) / (sin . x)) / (sin . x)) by XCMPLX_1:78 .= ((cos . x) * (cot . x)) - (1 / (sin . x)) by A4, A8, FDIFF_8:2, XCMPLX_1:60 ; hence ((sin (#) cot) `| Z) . x = ((cos . x) * (cot . x)) - (1 / (sin . x)) ; ::_thesis: verum end; hence ( sin (#) cot is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) cot) `| Z) . x = ((cos . x) * (cot . x)) - (1 / (sin . x)) ) ) by A2, A5, A6, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_10:14 for Z being open Subset of REAL st Z c= dom (cos (#) tan) holds ( cos (#) tan is_differentiable_on Z & ( for x being Real st x in Z holds ((cos (#) tan) `| Z) . x = (- (((sin . x) ^2) / (cos . x))) + (1 / (cos . x)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cos (#) tan) implies ( cos (#) tan is_differentiable_on Z & ( for x being Real st x in Z holds ((cos (#) tan) `| Z) . x = (- (((sin . x) ^2) / (cos . x))) + (1 / (cos . x)) ) ) ) A1: for x being Real st x in Z holds cos is_differentiable_in x by SIN_COS:63; assume A2: Z c= dom (cos (#) tan) ; ::_thesis: ( cos (#) tan is_differentiable_on Z & ( for x being Real st x in Z holds ((cos (#) tan) `| Z) . x = (- (((sin . x) ^2) / (cos . x))) + (1 / (cos . x)) ) ) then A3: Z c= (dom cos) /\ (dom tan) by VALUED_1:def_4; then A4: 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 A4, FDIFF_8:1; hence tan is_differentiable_in x by FDIFF_7:46; ::_thesis: verum end; then A5: tan is_differentiable_on Z by A4, FDIFF_1:9; Z c= dom cos by A3, XBOOLE_1:18; then A6: cos is_differentiable_on Z by A1, FDIFF_1:9; A7: for x being Real st x in Z holds diff (tan,x) = 1 / ((cos . x) ^2) proof let x be Real; ::_thesis: ( x in Z implies diff (tan,x) = 1 / ((cos . x) ^2) ) assume x in Z ; ::_thesis: diff (tan,x) = 1 / ((cos . x) ^2) then cos . x <> 0 by A4, FDIFF_8:1; hence diff (tan,x) = 1 / ((cos . x) ^2) by FDIFF_7:46; ::_thesis: verum end; for x being Real st x in Z holds ((cos (#) tan) `| Z) . x = (- (((sin . x) ^2) / (cos . x))) + (1 / (cos . x)) proof let x be Real; ::_thesis: ( x in Z implies ((cos (#) tan) `| Z) . x = (- (((sin . x) ^2) / (cos . x))) + (1 / (cos . x)) ) assume A8: x in Z ; ::_thesis: ((cos (#) tan) `| Z) . x = (- (((sin . x) ^2) / (cos . x))) + (1 / (cos . x)) then ((cos (#) tan) `| Z) . x = ((diff (cos,x)) * (tan . x)) + ((cos . x) * (diff (tan,x))) by A2, A5, A6, FDIFF_1:21 .= ((tan . x) * (- (sin . x))) + ((cos . x) * (diff (tan,x))) by SIN_COS:63 .= ((tan . x) * (- (sin . x))) + ((cos . x) * (1 / ((cos . x) ^2))) by A7, A8 .= (((sin . x) / (cos . x)) * (- ((sin . x) / 1))) + ((cos . x) / ((cos . x) ^2)) by A4, A8, RFUNCT_1:def_1 .= (- (((sin . x) ^2) / (cos . x))) + (((cos . x) / (cos . x)) / (cos . x)) by XCMPLX_1:78 .= (- (((sin . x) ^2) / (cos . x))) + (1 / (cos . x)) by A4, A8, FDIFF_8:1, XCMPLX_1:60 ; hence ((cos (#) tan) `| Z) . x = (- (((sin . x) ^2) / (cos . x))) + (1 / (cos . x)) ; ::_thesis: verum end; hence ( cos (#) tan is_differentiable_on Z & ( for x being Real st x in Z holds ((cos (#) tan) `| Z) . x = (- (((sin . x) ^2) / (cos . x))) + (1 / (cos . x)) ) ) by A2, A5, A6, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_10:15 for Z being open Subset of REAL st Z c= dom (sin (#) cos) holds ( sin (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) cos) `| Z) . x = ((cos . x) ^2) - ((sin . x) ^2) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sin (#) cos) implies ( sin (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) cos) `| Z) . x = ((cos . x) ^2) - ((sin . x) ^2) ) ) ) A1: for x being Real st x in Z holds sin is_differentiable_in x by SIN_COS:64; A2: for x being Real st x in Z holds cos is_differentiable_in x by SIN_COS:63; assume A3: Z c= dom (sin (#) cos) ; ::_thesis: ( sin (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) cos) `| Z) . x = ((cos . x) ^2) - ((sin . x) ^2) ) ) then A4: Z c= (dom sin) /\ (dom cos) by VALUED_1:def_4; then Z c= dom cos by XBOOLE_1:18; then A5: cos is_differentiable_on Z by A2, FDIFF_1:9; Z c= dom sin by A4, XBOOLE_1:18; then A6: sin is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((sin (#) cos) `| Z) . x = ((cos . x) ^2) - ((sin . x) ^2) proof let x be Real; ::_thesis: ( x in Z implies ((sin (#) cos) `| Z) . x = ((cos . x) ^2) - ((sin . x) ^2) ) assume x in Z ; ::_thesis: ((sin (#) cos) `| Z) . x = ((cos . x) ^2) - ((sin . x) ^2) then ((sin (#) cos) `| Z) . x = ((diff (sin,x)) * (cos . x)) + ((sin . x) * (diff (cos,x))) by A3, A6, A5, FDIFF_1:21 .= ((cos . x) * (cos . x)) + ((sin . x) * (diff (cos,x))) by SIN_COS:64 .= ((cos . x) * (cos . x)) + ((sin . x) * (- (sin . x))) by SIN_COS:63 .= ((cos . x) ^2) - ((sin . x) ^2) ; hence ((sin (#) cos) `| Z) . x = ((cos . x) ^2) - ((sin . x) ^2) ; ::_thesis: verum end; hence ( sin (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) cos) `| Z) . x = ((cos . x) ^2) - ((sin . x) ^2) ) ) by A3, A6, A5, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_10:16 for Z being open Subset of REAL st Z c= dom (ln (#) sin) holds ( ln (#) sin is_differentiable_on Z & ( for x being Real st x in Z holds ((ln (#) sin) `| Z) . x = ((sin . x) / x) + ((ln . x) * (cos . x)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (ln (#) sin) implies ( ln (#) sin is_differentiable_on Z & ( for x being Real st x in Z holds ((ln (#) sin) `| Z) . x = ((sin . x) / x) + ((ln . x) * (cos . x)) ) ) ) A1: for x being Real st x in Z holds sin is_differentiable_in x by SIN_COS:64; assume A2: Z c= dom (ln (#) sin) ; ::_thesis: ( ln (#) sin is_differentiable_on Z & ( for x being Real st x in Z holds ((ln (#) sin) `| Z) . x = ((sin . x) / x) + ((ln . x) * (cos . x)) ) ) then A3: Z c= (dom ln) /\ (dom sin) by VALUED_1:def_4; then Z c= dom sin by XBOOLE_1:18; then A4: sin is_differentiable_on Z by A1, FDIFF_1:9; A5: Z c= dom ln by A3, XBOOLE_1:18; A6: 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 A5, TAYLOR_1:18; then x in { g where g is Real : 0 < g } by XXREAL_1:230; then ex g being Real st ( x = g & 0 < g ) ; 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 A7: ln is_differentiable_on Z by A5, FDIFF_1:9; A8: 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 A6; then x in { g where g is Real : 0 < g } ; then x in right_open_halfline 0 by XXREAL_1:230; hence diff (ln,x) = 1 / x by TAYLOR_1:18; ::_thesis: verum end; for x being Real st x in Z holds ((ln (#) sin) `| Z) . x = ((sin . x) / x) + ((ln . x) * (cos . x)) proof let x be Real; ::_thesis: ( x in Z implies ((ln (#) sin) `| Z) . x = ((sin . x) / x) + ((ln . x) * (cos . x)) ) assume A9: x in Z ; ::_thesis: ((ln (#) sin) `| Z) . x = ((sin . x) / x) + ((ln . x) * (cos . x)) then ((ln (#) sin) `| Z) . x = ((sin . x) * (diff (ln,x))) + ((ln . x) * (diff (sin,x))) by A2, A7, A4, FDIFF_1:21 .= ((sin . x) * (1 / x)) + ((ln . x) * (diff (sin,x))) by A8, A9 .= ((sin . x) / x) + ((ln . x) * (cos . x)) by SIN_COS:64 ; hence ((ln (#) sin) `| Z) . x = ((sin . x) / x) + ((ln . x) * (cos . x)) ; ::_thesis: verum end; hence ( ln (#) sin is_differentiable_on Z & ( for x being Real st x in Z holds ((ln (#) sin) `| Z) . x = ((sin . x) / x) + ((ln . x) * (cos . x)) ) ) by A2, A7, A4, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_10:17 for Z being open Subset of REAL st Z c= dom (ln (#) cos) holds ( ln (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds ((ln (#) cos) `| Z) . x = ((cos . x) / x) - ((ln . x) * (sin . x)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (ln (#) cos) implies ( ln (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds ((ln (#) cos) `| Z) . x = ((cos . x) / x) - ((ln . x) * (sin . x)) ) ) ) A1: for x being Real st x in Z holds cos is_differentiable_in x by SIN_COS:63; assume A2: Z c= dom (ln (#) cos) ; ::_thesis: ( ln (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds ((ln (#) cos) `| Z) . x = ((cos . x) / x) - ((ln . x) * (sin . x)) ) ) then A3: Z c= (dom ln) /\ (dom cos) by VALUED_1:def_4; then Z c= dom cos by XBOOLE_1:18; then A4: cos is_differentiable_on Z by A1, FDIFF_1:9; A5: Z c= dom ln by A3, XBOOLE_1:18; A6: 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 A5, TAYLOR_1:18; then x in { g where g is Real : 0 < g } by XXREAL_1:230; then ex g being Real st ( x = g & 0 < g ) ; 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 A7: ln is_differentiable_on Z by A5, FDIFF_1:9; A8: 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 A6; then x in { g where g is Real : 0 < g } ; then x in right_open_halfline 0 by XXREAL_1:230; hence diff (ln,x) = 1 / x by TAYLOR_1:18; ::_thesis: verum end; for x being Real st x in Z holds ((ln (#) cos) `| Z) . x = ((cos . x) / x) - ((ln . x) * (sin . x)) proof let x be Real; ::_thesis: ( x in Z implies ((ln (#) cos) `| Z) . x = ((cos . x) / x) - ((ln . x) * (sin . x)) ) assume A9: x in Z ; ::_thesis: ((ln (#) cos) `| Z) . x = ((cos . x) / x) - ((ln . x) * (sin . x)) then ((ln (#) cos) `| Z) . x = ((cos . x) * (diff (ln,x))) + ((ln . x) * (diff (cos,x))) by A2, A7, A4, FDIFF_1:21 .= ((cos . x) * (1 / x)) + ((ln . x) * (diff (cos,x))) by A8, A9 .= ((cos . x) / x) + ((ln . x) * (- (sin . x))) by SIN_COS:63 ; hence ((ln (#) cos) `| Z) . x = ((cos . x) / x) - ((ln . x) * (sin . x)) ; ::_thesis: verum end; hence ( ln (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds ((ln (#) cos) `| Z) . x = ((cos . x) / x) - ((ln . x) * (sin . x)) ) ) by A2, A7, A4, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_10:18 for Z being open Subset of REAL st Z c= dom (ln (#) exp_R) holds ( ln (#) exp_R is_differentiable_on Z & ( for x being Real st x in Z holds ((ln (#) exp_R) `| Z) . x = ((exp_R . x) / x) + ((ln . x) * (exp_R . x)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (ln (#) exp_R) implies ( ln (#) exp_R is_differentiable_on Z & ( for x being Real st x in Z holds ((ln (#) exp_R) `| Z) . x = ((exp_R . x) / x) + ((ln . x) * (exp_R . x)) ) ) ) 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 (ln (#) exp_R) ; ::_thesis: ( ln (#) exp_R is_differentiable_on Z & ( for x being Real st x in Z holds ((ln (#) exp_R) `| Z) . x = ((exp_R . x) / x) + ((ln . x) * (exp_R . x)) ) ) then A3: Z c= (dom ln) /\ (dom exp_R) by VALUED_1:def_4; then Z c= dom exp_R by XBOOLE_1:18; then A4: exp_R is_differentiable_on Z by A1, FDIFF_1:9; A5: Z c= dom ln by A3, XBOOLE_1:18; A6: 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 A5, TAYLOR_1:18; then x in { g where g is Real : 0 < g } by XXREAL_1:230; then ex g being Real st ( x = g & 0 < g ) ; 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 A7: ln is_differentiable_on Z by A5, FDIFF_1:9; A8: 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 A6; then x in { g where g is Real : 0 < g } ; then x in right_open_halfline 0 by XXREAL_1:230; hence diff (ln,x) = 1 / x by TAYLOR_1:18; ::_thesis: verum end; for x being Real st x in Z holds ((ln (#) exp_R) `| Z) . x = ((exp_R . x) / x) + ((ln . x) * (exp_R . x)) proof let x be Real; ::_thesis: ( x in Z implies ((ln (#) exp_R) `| Z) . x = ((exp_R . x) / x) + ((ln . x) * (exp_R . x)) ) assume A9: x in Z ; ::_thesis: ((ln (#) exp_R) `| Z) . x = ((exp_R . x) / x) + ((ln . x) * (exp_R . x)) then ((ln (#) exp_R) `| Z) . x = ((exp_R . x) * (diff (ln,x))) + ((ln . x) * (diff (exp_R,x))) by A2, A7, A4, FDIFF_1:21 .= ((exp_R . x) * (1 / x)) + ((ln . x) * (diff (exp_R,x))) by A8, A9 .= ((exp_R . x) * (1 / x)) + ((ln . x) * (exp_R . x)) by SIN_COS:65 ; hence ((ln (#) exp_R) `| Z) . x = ((exp_R . x) / x) + ((ln . x) * (exp_R . x)) ; ::_thesis: verum end; hence ( ln (#) exp_R is_differentiable_on Z & ( for x being Real st x in Z holds ((ln (#) exp_R) `| Z) . x = ((exp_R . x) / x) + ((ln . x) * (exp_R . x)) ) ) by A2, A7, A4, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_10:19 for Z being open Subset of REAL st Z c= dom (ln * ln) & ( for x being Real st x in Z holds x > 0 ) holds ( ln * ln is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * ln) `| Z) . x = 1 / ((ln . x) * x) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (ln * ln) & ( for x being Real st x in Z holds x > 0 ) implies ( ln * ln is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * ln) `| Z) . x = 1 / ((ln . x) * x) ) ) ) assume that A1: Z c= dom (ln * ln) and A2: for x being Real st x in Z holds x > 0 ; ::_thesis: ( ln * ln is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * ln) `| Z) . x = 1 / ((ln . x) * x) ) ) A3: for x being Real st x in Z holds ln . x > 0 proof let x be Real; ::_thesis: ( x in Z implies ln . x > 0 ) assume x in Z ; ::_thesis: ln . x > 0 then A4: ln . x in right_open_halfline 0 by A1, FUNCT_1:11, TAYLOR_1:18; ].0,+infty.[ = { g where g is Real : 0 < g } by XXREAL_1:230; then ex g being Real st ( ln . x = g & 0 < g ) by A4; hence ln . x > 0 ; ::_thesis: verum end; A5: for x being Real st x in Z holds ln * ln is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies ln * ln is_differentiable_in x ) assume A6: x in Z ; ::_thesis: ln * ln is_differentiable_in x then A7: ln . x > 0 by A3; ln is_differentiable_in x by A2, A6, TAYLOR_1:18; hence ln * ln is_differentiable_in x by A7, TAYLOR_1:20; ::_thesis: verum end; then A8: ln * ln is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((ln * ln) `| Z) . x = 1 / ((ln . x) * x) proof let x be Real; ::_thesis: ( x in Z implies ((ln * ln) `| Z) . x = 1 / ((ln . x) * x) ) A9: ].0,+infty.[ = { g where g is Real : 0 < g } by XXREAL_1:230; assume A10: x in Z ; ::_thesis: ((ln * ln) `| Z) . x = 1 / ((ln . x) * x) then A11: ln . x > 0 by A3; x > 0 by A2, A10; then A12: x in right_open_halfline 0 by A9; ln is_differentiable_in x by A2, A10, TAYLOR_1:18; then diff ((ln * ln),x) = (diff (ln,x)) / (ln . x) by A11, TAYLOR_1:20 .= (1 / (ln . x)) * (1 / x) by A12, TAYLOR_1:18 .= 1 / ((ln . x) * x) by XCMPLX_1:102 ; hence ((ln * ln) `| Z) . x = 1 / ((ln . x) * x) by A8, A10, FDIFF_1:def_7; ::_thesis: verum end; hence ( ln * ln is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * ln) `| Z) . x = 1 / ((ln . x) * x) ) ) by A1, A5, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_10:20 for Z being open Subset of REAL st Z c= dom (exp_R * exp_R) holds ( exp_R * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R * exp_R) `| Z) . x = (exp_R . (exp_R . x)) * (exp_R . x) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (exp_R * exp_R) implies ( exp_R * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R * exp_R) `| Z) . x = (exp_R . (exp_R . x)) * (exp_R . x) ) ) ) A1: for x being Real st x in Z holds exp_R * exp_R is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies exp_R * exp_R is_differentiable_in x ) assume x in Z ; ::_thesis: exp_R * exp_R is_differentiable_in x A2: exp_R is_differentiable_in exp_R . x by SIN_COS:65; exp_R is_differentiable_in x by SIN_COS:65; hence exp_R * exp_R is_differentiable_in x by A2, FDIFF_2:13; ::_thesis: verum end; assume A3: Z c= dom (exp_R * exp_R) ; ::_thesis: ( exp_R * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R * exp_R) `| Z) . x = (exp_R . (exp_R . x)) * (exp_R . x) ) ) then A4: exp_R * exp_R is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((exp_R * exp_R) `| Z) . x = (exp_R . (exp_R . x)) * (exp_R . x) proof let x be Real; ::_thesis: ( x in Z implies ((exp_R * exp_R) `| Z) . x = (exp_R . (exp_R . x)) * (exp_R . x) ) assume A5: x in Z ; ::_thesis: ((exp_R * exp_R) `| Z) . x = (exp_R . (exp_R . x)) * (exp_R . x) A6: exp_R is_differentiable_in exp_R . x by SIN_COS:65; exp_R is_differentiable_in x by SIN_COS:65; then diff ((exp_R * exp_R),x) = (diff (exp_R,(exp_R . x))) * (diff (exp_R,x)) by A6, FDIFF_2:13 .= (exp_R . (exp_R . x)) * (diff (exp_R,x)) by SIN_COS:65 .= (exp_R . (exp_R . x)) * (exp_R . x) by SIN_COS:65 ; hence ((exp_R * exp_R) `| Z) . x = (exp_R . (exp_R . x)) * (exp_R . x) by A4, A5, FDIFF_1:def_7; ::_thesis: verum end; hence ( exp_R * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R * exp_R) `| Z) . x = (exp_R . (exp_R . x)) * (exp_R . x) ) ) by A3, A1, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_10:21 for Z being open Subset of REAL st Z c= dom (sin * tan) holds ( sin * tan is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * tan) `| Z) . x = (cos (tan . x)) / ((cos . x) ^2) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sin * tan) implies ( sin * tan is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * tan) `| Z) . x = (cos (tan . x)) / ((cos . x) ^2) ) ) ) assume A1: Z c= dom (sin * tan) ; ::_thesis: ( sin * tan is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * tan) `| Z) . x = (cos (tan . x)) / ((cos . x) ^2) ) ) A2: for x being Real st x in Z holds cos . x <> 0 proof let x be Real; ::_thesis: ( x in Z implies cos . x <> 0 ) assume x in Z ; ::_thesis: cos . x <> 0 then x in dom (sin / cos) by A1, FUNCT_1:11; hence cos . x <> 0 by FDIFF_8:1; ::_thesis: verum end; A3: for x being Real st x in Z holds sin * tan is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies sin * tan is_differentiable_in x ) assume x in Z ; ::_thesis: sin * tan is_differentiable_in x then cos . x <> 0 by A2; then A4: tan is_differentiable_in x by FDIFF_7:46; sin is_differentiable_in tan . x by SIN_COS:64; hence sin * tan is_differentiable_in x by A4, FDIFF_2:13; ::_thesis: verum end; then A5: sin * tan is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((sin * tan) `| Z) . x = (cos (tan . x)) / ((cos . x) ^2) proof let x be Real; ::_thesis: ( x in Z implies ((sin * tan) `| Z) . x = (cos (tan . x)) / ((cos . x) ^2) ) A6: sin is_differentiable_in tan . x by SIN_COS:64; assume A7: x in Z ; ::_thesis: ((sin * tan) `| Z) . x = (cos (tan . x)) / ((cos . x) ^2) then A8: cos . x <> 0 by A2; then tan is_differentiable_in x by FDIFF_7:46; then diff ((sin * tan),x) = (diff (sin,(tan . x))) * (diff (tan,x)) by A6, FDIFF_2:13 .= (cos (tan . x)) * (diff (tan,x)) by SIN_COS:64 .= (cos (tan . x)) * (1 / ((cos . x) ^2)) by A8, FDIFF_7:46 .= (cos (tan . x)) / ((cos . x) ^2) ; hence ((sin * tan) `| Z) . x = (cos (tan . x)) / ((cos . x) ^2) by A5, A7, FDIFF_1:def_7; ::_thesis: verum end; hence ( sin * tan is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * tan) `| Z) . x = (cos (tan . x)) / ((cos . x) ^2) ) ) by A1, A3, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_10:22 for Z being open Subset of REAL st Z c= dom (sin * cot) holds ( sin * cot is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * cot) `| Z) . x = - ((cos (cot . x)) / ((sin . x) ^2)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sin * cot) implies ( sin * cot is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * cot) `| Z) . x = - ((cos (cot . x)) / ((sin . x) ^2)) ) ) ) assume A1: Z c= dom (sin * cot) ; ::_thesis: ( sin * cot is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * cot) `| Z) . x = - ((cos (cot . x)) / ((sin . x) ^2)) ) ) A2: for x being Real st x in Z holds sin . x <> 0 proof let x be Real; ::_thesis: ( x in Z implies sin . x <> 0 ) assume x in Z ; ::_thesis: sin . x <> 0 then x in dom (cos / sin) by A1, FUNCT_1:11; hence sin . x <> 0 by FDIFF_8:2; ::_thesis: verum end; A3: for x being Real st x in Z holds sin * cot is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies sin * cot is_differentiable_in x ) assume x in Z ; ::_thesis: sin * cot is_differentiable_in x then sin . x <> 0 by A2; then A4: cot is_differentiable_in x by FDIFF_7:47; sin is_differentiable_in cot . x by SIN_COS:64; hence sin * cot is_differentiable_in x by A4, FDIFF_2:13; ::_thesis: verum end; then A5: sin * cot is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((sin * cot) `| Z) . x = - ((cos (cot . x)) / ((sin . x) ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((sin * cot) `| Z) . x = - ((cos (cot . x)) / ((sin . x) ^2)) ) A6: sin is_differentiable_in cot . x by SIN_COS:64; assume A7: x in Z ; ::_thesis: ((sin * cot) `| Z) . x = - ((cos (cot . x)) / ((sin . x) ^2)) then A8: sin . x <> 0 by A2; then cot is_differentiable_in x by FDIFF_7:47; then diff ((sin * cot),x) = (diff (sin,(cot . x))) * (diff (cot,x)) by A6, FDIFF_2:13 .= (cos (cot . x)) * (diff (cot,x)) by SIN_COS:64 .= (cos (cot . x)) * (- (1 / ((sin . x) ^2))) by A8, FDIFF_7:47 .= - ((cos (cot . x)) / ((sin . x) ^2)) ; hence ((sin * cot) `| Z) . x = - ((cos (cot . x)) / ((sin . x) ^2)) by A5, A7, FDIFF_1:def_7; ::_thesis: verum end; hence ( sin * cot is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * cot) `| Z) . x = - ((cos (cot . x)) / ((sin . x) ^2)) ) ) by A1, A3, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_10:23 for Z being open Subset of REAL st Z c= dom (cos * tan) holds ( cos * tan is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * tan) `| Z) . x = - ((sin (tan . x)) / ((cos . x) ^2)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cos * tan) implies ( cos * tan is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * tan) `| Z) . x = - ((sin (tan . x)) / ((cos . x) ^2)) ) ) ) assume A1: Z c= dom (cos * tan) ; ::_thesis: ( cos * tan is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * tan) `| Z) . x = - ((sin (tan . x)) / ((cos . x) ^2)) ) ) A2: for x being Real st x in Z holds cos . x <> 0 proof let x be Real; ::_thesis: ( x in Z implies cos . x <> 0 ) assume x in Z ; ::_thesis: cos . x <> 0 then x in dom (sin / cos) by A1, FUNCT_1:11; hence cos . x <> 0 by FDIFF_8:1; ::_thesis: verum end; A3: for x being Real st x in Z holds cos * tan is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies cos * tan is_differentiable_in x ) assume x in Z ; ::_thesis: cos * tan is_differentiable_in x then cos . x <> 0 by A2; then A4: tan is_differentiable_in x by FDIFF_7:46; cos is_differentiable_in tan . x by SIN_COS:63; hence cos * tan is_differentiable_in x by A4, FDIFF_2:13; ::_thesis: verum end; then A5: cos * tan is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((cos * tan) `| Z) . x = - ((sin (tan . x)) / ((cos . x) ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((cos * tan) `| Z) . x = - ((sin (tan . x)) / ((cos . x) ^2)) ) A6: cos is_differentiable_in tan . x by SIN_COS:63; assume A7: x in Z ; ::_thesis: ((cos * tan) `| Z) . x = - ((sin (tan . x)) / ((cos . x) ^2)) then A8: cos . x <> 0 by A2; then tan is_differentiable_in x by FDIFF_7:46; then diff ((cos * tan),x) = (diff (cos,(tan . x))) * (diff (tan,x)) by A6, FDIFF_2:13 .= (- (sin (tan . x))) * (diff (tan,x)) by SIN_COS:63 .= (- (sin (tan . x))) * (1 / ((cos . x) ^2)) by A8, FDIFF_7:46 .= - ((sin (tan . x)) / ((cos . x) ^2)) ; hence ((cos * tan) `| Z) . x = - ((sin (tan . x)) / ((cos . x) ^2)) by A5, A7, FDIFF_1:def_7; ::_thesis: verum end; hence ( cos * tan is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * tan) `| Z) . x = - ((sin (tan . x)) / ((cos . x) ^2)) ) ) by A1, A3, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_10:24 for Z being open Subset of REAL st Z c= dom (cos * cot) holds ( cos * cot is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * cot) `| Z) . x = (sin (cot . x)) / ((sin . x) ^2) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cos * cot) implies ( cos * cot is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * cot) `| Z) . x = (sin (cot . x)) / ((sin . x) ^2) ) ) ) assume A1: Z c= dom (cos * cot) ; ::_thesis: ( cos * cot is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * cot) `| Z) . x = (sin (cot . x)) / ((sin . x) ^2) ) ) A2: for x being Real st x in Z holds sin . x <> 0 proof let x be Real; ::_thesis: ( x in Z implies sin . x <> 0 ) assume x in Z ; ::_thesis: sin . x <> 0 then x in dom (cos / sin) by A1, FUNCT_1:11; hence sin . x <> 0 by FDIFF_8:2; ::_thesis: verum end; A3: for x being Real st x in Z holds cos * cot is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies cos * cot is_differentiable_in x ) assume x in Z ; ::_thesis: cos * cot is_differentiable_in x then sin . x <> 0 by A2; then A4: cot is_differentiable_in x by FDIFF_7:47; cos is_differentiable_in cot . x by SIN_COS:63; hence cos * cot is_differentiable_in x by A4, FDIFF_2:13; ::_thesis: verum end; then A5: cos * cot is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((cos * cot) `| Z) . x = (sin (cot . x)) / ((sin . x) ^2) proof let x be Real; ::_thesis: ( x in Z implies ((cos * cot) `| Z) . x = (sin (cot . x)) / ((sin . x) ^2) ) A6: cos is_differentiable_in cot . x by SIN_COS:63; assume A7: x in Z ; ::_thesis: ((cos * cot) `| Z) . x = (sin (cot . x)) / ((sin . x) ^2) then A8: sin . x <> 0 by A2; then cot is_differentiable_in x by FDIFF_7:47; then diff ((cos * cot),x) = (diff (cos,(cot . x))) * (diff (cot,x)) by A6, FDIFF_2:13 .= (- (sin (cot . x))) * (diff (cot,x)) by SIN_COS:63 .= (- (sin (cot . x))) * (- (1 / ((sin . x) ^2))) by A8, FDIFF_7:47 .= (sin (cot . x)) / ((sin . x) ^2) ; hence ((cos * cot) `| Z) . x = (sin (cot . x)) / ((sin . x) ^2) by A5, A7, FDIFF_1:def_7; ::_thesis: verum end; hence ( cos * cot is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * cot) `| Z) . x = (sin (cot . x)) / ((sin . x) ^2) ) ) by A1, A3, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_10:25 for Z being open Subset of REAL st Z c= dom (sin (#) (tan + cot)) holds ( sin (#) (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) (tan + cot)) `| Z) . x = ((cos . x) * ((tan . x) + (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sin (#) (tan + cot)) implies ( sin (#) (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) (tan + cot)) `| Z) . x = ((cos . x) * ((tan . x) + (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) ) ) A1: for x being Real st x in Z holds sin is_differentiable_in x by SIN_COS:64; assume A2: Z c= dom (sin (#) (tan + cot)) ; ::_thesis: ( sin (#) (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) (tan + cot)) `| Z) . x = ((cos . x) * ((tan . x) + (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) ) then A3: Z c= (dom (tan + cot)) /\ (dom sin) by VALUED_1:def_4; then A4: Z c= dom (tan + cot) by XBOOLE_1:18; then A5: tan + cot is_differentiable_on Z by Th6; Z c= dom sin by A3, XBOOLE_1:18; then A6: sin is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((sin (#) (tan + cot)) `| Z) . x = ((cos . x) * ((tan . x) + (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) proof let x be Real; ::_thesis: ( x in Z implies ((sin (#) (tan + cot)) `| Z) . x = ((cos . x) * ((tan . x) + (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) assume A7: x in Z ; ::_thesis: ((sin (#) (tan + cot)) `| Z) . x = ((cos . x) * ((tan . x) + (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) then ((sin (#) (tan + cot)) `| Z) . x = (((tan + cot) . x) * (diff (sin,x))) + ((sin . x) * (diff ((tan + cot),x))) by A2, A5, A6, FDIFF_1:21 .= (((tan . x) + (cot . x)) * (diff (sin,x))) + ((sin . x) * (diff ((tan + cot),x))) by A4, A7, VALUED_1:def_1 .= (((tan . x) + (cot . x)) * (cos . x)) + ((sin . x) * (diff ((tan + cot),x))) by SIN_COS:64 .= (((tan . x) + (cot . x)) * (cos . x)) + ((sin . x) * (((tan + cot) `| Z) . x)) by A5, A7, FDIFF_1:def_7 .= (((tan . x) + (cot . x)) * (cos . x)) + ((sin . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) by A4, A7, Th6 ; hence ((sin (#) (tan + cot)) `| Z) . x = ((cos . x) * ((tan . x) + (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ; ::_thesis: verum end; hence ( sin (#) (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) (tan + cot)) `| Z) . x = ((cos . x) * ((tan . x) + (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) ) by A2, A5, A6, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_10:26 for Z being open Subset of REAL st Z c= dom (cos (#) (tan + cot)) holds ( cos (#) (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((cos (#) (tan + cot)) `| Z) . x = (- ((sin . x) * ((tan . x) + (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cos (#) (tan + cot)) implies ( cos (#) (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((cos (#) (tan + cot)) `| Z) . x = (- ((sin . x) * ((tan . x) + (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) ) ) A1: for x being Real st x in Z holds cos is_differentiable_in x by SIN_COS:63; assume A2: Z c= dom (cos (#) (tan + cot)) ; ::_thesis: ( cos (#) (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((cos (#) (tan + cot)) `| Z) . x = (- ((sin . x) * ((tan . x) + (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) ) then A3: Z c= (dom (tan + cot)) /\ (dom cos) by VALUED_1:def_4; then A4: Z c= dom (tan + cot) by XBOOLE_1:18; then A5: tan + cot is_differentiable_on Z by Th6; Z c= dom cos by A3, XBOOLE_1:18; then A6: cos is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((cos (#) (tan + cot)) `| Z) . x = (- ((sin . x) * ((tan . x) + (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) proof let x be Real; ::_thesis: ( x in Z implies ((cos (#) (tan + cot)) `| Z) . x = (- ((sin . x) * ((tan . x) + (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) assume A7: x in Z ; ::_thesis: ((cos (#) (tan + cot)) `| Z) . x = (- ((sin . x) * ((tan . x) + (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) then ((cos (#) (tan + cot)) `| Z) . x = (((tan + cot) . x) * (diff (cos,x))) + ((cos . x) * (diff ((tan + cot),x))) by A2, A5, A6, FDIFF_1:21 .= (((tan . x) + (cot . x)) * (diff (cos,x))) + ((cos . x) * (diff ((tan + cot),x))) by A4, A7, VALUED_1:def_1 .= (((tan . x) + (cot . x)) * (- (sin . x))) + ((cos . x) * (diff ((tan + cot),x))) by SIN_COS:63 .= (((tan . x) + (cot . x)) * (- (sin . x))) + ((cos . x) * (((tan + cot) `| Z) . x)) by A5, A7, FDIFF_1:def_7 .= (((tan . x) + (cot . x)) * (- (sin . x))) + ((cos . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) by A4, A7, Th6 ; hence ((cos (#) (tan + cot)) `| Z) . x = (- ((sin . x) * ((tan . x) + (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ; ::_thesis: verum end; hence ( cos (#) (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((cos (#) (tan + cot)) `| Z) . x = (- ((sin . x) * ((tan . x) + (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) ) by A2, A5, A6, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_10:27 for Z being open Subset of REAL st Z c= dom (sin (#) (tan - cot)) holds ( sin (#) (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) (tan - cot)) `| Z) . x = ((cos . x) * ((tan . x) - (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sin (#) (tan - cot)) implies ( sin (#) (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) (tan - cot)) `| Z) . x = ((cos . x) * ((tan . x) - (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) ) ) A1: for x being Real st x in Z holds sin is_differentiable_in x by SIN_COS:64; assume A2: Z c= dom (sin (#) (tan - cot)) ; ::_thesis: ( sin (#) (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) (tan - cot)) `| Z) . x = ((cos . x) * ((tan . x) - (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) ) then A3: Z c= (dom (tan - cot)) /\ (dom sin) by VALUED_1:def_4; then A4: Z c= dom (tan - cot) by XBOOLE_1:18; then A5: tan - cot is_differentiable_on Z by Th5; Z c= dom sin by A3, XBOOLE_1:18; then A6: sin is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((sin (#) (tan - cot)) `| Z) . x = ((cos . x) * ((tan . x) - (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) proof let x be Real; ::_thesis: ( x in Z implies ((sin (#) (tan - cot)) `| Z) . x = ((cos . x) * ((tan . x) - (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) assume A7: x in Z ; ::_thesis: ((sin (#) (tan - cot)) `| Z) . x = ((cos . x) * ((tan . x) - (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) then ((sin (#) (tan - cot)) `| Z) . x = (((tan - cot) . x) * (diff (sin,x))) + ((sin . x) * (diff ((tan - cot),x))) by A2, A5, A6, FDIFF_1:21 .= (((tan . x) - (cot . x)) * (diff (sin,x))) + ((sin . x) * (diff ((tan - cot),x))) by A4, A7, VALUED_1:13 .= (((tan . x) - (cot . x)) * (cos . x)) + ((sin . x) * (diff ((tan - cot),x))) by SIN_COS:64 .= (((tan . x) - (cot . x)) * (cos . x)) + ((sin . x) * (((tan - cot) `| Z) . x)) by A5, A7, FDIFF_1:def_7 .= (((tan . x) - (cot . x)) * (cos . x)) + ((sin . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) by A4, A7, Th5 ; hence ((sin (#) (tan - cot)) `| Z) . x = ((cos . x) * ((tan . x) - (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ; ::_thesis: verum end; hence ( sin (#) (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) (tan - cot)) `| Z) . x = ((cos . x) * ((tan . x) - (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) ) by A2, A5, A6, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_10:28 for Z being open Subset of REAL st Z c= dom (cos (#) (tan - cot)) holds ( cos (#) (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((cos (#) (tan - cot)) `| Z) . x = (- ((sin . x) * ((tan . x) - (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cos (#) (tan - cot)) implies ( cos (#) (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((cos (#) (tan - cot)) `| Z) . x = (- ((sin . x) * ((tan . x) - (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) ) ) A1: for x being Real st x in Z holds cos is_differentiable_in x by SIN_COS:63; assume A2: Z c= dom (cos (#) (tan - cot)) ; ::_thesis: ( cos (#) (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((cos (#) (tan - cot)) `| Z) . x = (- ((sin . x) * ((tan . x) - (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) ) then A3: Z c= (dom (tan - cot)) /\ (dom cos) by VALUED_1:def_4; then A4: Z c= dom (tan - cot) by XBOOLE_1:18; then A5: tan - cot is_differentiable_on Z by Th5; Z c= dom cos by A3, XBOOLE_1:18; then A6: cos is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((cos (#) (tan - cot)) `| Z) . x = (- ((sin . x) * ((tan . x) - (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) proof let x be Real; ::_thesis: ( x in Z implies ((cos (#) (tan - cot)) `| Z) . x = (- ((sin . x) * ((tan . x) - (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) assume A7: x in Z ; ::_thesis: ((cos (#) (tan - cot)) `| Z) . x = (- ((sin . x) * ((tan . x) - (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) then ((cos (#) (tan - cot)) `| Z) . x = (((tan - cot) . x) * (diff (cos,x))) + ((cos . x) * (diff ((tan - cot),x))) by A2, A5, A6, FDIFF_1:21 .= (((tan . x) - (cot . x)) * (diff (cos,x))) + ((cos . x) * (diff ((tan - cot),x))) by A4, A7, VALUED_1:13 .= (((tan . x) - (cot . x)) * (- (sin . x))) + ((cos . x) * (diff ((tan - cot),x))) by SIN_COS:63 .= (((tan . x) - (cot . x)) * (- (sin . x))) + ((cos . x) * (((tan - cot) `| Z) . x)) by A5, A7, FDIFF_1:def_7 .= (((tan . x) - (cot . x)) * (- (sin . x))) + ((cos . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) by A4, A7, Th5 ; hence ((cos (#) (tan - cot)) `| Z) . x = (- ((sin . x) * ((tan . x) - (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ; ::_thesis: verum end; hence ( cos (#) (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((cos (#) (tan - cot)) `| Z) . x = (- ((sin . x) * ((tan . x) - (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) ) by A2, A5, A6, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_10:29 for Z being open Subset of REAL st Z c= dom (exp_R (#) (tan + cot)) holds ( exp_R (#) (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) (tan + cot)) `| Z) . x = ((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (exp_R (#) (tan + cot)) implies ( exp_R (#) (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) (tan + cot)) `| Z) . x = ((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) ) ) assume A1: Z c= dom (exp_R (#) (tan + cot)) ; ::_thesis: ( exp_R (#) (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) (tan + cot)) `| Z) . x = ((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) ) then Z c= (dom (tan + cot)) /\ (dom exp_R) by VALUED_1:def_4; then A2: Z c= dom (tan + cot) by XBOOLE_1:18; then A3: tan + cot is_differentiable_on Z by Th6; A4: exp_R is_differentiable_on Z by FDIFF_1:26, TAYLOR_1:16; for x being Real st x in Z holds ((exp_R (#) (tan + cot)) `| Z) . x = ((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) proof let x be Real; ::_thesis: ( x in Z implies ((exp_R (#) (tan + cot)) `| Z) . x = ((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) assume A5: x in Z ; ::_thesis: ((exp_R (#) (tan + cot)) `| Z) . x = ((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) then ((exp_R (#) (tan + cot)) `| Z) . x = (((tan + cot) . x) * (diff (exp_R,x))) + ((exp_R . x) * (diff ((tan + cot),x))) by A1, A3, A4, FDIFF_1:21 .= (((tan . x) + (cot . x)) * (diff (exp_R,x))) + ((exp_R . x) * (diff ((tan + cot),x))) by A2, A5, VALUED_1:def_1 .= ((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * (diff ((tan + cot),x))) by TAYLOR_1:16 .= ((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * (((tan + cot) `| Z) . x)) by A3, A5, FDIFF_1:def_7 .= ((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) by A2, A5, Th6 ; hence ((exp_R (#) (tan + cot)) `| Z) . x = ((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ; ::_thesis: verum end; hence ( exp_R (#) (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) (tan + cot)) `| Z) . x = ((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) ) by A1, A3, A4, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_10:30 for Z being open Subset of REAL st Z c= dom (exp_R (#) (tan - cot)) holds ( exp_R (#) (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) (tan - cot)) `| Z) . x = ((exp_R . x) * ((tan . x) - (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (exp_R (#) (tan - cot)) implies ( exp_R (#) (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) (tan - cot)) `| Z) . x = ((exp_R . x) * ((tan . x) - (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) ) ) assume A1: Z c= dom (exp_R (#) (tan - cot)) ; ::_thesis: ( exp_R (#) (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) (tan - cot)) `| Z) . x = ((exp_R . x) * ((tan . x) - (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) ) then Z c= (dom (tan - cot)) /\ (dom exp_R) by VALUED_1:def_4; then A2: Z c= dom (tan - cot) by XBOOLE_1:18; then A3: tan - cot is_differentiable_on Z by Th5; A4: exp_R is_differentiable_on Z by FDIFF_1:26, TAYLOR_1:16; for x being Real st x in Z holds ((exp_R (#) (tan - cot)) `| Z) . x = ((exp_R . x) * ((tan . x) - (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) proof let x be Real; ::_thesis: ( x in Z implies ((exp_R (#) (tan - cot)) `| Z) . x = ((exp_R . x) * ((tan . x) - (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) assume A5: x in Z ; ::_thesis: ((exp_R (#) (tan - cot)) `| Z) . x = ((exp_R . x) * ((tan . x) - (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) then ((exp_R (#) (tan - cot)) `| Z) . x = (((tan - cot) . x) * (diff (exp_R,x))) + ((exp_R . x) * (diff ((tan - cot),x))) by A1, A3, A4, FDIFF_1:21 .= (((tan . x) - (cot . x)) * (diff (exp_R,x))) + ((exp_R . x) * (diff ((tan - cot),x))) by A2, A5, VALUED_1:13 .= ((exp_R . x) * ((tan . x) - (cot . x))) + ((exp_R . x) * (diff ((tan - cot),x))) by TAYLOR_1:16 .= ((exp_R . x) * ((tan . x) - (cot . x))) + ((exp_R . x) * (((tan - cot) `| Z) . x)) by A3, A5, FDIFF_1:def_7 .= ((exp_R . x) * ((tan . x) - (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) by A2, A5, Th5 ; hence ((exp_R (#) (tan - cot)) `| Z) . x = ((exp_R . x) * ((tan . x) - (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ; ::_thesis: verum end; hence ( exp_R (#) (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) (tan - cot)) `| Z) . x = ((exp_R . x) * ((tan . x) - (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) ) by A1, A3, A4, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_10:31 for Z being open Subset of REAL st Z c= dom (sin (#) (sin + cos)) holds ( sin (#) (sin + cos) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) (sin + cos)) `| Z) . x = (((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sin (#) (sin + cos)) implies ( sin (#) (sin + cos) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) (sin + cos)) `| Z) . x = (((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) ) ) ) A1: for x being Real st x in Z holds sin is_differentiable_in x by SIN_COS:64; assume A2: Z c= dom (sin (#) (sin + cos)) ; ::_thesis: ( sin (#) (sin + cos) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) (sin + cos)) `| Z) . x = (((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) ) ) then A3: Z c= (dom (sin + cos)) /\ (dom sin) by VALUED_1:def_4; then A4: Z c= dom (sin + cos) by XBOOLE_1:18; then A5: sin + cos is_differentiable_on Z by FDIFF_7:38; Z c= dom sin by A3, XBOOLE_1:18; then A6: sin is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((sin (#) (sin + cos)) `| Z) . x = (((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) proof let x be Real; ::_thesis: ( x in Z implies ((sin (#) (sin + cos)) `| Z) . x = (((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) ) assume A7: x in Z ; ::_thesis: ((sin (#) (sin + cos)) `| Z) . x = (((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) then ((sin (#) (sin + cos)) `| Z) . x = (((sin + cos) . x) * (diff (sin,x))) + ((sin . x) * (diff ((sin + cos),x))) by A2, A5, A6, FDIFF_1:21 .= (((sin . x) + (cos . x)) * (diff (sin,x))) + ((sin . x) * (diff ((sin + cos),x))) by VALUED_1:1 .= (((sin . x) + (cos . x)) * (cos . x)) + ((sin . x) * (diff ((sin + cos),x))) by SIN_COS:64 .= (((sin . x) + (cos . x)) * (cos . x)) + ((sin . x) * (((sin + cos) `| Z) . x)) by A5, A7, FDIFF_1:def_7 .= (((sin . x) + (cos . x)) * (cos . x)) + ((sin . x) * ((cos . x) - (sin . x))) by A4, A7, FDIFF_7:38 ; hence ((sin (#) (sin + cos)) `| Z) . x = (((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) ; ::_thesis: verum end; hence ( sin (#) (sin + cos) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) (sin + cos)) `| Z) . x = (((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) ) ) by A2, A5, A6, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_10:32 for Z being open Subset of REAL st Z c= dom (sin (#) (sin - cos)) holds ( sin (#) (sin - cos) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) (sin - cos)) `| Z) . x = (((sin . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((cos . x) ^2) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sin (#) (sin - cos)) implies ( sin (#) (sin - cos) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) (sin - cos)) `| Z) . x = (((sin . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((cos . x) ^2) ) ) ) A1: for x being Real st x in Z holds sin is_differentiable_in x by SIN_COS:64; assume A2: Z c= dom (sin (#) (sin - cos)) ; ::_thesis: ( sin (#) (sin - cos) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) (sin - cos)) `| Z) . x = (((sin . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((cos . x) ^2) ) ) then A3: Z c= (dom (sin - cos)) /\ (dom sin) by VALUED_1:def_4; then A4: Z c= dom (sin - cos) by XBOOLE_1:18; then A5: sin - cos is_differentiable_on Z by FDIFF_7:39; Z c= dom sin by A3, XBOOLE_1:18; then A6: sin is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((sin (#) (sin - cos)) `| Z) . x = (((sin . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((cos . x) ^2) proof let x be Real; ::_thesis: ( x in Z implies ((sin (#) (sin - cos)) `| Z) . x = (((sin . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((cos . x) ^2) ) assume A7: x in Z ; ::_thesis: ((sin (#) (sin - cos)) `| Z) . x = (((sin . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((cos . x) ^2) then ((sin (#) (sin - cos)) `| Z) . x = (((sin - cos) . x) * (diff (sin,x))) + ((sin . x) * (diff ((sin - cos),x))) by A2, A5, A6, FDIFF_1:21 .= (((sin . x) - (cos . x)) * (diff (sin,x))) + ((sin . x) * (diff ((sin - cos),x))) by A4, A7, VALUED_1:13 .= (((sin . x) - (cos . x)) * (cos . x)) + ((sin . x) * (diff ((sin - cos),x))) by SIN_COS:64 .= (((sin . x) - (cos . x)) * (cos . x)) + ((sin . x) * (((sin - cos) `| Z) . x)) by A5, A7, FDIFF_1:def_7 .= (((sin . x) - (cos . x)) * (cos . x)) + ((sin . x) * ((cos . x) + (sin . x))) by A4, A7, FDIFF_7:39 ; hence ((sin (#) (sin - cos)) `| Z) . x = (((sin . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((cos . x) ^2) ; ::_thesis: verum end; hence ( sin (#) (sin - cos) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) (sin - cos)) `| Z) . x = (((sin . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((cos . x) ^2) ) ) by A2, A5, A6, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_10:33 for Z being open Subset of REAL st Z c= dom (cos (#) (sin - cos)) holds ( cos (#) (sin - cos) is_differentiable_on Z & ( for x being Real st x in Z holds ((cos (#) (sin - cos)) `| Z) . x = (((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cos (#) (sin - cos)) implies ( cos (#) (sin - cos) is_differentiable_on Z & ( for x being Real st x in Z holds ((cos (#) (sin - cos)) `| Z) . x = (((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) ) ) ) A1: for x being Real st x in Z holds cos is_differentiable_in x by SIN_COS:63; assume A2: Z c= dom (cos (#) (sin - cos)) ; ::_thesis: ( cos (#) (sin - cos) is_differentiable_on Z & ( for x being Real st x in Z holds ((cos (#) (sin - cos)) `| Z) . x = (((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) ) ) then A3: Z c= (dom (sin - cos)) /\ (dom cos) by VALUED_1:def_4; then A4: Z c= dom (sin - cos) by XBOOLE_1:18; then A5: sin - cos is_differentiable_on Z by FDIFF_7:39; Z c= dom cos by A3, XBOOLE_1:18; then A6: cos is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((cos (#) (sin - cos)) `| Z) . x = (((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) proof let x be Real; ::_thesis: ( x in Z implies ((cos (#) (sin - cos)) `| Z) . x = (((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) ) assume A7: x in Z ; ::_thesis: ((cos (#) (sin - cos)) `| Z) . x = (((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) then ((cos (#) (sin - cos)) `| Z) . x = (((sin - cos) . x) * (diff (cos,x))) + ((cos . x) * (diff ((sin - cos),x))) by A2, A5, A6, FDIFF_1:21 .= (((sin . x) - (cos . x)) * (diff (cos,x))) + ((cos . x) * (diff ((sin - cos),x))) by A4, A7, VALUED_1:13 .= (((sin . x) - (cos . x)) * (- (sin . x))) + ((cos . x) * (diff ((sin - cos),x))) by SIN_COS:63 .= (((sin . x) - (cos . x)) * (- (sin . x))) + ((cos . x) * (((sin - cos) `| Z) . x)) by A5, A7, FDIFF_1:def_7 .= (((sin . x) - (cos . x)) * (- (sin . x))) + ((cos . x) * ((cos . x) + (sin . x))) by A4, A7, FDIFF_7:39 ; hence ((cos (#) (sin - cos)) `| Z) . x = (((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) ; ::_thesis: verum end; hence ( cos (#) (sin - cos) is_differentiable_on Z & ( for x being Real st x in Z holds ((cos (#) (sin - cos)) `| Z) . x = (((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) ) ) by A2, A5, A6, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_10:34 for Z being open Subset of REAL st Z c= dom (cos (#) (sin + cos)) holds ( cos (#) (sin + cos) is_differentiable_on Z & ( for x being Real st x in Z holds ((cos (#) (sin + cos)) `| Z) . x = (((cos . x) ^2) - ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cos (#) (sin + cos)) implies ( cos (#) (sin + cos) is_differentiable_on Z & ( for x being Real st x in Z holds ((cos (#) (sin + cos)) `| Z) . x = (((cos . x) ^2) - ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) ) ) ) A1: for x being Real st x in Z holds cos is_differentiable_in x by SIN_COS:63; assume A2: Z c= dom (cos (#) (sin + cos)) ; ::_thesis: ( cos (#) (sin + cos) is_differentiable_on Z & ( for x being Real st x in Z holds ((cos (#) (sin + cos)) `| Z) . x = (((cos . x) ^2) - ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) ) ) then A3: Z c= (dom (sin + cos)) /\ (dom cos) by VALUED_1:def_4; then A4: Z c= dom (sin + cos) by XBOOLE_1:18; then A5: sin + cos is_differentiable_on Z by FDIFF_7:38; Z c= dom cos by A3, XBOOLE_1:18; then A6: cos is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((cos (#) (sin + cos)) `| Z) . x = (((cos . x) ^2) - ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) proof let x be Real; ::_thesis: ( x in Z implies ((cos (#) (sin + cos)) `| Z) . x = (((cos . x) ^2) - ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) ) assume A7: x in Z ; ::_thesis: ((cos (#) (sin + cos)) `| Z) . x = (((cos . x) ^2) - ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) then ((cos (#) (sin + cos)) `| Z) . x = (((sin + cos) . x) * (diff (cos,x))) + ((cos . x) * (diff ((sin + cos),x))) by A2, A5, A6, FDIFF_1:21 .= (((sin . x) + (cos . x)) * (diff (cos,x))) + ((cos . x) * (diff ((sin + cos),x))) by VALUED_1:1 .= (((sin . x) + (cos . x)) * (- (sin . x))) + ((cos . x) * (diff ((sin + cos),x))) by SIN_COS:63 .= (((sin . x) + (cos . x)) * (- (sin . x))) + ((cos . x) * (((sin + cos) `| Z) . x)) by A5, A7, FDIFF_1:def_7 .= (((sin . x) + (cos . x)) * (- (sin . x))) + ((cos . x) * ((cos . x) - (sin . x))) by A4, A7, FDIFF_7:38 ; hence ((cos (#) (sin + cos)) `| Z) . x = (((cos . x) ^2) - ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) ; ::_thesis: verum end; hence ( cos (#) (sin + cos) is_differentiable_on Z & ( for x being Real st x in Z holds ((cos (#) (sin + cos)) `| Z) . x = (((cos . x) ^2) - ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) ) ) by A2, A5, A6, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_10:35 for Z being open Subset of REAL st Z c= dom (sin * (tan + cot)) holds ( sin * (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * (tan + cot)) `| Z) . x = (cos . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sin * (tan + cot)) implies ( sin * (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * (tan + cot)) `| Z) . x = (cos . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) ) ) ) assume A1: Z c= dom (sin * (tan + cot)) ; ::_thesis: ( sin * (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * (tan + cot)) `| Z) . x = (cos . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) ) ) dom (sin * (tan + cot)) c= dom (tan + cot) by RELAT_1:25; then A2: Z c= dom (tan + cot) by A1, XBOOLE_1:1; then A3: tan + cot is_differentiable_on Z by Th6; A4: for x being Real st x in Z holds sin * (tan + cot) is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies sin * (tan + cot) is_differentiable_in x ) assume x in Z ; ::_thesis: sin * (tan + cot) is_differentiable_in x then A5: tan + cot is_differentiable_in x by A3, FDIFF_1:9; sin is_differentiable_in (tan + cot) . x by SIN_COS:64; hence sin * (tan + cot) is_differentiable_in x by A5, FDIFF_2:13; ::_thesis: verum end; then A6: sin * (tan + cot) is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((sin * (tan + cot)) `| Z) . x = (cos . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) proof let x be Real; ::_thesis: ( x in Z implies ((sin * (tan + cot)) `| Z) . x = (cos . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) ) A7: sin is_differentiable_in (tan + cot) . x by SIN_COS:64; assume A8: x in Z ; ::_thesis: ((sin * (tan + cot)) `| Z) . x = (cos . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) then tan + cot is_differentiable_in x by A3, FDIFF_1:9; then diff ((sin * (tan + cot)),x) = (diff (sin,((tan + cot) . x))) * (diff ((tan + cot),x)) by A7, FDIFF_2:13 .= (cos . ((tan + cot) . x)) * (diff ((tan + cot),x)) by SIN_COS:64 .= (cos . ((tan + cot) . x)) * (((tan + cot) `| Z) . x) by A3, A8, FDIFF_1:def_7 .= (cos . ((tan + cot) . x)) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) by A2, A8, Th6 .= (cos . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) by A2, A8, VALUED_1:def_1 ; hence ((sin * (tan + cot)) `| Z) . x = (cos . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) by A6, A8, FDIFF_1:def_7; ::_thesis: verum end; hence ( sin * (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * (tan + cot)) `| Z) . x = (cos . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) ) ) by A1, A4, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_10:36 for Z being open Subset of REAL st Z c= dom (sin * (tan - cot)) holds ( sin * (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * (tan - cot)) `| Z) . x = (cos . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sin * (tan - cot)) implies ( sin * (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * (tan - cot)) `| Z) . x = (cos . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) ) ) ) assume A1: Z c= dom (sin * (tan - cot)) ; ::_thesis: ( sin * (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * (tan - cot)) `| Z) . x = (cos . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) ) ) dom (sin * (tan - cot)) c= dom (tan - cot) by RELAT_1:25; then A2: Z c= dom (tan - cot) by A1, XBOOLE_1:1; then A3: tan - cot is_differentiable_on Z by Th5; A4: for x being Real st x in Z holds sin * (tan - cot) is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies sin * (tan - cot) is_differentiable_in x ) assume x in Z ; ::_thesis: sin * (tan - cot) is_differentiable_in x then A5: tan - cot is_differentiable_in x by A3, FDIFF_1:9; sin is_differentiable_in (tan - cot) . x by SIN_COS:64; hence sin * (tan - cot) is_differentiable_in x by A5, FDIFF_2:13; ::_thesis: verum end; then A6: sin * (tan - cot) is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((sin * (tan - cot)) `| Z) . x = (cos . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) proof let x be Real; ::_thesis: ( x in Z implies ((sin * (tan - cot)) `| Z) . x = (cos . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) ) A7: sin is_differentiable_in (tan - cot) . x by SIN_COS:64; assume A8: x in Z ; ::_thesis: ((sin * (tan - cot)) `| Z) . x = (cos . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) then tan - cot is_differentiable_in x by A3, FDIFF_1:9; then diff ((sin * (tan - cot)),x) = (diff (sin,((tan - cot) . x))) * (diff ((tan - cot),x)) by A7, FDIFF_2:13 .= (cos . ((tan - cot) . x)) * (diff ((tan - cot),x)) by SIN_COS:64 .= (cos . ((tan - cot) . x)) * (((tan - cot) `| Z) . x) by A3, A8, FDIFF_1:def_7 .= (cos . ((tan - cot) . x)) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) by A2, A8, Th5 .= (cos . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) by A2, A8, VALUED_1:13 ; hence ((sin * (tan - cot)) `| Z) . x = (cos . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) by A6, A8, FDIFF_1:def_7; ::_thesis: verum end; hence ( sin * (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * (tan - cot)) `| Z) . x = (cos . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) ) ) by A1, A4, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_10:37 for Z being open Subset of REAL st Z c= dom (cos * (tan - cot)) holds ( cos * (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * (tan - cot)) `| Z) . x = - ((sin . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cos * (tan - cot)) implies ( cos * (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * (tan - cot)) `| Z) . x = - ((sin . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) ) ) assume A1: Z c= dom (cos * (tan - cot)) ; ::_thesis: ( cos * (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * (tan - cot)) `| Z) . x = - ((sin . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) ) dom (cos * (tan - cot)) c= dom (tan - cot) by RELAT_1:25; then A2: Z c= dom (tan - cot) by A1, XBOOLE_1:1; then A3: tan - cot is_differentiable_on Z by Th5; A4: for x being Real st x in Z holds cos * (tan - cot) is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies cos * (tan - cot) is_differentiable_in x ) assume x in Z ; ::_thesis: cos * (tan - cot) is_differentiable_in x then A5: tan - cot is_differentiable_in x by A3, FDIFF_1:9; cos is_differentiable_in (tan - cot) . x by SIN_COS:63; hence cos * (tan - cot) is_differentiable_in x by A5, FDIFF_2:13; ::_thesis: verum end; then A6: cos * (tan - cot) is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((cos * (tan - cot)) `| Z) . x = - ((sin . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) proof let x be Real; ::_thesis: ( x in Z implies ((cos * (tan - cot)) `| Z) . x = - ((sin . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) A7: cos is_differentiable_in (tan - cot) . x by SIN_COS:63; assume A8: x in Z ; ::_thesis: ((cos * (tan - cot)) `| Z) . x = - ((sin . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) then tan - cot is_differentiable_in x by A3, FDIFF_1:9; then diff ((cos * (tan - cot)),x) = (diff (cos,((tan - cot) . x))) * (diff ((tan - cot),x)) by A7, FDIFF_2:13 .= (- (sin . ((tan - cot) . x))) * (diff ((tan - cot),x)) by SIN_COS:63 .= (- (sin . ((tan - cot) . x))) * (((tan - cot) `| Z) . x) by A3, A8, FDIFF_1:def_7 .= (- (sin . ((tan - cot) . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) by A2, A8, Th5 .= (- (sin . ((tan . x) - (cot . x)))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) by A2, A8, VALUED_1:13 ; hence ((cos * (tan - cot)) `| Z) . x = - ((sin . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) by A6, A8, FDIFF_1:def_7; ::_thesis: verum end; hence ( cos * (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * (tan - cot)) `| Z) . x = - ((sin . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) ) by A1, A4, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_10:38 for Z being open Subset of REAL st Z c= dom (cos * (tan + cot)) holds ( cos * (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * (tan + cot)) `| Z) . x = - ((sin . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cos * (tan + cot)) implies ( cos * (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * (tan + cot)) `| Z) . x = - ((sin . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) ) ) assume A1: Z c= dom (cos * (tan + cot)) ; ::_thesis: ( cos * (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * (tan + cot)) `| Z) . x = - ((sin . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) ) dom (cos * (tan + cot)) c= dom (tan + cot) by RELAT_1:25; then A2: Z c= dom (tan + cot) by A1, XBOOLE_1:1; then A3: tan + cot is_differentiable_on Z by Th6; A4: for x being Real st x in Z holds cos * (tan + cot) is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies cos * (tan + cot) is_differentiable_in x ) assume x in Z ; ::_thesis: cos * (tan + cot) is_differentiable_in x then A5: tan + cot is_differentiable_in x by A3, FDIFF_1:9; cos is_differentiable_in (tan + cot) . x by SIN_COS:63; hence cos * (tan + cot) is_differentiable_in x by A5, FDIFF_2:13; ::_thesis: verum end; then A6: cos * (tan + cot) is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((cos * (tan + cot)) `| Z) . x = - ((sin . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) proof let x be Real; ::_thesis: ( x in Z implies ((cos * (tan + cot)) `| Z) . x = - ((sin . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) A7: cos is_differentiable_in (tan + cot) . x by SIN_COS:63; assume A8: x in Z ; ::_thesis: ((cos * (tan + cot)) `| Z) . x = - ((sin . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) then tan + cot is_differentiable_in x by A3, FDIFF_1:9; then diff ((cos * (tan + cot)),x) = (diff (cos,((tan + cot) . x))) * (diff ((tan + cot),x)) by A7, FDIFF_2:13 .= (- (sin . ((tan + cot) . x))) * (diff ((tan + cot),x)) by SIN_COS:63 .= (- (sin . ((tan + cot) . x))) * (((tan + cot) `| Z) . x) by A3, A8, FDIFF_1:def_7 .= (- (sin . ((tan + cot) . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) by A2, A8, Th6 .= (- (sin . ((tan . x) + (cot . x)))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) by A2, A8, VALUED_1:def_1 ; hence ((cos * (tan + cot)) `| Z) . x = - ((sin . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) by A6, A8, FDIFF_1:def_7; ::_thesis: verum end; hence ( cos * (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * (tan + cot)) `| Z) . x = - ((sin . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) ) by A1, A4, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_10:39 for Z being open Subset of REAL st Z c= dom (exp_R * (tan + cot)) holds ( exp_R * (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R * (tan + cot)) `| Z) . x = (exp_R . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (exp_R * (tan + cot)) implies ( exp_R * (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R * (tan + cot)) `| Z) . x = (exp_R . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) ) ) ) assume A1: Z c= dom (exp_R * (tan + cot)) ; ::_thesis: ( exp_R * (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R * (tan + cot)) `| Z) . x = (exp_R . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) ) ) dom (exp_R * (tan + cot)) c= dom (tan + cot) by RELAT_1:25; then A2: Z c= dom (tan + cot) by A1, XBOOLE_1:1; then A3: tan + cot is_differentiable_on Z by Th6; A4: for x being Real st x in Z holds exp_R * (tan + cot) is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies exp_R * (tan + cot) is_differentiable_in x ) assume x in Z ; ::_thesis: exp_R * (tan + cot) is_differentiable_in x then A5: tan + cot is_differentiable_in x by A3, FDIFF_1:9; exp_R is_differentiable_in (tan + cot) . x by SIN_COS:65; hence exp_R * (tan + cot) is_differentiable_in x by A5, FDIFF_2:13; ::_thesis: verum end; then A6: exp_R * (tan + cot) is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((exp_R * (tan + cot)) `| Z) . x = (exp_R . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) proof let x be Real; ::_thesis: ( x in Z implies ((exp_R * (tan + cot)) `| Z) . x = (exp_R . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) ) A7: exp_R is_differentiable_in (tan + cot) . x by SIN_COS:65; assume A8: x in Z ; ::_thesis: ((exp_R * (tan + cot)) `| Z) . x = (exp_R . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) then tan + cot is_differentiable_in x by A3, FDIFF_1:9; then diff ((exp_R * (tan + cot)),x) = (diff (exp_R,((tan + cot) . x))) * (diff ((tan + cot),x)) by A7, FDIFF_2:13 .= (exp_R . ((tan + cot) . x)) * (diff ((tan + cot),x)) by SIN_COS:65 .= (exp_R . ((tan + cot) . x)) * (((tan + cot) `| Z) . x) by A3, A8, FDIFF_1:def_7 .= (exp_R . ((tan + cot) . x)) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) by A2, A8, Th6 .= (exp_R . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) by A2, A8, VALUED_1:def_1 ; hence ((exp_R * (tan + cot)) `| Z) . x = (exp_R . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) by A6, A8, FDIFF_1:def_7; ::_thesis: verum end; hence ( exp_R * (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R * (tan + cot)) `| Z) . x = (exp_R . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) ) ) by A1, A4, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_10:40 for Z being open Subset of REAL st Z c= dom (exp_R * (tan - cot)) holds ( exp_R * (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R * (tan - cot)) `| Z) . x = (exp_R . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (exp_R * (tan - cot)) implies ( exp_R * (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R * (tan - cot)) `| Z) . x = (exp_R . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) ) ) ) assume A1: Z c= dom (exp_R * (tan - cot)) ; ::_thesis: ( exp_R * (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R * (tan - cot)) `| Z) . x = (exp_R . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) ) ) dom (exp_R * (tan - cot)) c= dom (tan - cot) by RELAT_1:25; then A2: Z c= dom (tan - cot) by A1, XBOOLE_1:1; then A3: tan - cot is_differentiable_on Z by Th5; A4: for x being Real st x in Z holds exp_R * (tan - cot) is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies exp_R * (tan - cot) is_differentiable_in x ) assume x in Z ; ::_thesis: exp_R * (tan - cot) is_differentiable_in x then A5: tan - cot is_differentiable_in x by A3, FDIFF_1:9; exp_R is_differentiable_in (tan - cot) . x by SIN_COS:65; hence exp_R * (tan - cot) is_differentiable_in x by A5, FDIFF_2:13; ::_thesis: verum end; then A6: exp_R * (tan - cot) is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((exp_R * (tan - cot)) `| Z) . x = (exp_R . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) proof let x be Real; ::_thesis: ( x in Z implies ((exp_R * (tan - cot)) `| Z) . x = (exp_R . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) ) A7: exp_R is_differentiable_in (tan - cot) . x by SIN_COS:65; assume A8: x in Z ; ::_thesis: ((exp_R * (tan - cot)) `| Z) . x = (exp_R . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) then tan - cot is_differentiable_in x by A3, FDIFF_1:9; then diff ((exp_R * (tan - cot)),x) = (diff (exp_R,((tan - cot) . x))) * (diff ((tan - cot),x)) by A7, FDIFF_2:13 .= (exp_R . ((tan - cot) . x)) * (diff ((tan - cot),x)) by SIN_COS:65 .= (exp_R . ((tan - cot) . x)) * (((tan - cot) `| Z) . x) by A3, A8, FDIFF_1:def_7 .= (exp_R . ((tan - cot) . x)) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) by A2, A8, Th5 .= (exp_R . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) by A2, A8, VALUED_1:13 ; hence ((exp_R * (tan - cot)) `| Z) . x = (exp_R . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) by A6, A8, FDIFF_1:def_7; ::_thesis: verum end; hence ( exp_R * (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R * (tan - cot)) `| Z) . x = (exp_R . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) ) ) by A1, A4, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_10:41 for Z being open Subset of REAL st Z c= dom ((tan - cot) / exp_R) holds ( (tan - cot) / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds (((tan - cot) / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - (tan . x)) + (cot . x)) / (exp_R . x) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((tan - cot) / exp_R) implies ( (tan - cot) / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds (((tan - cot) / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - (tan . x)) + (cot . x)) / (exp_R . x) ) ) ) A1: for x being Real st x in Z holds exp_R . x <> 0 by SIN_COS:54; assume Z c= dom ((tan - cot) / exp_R) ; ::_thesis: ( (tan - cot) / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds (((tan - cot) / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - (tan . x)) + (cot . x)) / (exp_R . x) ) ) then Z c= (dom (tan - cot)) /\ ((dom exp_R) \ (exp_R " {0})) by RFUNCT_1:def_1; then A2: Z c= dom (tan - cot) by XBOOLE_1:18; then A3: tan - cot is_differentiable_on Z by Th5; A4: exp_R is_differentiable_on Z by FDIFF_1:26, TAYLOR_1:16; then A5: (tan - cot) / exp_R is_differentiable_on Z by A3, A1, FDIFF_2:21; for x being Real st x in Z holds (((tan - cot) / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - (tan . x)) + (cot . x)) / (exp_R . x) proof let x be Real; ::_thesis: ( x in Z implies (((tan - cot) / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - (tan . x)) + (cot . x)) / (exp_R . x) ) A6: exp_R is_differentiable_in x by SIN_COS:65; A7: exp_R . x <> 0 by SIN_COS:54; assume A8: x in Z ; ::_thesis: (((tan - cot) / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - (tan . x)) + (cot . x)) / (exp_R . x) then A9: (tan - cot) . x = (tan . x) - (cot . x) by A2, VALUED_1:13; tan - cot is_differentiable_in x by A3, A8, FDIFF_1:9; then diff (((tan - cot) / exp_R),x) = (((diff ((tan - cot),x)) * (exp_R . x)) - ((diff (exp_R,x)) * ((tan - cot) . x))) / ((exp_R . x) ^2) by A6, A7, FDIFF_2:14 .= (((((tan - cot) `| Z) . x) * (exp_R . x)) - ((diff (exp_R,x)) * ((tan - cot) . x))) / ((exp_R . x) ^2) by A3, A8, FDIFF_1:def_7 .= ((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) * (exp_R . x)) - ((diff (exp_R,x)) * ((tan - cot) . x))) / ((exp_R . x) ^2) by A2, A8, Th5 .= ((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) * (exp_R . x)) - ((exp_R . x) * ((tan . x) - (cot . x)))) / ((exp_R . x) * (exp_R . x)) by A9, SIN_COS:65 .= (((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - ((tan . x) - (cot . x))) * ((exp_R . x) / ((exp_R . x) * (exp_R . x))) .= (((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - ((tan . x) - (cot . x))) * (((exp_R . x) / (exp_R . x)) / (exp_R . x)) by XCMPLX_1:78 .= (((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - ((tan . x) - (cot . x))) * (1 / (exp_R . x)) by A7, XCMPLX_1:60 .= (((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - ((tan . x) - (cot . x))) / (exp_R . x) ; hence (((tan - cot) / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - (tan . x)) + (cot . x)) / (exp_R . x) by A5, A8, FDIFF_1:def_7; ::_thesis: verum end; hence ( (tan - cot) / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds (((tan - cot) / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - (tan . x)) + (cot . x)) / (exp_R . x) ) ) by A3, A4, A1, FDIFF_2:21; ::_thesis: verum end; theorem :: FDIFF_10:42 for Z being open Subset of REAL st Z c= dom ((tan + cot) / exp_R) holds ( (tan + cot) / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds (((tan + cot) / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - (tan . x)) - (cot . x)) / (exp_R . x) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((tan + cot) / exp_R) implies ( (tan + cot) / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds (((tan + cot) / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - (tan . x)) - (cot . x)) / (exp_R . x) ) ) ) A1: for x being Real st x in Z holds exp_R . x <> 0 by SIN_COS:54; assume Z c= dom ((tan + cot) / exp_R) ; ::_thesis: ( (tan + cot) / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds (((tan + cot) / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - (tan . x)) - (cot . x)) / (exp_R . x) ) ) then Z c= (dom (tan + cot)) /\ ((dom exp_R) \ (exp_R " {0})) by RFUNCT_1:def_1; then A2: Z c= dom (tan + cot) by XBOOLE_1:18; then A3: tan + cot is_differentiable_on Z by Th6; A4: exp_R is_differentiable_on Z by FDIFF_1:26, TAYLOR_1:16; then A5: (tan + cot) / exp_R is_differentiable_on Z by A3, A1, FDIFF_2:21; for x being Real st x in Z holds (((tan + cot) / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - (tan . x)) - (cot . x)) / (exp_R . x) proof let x be Real; ::_thesis: ( x in Z implies (((tan + cot) / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - (tan . x)) - (cot . x)) / (exp_R . x) ) A6: exp_R is_differentiable_in x by SIN_COS:65; A7: exp_R . x <> 0 by SIN_COS:54; assume A8: x in Z ; ::_thesis: (((tan + cot) / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - (tan . x)) - (cot . x)) / (exp_R . x) then A9: (tan + cot) . x = (tan . x) + (cot . x) by A2, VALUED_1:def_1; tan + cot is_differentiable_in x by A3, A8, FDIFF_1:9; then diff (((tan + cot) / exp_R),x) = (((diff ((tan + cot),x)) * (exp_R . x)) - ((diff (exp_R,x)) * ((tan + cot) . x))) / ((exp_R . x) ^2) by A6, A7, FDIFF_2:14 .= (((((tan + cot) `| Z) . x) * (exp_R . x)) - ((diff (exp_R,x)) * ((tan + cot) . x))) / ((exp_R . x) ^2) by A3, A8, FDIFF_1:def_7 .= ((((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) * (exp_R . x)) - ((diff (exp_R,x)) * ((tan + cot) . x))) / ((exp_R . x) ^2) by A2, A8, Th6 .= ((((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) * (exp_R . x)) - ((exp_R . x) * ((tan . x) + (cot . x)))) / ((exp_R . x) * (exp_R . x)) by A9, SIN_COS:65 .= (((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - ((tan . x) + (cot . x))) * ((exp_R . x) / ((exp_R . x) * (exp_R . x))) .= (((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - ((tan . x) + (cot . x))) * (((exp_R . x) / (exp_R . x)) / (exp_R . x)) by XCMPLX_1:78 .= (((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - ((tan . x) + (cot . x))) * (1 / (exp_R . x)) by A7, XCMPLX_1:60 .= (((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - ((tan . x) + (cot . x))) / (exp_R . x) ; hence (((tan + cot) / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - (tan . x)) - (cot . x)) / (exp_R . x) by A5, A8, FDIFF_1:def_7; ::_thesis: verum end; hence ( (tan + cot) / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds (((tan + cot) / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - (tan . x)) - (cot . x)) / (exp_R . x) ) ) by A3, A4, A1, FDIFF_2:21; ::_thesis: verum end; theorem :: FDIFF_10:43 for Z being open Subset of REAL st Z c= dom (sin * sec) holds ( sin * sec is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * sec) `| Z) . x = ((cos . (sec . x)) * (sin . x)) / ((cos . x) ^2) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sin * sec) implies ( sin * sec is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * sec) `| Z) . x = ((cos . (sec . x)) * (sin . x)) / ((cos . x) ^2) ) ) ) assume A1: Z c= dom (sin * sec) ; ::_thesis: ( sin * sec is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * sec) `| Z) . x = ((cos . (sec . x)) * (sin . x)) / ((cos . x) ^2) ) ) dom (sin * sec) c= dom sec by RELAT_1:25; then A2: Z c= dom sec by A1, XBOOLE_1:1; A3: for x being Real st x in Z holds sin * sec is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies sin * sec is_differentiable_in x ) assume x in Z ; ::_thesis: sin * sec is_differentiable_in x then cos . x <> 0 by A2, RFUNCT_1:3; then A4: sec is_differentiable_in x by FDIFF_9:1; sin is_differentiable_in sec . x by SIN_COS:64; hence sin * sec is_differentiable_in x by A4, FDIFF_2:13; ::_thesis: verum end; then A5: sin * sec is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((sin * sec) `| Z) . x = ((cos . (sec . x)) * (sin . x)) / ((cos . x) ^2) proof let x be Real; ::_thesis: ( x in Z implies ((sin * sec) `| Z) . x = ((cos . (sec . x)) * (sin . x)) / ((cos . x) ^2) ) A6: sin is_differentiable_in sec . x by SIN_COS:64; assume A7: x in Z ; ::_thesis: ((sin * sec) `| Z) . x = ((cos . (sec . x)) * (sin . x)) / ((cos . x) ^2) then A8: cos . x <> 0 by A2, RFUNCT_1:3; then sec is_differentiable_in x by FDIFF_9:1; then diff ((sin * sec),x) = (diff (sin,(sec . x))) * (diff (sec,x)) by A6, FDIFF_2:13 .= (cos (sec . x)) * (diff (sec,x)) by SIN_COS:64 .= (cos (sec . x)) * ((sin . x) / ((cos . x) ^2)) by A8, FDIFF_9:1 .= ((cos . (sec . x)) * (sin . x)) / ((cos . x) ^2) ; hence ((sin * sec) `| Z) . x = ((cos . (sec . x)) * (sin . x)) / ((cos . x) ^2) by A5, A7, FDIFF_1:def_7; ::_thesis: verum end; hence ( sin * sec is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * sec) `| Z) . x = ((cos . (sec . x)) * (sin . x)) / ((cos . x) ^2) ) ) by A1, A3, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_10:44 for Z being open Subset of REAL st Z c= dom (cos * sec) holds ( cos * sec is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * sec) `| Z) . x = - (((sin . (sec . x)) * (sin . x)) / ((cos . x) ^2)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cos * sec) implies ( cos * sec is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * sec) `| Z) . x = - (((sin . (sec . x)) * (sin . x)) / ((cos . x) ^2)) ) ) ) assume A1: Z c= dom (cos * sec) ; ::_thesis: ( cos * sec is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * sec) `| Z) . x = - (((sin . (sec . x)) * (sin . x)) / ((cos . x) ^2)) ) ) dom (cos * sec) c= dom sec by RELAT_1:25; then A2: Z c= dom sec by A1, XBOOLE_1:1; A3: for x being Real st x in Z holds cos * sec is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies cos * sec is_differentiable_in x ) assume x in Z ; ::_thesis: cos * sec is_differentiable_in x then cos . x <> 0 by A2, RFUNCT_1:3; then A4: sec is_differentiable_in x by FDIFF_9:1; cos is_differentiable_in sec . x by SIN_COS:63; hence cos * sec is_differentiable_in x by A4, FDIFF_2:13; ::_thesis: verum end; then A5: cos * sec is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((cos * sec) `| Z) . x = - (((sin . (sec . x)) * (sin . x)) / ((cos . x) ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((cos * sec) `| Z) . x = - (((sin . (sec . x)) * (sin . x)) / ((cos . x) ^2)) ) A6: cos is_differentiable_in sec . x by SIN_COS:63; assume A7: x in Z ; ::_thesis: ((cos * sec) `| Z) . x = - (((sin . (sec . x)) * (sin . x)) / ((cos . x) ^2)) then A8: cos . x <> 0 by A2, RFUNCT_1:3; then sec is_differentiable_in x by FDIFF_9:1; then diff ((cos * sec),x) = (diff (cos,(sec . x))) * (diff (sec,x)) by A6, FDIFF_2:13 .= (- (sin (sec . x))) * (diff (sec,x)) by SIN_COS:63 .= (- (sin (sec . x))) * ((sin . x) / ((cos . x) ^2)) by A8, FDIFF_9:1 .= - (((sin . (sec . x)) * (sin . x)) / ((cos . x) ^2)) ; hence ((cos * sec) `| Z) . x = - (((sin . (sec . x)) * (sin . x)) / ((cos . x) ^2)) by A5, A7, FDIFF_1:def_7; ::_thesis: verum end; hence ( cos * sec is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * sec) `| Z) . x = - (((sin . (sec . x)) * (sin . x)) / ((cos . x) ^2)) ) ) by A1, A3, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_10:45 for Z being open Subset of REAL st Z c= dom (sin * cosec) holds ( sin * cosec is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * cosec) `| Z) . x = - (((cos . (cosec . x)) * (cos . x)) / ((sin . x) ^2)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sin * cosec) implies ( sin * cosec is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * cosec) `| Z) . x = - (((cos . (cosec . x)) * (cos . x)) / ((sin . x) ^2)) ) ) ) assume A1: Z c= dom (sin * cosec) ; ::_thesis: ( sin * cosec is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * cosec) `| Z) . x = - (((cos . (cosec . x)) * (cos . x)) / ((sin . x) ^2)) ) ) dom (sin * cosec) c= dom cosec by RELAT_1:25; then A2: Z c= dom cosec by A1, XBOOLE_1:1; A3: for x being Real st x in Z holds sin * cosec is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies sin * cosec is_differentiable_in x ) assume x in Z ; ::_thesis: sin * cosec is_differentiable_in x then sin . x <> 0 by A2, RFUNCT_1:3; then A4: cosec is_differentiable_in x by FDIFF_9:2; sin is_differentiable_in cosec . x by SIN_COS:64; hence sin * cosec is_differentiable_in x by A4, FDIFF_2:13; ::_thesis: verum end; then A5: sin * cosec is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((sin * cosec) `| Z) . x = - (((cos . (cosec . x)) * (cos . x)) / ((sin . x) ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((sin * cosec) `| Z) . x = - (((cos . (cosec . x)) * (cos . x)) / ((sin . x) ^2)) ) A6: sin is_differentiable_in cosec . x by SIN_COS:64; assume A7: x in Z ; ::_thesis: ((sin * cosec) `| Z) . x = - (((cos . (cosec . x)) * (cos . x)) / ((sin . x) ^2)) then A8: sin . x <> 0 by A2, RFUNCT_1:3; then cosec is_differentiable_in x by FDIFF_9:2; then diff ((sin * cosec),x) = (diff (sin,(cosec . x))) * (diff (cosec,x)) by A6, FDIFF_2:13 .= (cos (cosec . x)) * (diff (cosec,x)) by SIN_COS:64 .= (cos (cosec . x)) * (- ((cos . x) / ((sin . x) ^2))) by A8, FDIFF_9:2 .= - (((cos . (cosec . x)) * (cos . x)) / ((sin . x) ^2)) ; hence ((sin * cosec) `| Z) . x = - (((cos . (cosec . x)) * (cos . x)) / ((sin . x) ^2)) by A5, A7, FDIFF_1:def_7; ::_thesis: verum end; hence ( sin * cosec is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * cosec) `| Z) . x = - (((cos . (cosec . x)) * (cos . x)) / ((sin . x) ^2)) ) ) by A1, A3, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_10:46 for Z being open Subset of REAL st Z c= dom (cos * cosec) holds ( cos * cosec is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * cosec) `| Z) . x = ((sin . (cosec . x)) * (cos . x)) / ((sin . x) ^2) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cos * cosec) implies ( cos * cosec is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * cosec) `| Z) . x = ((sin . (cosec . x)) * (cos . x)) / ((sin . x) ^2) ) ) ) assume A1: Z c= dom (cos * cosec) ; ::_thesis: ( cos * cosec is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * cosec) `| Z) . x = ((sin . (cosec . x)) * (cos . x)) / ((sin . x) ^2) ) ) dom (cos * cosec) c= dom cosec by RELAT_1:25; then A2: Z c= dom cosec by A1, XBOOLE_1:1; A3: for x being Real st x in Z holds cos * cosec is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies cos * cosec is_differentiable_in x ) assume x in Z ; ::_thesis: cos * cosec is_differentiable_in x then sin . x <> 0 by A2, RFUNCT_1:3; then A4: cosec is_differentiable_in x by FDIFF_9:2; cos is_differentiable_in cosec . x by SIN_COS:63; hence cos * cosec is_differentiable_in x by A4, FDIFF_2:13; ::_thesis: verum end; then A5: cos * cosec is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((cos * cosec) `| Z) . x = ((sin . (cosec . x)) * (cos . x)) / ((sin . x) ^2) proof let x be Real; ::_thesis: ( x in Z implies ((cos * cosec) `| Z) . x = ((sin . (cosec . x)) * (cos . x)) / ((sin . x) ^2) ) A6: cos is_differentiable_in cosec . x by SIN_COS:63; assume A7: x in Z ; ::_thesis: ((cos * cosec) `| Z) . x = ((sin . (cosec . x)) * (cos . x)) / ((sin . x) ^2) then A8: sin . x <> 0 by A2, RFUNCT_1:3; then cosec is_differentiable_in x by FDIFF_9:2; then diff ((cos * cosec),x) = (diff (cos,(cosec . x))) * (diff (cosec,x)) by A6, FDIFF_2:13 .= (- (sin (cosec . x))) * (diff (cosec,x)) by SIN_COS:63 .= (- (sin (cosec . x))) * (- ((cos . x) / ((sin . x) ^2))) by A8, FDIFF_9:2 ; hence ((cos * cosec) `| Z) . x = ((sin . (cosec . x)) * (cos . x)) / ((sin . x) ^2) by A5, A7, FDIFF_1:def_7; ::_thesis: verum end; hence ( cos * cosec is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * cosec) `| Z) . x = ((sin . (cosec . x)) * (cos . x)) / ((sin . x) ^2) ) ) by A1, A3, FDIFF_1:9; ::_thesis: verum end;