:: FDIFF_7 semantic presentation begin theorem Th1: :: FDIFF_7:1 for x being Real holds x #Z 2 = x ^2 proof let x be Real; ::_thesis: x #Z 2 = x ^2 x #Z 2 = x |^ 2 by PREPOWER:36 .= x ^2 by NEWTON:81 ; hence x #Z 2 = x ^2 ; ::_thesis: verum end; theorem Th2: :: FDIFF_7:2 for x being Real st x > 0 holds x #R (1 / 2) = sqrt x proof let x be Real; ::_thesis: ( x > 0 implies x #R (1 / 2) = sqrt x ) assume A1: x > 0 ; ::_thesis: x #R (1 / 2) = sqrt x then A2: x #R (1 / 2) > 0 by PREPOWER:81; x = x #R ((1 / 2) * 2) by A1, PREPOWER:72 .= (x #R (1 / 2)) #R 2 by A1, PREPOWER:91 .= (x #R (1 / 2)) #Q 2 by A1, PREPOWER:74, PREPOWER:81 .= (x #R (1 / 2)) to_power 2 by A1, POWER:44, PREPOWER:81 .= (x #R (1 / 2)) ^2 by POWER:46 ; hence x #R (1 / 2) = sqrt x by A1, A2, SQUARE_1:def_2; ::_thesis: verum end; theorem Th3: :: FDIFF_7:3 for x being Real st x > 0 holds x #R (- (1 / 2)) = 1 / (sqrt x) proof let x be Real; ::_thesis: ( x > 0 implies x #R (- (1 / 2)) = 1 / (sqrt x) ) assume A1: x > 0 ; ::_thesis: x #R (- (1 / 2)) = 1 / (sqrt x) hence x #R (- (1 / 2)) = 1 / (x #R (1 / 2)) by PREPOWER:76 .= 1 / (sqrt x) by A1, Th2 ; ::_thesis: verum end; Lm1: for x being Real holds 2 * ((cos . (x / 2)) ^2) = 1 + (cos . x) proof let x be Real; ::_thesis: 2 * ((cos . (x / 2)) ^2) = 1 + (cos . x) (cos (x / 2)) ^2 = (1 + (cos (2 * (x / 2)))) / 2 by SIN_COS5:21 .= (1 + (cos x)) / 2 ; then 2 * ((cos . (x / 2)) ^2) = 2 * ((1 + (cos x)) / 2) by SIN_COS:def_19 .= 1 + (cos . x) by SIN_COS:def_19 ; hence 2 * ((cos . (x / 2)) ^2) = 1 + (cos . x) ; ::_thesis: verum end; Lm2: for x being Real holds 2 * ((sin . (x / 2)) ^2) = 1 - (cos . x) proof let x be Real; ::_thesis: 2 * ((sin . (x / 2)) ^2) = 1 - (cos . x) (sin (x / 2)) ^2 = (1 - (cos (2 * (x / 2)))) / 2 by SIN_COS5:20 .= (1 - (cos x)) / 2 ; then 2 * ((sin . (x / 2)) ^2) = 2 * ((1 - (cos x)) / 2) by SIN_COS:def_17 .= 1 - (cos . x) by SIN_COS:def_19 ; hence 2 * ((sin . (x / 2)) ^2) = 1 - (cos . x) ; ::_thesis: verum end; theorem :: FDIFF_7:4 for r being Real for Z being open Subset of REAL st Z c= ].(- 1),1.[ & Z c= dom (r (#) arcsin) holds ( r (#) arcsin is_differentiable_on Z & ( for x being Real st x in Z holds ((r (#) arcsin) `| Z) . x = r / (sqrt (1 - (x ^2))) ) ) proof let r be Real; ::_thesis: for Z being open Subset of REAL st Z c= ].(- 1),1.[ & Z c= dom (r (#) arcsin) holds ( r (#) arcsin is_differentiable_on Z & ( for x being Real st x in Z holds ((r (#) arcsin) `| Z) . x = r / (sqrt (1 - (x ^2))) ) ) let Z be open Subset of REAL; ::_thesis: ( Z c= ].(- 1),1.[ & Z c= dom (r (#) arcsin) implies ( r (#) arcsin is_differentiable_on Z & ( for x being Real st x in Z holds ((r (#) arcsin) `| Z) . x = r / (sqrt (1 - (x ^2))) ) ) ) assume that A1: Z c= ].(- 1),1.[ and A2: Z c= dom (r (#) arcsin) ; ::_thesis: ( r (#) arcsin is_differentiable_on Z & ( for x being Real st x in Z holds ((r (#) arcsin) `| Z) . x = r / (sqrt (1 - (x ^2))) ) ) A3: arcsin is_differentiable_on Z by A1, FDIFF_1:26, SIN_COS6:83; for x being Real st x in Z holds ((r (#) arcsin) `| Z) . x = r / (sqrt (1 - (x ^2))) proof let x be Real; ::_thesis: ( x in Z implies ((r (#) arcsin) `| Z) . x = r / (sqrt (1 - (x ^2))) ) assume A4: x in Z ; ::_thesis: ((r (#) arcsin) `| Z) . x = r / (sqrt (1 - (x ^2))) then A5: ( - 1 < x & x < 1 ) by A1, XXREAL_1:4; ((r (#) arcsin) `| Z) . x = r * (diff (arcsin,x)) by A2, A3, A4, FDIFF_1:20 .= r * (1 / (sqrt (1 - (x ^2)))) by A5, SIN_COS6:83 .= r / (sqrt (1 - (x ^2))) by XCMPLX_1:99 ; hence ((r (#) arcsin) `| Z) . x = r / (sqrt (1 - (x ^2))) ; ::_thesis: verum end; hence ( r (#) arcsin is_differentiable_on Z & ( for x being Real st x in Z holds ((r (#) arcsin) `| Z) . x = r / (sqrt (1 - (x ^2))) ) ) by A2, A3, FDIFF_1:20; ::_thesis: verum end; theorem :: FDIFF_7:5 for r being Real for Z being open Subset of REAL st Z c= ].(- 1),1.[ & Z c= dom (r (#) arccos) holds ( r (#) arccos is_differentiable_on Z & ( for x being Real st x in Z holds ((r (#) arccos) `| Z) . x = - (r / (sqrt (1 - (x ^2)))) ) ) proof let r be Real; ::_thesis: for Z being open Subset of REAL st Z c= ].(- 1),1.[ & Z c= dom (r (#) arccos) holds ( r (#) arccos is_differentiable_on Z & ( for x being Real st x in Z holds ((r (#) arccos) `| Z) . x = - (r / (sqrt (1 - (x ^2)))) ) ) let Z be open Subset of REAL; ::_thesis: ( Z c= ].(- 1),1.[ & Z c= dom (r (#) arccos) implies ( r (#) arccos is_differentiable_on Z & ( for x being Real st x in Z holds ((r (#) arccos) `| Z) . x = - (r / (sqrt (1 - (x ^2)))) ) ) ) assume that A1: Z c= ].(- 1),1.[ and A2: Z c= dom (r (#) arccos) ; ::_thesis: ( r (#) arccos is_differentiable_on Z & ( for x being Real st x in Z holds ((r (#) arccos) `| Z) . x = - (r / (sqrt (1 - (x ^2)))) ) ) A3: arccos is_differentiable_on Z by A1, FDIFF_1:26, SIN_COS6:106; for x being Real st x in Z holds ((r (#) arccos) `| Z) . x = - (r / (sqrt (1 - (x ^2)))) proof let x be Real; ::_thesis: ( x in Z implies ((r (#) arccos) `| Z) . x = - (r / (sqrt (1 - (x ^2)))) ) assume A4: x in Z ; ::_thesis: ((r (#) arccos) `| Z) . x = - (r / (sqrt (1 - (x ^2)))) then A5: ( - 1 < x & x < 1 ) by A1, XXREAL_1:4; ((r (#) arccos) `| Z) . x = r * (diff (arccos,x)) by A2, A3, A4, FDIFF_1:20 .= r * (- (1 / (sqrt (1 - (x ^2))))) by A5, SIN_COS6:106 .= - (r * (1 / (sqrt (1 - (x ^2))))) .= - (r / (sqrt (1 - (x ^2)))) by XCMPLX_1:99 ; hence ((r (#) arccos) `| Z) . x = - (r / (sqrt (1 - (x ^2)))) ; ::_thesis: verum end; hence ( r (#) arccos is_differentiable_on Z & ( for x being Real st x in Z holds ((r (#) arccos) `| Z) . x = - (r / (sqrt (1 - (x ^2)))) ) ) by A2, A3, FDIFF_1:20; ::_thesis: verum end; theorem Th6: :: FDIFF_7:6 for x being Real for f being PartFunc of REAL,REAL st f is_differentiable_in x & f . x > - 1 & f . x < 1 holds ( arcsin * f is_differentiable_in x & diff ((arcsin * f),x) = (diff (f,x)) / (sqrt (1 - ((f . x) ^2))) ) proof let x be Real; ::_thesis: for f being PartFunc of REAL,REAL st f is_differentiable_in x & f . x > - 1 & f . x < 1 holds ( arcsin * f is_differentiable_in x & diff ((arcsin * f),x) = (diff (f,x)) / (sqrt (1 - ((f . x) ^2))) ) let f be PartFunc of REAL,REAL; ::_thesis: ( f is_differentiable_in x & f . x > - 1 & f . x < 1 implies ( arcsin * f is_differentiable_in x & diff ((arcsin * f),x) = (diff (f,x)) / (sqrt (1 - ((f . x) ^2))) ) ) assume that A1: f is_differentiable_in x and A2: ( f . x > - 1 & f . x < 1 ) ; ::_thesis: ( arcsin * f is_differentiable_in x & diff ((arcsin * f),x) = (diff (f,x)) / (sqrt (1 - ((f . x) ^2))) ) f . x in ].(- 1),1.[ by A2; then A3: arcsin is_differentiable_in f . x by FDIFF_1:9, SIN_COS6:83; then diff ((arcsin * f),x) = (diff (arcsin,(f . x))) * (diff (f,x)) by A1, FDIFF_2:13 .= (diff (f,x)) * (1 / (sqrt (1 - ((f . x) ^2)))) by A2, SIN_COS6:83 .= (diff (f,x)) / (sqrt (1 - ((f . x) ^2))) by XCMPLX_1:99 ; hence ( arcsin * f is_differentiable_in x & diff ((arcsin * f),x) = (diff (f,x)) / (sqrt (1 - ((f . x) ^2))) ) by A1, A3, FDIFF_2:13; ::_thesis: verum end; theorem Th7: :: FDIFF_7:7 for x being Real for f being PartFunc of REAL,REAL st f is_differentiable_in x & f . x > - 1 & f . x < 1 holds ( arccos * f is_differentiable_in x & diff ((arccos * f),x) = - ((diff (f,x)) / (sqrt (1 - ((f . x) ^2)))) ) proof let x be Real; ::_thesis: for f being PartFunc of REAL,REAL st f is_differentiable_in x & f . x > - 1 & f . x < 1 holds ( arccos * f is_differentiable_in x & diff ((arccos * f),x) = - ((diff (f,x)) / (sqrt (1 - ((f . x) ^2)))) ) let f be PartFunc of REAL,REAL; ::_thesis: ( f is_differentiable_in x & f . x > - 1 & f . x < 1 implies ( arccos * f is_differentiable_in x & diff ((arccos * f),x) = - ((diff (f,x)) / (sqrt (1 - ((f . x) ^2)))) ) ) assume that A1: f is_differentiable_in x and A2: ( f . x > - 1 & f . x < 1 ) ; ::_thesis: ( arccos * f is_differentiable_in x & diff ((arccos * f),x) = - ((diff (f,x)) / (sqrt (1 - ((f . x) ^2)))) ) f . x in ].(- 1),1.[ by A2; then A3: arccos is_differentiable_in f . x by FDIFF_1:9, SIN_COS6:106; then diff ((arccos * f),x) = (diff (arccos,(f . x))) * (diff (f,x)) by A1, FDIFF_2:13 .= (- (1 / (sqrt (1 - ((f . x) ^2))))) * (diff (f,x)) by A2, SIN_COS6:106 .= - ((diff (f,x)) * (1 / (sqrt (1 - ((f . x) ^2))))) .= - ((diff (f,x)) / (sqrt (1 - ((f . x) ^2)))) by XCMPLX_1:99 ; hence ( arccos * f is_differentiable_in x & diff ((arccos * f),x) = - ((diff (f,x)) / (sqrt (1 - ((f . x) ^2)))) ) by A1, A3, FDIFF_2:13; ::_thesis: verum end; theorem :: FDIFF_7:8 for Z being open Subset of REAL st Z c= dom (ln * arcsin) & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds arcsin . x > 0 ) holds ( ln * arcsin is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * arcsin) `| Z) . x = 1 / ((sqrt (1 - (x ^2))) * (arcsin . x)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (ln * arcsin) & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds arcsin . x > 0 ) implies ( ln * arcsin is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * arcsin) `| Z) . x = 1 / ((sqrt (1 - (x ^2))) * (arcsin . x)) ) ) ) assume that A1: Z c= dom (ln * arcsin) and A2: Z c= ].(- 1),1.[ and A3: for x being Real st x in Z holds arcsin . x > 0 ; ::_thesis: ( ln * arcsin is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * arcsin) `| Z) . x = 1 / ((sqrt (1 - (x ^2))) * (arcsin . x)) ) ) A4: for x being Real st x in Z holds ln * arcsin is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies ln * arcsin is_differentiable_in x ) assume x in Z ; ::_thesis: ln * arcsin is_differentiable_in x then ( arcsin is_differentiable_in x & arcsin . x > 0 ) by A2, A3, FDIFF_1:9, SIN_COS6:83; hence ln * arcsin is_differentiable_in x by TAYLOR_1:20; ::_thesis: verum end; then A5: ln * arcsin is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((ln * arcsin) `| Z) . x = 1 / ((sqrt (1 - (x ^2))) * (arcsin . x)) proof let x be Real; ::_thesis: ( x in Z implies ((ln * arcsin) `| Z) . x = 1 / ((sqrt (1 - (x ^2))) * (arcsin . x)) ) assume A6: x in Z ; ::_thesis: ((ln * arcsin) `| Z) . x = 1 / ((sqrt (1 - (x ^2))) * (arcsin . x)) then A7: ( - 1 < x & x < 1 ) by A2, XXREAL_1:4; ( arcsin is_differentiable_in x & arcsin . x > 0 ) by A2, A3, A6, FDIFF_1:9, SIN_COS6:83; then diff ((ln * arcsin),x) = (diff (arcsin,x)) / (arcsin . x) by TAYLOR_1:20 .= (1 / (sqrt (1 - (x ^2)))) / (arcsin . x) by A7, SIN_COS6:83 .= 1 / ((sqrt (1 - (x ^2))) * (arcsin . x)) by XCMPLX_1:78 ; hence ((ln * arcsin) `| Z) . x = 1 / ((sqrt (1 - (x ^2))) * (arcsin . x)) by A5, A6, FDIFF_1:def_7; ::_thesis: verum end; hence ( ln * arcsin is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * arcsin) `| Z) . x = 1 / ((sqrt (1 - (x ^2))) * (arcsin . x)) ) ) by A1, A4, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_7:9 for Z being open Subset of REAL st Z c= dom (ln * arccos) & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds arccos . x > 0 ) holds ( ln * arccos is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * arccos) `| Z) . x = - (1 / ((sqrt (1 - (x ^2))) * (arccos . x))) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (ln * arccos) & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds arccos . x > 0 ) implies ( ln * arccos is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * arccos) `| Z) . x = - (1 / ((sqrt (1 - (x ^2))) * (arccos . x))) ) ) ) assume that A1: Z c= dom (ln * arccos) and A2: Z c= ].(- 1),1.[ and A3: for x being Real st x in Z holds arccos . x > 0 ; ::_thesis: ( ln * arccos is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * arccos) `| Z) . x = - (1 / ((sqrt (1 - (x ^2))) * (arccos . x))) ) ) A4: for x being Real st x in Z holds ln * arccos is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies ln * arccos is_differentiable_in x ) assume x in Z ; ::_thesis: ln * arccos is_differentiable_in x then ( arccos is_differentiable_in x & arccos . x > 0 ) by A2, A3, FDIFF_1:9, SIN_COS6:106; hence ln * arccos is_differentiable_in x by TAYLOR_1:20; ::_thesis: verum end; then A5: ln * arccos is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((ln * arccos) `| Z) . x = - (1 / ((sqrt (1 - (x ^2))) * (arccos . x))) proof let x be Real; ::_thesis: ( x in Z implies ((ln * arccos) `| Z) . x = - (1 / ((sqrt (1 - (x ^2))) * (arccos . x))) ) assume A6: x in Z ; ::_thesis: ((ln * arccos) `| Z) . x = - (1 / ((sqrt (1 - (x ^2))) * (arccos . x))) then A7: ( - 1 < x & x < 1 ) by A2, XXREAL_1:4; ( arccos is_differentiable_in x & arccos . x > 0 ) by A2, A3, A6, FDIFF_1:9, SIN_COS6:106; then diff ((ln * arccos),x) = (diff (arccos,x)) / (arccos . x) by TAYLOR_1:20 .= (- (1 / (sqrt (1 - (x ^2))))) / (arccos . x) by A7, SIN_COS6:106 .= - ((1 / (sqrt (1 - (x ^2)))) / (arccos . x)) by XCMPLX_1:187 .= - (1 / ((sqrt (1 - (x ^2))) * (arccos . x))) by XCMPLX_1:78 ; hence ((ln * arccos) `| Z) . x = - (1 / ((sqrt (1 - (x ^2))) * (arccos . x))) by A5, A6, FDIFF_1:def_7; ::_thesis: verum end; hence ( ln * arccos is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * arccos) `| Z) . x = - (1 / ((sqrt (1 - (x ^2))) * (arccos . x))) ) ) by A1, A4, FDIFF_1:9; ::_thesis: verum end; theorem Th10: :: FDIFF_7:10 for n being Element of NAT for Z being open Subset of REAL st Z c= dom ((#Z n) * arcsin) & Z c= ].(- 1),1.[ holds ( (#Z n) * arcsin is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z n) * arcsin) `| Z) . x = (n * ((arcsin . x) #Z (n - 1))) / (sqrt (1 - (x ^2))) ) ) proof let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL st Z c= dom ((#Z n) * arcsin) & Z c= ].(- 1),1.[ holds ( (#Z n) * arcsin is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z n) * arcsin) `| Z) . x = (n * ((arcsin . x) #Z (n - 1))) / (sqrt (1 - (x ^2))) ) ) let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((#Z n) * arcsin) & Z c= ].(- 1),1.[ implies ( (#Z n) * arcsin is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z n) * arcsin) `| Z) . x = (n * ((arcsin . x) #Z (n - 1))) / (sqrt (1 - (x ^2))) ) ) ) assume that A1: Z c= dom ((#Z n) * arcsin) and A2: Z c= ].(- 1),1.[ ; ::_thesis: ( (#Z n) * arcsin is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z n) * arcsin) `| Z) . x = (n * ((arcsin . x) #Z (n - 1))) / (sqrt (1 - (x ^2))) ) ) A3: for x being Real st x in Z holds (#Z n) * arcsin is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies (#Z n) * arcsin is_differentiable_in x ) assume x in Z ; ::_thesis: (#Z n) * arcsin is_differentiable_in x then arcsin is_differentiable_in x by A2, FDIFF_1:9, SIN_COS6:83; hence (#Z n) * arcsin is_differentiable_in x by TAYLOR_1:3; ::_thesis: verum end; then A4: (#Z n) * arcsin is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds (((#Z n) * arcsin) `| Z) . x = (n * ((arcsin . x) #Z (n - 1))) / (sqrt (1 - (x ^2))) proof let x be Real; ::_thesis: ( x in Z implies (((#Z n) * arcsin) `| Z) . x = (n * ((arcsin . x) #Z (n - 1))) / (sqrt (1 - (x ^2))) ) assume A5: x in Z ; ::_thesis: (((#Z n) * arcsin) `| Z) . x = (n * ((arcsin . x) #Z (n - 1))) / (sqrt (1 - (x ^2))) then A6: ( - 1 < x & x < 1 ) by A2, XXREAL_1:4; A7: arcsin is_differentiable_in x by A2, A5, FDIFF_1:9, SIN_COS6:83; (((#Z n) * arcsin) `| Z) . x = diff (((#Z n) * arcsin),x) by A4, A5, FDIFF_1:def_7 .= (n * ((arcsin . x) #Z (n - 1))) * (diff (arcsin,x)) by A7, TAYLOR_1:3 .= (n * ((arcsin . x) #Z (n - 1))) * (1 / (sqrt (1 - (x ^2)))) by A6, SIN_COS6:83 .= (n * ((arcsin . x) #Z (n - 1))) / (sqrt (1 - (x ^2))) by XCMPLX_1:99 ; hence (((#Z n) * arcsin) `| Z) . x = (n * ((arcsin . x) #Z (n - 1))) / (sqrt (1 - (x ^2))) ; ::_thesis: verum end; hence ( (#Z n) * arcsin is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z n) * arcsin) `| Z) . x = (n * ((arcsin . x) #Z (n - 1))) / (sqrt (1 - (x ^2))) ) ) by A1, A3, FDIFF_1:9; ::_thesis: verum end; theorem Th11: :: FDIFF_7:11 for n being Element of NAT for Z being open Subset of REAL st Z c= dom ((#Z n) * arccos) & Z c= ].(- 1),1.[ holds ( (#Z n) * arccos is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z n) * arccos) `| Z) . x = - ((n * ((arccos . x) #Z (n - 1))) / (sqrt (1 - (x ^2)))) ) ) proof let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL st Z c= dom ((#Z n) * arccos) & Z c= ].(- 1),1.[ holds ( (#Z n) * arccos is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z n) * arccos) `| Z) . x = - ((n * ((arccos . x) #Z (n - 1))) / (sqrt (1 - (x ^2)))) ) ) let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((#Z n) * arccos) & Z c= ].(- 1),1.[ implies ( (#Z n) * arccos is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z n) * arccos) `| Z) . x = - ((n * ((arccos . x) #Z (n - 1))) / (sqrt (1 - (x ^2)))) ) ) ) assume that A1: Z c= dom ((#Z n) * arccos) and A2: Z c= ].(- 1),1.[ ; ::_thesis: ( (#Z n) * arccos is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z n) * arccos) `| Z) . x = - ((n * ((arccos . x) #Z (n - 1))) / (sqrt (1 - (x ^2)))) ) ) A3: for x being Real st x in Z holds (#Z n) * arccos is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies (#Z n) * arccos is_differentiable_in x ) assume x in Z ; ::_thesis: (#Z n) * arccos is_differentiable_in x then arccos is_differentiable_in x by A2, FDIFF_1:9, SIN_COS6:106; hence (#Z n) * arccos is_differentiable_in x by TAYLOR_1:3; ::_thesis: verum end; then A4: (#Z n) * arccos is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds (((#Z n) * arccos) `| Z) . x = - ((n * ((arccos . x) #Z (n - 1))) / (sqrt (1 - (x ^2)))) proof let x be Real; ::_thesis: ( x in Z implies (((#Z n) * arccos) `| Z) . x = - ((n * ((arccos . x) #Z (n - 1))) / (sqrt (1 - (x ^2)))) ) assume A5: x in Z ; ::_thesis: (((#Z n) * arccos) `| Z) . x = - ((n * ((arccos . x) #Z (n - 1))) / (sqrt (1 - (x ^2)))) then A6: ( - 1 < x & x < 1 ) by A2, XXREAL_1:4; A7: arccos is_differentiable_in x by A2, A5, FDIFF_1:9, SIN_COS6:106; (((#Z n) * arccos) `| Z) . x = diff (((#Z n) * arccos),x) by A4, A5, FDIFF_1:def_7 .= (n * ((arccos . x) #Z (n - 1))) * (diff (arccos,x)) by A7, TAYLOR_1:3 .= (n * ((arccos . x) #Z (n - 1))) * (- (1 / (sqrt (1 - (x ^2))))) by A6, SIN_COS6:106 .= - ((n * ((arccos . x) #Z (n - 1))) * (1 / (sqrt (1 - (x ^2))))) .= - ((n * ((arccos . x) #Z (n - 1))) / (sqrt (1 - (x ^2)))) by XCMPLX_1:99 ; hence (((#Z n) * arccos) `| Z) . x = - ((n * ((arccos . x) #Z (n - 1))) / (sqrt (1 - (x ^2)))) ; ::_thesis: verum end; hence ( (#Z n) * arccos is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z n) * arccos) `| Z) . x = - ((n * ((arccos . x) #Z (n - 1))) / (sqrt (1 - (x ^2)))) ) ) by A1, A3, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_7:12 for Z being open Subset of REAL st Z c= dom ((1 / 2) (#) ((#Z 2) * arcsin)) & Z c= ].(- 1),1.[ holds ( (1 / 2) (#) ((#Z 2) * arcsin) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) ((#Z 2) * arcsin)) `| Z) . x = (arcsin . x) / (sqrt (1 - (x ^2))) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((1 / 2) (#) ((#Z 2) * arcsin)) & Z c= ].(- 1),1.[ implies ( (1 / 2) (#) ((#Z 2) * arcsin) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) ((#Z 2) * arcsin)) `| Z) . x = (arcsin . x) / (sqrt (1 - (x ^2))) ) ) ) assume that A1: Z c= dom ((1 / 2) (#) ((#Z 2) * arcsin)) and A2: Z c= ].(- 1),1.[ ; ::_thesis: ( (1 / 2) (#) ((#Z 2) * arcsin) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) ((#Z 2) * arcsin)) `| Z) . x = (arcsin . x) / (sqrt (1 - (x ^2))) ) ) A3: Z c= dom ((#Z 2) * arcsin) by A1, VALUED_1:def_5; then A4: (#Z 2) * arcsin is_differentiable_on Z by A2, Th10; for x being Real st x in Z holds (((1 / 2) (#) ((#Z 2) * arcsin)) `| Z) . x = (arcsin . x) / (sqrt (1 - (x ^2))) proof let x be Real; ::_thesis: ( x in Z implies (((1 / 2) (#) ((#Z 2) * arcsin)) `| Z) . x = (arcsin . x) / (sqrt (1 - (x ^2))) ) assume A5: x in Z ; ::_thesis: (((1 / 2) (#) ((#Z 2) * arcsin)) `| Z) . x = (arcsin . x) / (sqrt (1 - (x ^2))) then (((1 / 2) (#) ((#Z 2) * arcsin)) `| Z) . x = (1 / 2) * (diff (((#Z 2) * arcsin),x)) by A1, A4, FDIFF_1:20 .= (1 / 2) * ((((#Z 2) * arcsin) `| Z) . x) by A4, A5, FDIFF_1:def_7 .= (1 / 2) * ((2 * ((arcsin . x) #Z (2 - 1))) / (sqrt (1 - (x ^2)))) by A2, A3, A5, Th10 .= ((1 / 2) * (2 * ((arcsin . x) #Z (2 - 1)))) / (sqrt (1 - (x ^2))) by XCMPLX_1:74 .= (arcsin . x) / (sqrt (1 - (x ^2))) by PREPOWER:35 ; hence (((1 / 2) (#) ((#Z 2) * arcsin)) `| Z) . x = (arcsin . x) / (sqrt (1 - (x ^2))) ; ::_thesis: verum end; hence ( (1 / 2) (#) ((#Z 2) * arcsin) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) ((#Z 2) * arcsin)) `| Z) . x = (arcsin . x) / (sqrt (1 - (x ^2))) ) ) by A1, A4, FDIFF_1:20; ::_thesis: verum end; theorem :: FDIFF_7:13 for Z being open Subset of REAL st Z c= dom ((1 / 2) (#) ((#Z 2) * arccos)) & Z c= ].(- 1),1.[ holds ( (1 / 2) (#) ((#Z 2) * arccos) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) ((#Z 2) * arccos)) `| Z) . x = - ((arccos . x) / (sqrt (1 - (x ^2)))) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((1 / 2) (#) ((#Z 2) * arccos)) & Z c= ].(- 1),1.[ implies ( (1 / 2) (#) ((#Z 2) * arccos) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) ((#Z 2) * arccos)) `| Z) . x = - ((arccos . x) / (sqrt (1 - (x ^2)))) ) ) ) assume that A1: Z c= dom ((1 / 2) (#) ((#Z 2) * arccos)) and A2: Z c= ].(- 1),1.[ ; ::_thesis: ( (1 / 2) (#) ((#Z 2) * arccos) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) ((#Z 2) * arccos)) `| Z) . x = - ((arccos . x) / (sqrt (1 - (x ^2)))) ) ) A3: Z c= dom ((#Z 2) * arccos) by A1, VALUED_1:def_5; then A4: (#Z 2) * arccos is_differentiable_on Z by A2, Th11; for x being Real st x in Z holds (((1 / 2) (#) ((#Z 2) * arccos)) `| Z) . x = - ((arccos . x) / (sqrt (1 - (x ^2)))) proof let x be Real; ::_thesis: ( x in Z implies (((1 / 2) (#) ((#Z 2) * arccos)) `| Z) . x = - ((arccos . x) / (sqrt (1 - (x ^2)))) ) assume A5: x in Z ; ::_thesis: (((1 / 2) (#) ((#Z 2) * arccos)) `| Z) . x = - ((arccos . x) / (sqrt (1 - (x ^2)))) then (((1 / 2) (#) ((#Z 2) * arccos)) `| Z) . x = (1 / 2) * (diff (((#Z 2) * arccos),x)) by A1, A4, FDIFF_1:20 .= (1 / 2) * ((((#Z 2) * arccos) `| Z) . x) by A4, A5, FDIFF_1:def_7 .= (1 / 2) * (- ((2 * ((arccos . x) #Z (2 - 1))) / (sqrt (1 - (x ^2))))) by A2, A3, A5, Th11 .= - ((1 / 2) * ((2 * ((arccos . x) #Z (2 - 1))) / (sqrt (1 - (x ^2))))) .= - (((1 / 2) * (2 * ((arccos . x) #Z (2 - 1)))) / (sqrt (1 - (x ^2)))) by XCMPLX_1:74 .= - ((arccos . x) / (sqrt (1 - (x ^2)))) by PREPOWER:35 ; hence (((1 / 2) (#) ((#Z 2) * arccos)) `| Z) . x = - ((arccos . x) / (sqrt (1 - (x ^2)))) ; ::_thesis: verum end; hence ( (1 / 2) (#) ((#Z 2) * arccos) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) ((#Z 2) * arccos)) `| Z) . x = - ((arccos . x) / (sqrt (1 - (x ^2)))) ) ) by A1, A4, FDIFF_1:20; ::_thesis: verum end; theorem Th14: :: FDIFF_7:14 for a, b being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (arcsin * f) & ( for x being Real st x in Z holds ( f . x = (a * x) + b & f . x > - 1 & f . x < 1 ) ) holds ( arcsin * f is_differentiable_on Z & ( for x being Real st x in Z holds ((arcsin * f) `| Z) . x = a / (sqrt (1 - (((a * x) + b) ^2))) ) ) proof let a, b be Real; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (arcsin * f) & ( for x being Real st x in Z holds ( f . x = (a * x) + b & f . x > - 1 & f . x < 1 ) ) holds ( arcsin * f is_differentiable_on Z & ( for x being Real st x in Z holds ((arcsin * f) `| Z) . x = a / (sqrt (1 - (((a * x) + b) ^2))) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom (arcsin * f) & ( for x being Real st x in Z holds ( f . x = (a * x) + b & f . x > - 1 & f . x < 1 ) ) holds ( arcsin * f is_differentiable_on Z & ( for x being Real st x in Z holds ((arcsin * f) `| Z) . x = a / (sqrt (1 - (((a * x) + b) ^2))) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (arcsin * f) & ( for x being Real st x in Z holds ( f . x = (a * x) + b & f . x > - 1 & f . x < 1 ) ) implies ( arcsin * f is_differentiable_on Z & ( for x being Real st x in Z holds ((arcsin * f) `| Z) . x = a / (sqrt (1 - (((a * x) + b) ^2))) ) ) ) assume that A1: Z c= dom (arcsin * f) and A2: for x being Real st x in Z holds ( f . x = (a * x) + b & f . x > - 1 & f . x < 1 ) ; ::_thesis: ( arcsin * f is_differentiable_on Z & ( for x being Real st x in Z holds ((arcsin * f) `| Z) . x = a / (sqrt (1 - (((a * x) + b) ^2))) ) ) for y being set st y in Z holds y in dom f by A1, FUNCT_1:11; then A3: Z c= dom f by TARSKI:def_3; A4: for x being Real st x in Z holds f . x = (a * x) + b by A2; then A5: f is_differentiable_on Z by A3, FDIFF_1:23; A6: for x being Real st x in Z holds arcsin * f is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies arcsin * f is_differentiable_in x ) assume A7: x in Z ; ::_thesis: arcsin * f is_differentiable_in x then A8: f . x < 1 by A2; ( f is_differentiable_in x & f . x > - 1 ) by A2, A5, A7, FDIFF_1:9; hence arcsin * f is_differentiable_in x by A8, Th6; ::_thesis: verum end; then A9: arcsin * f is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((arcsin * f) `| Z) . x = a / (sqrt (1 - (((a * x) + b) ^2))) proof let x be Real; ::_thesis: ( x in Z implies ((arcsin * f) `| Z) . x = a / (sqrt (1 - (((a * x) + b) ^2))) ) assume A10: x in Z ; ::_thesis: ((arcsin * f) `| Z) . x = a / (sqrt (1 - (((a * x) + b) ^2))) then A11: f . x < 1 by A2; ( f is_differentiable_in x & f . x > - 1 ) by A2, A5, A10, FDIFF_1:9; then diff ((arcsin * f),x) = (diff (f,x)) / (sqrt (1 - ((f . x) ^2))) by A11, Th6 .= ((f `| Z) . x) / (sqrt (1 - ((f . x) ^2))) by A5, A10, FDIFF_1:def_7 .= a / (sqrt (1 - ((f . x) ^2))) by A4, A3, A10, FDIFF_1:23 .= a / (sqrt (1 - (((a * x) + b) ^2))) by A2, A10 ; hence ((arcsin * f) `| Z) . x = a / (sqrt (1 - (((a * x) + b) ^2))) by A9, A10, FDIFF_1:def_7; ::_thesis: verum end; hence ( arcsin * f is_differentiable_on Z & ( for x being Real st x in Z holds ((arcsin * f) `| Z) . x = a / (sqrt (1 - (((a * x) + b) ^2))) ) ) by A1, A6, FDIFF_1:9; ::_thesis: verum end; theorem Th15: :: FDIFF_7:15 for a, b being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (arccos * f) & ( for x being Real st x in Z holds ( f . x = (a * x) + b & f . x > - 1 & f . x < 1 ) ) holds ( arccos * f is_differentiable_on Z & ( for x being Real st x in Z holds ((arccos * f) `| Z) . x = - (a / (sqrt (1 - (((a * x) + b) ^2)))) ) ) proof let a, b be Real; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (arccos * f) & ( for x being Real st x in Z holds ( f . x = (a * x) + b & f . x > - 1 & f . x < 1 ) ) holds ( arccos * f is_differentiable_on Z & ( for x being Real st x in Z holds ((arccos * f) `| Z) . x = - (a / (sqrt (1 - (((a * x) + b) ^2)))) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom (arccos * f) & ( for x being Real st x in Z holds ( f . x = (a * x) + b & f . x > - 1 & f . x < 1 ) ) holds ( arccos * f is_differentiable_on Z & ( for x being Real st x in Z holds ((arccos * f) `| Z) . x = - (a / (sqrt (1 - (((a * x) + b) ^2)))) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (arccos * f) & ( for x being Real st x in Z holds ( f . x = (a * x) + b & f . x > - 1 & f . x < 1 ) ) implies ( arccos * f is_differentiable_on Z & ( for x being Real st x in Z holds ((arccos * f) `| Z) . x = - (a / (sqrt (1 - (((a * x) + b) ^2)))) ) ) ) assume that A1: Z c= dom (arccos * f) and A2: for x being Real st x in Z holds ( f . x = (a * x) + b & f . x > - 1 & f . x < 1 ) ; ::_thesis: ( arccos * f is_differentiable_on Z & ( for x being Real st x in Z holds ((arccos * f) `| Z) . x = - (a / (sqrt (1 - (((a * x) + b) ^2)))) ) ) for y being set st y in Z holds y in dom f by A1, FUNCT_1:11; then A3: Z c= dom f by TARSKI:def_3; A4: for x being Real st x in Z holds f . x = (a * x) + b by A2; then A5: f is_differentiable_on Z by A3, FDIFF_1:23; A6: for x being Real st x in Z holds arccos * f is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies arccos * f is_differentiable_in x ) assume A7: x in Z ; ::_thesis: arccos * f is_differentiable_in x then A8: f . x < 1 by A2; ( f is_differentiable_in x & f . x > - 1 ) by A2, A5, A7, FDIFF_1:9; hence arccos * f is_differentiable_in x by A8, Th7; ::_thesis: verum end; then A9: arccos * f is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((arccos * f) `| Z) . x = - (a / (sqrt (1 - (((a * x) + b) ^2)))) proof let x be Real; ::_thesis: ( x in Z implies ((arccos * f) `| Z) . x = - (a / (sqrt (1 - (((a * x) + b) ^2)))) ) assume A10: x in Z ; ::_thesis: ((arccos * f) `| Z) . x = - (a / (sqrt (1 - (((a * x) + b) ^2)))) then A11: f . x < 1 by A2; ( f is_differentiable_in x & f . x > - 1 ) by A2, A5, A10, FDIFF_1:9; then diff ((arccos * f),x) = - ((diff (f,x)) / (sqrt (1 - ((f . x) ^2)))) by A11, Th7 .= - (((f `| Z) . x) / (sqrt (1 - ((f . x) ^2)))) by A5, A10, FDIFF_1:def_7 .= - (a / (sqrt (1 - ((f . x) ^2)))) by A4, A3, A10, FDIFF_1:23 .= - (a / (sqrt (1 - (((a * x) + b) ^2)))) by A2, A10 ; hence ((arccos * f) `| Z) . x = - (a / (sqrt (1 - (((a * x) + b) ^2)))) by A9, A10, FDIFF_1:def_7; ::_thesis: verum end; hence ( arccos * f is_differentiable_on Z & ( for x being Real st x in Z holds ((arccos * f) `| Z) . x = - (a / (sqrt (1 - (((a * x) + b) ^2)))) ) ) by A1, A6, FDIFF_1:9; ::_thesis: verum end; theorem Th16: :: FDIFF_7:16 for Z being open Subset of REAL st Z c= dom ((id Z) (#) arcsin) & Z c= ].(- 1),1.[ holds ( (id Z) (#) arcsin is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) arcsin) `| Z) . x = (arcsin . x) + (x / (sqrt (1 - (x ^2)))) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((id Z) (#) arcsin) & Z c= ].(- 1),1.[ implies ( (id Z) (#) arcsin is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) arcsin) `| Z) . x = (arcsin . x) + (x / (sqrt (1 - (x ^2)))) ) ) ) assume that A1: Z c= dom ((id Z) (#) arcsin) and A2: Z c= ].(- 1),1.[ ; ::_thesis: ( (id Z) (#) arcsin is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) arcsin) `| Z) . x = (arcsin . x) + (x / (sqrt (1 - (x ^2)))) ) ) A3: for x being Real st x in Z holds (id Z) . x = (1 * x) + 0 by FUNCT_1:18; Z c= (dom (id Z)) /\ (dom arcsin) by A1, VALUED_1:def_4; then A4: Z c= dom (id Z) by XBOOLE_1:18; then A5: id Z is_differentiable_on Z by A3, FDIFF_1:23; A6: arcsin is_differentiable_on Z by A2, FDIFF_1:26, SIN_COS6:83; for x being Real st x in Z holds (((id Z) (#) arcsin) `| Z) . x = (arcsin . x) + (x / (sqrt (1 - (x ^2)))) proof let x be Real; ::_thesis: ( x in Z implies (((id Z) (#) arcsin) `| Z) . x = (arcsin . x) + (x / (sqrt (1 - (x ^2)))) ) assume A7: x in Z ; ::_thesis: (((id Z) (#) arcsin) `| Z) . x = (arcsin . x) + (x / (sqrt (1 - (x ^2)))) then A8: ( - 1 < x & x < 1 ) by A2, XXREAL_1:4; (((id Z) (#) arcsin) `| Z) . x = ((arcsin . x) * (diff ((id Z),x))) + (((id Z) . x) * (diff (arcsin,x))) by A1, A5, A6, A7, FDIFF_1:21 .= ((arcsin . x) * (((id Z) `| Z) . x)) + (((id Z) . x) * (diff (arcsin,x))) by A5, A7, FDIFF_1:def_7 .= ((arcsin . x) * 1) + (((id Z) . x) * (diff (arcsin,x))) by A4, A3, A7, FDIFF_1:23 .= ((arcsin . x) * 1) + (((id Z) . x) * (1 / (sqrt (1 - (x ^2))))) by A8, SIN_COS6:83 .= (arcsin . x) + (x * (1 / (sqrt (1 - (x ^2))))) by A7, FUNCT_1:18 .= (arcsin . x) + (x / (sqrt (1 - (x ^2)))) by XCMPLX_1:99 ; hence (((id Z) (#) arcsin) `| Z) . x = (arcsin . x) + (x / (sqrt (1 - (x ^2)))) ; ::_thesis: verum end; hence ( (id Z) (#) arcsin is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) arcsin) `| Z) . x = (arcsin . x) + (x / (sqrt (1 - (x ^2)))) ) ) by A1, A5, A6, FDIFF_1:21; ::_thesis: verum end; theorem Th17: :: FDIFF_7:17 for Z being open Subset of REAL st Z c= dom ((id Z) (#) arccos) & Z c= ].(- 1),1.[ holds ( (id Z) (#) arccos is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) arccos) `| Z) . x = (arccos . x) - (x / (sqrt (1 - (x ^2)))) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((id Z) (#) arccos) & Z c= ].(- 1),1.[ implies ( (id Z) (#) arccos is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) arccos) `| Z) . x = (arccos . x) - (x / (sqrt (1 - (x ^2)))) ) ) ) assume that A1: Z c= dom ((id Z) (#) arccos) and A2: Z c= ].(- 1),1.[ ; ::_thesis: ( (id Z) (#) arccos is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) arccos) `| Z) . x = (arccos . x) - (x / (sqrt (1 - (x ^2)))) ) ) A3: for x being Real st x in Z holds (id Z) . x = (1 * x) + 0 by FUNCT_1:18; Z c= (dom (id Z)) /\ (dom arccos) by A1, VALUED_1:def_4; then A4: Z c= dom (id Z) by XBOOLE_1:18; then A5: id Z is_differentiable_on Z by A3, FDIFF_1:23; A6: arccos is_differentiable_on Z by A2, FDIFF_1:26, SIN_COS6:106; for x being Real st x in Z holds (((id Z) (#) arccos) `| Z) . x = (arccos . x) - (x / (sqrt (1 - (x ^2)))) proof let x be Real; ::_thesis: ( x in Z implies (((id Z) (#) arccos) `| Z) . x = (arccos . x) - (x / (sqrt (1 - (x ^2)))) ) assume A7: x in Z ; ::_thesis: (((id Z) (#) arccos) `| Z) . x = (arccos . x) - (x / (sqrt (1 - (x ^2)))) then A8: ( - 1 < x & x < 1 ) by A2, XXREAL_1:4; (((id Z) (#) arccos) `| Z) . x = ((arccos . x) * (diff ((id Z),x))) + (((id Z) . x) * (diff (arccos,x))) by A1, A5, A6, A7, FDIFF_1:21 .= ((arccos . x) * (((id Z) `| Z) . x)) + (((id Z) . x) * (diff (arccos,x))) by A5, A7, FDIFF_1:def_7 .= ((arccos . x) * 1) + (((id Z) . x) * (diff (arccos,x))) by A4, A3, A7, FDIFF_1:23 .= ((arccos . x) * 1) + (((id Z) . x) * (- (1 / (sqrt (1 - (x ^2)))))) by A8, SIN_COS6:106 .= (arccos . x) + (x * (- (1 / (sqrt (1 - (x ^2)))))) by A7, FUNCT_1:18 .= (arccos . x) - (x * (1 / (sqrt (1 - (x ^2))))) .= (arccos . x) - (x / (sqrt (1 - (x ^2)))) by XCMPLX_1:99 ; hence (((id Z) (#) arccos) `| Z) . x = (arccos . x) - (x / (sqrt (1 - (x ^2)))) ; ::_thesis: verum end; hence ( (id Z) (#) arccos is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) arccos) `| Z) . x = (arccos . x) - (x / (sqrt (1 - (x ^2)))) ) ) by A1, A5, A6, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_7:18 for a, b being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (f (#) arcsin) & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds f . x = (a * x) + b ) holds ( f (#) arcsin is_differentiable_on Z & ( for x being Real st x in Z holds ((f (#) arcsin) `| Z) . x = (a * (arcsin . x)) + (((a * x) + b) / (sqrt (1 - (x ^2)))) ) ) proof let a, b be Real; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (f (#) arcsin) & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds f . x = (a * x) + b ) holds ( f (#) arcsin is_differentiable_on Z & ( for x being Real st x in Z holds ((f (#) arcsin) `| Z) . x = (a * (arcsin . x)) + (((a * x) + b) / (sqrt (1 - (x ^2)))) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom (f (#) arcsin) & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds f . x = (a * x) + b ) holds ( f (#) arcsin is_differentiable_on Z & ( for x being Real st x in Z holds ((f (#) arcsin) `| Z) . x = (a * (arcsin . x)) + (((a * x) + b) / (sqrt (1 - (x ^2)))) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (f (#) arcsin) & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds f . x = (a * x) + b ) implies ( f (#) arcsin is_differentiable_on Z & ( for x being Real st x in Z holds ((f (#) arcsin) `| Z) . x = (a * (arcsin . x)) + (((a * x) + b) / (sqrt (1 - (x ^2)))) ) ) ) assume that A1: Z c= dom (f (#) arcsin) and A2: Z c= ].(- 1),1.[ and A3: for x being Real st x in Z holds f . x = (a * x) + b ; ::_thesis: ( f (#) arcsin is_differentiable_on Z & ( for x being Real st x in Z holds ((f (#) arcsin) `| Z) . x = (a * (arcsin . x)) + (((a * x) + b) / (sqrt (1 - (x ^2)))) ) ) Z c= (dom f) /\ (dom arcsin) by A1, VALUED_1:def_4; then A4: Z c= dom f by XBOOLE_1:18; then A5: f is_differentiable_on Z by A3, FDIFF_1:23; A6: arcsin is_differentiable_on Z by A2, FDIFF_1:26, SIN_COS6:83; for x being Real st x in Z holds ((f (#) arcsin) `| Z) . x = (a * (arcsin . x)) + (((a * x) + b) / (sqrt (1 - (x ^2)))) proof let x be Real; ::_thesis: ( x in Z implies ((f (#) arcsin) `| Z) . x = (a * (arcsin . x)) + (((a * x) + b) / (sqrt (1 - (x ^2)))) ) assume A7: x in Z ; ::_thesis: ((f (#) arcsin) `| Z) . x = (a * (arcsin . x)) + (((a * x) + b) / (sqrt (1 - (x ^2)))) then A8: ( - 1 < x & x < 1 ) by A2, XXREAL_1:4; ((f (#) arcsin) `| Z) . x = ((arcsin . x) * (diff (f,x))) + ((f . x) * (diff (arcsin,x))) by A1, A5, A6, A7, FDIFF_1:21 .= ((arcsin . x) * ((f `| Z) . x)) + ((f . x) * (diff (arcsin,x))) by A5, A7, FDIFF_1:def_7 .= ((arcsin . x) * a) + ((f . x) * (diff (arcsin,x))) by A3, A4, A7, FDIFF_1:23 .= ((arcsin . x) * a) + ((f . x) * (1 / (sqrt (1 - (x ^2))))) by A8, SIN_COS6:83 .= (a * (arcsin . x)) + (((a * x) + b) * (1 / (sqrt (1 - (x ^2))))) by A3, A7 .= (a * (arcsin . x)) + (((a * x) + b) / (sqrt (1 - (x ^2)))) by XCMPLX_1:99 ; hence ((f (#) arcsin) `| Z) . x = (a * (arcsin . x)) + (((a * x) + b) / (sqrt (1 - (x ^2)))) ; ::_thesis: verum end; hence ( f (#) arcsin is_differentiable_on Z & ( for x being Real st x in Z holds ((f (#) arcsin) `| Z) . x = (a * (arcsin . x)) + (((a * x) + b) / (sqrt (1 - (x ^2)))) ) ) by A1, A5, A6, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_7:19 for a, b being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (f (#) arccos) & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds f . x = (a * x) + b ) holds ( f (#) arccos is_differentiable_on Z & ( for x being Real st x in Z holds ((f (#) arccos) `| Z) . x = (a * (arccos . x)) - (((a * x) + b) / (sqrt (1 - (x ^2)))) ) ) proof let a, b be Real; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (f (#) arccos) & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds f . x = (a * x) + b ) holds ( f (#) arccos is_differentiable_on Z & ( for x being Real st x in Z holds ((f (#) arccos) `| Z) . x = (a * (arccos . x)) - (((a * x) + b) / (sqrt (1 - (x ^2)))) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom (f (#) arccos) & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds f . x = (a * x) + b ) holds ( f (#) arccos is_differentiable_on Z & ( for x being Real st x in Z holds ((f (#) arccos) `| Z) . x = (a * (arccos . x)) - (((a * x) + b) / (sqrt (1 - (x ^2)))) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (f (#) arccos) & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds f . x = (a * x) + b ) implies ( f (#) arccos is_differentiable_on Z & ( for x being Real st x in Z holds ((f (#) arccos) `| Z) . x = (a * (arccos . x)) - (((a * x) + b) / (sqrt (1 - (x ^2)))) ) ) ) assume that A1: Z c= dom (f (#) arccos) and A2: Z c= ].(- 1),1.[ and A3: for x being Real st x in Z holds f . x = (a * x) + b ; ::_thesis: ( f (#) arccos is_differentiable_on Z & ( for x being Real st x in Z holds ((f (#) arccos) `| Z) . x = (a * (arccos . x)) - (((a * x) + b) / (sqrt (1 - (x ^2)))) ) ) Z c= (dom f) /\ (dom arccos) by A1, VALUED_1:def_4; then A4: Z c= dom f by XBOOLE_1:18; then A5: f is_differentiable_on Z by A3, FDIFF_1:23; A6: arccos is_differentiable_on Z by A2, FDIFF_1:26, SIN_COS6:106; for x being Real st x in Z holds ((f (#) arccos) `| Z) . x = (a * (arccos . x)) - (((a * x) + b) / (sqrt (1 - (x ^2)))) proof let x be Real; ::_thesis: ( x in Z implies ((f (#) arccos) `| Z) . x = (a * (arccos . x)) - (((a * x) + b) / (sqrt (1 - (x ^2)))) ) assume A7: x in Z ; ::_thesis: ((f (#) arccos) `| Z) . x = (a * (arccos . x)) - (((a * x) + b) / (sqrt (1 - (x ^2)))) then A8: ( - 1 < x & x < 1 ) by A2, XXREAL_1:4; ((f (#) arccos) `| Z) . x = ((arccos . x) * (diff (f,x))) + ((f . x) * (diff (arccos,x))) by A1, A5, A6, A7, FDIFF_1:21 .= ((arccos . x) * ((f `| Z) . x)) + ((f . x) * (diff (arccos,x))) by A5, A7, FDIFF_1:def_7 .= ((arccos . x) * a) + ((f . x) * (diff (arccos,x))) by A3, A4, A7, FDIFF_1:23 .= ((arccos . x) * a) + ((f . x) * (- (1 / (sqrt (1 - (x ^2)))))) by A8, SIN_COS6:106 .= ((arccos . x) * a) - ((f . x) * (1 / (sqrt (1 - (x ^2))))) .= (a * (arccos . x)) - (((a * x) + b) * (1 / (sqrt (1 - (x ^2))))) by A3, A7 .= (a * (arccos . x)) - (((a * x) + b) / (sqrt (1 - (x ^2)))) by XCMPLX_1:99 ; hence ((f (#) arccos) `| Z) . x = (a * (arccos . x)) - (((a * x) + b) / (sqrt (1 - (x ^2)))) ; ::_thesis: verum end; hence ( f (#) arccos is_differentiable_on Z & ( for x being Real st x in Z holds ((f (#) arccos) `| Z) . x = (a * (arccos . x)) - (((a * x) + b) / (sqrt (1 - (x ^2)))) ) ) by A1, A5, A6, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_7:20 for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((1 / 2) (#) (arcsin * f)) & ( for x being Real st x in Z holds ( f . x = 2 * x & f . x > - 1 & f . x < 1 ) ) holds ( (1 / 2) (#) (arcsin * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) (arcsin * f)) `| Z) . x = 1 / (sqrt (1 - ((2 * x) ^2))) ) ) proof let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom ((1 / 2) (#) (arcsin * f)) & ( for x being Real st x in Z holds ( f . x = 2 * x & f . x > - 1 & f . x < 1 ) ) holds ( (1 / 2) (#) (arcsin * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) (arcsin * f)) `| Z) . x = 1 / (sqrt (1 - ((2 * x) ^2))) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom ((1 / 2) (#) (arcsin * f)) & ( for x being Real st x in Z holds ( f . x = 2 * x & f . x > - 1 & f . x < 1 ) ) implies ( (1 / 2) (#) (arcsin * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) (arcsin * f)) `| Z) . x = 1 / (sqrt (1 - ((2 * x) ^2))) ) ) ) assume that A1: Z c= dom ((1 / 2) (#) (arcsin * f)) and A2: for x being Real st x in Z holds ( f . x = 2 * x & f . x > - 1 & f . x < 1 ) ; ::_thesis: ( (1 / 2) (#) (arcsin * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) (arcsin * f)) `| Z) . x = 1 / (sqrt (1 - ((2 * x) ^2))) ) ) A3: ( Z c= dom (arcsin * f) & ( for x being Real st x in Z holds ( f . x = (2 * x) + 0 & f . x > - 1 & f . x < 1 ) ) ) by A1, A2, VALUED_1:def_5; then A4: arcsin * f is_differentiable_on Z by Th14; for x being Real st x in Z holds (((1 / 2) (#) (arcsin * f)) `| Z) . x = 1 / (sqrt (1 - ((2 * x) ^2))) proof let x be Real; ::_thesis: ( x in Z implies (((1 / 2) (#) (arcsin * f)) `| Z) . x = 1 / (sqrt (1 - ((2 * x) ^2))) ) assume A5: x in Z ; ::_thesis: (((1 / 2) (#) (arcsin * f)) `| Z) . x = 1 / (sqrt (1 - ((2 * x) ^2))) then (((1 / 2) (#) (arcsin * f)) `| Z) . x = (1 / 2) * (diff ((arcsin * f),x)) by A1, A4, FDIFF_1:20 .= (1 / 2) * (((arcsin * f) `| Z) . x) by A4, A5, FDIFF_1:def_7 .= (1 / 2) * (2 / (sqrt (1 - (((2 * x) + 0) ^2)))) by A3, A5, Th14 .= ((1 / 2) * 2) / (sqrt (1 - ((2 * x) ^2))) by XCMPLX_1:74 .= 1 / (sqrt (1 - ((2 * x) ^2))) ; hence (((1 / 2) (#) (arcsin * f)) `| Z) . x = 1 / (sqrt (1 - ((2 * x) ^2))) ; ::_thesis: verum end; hence ( (1 / 2) (#) (arcsin * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) (arcsin * f)) `| Z) . x = 1 / (sqrt (1 - ((2 * x) ^2))) ) ) by A1, A4, FDIFF_1:20; ::_thesis: verum end; theorem :: FDIFF_7:21 for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((1 / 2) (#) (arccos * f)) & ( for x being Real st x in Z holds ( f . x = 2 * x & f . x > - 1 & f . x < 1 ) ) holds ( (1 / 2) (#) (arccos * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) (arccos * f)) `| Z) . x = - (1 / (sqrt (1 - ((2 * x) ^2)))) ) ) proof let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom ((1 / 2) (#) (arccos * f)) & ( for x being Real st x in Z holds ( f . x = 2 * x & f . x > - 1 & f . x < 1 ) ) holds ( (1 / 2) (#) (arccos * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) (arccos * f)) `| Z) . x = - (1 / (sqrt (1 - ((2 * x) ^2)))) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom ((1 / 2) (#) (arccos * f)) & ( for x being Real st x in Z holds ( f . x = 2 * x & f . x > - 1 & f . x < 1 ) ) implies ( (1 / 2) (#) (arccos * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) (arccos * f)) `| Z) . x = - (1 / (sqrt (1 - ((2 * x) ^2)))) ) ) ) assume that A1: Z c= dom ((1 / 2) (#) (arccos * f)) and A2: for x being Real st x in Z holds ( f . x = 2 * x & f . x > - 1 & f . x < 1 ) ; ::_thesis: ( (1 / 2) (#) (arccos * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) (arccos * f)) `| Z) . x = - (1 / (sqrt (1 - ((2 * x) ^2)))) ) ) A3: ( Z c= dom (arccos * f) & ( for x being Real st x in Z holds ( f . x = (2 * x) + 0 & f . x > - 1 & f . x < 1 ) ) ) by A1, A2, VALUED_1:def_5; then A4: arccos * f is_differentiable_on Z by Th15; for x being Real st x in Z holds (((1 / 2) (#) (arccos * f)) `| Z) . x = - (1 / (sqrt (1 - ((2 * x) ^2)))) proof let x be Real; ::_thesis: ( x in Z implies (((1 / 2) (#) (arccos * f)) `| Z) . x = - (1 / (sqrt (1 - ((2 * x) ^2)))) ) assume A5: x in Z ; ::_thesis: (((1 / 2) (#) (arccos * f)) `| Z) . x = - (1 / (sqrt (1 - ((2 * x) ^2)))) then (((1 / 2) (#) (arccos * f)) `| Z) . x = (1 / 2) * (diff ((arccos * f),x)) by A1, A4, FDIFF_1:20 .= (1 / 2) * (((arccos * f) `| Z) . x) by A4, A5, FDIFF_1:def_7 .= (1 / 2) * (- (2 / (sqrt (1 - (((2 * x) + 0) ^2))))) by A3, A5, Th15 .= - ((1 / 2) * (2 / (sqrt (1 - ((2 * x) ^2))))) .= - (((1 / 2) * 2) / (sqrt (1 - ((2 * x) ^2)))) by XCMPLX_1:74 .= - (1 / (sqrt (1 - ((2 * x) ^2)))) ; hence (((1 / 2) (#) (arccos * f)) `| Z) . x = - (1 / (sqrt (1 - ((2 * x) ^2)))) ; ::_thesis: verum end; hence ( (1 / 2) (#) (arccos * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) (arccos * f)) `| Z) . x = - (1 / (sqrt (1 - ((2 * x) ^2)))) ) ) by A1, A4, FDIFF_1:20; ::_thesis: verum end; theorem Th22: :: FDIFF_7:22 for Z being open Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom ((#R (1 / 2)) * f) & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = 1 & f . x > 0 ) ) holds ( (#R (1 / 2)) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((#R (1 / 2)) * f) `| Z) . x = - (x * ((1 - (x #Z 2)) #R (- (1 / 2)))) ) ) proof let Z be open Subset of REAL; ::_thesis: for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom ((#R (1 / 2)) * f) & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = 1 & f . x > 0 ) ) holds ( (#R (1 / 2)) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((#R (1 / 2)) * f) `| Z) . x = - (x * ((1 - (x #Z 2)) #R (- (1 / 2)))) ) ) let f, f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom ((#R (1 / 2)) * f) & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = 1 & f . x > 0 ) ) implies ( (#R (1 / 2)) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((#R (1 / 2)) * f) `| Z) . x = - (x * ((1 - (x #Z 2)) #R (- (1 / 2)))) ) ) ) assume that A1: Z c= dom ((#R (1 / 2)) * f) and A2: f = f1 - f2 and A3: f2 = #Z 2 and A4: for x being Real st x in Z holds ( f1 . x = 1 & f . x > 0 ) ; ::_thesis: ( (#R (1 / 2)) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((#R (1 / 2)) * f) `| Z) . x = - (x * ((1 - (x #Z 2)) #R (- (1 / 2)))) ) ) for y being set st y in Z holds y in dom f by A1, FUNCT_1:11; then A5: Z c= dom (f1 + ((- 1) (#) f2)) by A2, TARSKI:def_3; A6: for x being Real st x in Z holds f1 . x = 1 + (0 * x) by A4; then A7: f is_differentiable_on Z by A2, A3, A5, FDIFF_4:12; A8: for x being Real st x in Z holds (#R (1 / 2)) * f is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies (#R (1 / 2)) * f is_differentiable_in x ) assume x in Z ; ::_thesis: (#R (1 / 2)) * f is_differentiable_in x then ( f is_differentiable_in x & f . x > 0 ) by A4, A7, FDIFF_1:9; hence (#R (1 / 2)) * f is_differentiable_in x by TAYLOR_1:22; ::_thesis: verum end; then A9: (#R (1 / 2)) * f is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds (((#R (1 / 2)) * f) `| Z) . x = - (x * ((1 - (x #Z 2)) #R (- (1 / 2)))) proof let x be Real; ::_thesis: ( x in Z implies (((#R (1 / 2)) * f) `| Z) . x = - (x * ((1 - (x #Z 2)) #R (- (1 / 2)))) ) assume A10: x in Z ; ::_thesis: (((#R (1 / 2)) * f) `| Z) . x = - (x * ((1 - (x #Z 2)) #R (- (1 / 2)))) then A11: ( f is_differentiable_in x & f . x > 0 ) by A4, A7, FDIFF_1:9; x in dom (f1 - f2) by A1, A2, A10, FUNCT_1:11; then A12: (f1 - f2) . x = (f1 . x) - (f2 . x) by VALUED_1:13 .= 1 - (f2 . x) by A4, A10 .= 1 - (x #Z 2) by A3, TAYLOR_1:def_1 ; (((#R (1 / 2)) * f) `| Z) . x = diff (((#R (1 / 2)) * f),x) by A9, A10, FDIFF_1:def_7 .= ((1 / 2) * ((f . x) #R ((1 / 2) - 1))) * (diff (f,x)) by A11, TAYLOR_1:22 .= ((1 / 2) * ((f . x) #R ((1 / 2) - 1))) * ((f `| Z) . x) by A7, A10, FDIFF_1:def_7 .= ((1 / 2) * ((f . x) #R ((1 / 2) - 1))) * (0 + ((2 * (- 1)) * x)) by A2, A3, A5, A6, A10, FDIFF_4:12 .= - (x * ((1 - (x #Z 2)) #R (- (1 / 2)))) by A2, A12 ; hence (((#R (1 / 2)) * f) `| Z) . x = - (x * ((1 - (x #Z 2)) #R (- (1 / 2)))) ; ::_thesis: verum end; hence ( (#R (1 / 2)) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((#R (1 / 2)) * f) `| Z) . x = - (x * ((1 - (x #Z 2)) #R (- (1 / 2)))) ) ) by A1, A8, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_7:23 for Z being open Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom (((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) & Z c= ].(- 1),1.[ & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = 1 & f . x > 0 & x <> 0 ) ) holds ( ((id Z) (#) arcsin) + ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) `| Z) . x = arcsin . x ) ) proof let Z be open Subset of REAL; ::_thesis: for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom (((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) & Z c= ].(- 1),1.[ & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = 1 & f . x > 0 & x <> 0 ) ) holds ( ((id Z) (#) arcsin) + ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) `| Z) . x = arcsin . x ) ) let f, f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) & Z c= ].(- 1),1.[ & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = 1 & f . x > 0 & x <> 0 ) ) implies ( ((id Z) (#) arcsin) + ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) `| Z) . x = arcsin . x ) ) ) assume that A1: Z c= dom (((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) and A2: Z c= ].(- 1),1.[ and A3: f = f1 - f2 and A4: f2 = #Z 2 and A5: for x being Real st x in Z holds ( f1 . x = 1 & f . x > 0 & x <> 0 ) ; ::_thesis: ( ((id Z) (#) arcsin) + ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) `| Z) . x = arcsin . x ) ) A6: Z c= (dom ((id Z) (#) arcsin)) /\ (dom ((#R (1 / 2)) * f)) by A1, VALUED_1:def_1; then A7: Z c= dom ((#R (1 / 2)) * f) by XBOOLE_1:18; A8: Z c= dom ((id Z) (#) arcsin) by A6, XBOOLE_1:18; then A9: (id Z) (#) arcsin is_differentiable_on Z by A2, Th16; A10: for x being Real st x in Z holds ( f1 . x = 1 & f . x > 0 ) by A5; then A11: (#R (1 / 2)) * f is_differentiable_on Z by A3, A4, A7, Th22; A12: for x being Real st x in Z holds x * ((1 - (x #Z 2)) #R (- (1 / 2))) = x / (sqrt (1 - (x ^2))) proof let x be Real; ::_thesis: ( x in Z implies x * ((1 - (x #Z 2)) #R (- (1 / 2))) = x / (sqrt (1 - (x ^2))) ) assume A13: x in Z ; ::_thesis: x * ((1 - (x #Z 2)) #R (- (1 / 2))) = x / (sqrt (1 - (x ^2))) then x in dom (f1 - f2) by A3, A7, FUNCT_1:11; then A14: (f1 - f2) . x = (f1 . x) - (f2 . x) by VALUED_1:13 .= 1 - (f2 . x) by A5, A13 .= 1 - (x #Z 2) by A4, TAYLOR_1:def_1 ; f . x > 0 by A5, A13; then A15: 1 - (x ^2) > 0 by A3, A14, Th1; (1 - (x #Z 2)) #R (- (1 / 2)) = (1 - (x ^2)) #R (- (1 / 2)) by Th1 .= 1 / (sqrt (1 - (x ^2))) by A15, Th3 ; hence x * ((1 - (x #Z 2)) #R (- (1 / 2))) = x / (sqrt (1 - (x ^2))) by XCMPLX_1:99; ::_thesis: verum end; for x being Real st x in Z holds ((((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) `| Z) . x = arcsin . x proof let x be Real; ::_thesis: ( x in Z implies ((((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) `| Z) . x = arcsin . x ) assume A16: x in Z ; ::_thesis: ((((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) `| Z) . x = arcsin . x hence ((((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) `| Z) . x = (diff (((id Z) (#) arcsin),x)) + (diff (((#R (1 / 2)) * f),x)) by A1, A9, A11, FDIFF_1:18 .= ((((id Z) (#) arcsin) `| Z) . x) + (diff (((#R (1 / 2)) * f),x)) by A9, A16, FDIFF_1:def_7 .= ((((id Z) (#) arcsin) `| Z) . x) + ((((#R (1 / 2)) * f) `| Z) . x) by A11, A16, FDIFF_1:def_7 .= ((arcsin . x) + (x / (sqrt (1 - (x ^2))))) + ((((#R (1 / 2)) * f) `| Z) . x) by A2, A8, A16, Th16 .= ((arcsin . x) + (x / (sqrt (1 - (x ^2))))) + (- (x * ((1 - (x #Z 2)) #R (- (1 / 2))))) by A3, A4, A10, A7, A16, Th22 .= ((arcsin . x) + (x / (sqrt (1 - (x ^2))))) - (x * ((1 - (x #Z 2)) #R (- (1 / 2)))) .= ((arcsin . x) + (x / (sqrt (1 - (x ^2))))) - (x / (sqrt (1 - (x ^2)))) by A12, A16 .= arcsin . x ; ::_thesis: verum end; hence ( ((id Z) (#) arcsin) + ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) `| Z) . x = arcsin . x ) ) by A1, A9, A11, FDIFF_1:18; ::_thesis: verum end; theorem :: FDIFF_7:24 for Z being open Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom (((id Z) (#) arccos) - ((#R (1 / 2)) * f)) & Z c= ].(- 1),1.[ & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = 1 & f . x > 0 & x <> 0 ) ) holds ( ((id Z) (#) arccos) - ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) (#) arccos) - ((#R (1 / 2)) * f)) `| Z) . x = arccos . x ) ) proof let Z be open Subset of REAL; ::_thesis: for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom (((id Z) (#) arccos) - ((#R (1 / 2)) * f)) & Z c= ].(- 1),1.[ & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = 1 & f . x > 0 & x <> 0 ) ) holds ( ((id Z) (#) arccos) - ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) (#) arccos) - ((#R (1 / 2)) * f)) `| Z) . x = arccos . x ) ) let f, f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (((id Z) (#) arccos) - ((#R (1 / 2)) * f)) & Z c= ].(- 1),1.[ & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = 1 & f . x > 0 & x <> 0 ) ) implies ( ((id Z) (#) arccos) - ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) (#) arccos) - ((#R (1 / 2)) * f)) `| Z) . x = arccos . x ) ) ) assume that A1: Z c= dom (((id Z) (#) arccos) - ((#R (1 / 2)) * f)) and A2: Z c= ].(- 1),1.[ and A3: f = f1 - f2 and A4: f2 = #Z 2 and A5: for x being Real st x in Z holds ( f1 . x = 1 & f . x > 0 & x <> 0 ) ; ::_thesis: ( ((id Z) (#) arccos) - ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) (#) arccos) - ((#R (1 / 2)) * f)) `| Z) . x = arccos . x ) ) A6: Z c= (dom ((id Z) (#) arccos)) /\ (dom ((#R (1 / 2)) * f)) by A1, VALUED_1:12; then A7: Z c= dom ((#R (1 / 2)) * f) by XBOOLE_1:18; A8: Z c= dom ((id Z) (#) arccos) by A6, XBOOLE_1:18; then A9: (id Z) (#) arccos is_differentiable_on Z by A2, Th17; A10: for x being Real st x in Z holds ( f1 . x = 1 & f . x > 0 ) by A5; then A11: (#R (1 / 2)) * f is_differentiable_on Z by A3, A4, A7, Th22; A12: for x being Real st x in Z holds x * ((1 - (x #Z 2)) #R (- (1 / 2))) = x / (sqrt (1 - (x ^2))) proof let x be Real; ::_thesis: ( x in Z implies x * ((1 - (x #Z 2)) #R (- (1 / 2))) = x / (sqrt (1 - (x ^2))) ) assume A13: x in Z ; ::_thesis: x * ((1 - (x #Z 2)) #R (- (1 / 2))) = x / (sqrt (1 - (x ^2))) then x in dom (f1 - f2) by A3, A7, FUNCT_1:11; then A14: (f1 - f2) . x = (f1 . x) - (f2 . x) by VALUED_1:13 .= 1 - (f2 . x) by A5, A13 .= 1 - (x #Z 2) by A4, TAYLOR_1:def_1 ; f . x > 0 by A5, A13; then A15: 1 - (x ^2) > 0 by A3, A14, Th1; (1 - (x #Z 2)) #R (- (1 / 2)) = (1 - (x ^2)) #R (- (1 / 2)) by Th1 .= 1 / (sqrt (1 - (x ^2))) by A15, Th3 ; hence x * ((1 - (x #Z 2)) #R (- (1 / 2))) = x / (sqrt (1 - (x ^2))) by XCMPLX_1:99; ::_thesis: verum end; for x being Real st x in Z holds ((((id Z) (#) arccos) - ((#R (1 / 2)) * f)) `| Z) . x = arccos . x proof let x be Real; ::_thesis: ( x in Z implies ((((id Z) (#) arccos) - ((#R (1 / 2)) * f)) `| Z) . x = arccos . x ) assume A16: x in Z ; ::_thesis: ((((id Z) (#) arccos) - ((#R (1 / 2)) * f)) `| Z) . x = arccos . x hence ((((id Z) (#) arccos) - ((#R (1 / 2)) * f)) `| Z) . x = (diff (((id Z) (#) arccos),x)) - (diff (((#R (1 / 2)) * f),x)) by A1, A9, A11, FDIFF_1:19 .= ((((id Z) (#) arccos) `| Z) . x) - (diff (((#R (1 / 2)) * f),x)) by A9, A16, FDIFF_1:def_7 .= ((((id Z) (#) arccos) `| Z) . x) - ((((#R (1 / 2)) * f) `| Z) . x) by A11, A16, FDIFF_1:def_7 .= ((arccos . x) - (x / (sqrt (1 - (x ^2))))) - ((((#R (1 / 2)) * f) `| Z) . x) by A2, A8, A16, Th17 .= ((arccos . x) - (x / (sqrt (1 - (x ^2))))) - (- (x * ((1 - (x #Z 2)) #R (- (1 / 2))))) by A3, A4, A10, A7, A16, Th22 .= ((arccos . x) - (x / (sqrt (1 - (x ^2))))) + (x * ((1 - (x #Z 2)) #R (- (1 / 2)))) .= ((arccos . x) - (x / (sqrt (1 - (x ^2))))) + (x / (sqrt (1 - (x ^2)))) by A12, A16 .= arccos . x ; ::_thesis: verum end; hence ( ((id Z) (#) arccos) - ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) (#) arccos) - ((#R (1 / 2)) * f)) `| Z) . x = arccos . x ) ) by A1, A9, A11, FDIFF_1:19; ::_thesis: verum end; theorem Th25: :: FDIFF_7:25 for a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((id Z) (#) (arcsin * f)) & ( for x being Real st x in Z holds ( f . x = x / a & f . x > - 1 & f . x < 1 ) ) holds ( (id Z) (#) (arcsin * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) (arcsin * f)) `| Z) . x = (arcsin . (x / a)) + (x / (a * (sqrt (1 - ((x / a) ^2))))) ) ) proof let a be Real; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((id Z) (#) (arcsin * f)) & ( for x being Real st x in Z holds ( f . x = x / a & f . x > - 1 & f . x < 1 ) ) holds ( (id Z) (#) (arcsin * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) (arcsin * f)) `| Z) . x = (arcsin . (x / a)) + (x / (a * (sqrt (1 - ((x / a) ^2))))) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom ((id Z) (#) (arcsin * f)) & ( for x being Real st x in Z holds ( f . x = x / a & f . x > - 1 & f . x < 1 ) ) holds ( (id Z) (#) (arcsin * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) (arcsin * f)) `| Z) . x = (arcsin . (x / a)) + (x / (a * (sqrt (1 - ((x / a) ^2))))) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom ((id Z) (#) (arcsin * f)) & ( for x being Real st x in Z holds ( f . x = x / a & f . x > - 1 & f . x < 1 ) ) implies ( (id Z) (#) (arcsin * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) (arcsin * f)) `| Z) . x = (arcsin . (x / a)) + (x / (a * (sqrt (1 - ((x / a) ^2))))) ) ) ) assume that A1: Z c= dom ((id Z) (#) (arcsin * f)) and A2: for x being Real st x in Z holds ( f . x = x / a & f . x > - 1 & f . x < 1 ) ; ::_thesis: ( (id Z) (#) (arcsin * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) (arcsin * f)) `| Z) . x = (arcsin . (x / a)) + (x / (a * (sqrt (1 - ((x / a) ^2))))) ) ) A3: Z c= (dom (id Z)) /\ (dom (arcsin * f)) by A1, VALUED_1:def_4; then A4: Z c= dom (id Z) by XBOOLE_1:18; A5: Z c= dom (arcsin * f) by A3, XBOOLE_1:18; for x being Real st x in Z holds f . x = ((1 / a) * x) + 0 proof let x be Real; ::_thesis: ( x in Z implies f . x = ((1 / a) * x) + 0 ) assume x in Z ; ::_thesis: f . x = ((1 / a) * x) + 0 then f . x = x / a by A2; hence f . x = ((1 / a) * x) + 0 by XCMPLX_1:99; ::_thesis: verum end; then A6: for x being Real st x in Z holds ( f . x = ((1 / a) * x) + 0 & f . x > - 1 & f . x < 1 ) by A2; then A7: arcsin * f is_differentiable_on Z by A5, Th14; A8: for x being Real st x in Z holds (id Z) . x = (1 * x) + 0 by FUNCT_1:18; then A9: id Z is_differentiable_on Z by A4, FDIFF_1:23; A10: for x being Real st x in Z holds ((arcsin * f) `| Z) . x = 1 / (a * (sqrt (1 - ((x / a) ^2)))) proof let x be Real; ::_thesis: ( x in Z implies ((arcsin * f) `| Z) . x = 1 / (a * (sqrt (1 - ((x / a) ^2)))) ) assume x in Z ; ::_thesis: ((arcsin * f) `| Z) . x = 1 / (a * (sqrt (1 - ((x / a) ^2)))) then ((arcsin * f) `| Z) . x = (1 / a) / (sqrt (1 - ((((1 / a) * x) + 0) ^2))) by A6, A5, Th14 .= (1 / a) / (sqrt (1 - ((x / a) ^2))) by XCMPLX_1:99 .= 1 / (a * (sqrt (1 - ((x / a) ^2)))) by XCMPLX_1:78 ; hence ((arcsin * f) `| Z) . x = 1 / (a * (sqrt (1 - ((x / a) ^2)))) ; ::_thesis: verum end; for x being Real st x in Z holds (((id Z) (#) (arcsin * f)) `| Z) . x = (arcsin . (x / a)) + (x / (a * (sqrt (1 - ((x / a) ^2))))) proof let x be Real; ::_thesis: ( x in Z implies (((id Z) (#) (arcsin * f)) `| Z) . x = (arcsin . (x / a)) + (x / (a * (sqrt (1 - ((x / a) ^2))))) ) assume A11: x in Z ; ::_thesis: (((id Z) (#) (arcsin * f)) `| Z) . x = (arcsin . (x / a)) + (x / (a * (sqrt (1 - ((x / a) ^2))))) then A12: (arcsin * f) . x = arcsin . (f . x) by A5, FUNCT_1:12 .= arcsin . (x / a) by A2, A11 ; (((id Z) (#) (arcsin * f)) `| Z) . x = (((arcsin * f) . x) * (diff ((id Z),x))) + (((id Z) . x) * (diff ((arcsin * f),x))) by A1, A9, A7, A11, FDIFF_1:21 .= (((arcsin * f) . x) * (((id Z) `| Z) . x)) + (((id Z) . x) * (diff ((arcsin * f),x))) by A9, A11, FDIFF_1:def_7 .= (((arcsin * f) . x) * 1) + (((id Z) . x) * (diff ((arcsin * f),x))) by A4, A8, A11, FDIFF_1:23 .= (((arcsin * f) . x) * 1) + (((id Z) . x) * (((arcsin * f) `| Z) . x)) by A7, A11, FDIFF_1:def_7 .= ((arcsin * f) . x) + (x * (((arcsin * f) `| Z) . x)) by A11, FUNCT_1:18 .= (arcsin . (x / a)) + (x * (1 / (a * (sqrt (1 - ((x / a) ^2)))))) by A10, A11, A12 .= (arcsin . (x / a)) + (x / (a * (sqrt (1 - ((x / a) ^2))))) by XCMPLX_1:99 ; hence (((id Z) (#) (arcsin * f)) `| Z) . x = (arcsin . (x / a)) + (x / (a * (sqrt (1 - ((x / a) ^2))))) ; ::_thesis: verum end; hence ( (id Z) (#) (arcsin * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) (arcsin * f)) `| Z) . x = (arcsin . (x / a)) + (x / (a * (sqrt (1 - ((x / a) ^2))))) ) ) by A1, A9, A7, FDIFF_1:21; ::_thesis: verum end; theorem Th26: :: FDIFF_7:26 for a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((id Z) (#) (arccos * f)) & ( for x being Real st x in Z holds ( f . x = x / a & f . x > - 1 & f . x < 1 ) ) holds ( (id Z) (#) (arccos * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) (arccos * f)) `| Z) . x = (arccos . (x / a)) - (x / (a * (sqrt (1 - ((x / a) ^2))))) ) ) proof let a be Real; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((id Z) (#) (arccos * f)) & ( for x being Real st x in Z holds ( f . x = x / a & f . x > - 1 & f . x < 1 ) ) holds ( (id Z) (#) (arccos * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) (arccos * f)) `| Z) . x = (arccos . (x / a)) - (x / (a * (sqrt (1 - ((x / a) ^2))))) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom ((id Z) (#) (arccos * f)) & ( for x being Real st x in Z holds ( f . x = x / a & f . x > - 1 & f . x < 1 ) ) holds ( (id Z) (#) (arccos * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) (arccos * f)) `| Z) . x = (arccos . (x / a)) - (x / (a * (sqrt (1 - ((x / a) ^2))))) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom ((id Z) (#) (arccos * f)) & ( for x being Real st x in Z holds ( f . x = x / a & f . x > - 1 & f . x < 1 ) ) implies ( (id Z) (#) (arccos * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) (arccos * f)) `| Z) . x = (arccos . (x / a)) - (x / (a * (sqrt (1 - ((x / a) ^2))))) ) ) ) assume that A1: Z c= dom ((id Z) (#) (arccos * f)) and A2: for x being Real st x in Z holds ( f . x = x / a & f . x > - 1 & f . x < 1 ) ; ::_thesis: ( (id Z) (#) (arccos * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) (arccos * f)) `| Z) . x = (arccos . (x / a)) - (x / (a * (sqrt (1 - ((x / a) ^2))))) ) ) A3: Z c= (dom (id Z)) /\ (dom (arccos * f)) by A1, VALUED_1:def_4; then A4: Z c= dom (id Z) by XBOOLE_1:18; A5: Z c= dom (arccos * f) by A3, XBOOLE_1:18; for x being Real st x in Z holds f . x = ((1 / a) * x) + 0 proof let x be Real; ::_thesis: ( x in Z implies f . x = ((1 / a) * x) + 0 ) assume x in Z ; ::_thesis: f . x = ((1 / a) * x) + 0 then f . x = x / a by A2; hence f . x = ((1 / a) * x) + 0 by XCMPLX_1:99; ::_thesis: verum end; then A6: for x being Real st x in Z holds ( f . x = ((1 / a) * x) + 0 & f . x > - 1 & f . x < 1 ) by A2; then A7: arccos * f is_differentiable_on Z by A5, Th15; A8: for x being Real st x in Z holds (id Z) . x = (1 * x) + 0 by FUNCT_1:18; then A9: id Z is_differentiable_on Z by A4, FDIFF_1:23; A10: for x being Real st x in Z holds ((arccos * f) `| Z) . x = - (1 / (a * (sqrt (1 - ((x / a) ^2))))) proof let x be Real; ::_thesis: ( x in Z implies ((arccos * f) `| Z) . x = - (1 / (a * (sqrt (1 - ((x / a) ^2))))) ) assume x in Z ; ::_thesis: ((arccos * f) `| Z) . x = - (1 / (a * (sqrt (1 - ((x / a) ^2))))) then ((arccos * f) `| Z) . x = - ((1 / a) / (sqrt (1 - ((((1 / a) * x) + 0) ^2)))) by A6, A5, Th15 .= - ((1 / a) / (sqrt (1 - ((x / a) ^2)))) by XCMPLX_1:99 .= - (1 / (a * (sqrt (1 - ((x / a) ^2))))) by XCMPLX_1:78 ; hence ((arccos * f) `| Z) . x = - (1 / (a * (sqrt (1 - ((x / a) ^2))))) ; ::_thesis: verum end; for x being Real st x in Z holds (((id Z) (#) (arccos * f)) `| Z) . x = (arccos . (x / a)) - (x / (a * (sqrt (1 - ((x / a) ^2))))) proof let x be Real; ::_thesis: ( x in Z implies (((id Z) (#) (arccos * f)) `| Z) . x = (arccos . (x / a)) - (x / (a * (sqrt (1 - ((x / a) ^2))))) ) assume A11: x in Z ; ::_thesis: (((id Z) (#) (arccos * f)) `| Z) . x = (arccos . (x / a)) - (x / (a * (sqrt (1 - ((x / a) ^2))))) then A12: (arccos * f) . x = arccos . (f . x) by A5, FUNCT_1:12 .= arccos . (x / a) by A2, A11 ; (((id Z) (#) (arccos * f)) `| Z) . x = (((arccos * f) . x) * (diff ((id Z),x))) + (((id Z) . x) * (diff ((arccos * f),x))) by A1, A9, A7, A11, FDIFF_1:21 .= (((arccos * f) . x) * (((id Z) `| Z) . x)) + (((id Z) . x) * (diff ((arccos * f),x))) by A9, A11, FDIFF_1:def_7 .= (((arccos * f) . x) * 1) + (((id Z) . x) * (diff ((arccos * f),x))) by A4, A8, A11, FDIFF_1:23 .= (((arccos * f) . x) * 1) + (((id Z) . x) * (((arccos * f) `| Z) . x)) by A7, A11, FDIFF_1:def_7 .= ((arccos * f) . x) + (x * (((arccos * f) `| Z) . x)) by A11, FUNCT_1:18 .= (arccos . (x / a)) + (x * (- (1 / (a * (sqrt (1 - ((x / a) ^2))))))) by A10, A11, A12 .= (arccos . (x / a)) - (x * (1 / (a * (sqrt (1 - ((x / a) ^2)))))) .= (arccos . (x / a)) - (x / (a * (sqrt (1 - ((x / a) ^2))))) by XCMPLX_1:99 ; hence (((id Z) (#) (arccos * f)) `| Z) . x = (arccos . (x / a)) - (x / (a * (sqrt (1 - ((x / a) ^2))))) ; ::_thesis: verum end; hence ( (id Z) (#) (arccos * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) (arccos * f)) `| Z) . x = (arccos . (x / a)) - (x / (a * (sqrt (1 - ((x / a) ^2))))) ) ) by A1, A9, A7, FDIFF_1:21; ::_thesis: verum end; theorem Th27: :: FDIFF_7:27 for a being Real for Z being open Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom ((#R (1 / 2)) * f) & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & f . x > 0 ) ) holds ( (#R (1 / 2)) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((#R (1 / 2)) * f) `| Z) . x = - (x * (((a ^2) - (x #Z 2)) #R (- (1 / 2)))) ) ) proof let a be Real; ::_thesis: for Z being open Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom ((#R (1 / 2)) * f) & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & f . x > 0 ) ) holds ( (#R (1 / 2)) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((#R (1 / 2)) * f) `| Z) . x = - (x * (((a ^2) - (x #Z 2)) #R (- (1 / 2)))) ) ) let Z be open Subset of REAL; ::_thesis: for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom ((#R (1 / 2)) * f) & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & f . x > 0 ) ) holds ( (#R (1 / 2)) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((#R (1 / 2)) * f) `| Z) . x = - (x * (((a ^2) - (x #Z 2)) #R (- (1 / 2)))) ) ) let f, f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom ((#R (1 / 2)) * f) & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & f . x > 0 ) ) implies ( (#R (1 / 2)) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((#R (1 / 2)) * f) `| Z) . x = - (x * (((a ^2) - (x #Z 2)) #R (- (1 / 2)))) ) ) ) assume that A1: Z c= dom ((#R (1 / 2)) * f) and A2: f = f1 - f2 and A3: f2 = #Z 2 and A4: for x being Real st x in Z holds ( f1 . x = a ^2 & f . x > 0 ) ; ::_thesis: ( (#R (1 / 2)) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((#R (1 / 2)) * f) `| Z) . x = - (x * (((a ^2) - (x #Z 2)) #R (- (1 / 2)))) ) ) for y being set st y in Z holds y in dom f by A1, FUNCT_1:11; then A5: Z c= dom (f1 + ((- 1) (#) f2)) by A2, TARSKI:def_3; A6: for x being Real st x in Z holds f1 . x = (a ^2) + (0 * x) by A4; then A7: f is_differentiable_on Z by A2, A3, A5, FDIFF_4:12; A8: for x being Real st x in Z holds (#R (1 / 2)) * f is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies (#R (1 / 2)) * f is_differentiable_in x ) assume x in Z ; ::_thesis: (#R (1 / 2)) * f is_differentiable_in x then ( f is_differentiable_in x & f . x > 0 ) by A4, A7, FDIFF_1:9; hence (#R (1 / 2)) * f is_differentiable_in x by TAYLOR_1:22; ::_thesis: verum end; then A9: (#R (1 / 2)) * f is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds (((#R (1 / 2)) * f) `| Z) . x = - (x * (((a ^2) - (x #Z 2)) #R (- (1 / 2)))) proof let x be Real; ::_thesis: ( x in Z implies (((#R (1 / 2)) * f) `| Z) . x = - (x * (((a ^2) - (x #Z 2)) #R (- (1 / 2)))) ) assume A10: x in Z ; ::_thesis: (((#R (1 / 2)) * f) `| Z) . x = - (x * (((a ^2) - (x #Z 2)) #R (- (1 / 2)))) then A11: ( f is_differentiable_in x & f . x > 0 ) by A4, A7, FDIFF_1:9; x in dom (f1 - f2) by A1, A2, A10, FUNCT_1:11; then A12: (f1 - f2) . x = (f1 . x) - (f2 . x) by VALUED_1:13 .= (a ^2) - (f2 . x) by A4, A10 .= (a ^2) - (x #Z 2) by A3, TAYLOR_1:def_1 ; (((#R (1 / 2)) * f) `| Z) . x = diff (((#R (1 / 2)) * f),x) by A9, A10, FDIFF_1:def_7 .= ((1 / 2) * ((f . x) #R ((1 / 2) - 1))) * (diff (f,x)) by A11, TAYLOR_1:22 .= ((1 / 2) * ((f . x) #R ((1 / 2) - 1))) * ((f `| Z) . x) by A7, A10, FDIFF_1:def_7 .= ((1 / 2) * ((f . x) #R ((1 / 2) - 1))) * (0 + ((2 * (- 1)) * x)) by A2, A3, A5, A6, A10, FDIFF_4:12 .= - (x * (((a ^2) - (x #Z 2)) #R (- (1 / 2)))) by A2, A12 ; hence (((#R (1 / 2)) * f) `| Z) . x = - (x * (((a ^2) - (x #Z 2)) #R (- (1 / 2)))) ; ::_thesis: verum end; hence ( (#R (1 / 2)) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((#R (1 / 2)) * f) `| Z) . x = - (x * (((a ^2) - (x #Z 2)) #R (- (1 / 2)))) ) ) by A1, A8, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_7:28 for a being Real for Z being open Subset of REAL for f3, f, f1, f2 being PartFunc of REAL,REAL st Z c= dom (((id Z) (#) (arcsin * f3)) + ((#R (1 / 2)) * f)) & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & f . x > 0 & f3 . x = x / a & f3 . x > - 1 & f3 . x < 1 & x <> 0 & a > 0 ) ) holds ( ((id Z) (#) (arcsin * f3)) + ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) (#) (arcsin * f3)) + ((#R (1 / 2)) * f)) `| Z) . x = arcsin . (x / a) ) ) proof let a be Real; ::_thesis: for Z being open Subset of REAL for f3, f, f1, f2 being PartFunc of REAL,REAL st Z c= dom (((id Z) (#) (arcsin * f3)) + ((#R (1 / 2)) * f)) & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & f . x > 0 & f3 . x = x / a & f3 . x > - 1 & f3 . x < 1 & x <> 0 & a > 0 ) ) holds ( ((id Z) (#) (arcsin * f3)) + ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) (#) (arcsin * f3)) + ((#R (1 / 2)) * f)) `| Z) . x = arcsin . (x / a) ) ) let Z be open Subset of REAL; ::_thesis: for f3, f, f1, f2 being PartFunc of REAL,REAL st Z c= dom (((id Z) (#) (arcsin * f3)) + ((#R (1 / 2)) * f)) & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & f . x > 0 & f3 . x = x / a & f3 . x > - 1 & f3 . x < 1 & x <> 0 & a > 0 ) ) holds ( ((id Z) (#) (arcsin * f3)) + ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) (#) (arcsin * f3)) + ((#R (1 / 2)) * f)) `| Z) . x = arcsin . (x / a) ) ) let f3, f, f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (((id Z) (#) (arcsin * f3)) + ((#R (1 / 2)) * f)) & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & f . x > 0 & f3 . x = x / a & f3 . x > - 1 & f3 . x < 1 & x <> 0 & a > 0 ) ) implies ( ((id Z) (#) (arcsin * f3)) + ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) (#) (arcsin * f3)) + ((#R (1 / 2)) * f)) `| Z) . x = arcsin . (x / a) ) ) ) assume that A1: Z c= dom (((id Z) (#) (arcsin * f3)) + ((#R (1 / 2)) * f)) and A2: ( f = f1 - f2 & f2 = #Z 2 ) and A3: for x being Real st x in Z holds ( f1 . x = a ^2 & f . x > 0 & f3 . x = x / a & f3 . x > - 1 & f3 . x < 1 & x <> 0 & a > 0 ) ; ::_thesis: ( ((id Z) (#) (arcsin * f3)) + ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) (#) (arcsin * f3)) + ((#R (1 / 2)) * f)) `| Z) . x = arcsin . (x / a) ) ) A4: Z c= (dom ((id Z) (#) (arcsin * f3))) /\ (dom ((#R (1 / 2)) * f)) by A1, VALUED_1:def_1; then A5: Z c= dom ((#R (1 / 2)) * f) by XBOOLE_1:18; A6: for x being Real st x in Z holds ( f1 . x = a ^2 & f . x > 0 ) by A3; then A7: (#R (1 / 2)) * f is_differentiable_on Z by A2, A5, Th27; A8: for x being Real st x in Z holds ( f3 . x = x / a & f3 . x > - 1 & f3 . x < 1 ) by A3; A9: Z c= dom ((id Z) (#) (arcsin * f3)) by A4, XBOOLE_1:18; then A10: (id Z) (#) (arcsin * f3) is_differentiable_on Z by A8, Th25; A11: for x being Real st x in Z holds ((a ^2) - (x #Z 2)) #R (- (1 / 2)) = 1 / (a * (sqrt (1 - ((x / a) ^2)))) proof let x be Real; ::_thesis: ( x in Z implies ((a ^2) - (x #Z 2)) #R (- (1 / 2)) = 1 / (a * (sqrt (1 - ((x / a) ^2)))) ) assume A12: x in Z ; ::_thesis: ((a ^2) - (x #Z 2)) #R (- (1 / 2)) = 1 / (a * (sqrt (1 - ((x / a) ^2)))) then A13: f3 . x = x / a by A3; f3 . x < 1 by A3, A12; then A14: 1 - (f3 . x) > 1 - 1 by XREAL_1:10; f3 . x > - 1 by A3, A12; then 1 + (f3 . x) > 1 + (- 1) by XREAL_1:6; then A15: (1 + (f3 . x)) * (1 - (f3 . x)) > 0 by A14, XREAL_1:129; A16: a > 0 by A3, A12; then A17: a ^2 > 0 by SQUARE_1:12; 1 / (a * (sqrt (1 - ((x / a) ^2)))) = 1 / ((sqrt (a ^2)) * (sqrt (1 - ((x / a) ^2)))) by A16, SQUARE_1:22 .= 1 / (sqrt ((a ^2) * (1 - ((x / a) ^2)))) by A17, A13, A15, SQUARE_1:29 .= (((a ^2) * 1) - ((a * (x / a)) ^2)) #R (- (1 / 2)) by A17, A13, A15, Th3, XREAL_1:129 .= ((a ^2) - (((x * a) / a) ^2)) #R (- (1 / 2)) by XCMPLX_1:74 .= ((a ^2) - ((x * (a / a)) ^2)) #R (- (1 / 2)) by XCMPLX_1:74 .= ((a ^2) - ((x * 1) ^2)) #R (- (1 / 2)) by A16, XCMPLX_1:60 .= ((a ^2) - (x #Z 2)) #R (- (1 / 2)) by Th1 ; hence ((a ^2) - (x #Z 2)) #R (- (1 / 2)) = 1 / (a * (sqrt (1 - ((x / a) ^2)))) ; ::_thesis: verum end; for x being Real st x in Z holds ((((id Z) (#) (arcsin * f3)) + ((#R (1 / 2)) * f)) `| Z) . x = arcsin . (x / a) proof let x be Real; ::_thesis: ( x in Z implies ((((id Z) (#) (arcsin * f3)) + ((#R (1 / 2)) * f)) `| Z) . x = arcsin . (x / a) ) assume A18: x in Z ; ::_thesis: ((((id Z) (#) (arcsin * f3)) + ((#R (1 / 2)) * f)) `| Z) . x = arcsin . (x / a) then ((((id Z) (#) (arcsin * f3)) + ((#R (1 / 2)) * f)) `| Z) . x = (diff (((id Z) (#) (arcsin * f3)),x)) + (diff (((#R (1 / 2)) * f),x)) by A1, A10, A7, FDIFF_1:18 .= ((((id Z) (#) (arcsin * f3)) `| Z) . x) + (diff (((#R (1 / 2)) * f),x)) by A10, A18, FDIFF_1:def_7 .= ((((id Z) (#) (arcsin * f3)) `| Z) . x) + ((((#R (1 / 2)) * f) `| Z) . x) by A7, A18, FDIFF_1:def_7 .= ((arcsin . (x / a)) + (x / (a * (sqrt (1 - ((x / a) ^2)))))) + ((((#R (1 / 2)) * f) `| Z) . x) by A9, A8, A18, Th25 .= ((arcsin . (x / a)) + (x / (a * (sqrt (1 - ((x / a) ^2)))))) + (- (x * (((a ^2) - (x #Z 2)) #R (- (1 / 2))))) by A2, A5, A6, A18, Th27 .= ((arcsin . (x / a)) + (x / (a * (sqrt (1 - ((x / a) ^2)))))) - (x * (((a ^2) - (x #Z 2)) #R (- (1 / 2)))) .= ((arcsin . (x / a)) + (x / (a * (sqrt (1 - ((x / a) ^2)))))) - (x * (1 / (a * (sqrt (1 - ((x / a) ^2)))))) by A11, A18 .= ((arcsin . (x / a)) + (x / (a * (sqrt (1 - ((x / a) ^2)))))) - (x / (a * (sqrt (1 - ((x / a) ^2))))) by XCMPLX_1:99 .= arcsin . (x / a) ; hence ((((id Z) (#) (arcsin * f3)) + ((#R (1 / 2)) * f)) `| Z) . x = arcsin . (x / a) ; ::_thesis: verum end; hence ( ((id Z) (#) (arcsin * f3)) + ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) (#) (arcsin * f3)) + ((#R (1 / 2)) * f)) `| Z) . x = arcsin . (x / a) ) ) by A1, A10, A7, FDIFF_1:18; ::_thesis: verum end; theorem :: FDIFF_7:29 for a being Real for Z being open Subset of REAL for f3, f, f1, f2 being PartFunc of REAL,REAL st Z c= dom (((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & f . x > 0 & f3 . x = x / a & f3 . x > - 1 & f3 . x < 1 & x <> 0 & a > 0 ) ) holds ( ((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) `| Z) . x = arccos . (x / a) ) ) proof let a be Real; ::_thesis: for Z being open Subset of REAL for f3, f, f1, f2 being PartFunc of REAL,REAL st Z c= dom (((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & f . x > 0 & f3 . x = x / a & f3 . x > - 1 & f3 . x < 1 & x <> 0 & a > 0 ) ) holds ( ((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) `| Z) . x = arccos . (x / a) ) ) let Z be open Subset of REAL; ::_thesis: for f3, f, f1, f2 being PartFunc of REAL,REAL st Z c= dom (((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & f . x > 0 & f3 . x = x / a & f3 . x > - 1 & f3 . x < 1 & x <> 0 & a > 0 ) ) holds ( ((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) `| Z) . x = arccos . (x / a) ) ) let f3, f, f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & f . x > 0 & f3 . x = x / a & f3 . x > - 1 & f3 . x < 1 & x <> 0 & a > 0 ) ) implies ( ((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) `| Z) . x = arccos . (x / a) ) ) ) assume that A1: Z c= dom (((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) and A2: ( f = f1 - f2 & f2 = #Z 2 ) and A3: for x being Real st x in Z holds ( f1 . x = a ^2 & f . x > 0 & f3 . x = x / a & f3 . x > - 1 & f3 . x < 1 & x <> 0 & a > 0 ) ; ::_thesis: ( ((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) `| Z) . x = arccos . (x / a) ) ) A4: Z c= (dom ((id Z) (#) (arccos * f3))) /\ (dom ((#R (1 / 2)) * f)) by A1, VALUED_1:12; then A5: Z c= dom ((#R (1 / 2)) * f) by XBOOLE_1:18; A6: for x being Real st x in Z holds ( f1 . x = a ^2 & f . x > 0 ) by A3; then A7: (#R (1 / 2)) * f is_differentiable_on Z by A2, A5, Th27; A8: for x being Real st x in Z holds ( f3 . x = x / a & f3 . x > - 1 & f3 . x < 1 ) by A3; A9: Z c= dom ((id Z) (#) (arccos * f3)) by A4, XBOOLE_1:18; then A10: (id Z) (#) (arccos * f3) is_differentiable_on Z by A8, Th26; A11: for x being Real st x in Z holds ((a ^2) - (x #Z 2)) #R (- (1 / 2)) = 1 / (a * (sqrt (1 - ((x / a) ^2)))) proof let x be Real; ::_thesis: ( x in Z implies ((a ^2) - (x #Z 2)) #R (- (1 / 2)) = 1 / (a * (sqrt (1 - ((x / a) ^2)))) ) assume A12: x in Z ; ::_thesis: ((a ^2) - (x #Z 2)) #R (- (1 / 2)) = 1 / (a * (sqrt (1 - ((x / a) ^2)))) then A13: f3 . x = x / a by A3; f3 . x < 1 by A3, A12; then A14: 1 - (f3 . x) > 1 - 1 by XREAL_1:10; f3 . x > - 1 by A3, A12; then 1 + (f3 . x) > 1 + (- 1) by XREAL_1:6; then A15: (1 + (f3 . x)) * (1 - (f3 . x)) > 0 by A14, XREAL_1:129; A16: a > 0 by A3, A12; then A17: a ^2 > 0 by SQUARE_1:12; 1 / (a * (sqrt (1 - ((x / a) ^2)))) = 1 / ((sqrt (a ^2)) * (sqrt (1 - ((x / a) ^2)))) by A16, SQUARE_1:22 .= 1 / (sqrt ((a ^2) * (1 - ((x / a) ^2)))) by A17, A13, A15, SQUARE_1:29 .= (((a ^2) * 1) - ((a * (x / a)) ^2)) #R (- (1 / 2)) by A17, A13, A15, Th3, XREAL_1:129 .= ((a ^2) - (((x * a) / a) ^2)) #R (- (1 / 2)) by XCMPLX_1:74 .= ((a ^2) - ((x * (a / a)) ^2)) #R (- (1 / 2)) by XCMPLX_1:74 .= ((a ^2) - ((x * 1) ^2)) #R (- (1 / 2)) by A16, XCMPLX_1:60 .= ((a ^2) - (x #Z 2)) #R (- (1 / 2)) by Th1 ; hence ((a ^2) - (x #Z 2)) #R (- (1 / 2)) = 1 / (a * (sqrt (1 - ((x / a) ^2)))) ; ::_thesis: verum end; for x being Real st x in Z holds ((((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) `| Z) . x = arccos . (x / a) proof let x be Real; ::_thesis: ( x in Z implies ((((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) `| Z) . x = arccos . (x / a) ) assume A18: x in Z ; ::_thesis: ((((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) `| Z) . x = arccos . (x / a) then ((((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) `| Z) . x = (diff (((id Z) (#) (arccos * f3)),x)) - (diff (((#R (1 / 2)) * f),x)) by A1, A10, A7, FDIFF_1:19 .= ((((id Z) (#) (arccos * f3)) `| Z) . x) - (diff (((#R (1 / 2)) * f),x)) by A10, A18, FDIFF_1:def_7 .= ((((id Z) (#) (arccos * f3)) `| Z) . x) - ((((#R (1 / 2)) * f) `| Z) . x) by A7, A18, FDIFF_1:def_7 .= ((arccos . (x / a)) - (x / (a * (sqrt (1 - ((x / a) ^2)))))) - ((((#R (1 / 2)) * f) `| Z) . x) by A9, A8, A18, Th26 .= ((arccos . (x / a)) - (x / (a * (sqrt (1 - ((x / a) ^2)))))) - (- (x * (((a ^2) - (x #Z 2)) #R (- (1 / 2))))) by A2, A5, A6, A18, Th27 .= ((arccos . (x / a)) - (x / (a * (sqrt (1 - ((x / a) ^2)))))) + (x * (((a ^2) - (x #Z 2)) #R (- (1 / 2)))) .= ((arccos . (x / a)) - (x / (a * (sqrt (1 - ((x / a) ^2)))))) + (x * (1 / (a * (sqrt (1 - ((x / a) ^2)))))) by A11, A18 .= ((arccos . (x / a)) - (x / (a * (sqrt (1 - ((x / a) ^2)))))) + (x / (a * (sqrt (1 - ((x / a) ^2))))) by XCMPLX_1:99 .= arccos . (x / a) ; hence ((((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) `| Z) . x = arccos . (x / a) ; ::_thesis: verum end; hence ( ((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) `| Z) . x = arccos . (x / a) ) ) by A1, A10, A7, FDIFF_1:19; ::_thesis: verum end; theorem :: FDIFF_7:30 for n being Element of NAT for Z being open Subset of REAL st Z c= dom ((- (1 / n)) (#) ((#Z n) * (sin ^))) & n > 0 & ( for x being Real st x in Z holds sin . x <> 0 ) holds ( (- (1 / n)) (#) ((#Z n) * (sin ^)) is_differentiable_on Z & ( for x being Real st x in Z holds (((- (1 / n)) (#) ((#Z n) * (sin ^))) `| Z) . x = (cos . x) / ((sin . x) #Z (n + 1)) ) ) proof let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL st Z c= dom ((- (1 / n)) (#) ((#Z n) * (sin ^))) & n > 0 & ( for x being Real st x in Z holds sin . x <> 0 ) holds ( (- (1 / n)) (#) ((#Z n) * (sin ^)) is_differentiable_on Z & ( for x being Real st x in Z holds (((- (1 / n)) (#) ((#Z n) * (sin ^))) `| Z) . x = (cos . x) / ((sin . x) #Z (n + 1)) ) ) let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((- (1 / n)) (#) ((#Z n) * (sin ^))) & n > 0 & ( for x being Real st x in Z holds sin . x <> 0 ) implies ( (- (1 / n)) (#) ((#Z n) * (sin ^)) is_differentiable_on Z & ( for x being Real st x in Z holds (((- (1 / n)) (#) ((#Z n) * (sin ^))) `| Z) . x = (cos . x) / ((sin . x) #Z (n + 1)) ) ) ) assume that A1: Z c= dom ((- (1 / n)) (#) ((#Z n) * (sin ^))) and A2: n > 0 and A3: for x being Real st x in Z holds sin . x <> 0 ; ::_thesis: ( (- (1 / n)) (#) ((#Z n) * (sin ^)) is_differentiable_on Z & ( for x being Real st x in Z holds (((- (1 / n)) (#) ((#Z n) * (sin ^))) `| Z) . x = (cos . x) / ((sin . x) #Z (n + 1)) ) ) A4: Z c= dom ((#Z n) * (sin ^)) by A1, VALUED_1:def_5; A5: sin ^ is_differentiable_on Z by A3, FDIFF_4:40; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ (#Z_n)_*_(sin_^)_is_differentiable_in_x let x be Real; ::_thesis: ( x in Z implies (#Z n) * (sin ^) is_differentiable_in x ) assume x in Z ; ::_thesis: (#Z n) * (sin ^) is_differentiable_in x then sin ^ is_differentiable_in x by A5, FDIFF_1:9; hence (#Z n) * (sin ^) is_differentiable_in x by TAYLOR_1:3; ::_thesis: verum end; then A6: (#Z n) * (sin ^) is_differentiable_on Z by A4, FDIFF_1:9; for y being set st y in Z holds y in dom (sin ^) by A4, FUNCT_1:11; then A7: Z c= dom (sin ^) by TARSKI:def_3; for x being Real st x in Z holds (((- (1 / n)) (#) ((#Z n) * (sin ^))) `| Z) . x = (cos . x) / ((sin . x) #Z (n + 1)) proof let x be Real; ::_thesis: ( x in Z implies (((- (1 / n)) (#) ((#Z n) * (sin ^))) `| Z) . x = (cos . x) / ((sin . x) #Z (n + 1)) ) assume A8: x in Z ; ::_thesis: (((- (1 / n)) (#) ((#Z n) * (sin ^))) `| Z) . x = (cos . x) / ((sin . x) #Z (n + 1)) then A9: sin ^ is_differentiable_in x by A5, FDIFF_1:9; A10: (sin ^) . x = (sin . x) " by A7, A8, RFUNCT_1:def_2 .= 1 / (sin . x) by XCMPLX_1:215 ; (((- (1 / n)) (#) ((#Z n) * (sin ^))) `| Z) . x = (- (1 / n)) * (diff (((#Z n) * (sin ^)),x)) by A1, A6, A8, FDIFF_1:20 .= (- (1 / n)) * ((n * (((sin ^) . x) #Z (n - 1))) * (diff ((sin ^),x))) by A9, TAYLOR_1:3 .= (- (1 / n)) * ((n * (((sin ^) . x) #Z (n - 1))) * (((sin ^) `| Z) . x)) by A5, A8, FDIFF_1:def_7 .= (- (1 / n)) * ((n * (((sin ^) . x) #Z (n - 1))) * (- ((cos . x) / ((sin . x) ^2)))) by A3, A8, FDIFF_4:40 .= - ((((1 / n) * n) * (((sin ^) . x) #Z (n - 1))) * (- ((cos . x) / ((sin . x) ^2)))) .= - ((1 * (((sin ^) . x) #Z (n - 1))) * (- ((cos . x) / ((sin . x) ^2)))) by A2, XCMPLX_1:106 .= - (((1 / (sin . x)) #Z (n - 1)) * (- ((cos . x) / ((sin . x) #Z 2)))) by A10, Th1 .= - ((- ((cos . x) / ((sin . x) #Z 2))) * (1 / ((sin . x) #Z (n - 1)))) by PREPOWER:42 .= ((cos . x) / ((sin . x) #Z 2)) * (1 / ((sin . x) #Z (n - 1))) .= ((cos . x) / ((sin . x) #Z 2)) / ((sin . x) #Z (n - 1)) by XCMPLX_1:99 .= (cos . x) / (((sin . x) #Z 2) * ((sin . x) #Z (n - 1))) by XCMPLX_1:78 .= (cos . x) / ((sin . x) #Z (2 + (n - 1))) by A3, A8, PREPOWER:44 .= (cos . x) / ((sin . x) #Z (n + 1)) ; hence (((- (1 / n)) (#) ((#Z n) * (sin ^))) `| Z) . x = (cos . x) / ((sin . x) #Z (n + 1)) ; ::_thesis: verum end; hence ( (- (1 / n)) (#) ((#Z n) * (sin ^)) is_differentiable_on Z & ( for x being Real st x in Z holds (((- (1 / n)) (#) ((#Z n) * (sin ^))) `| Z) . x = (cos . x) / ((sin . x) #Z (n + 1)) ) ) by A1, A6, FDIFF_1:20; ::_thesis: verum end; theorem :: FDIFF_7:31 for n being Element of NAT for Z being open Subset of REAL st Z c= dom ((1 / n) (#) ((#Z n) * (cos ^))) & n > 0 & ( for x being Real st x in Z holds cos . x <> 0 ) holds ( (1 / n) (#) ((#Z n) * (cos ^)) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / n) (#) ((#Z n) * (cos ^))) `| Z) . x = (sin . x) / ((cos . x) #Z (n + 1)) ) ) proof let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL st Z c= dom ((1 / n) (#) ((#Z n) * (cos ^))) & n > 0 & ( for x being Real st x in Z holds cos . x <> 0 ) holds ( (1 / n) (#) ((#Z n) * (cos ^)) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / n) (#) ((#Z n) * (cos ^))) `| Z) . x = (sin . x) / ((cos . x) #Z (n + 1)) ) ) let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((1 / n) (#) ((#Z n) * (cos ^))) & n > 0 & ( for x being Real st x in Z holds cos . x <> 0 ) implies ( (1 / n) (#) ((#Z n) * (cos ^)) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / n) (#) ((#Z n) * (cos ^))) `| Z) . x = (sin . x) / ((cos . x) #Z (n + 1)) ) ) ) assume that A1: Z c= dom ((1 / n) (#) ((#Z n) * (cos ^))) and A2: n > 0 and A3: for x being Real st x in Z holds cos . x <> 0 ; ::_thesis: ( (1 / n) (#) ((#Z n) * (cos ^)) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / n) (#) ((#Z n) * (cos ^))) `| Z) . x = (sin . x) / ((cos . x) #Z (n + 1)) ) ) A4: Z c= dom ((#Z n) * (cos ^)) by A1, VALUED_1:def_5; A5: cos ^ is_differentiable_on Z by A3, FDIFF_4:39; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ (#Z_n)_*_(cos_^)_is_differentiable_in_x let x be Real; ::_thesis: ( x in Z implies (#Z n) * (cos ^) is_differentiable_in x ) assume x in Z ; ::_thesis: (#Z n) * (cos ^) is_differentiable_in x then cos ^ is_differentiable_in x by A5, FDIFF_1:9; hence (#Z n) * (cos ^) is_differentiable_in x by TAYLOR_1:3; ::_thesis: verum end; then A6: (#Z n) * (cos ^) is_differentiable_on Z by A4, FDIFF_1:9; for y being set st y in Z holds y in dom (cos ^) by A4, FUNCT_1:11; then A7: Z c= dom (cos ^) by TARSKI:def_3; for x being Real st x in Z holds (((1 / n) (#) ((#Z n) * (cos ^))) `| Z) . x = (sin . x) / ((cos . x) #Z (n + 1)) proof let x be Real; ::_thesis: ( x in Z implies (((1 / n) (#) ((#Z n) * (cos ^))) `| Z) . x = (sin . x) / ((cos . x) #Z (n + 1)) ) assume A8: x in Z ; ::_thesis: (((1 / n) (#) ((#Z n) * (cos ^))) `| Z) . x = (sin . x) / ((cos . x) #Z (n + 1)) then A9: cos ^ is_differentiable_in x by A5, FDIFF_1:9; A10: (cos ^) . x = (cos . x) " by A7, A8, RFUNCT_1:def_2 .= 1 / (cos . x) by XCMPLX_1:215 ; (((1 / n) (#) ((#Z n) * (cos ^))) `| Z) . x = (1 / n) * (diff (((#Z n) * (cos ^)),x)) by A1, A6, A8, FDIFF_1:20 .= (1 / n) * ((n * (((cos ^) . x) #Z (n - 1))) * (diff ((cos ^),x))) by A9, TAYLOR_1:3 .= (1 / n) * ((n * (((cos ^) . x) #Z (n - 1))) * (((cos ^) `| Z) . x)) by A5, A8, FDIFF_1:def_7 .= (1 / n) * ((n * (((cos ^) . x) #Z (n - 1))) * ((sin . x) / ((cos . x) ^2))) by A3, A8, FDIFF_4:39 .= (((1 / n) * n) * (((cos ^) . x) #Z (n - 1))) * ((sin . x) / ((cos . x) ^2)) .= (1 * (((cos ^) . x) #Z (n - 1))) * ((sin . x) / ((cos . x) ^2)) by A2, XCMPLX_1:106 .= ((1 / (cos . x)) #Z (n - 1)) * ((sin . x) / ((cos . x) #Z 2)) by A10, Th1 .= (1 / ((cos . x) #Z (n - 1))) * ((sin . x) / ((cos . x) #Z 2)) by PREPOWER:42 .= ((sin . x) / ((cos . x) #Z 2)) / ((cos . x) #Z (n - 1)) by XCMPLX_1:99 .= (sin . x) / (((cos . x) #Z 2) * ((cos . x) #Z (n - 1))) by XCMPLX_1:78 .= (sin . x) / ((cos . x) #Z (2 + (n - 1))) by A3, A8, PREPOWER:44 .= (sin . x) / ((cos . x) #Z (n + 1)) ; hence (((1 / n) (#) ((#Z n) * (cos ^))) `| Z) . x = (sin . x) / ((cos . x) #Z (n + 1)) ; ::_thesis: verum end; hence ( (1 / n) (#) ((#Z n) * (cos ^)) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / n) (#) ((#Z n) * (cos ^))) `| Z) . x = (sin . x) / ((cos . x) #Z (n + 1)) ) ) by A1, A6, FDIFF_1:20; ::_thesis: verum end; Lm3: right_open_halfline 0 = { g where g is Real : 0 < g } by XXREAL_1:230; theorem :: FDIFF_7:32 for Z being open Subset of REAL st Z c= dom (sin * ln) & ( for x being Real st x in Z holds x > 0 ) holds ( sin * ln is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * ln) `| Z) . x = (cos . (ln . x)) / x ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sin * ln) & ( for x being Real st x in Z holds x > 0 ) implies ( sin * ln is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * ln) `| Z) . x = (cos . (ln . x)) / x ) ) ) assume that A1: Z c= dom (sin * ln) and A2: for x being Real st x in Z holds x > 0 ; ::_thesis: ( sin * ln is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * ln) `| Z) . x = (cos . (ln . x)) / x ) ) A3: for x being Real st x in Z holds sin * ln is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies sin * ln is_differentiable_in x ) assume x in Z ; ::_thesis: sin * ln is_differentiable_in x then A4: ln is_differentiable_in x by A2, TAYLOR_1:18; sin is_differentiable_in ln . x by SIN_COS:64; hence sin * ln is_differentiable_in x by A4, FDIFF_2:13; ::_thesis: verum end; then A5: sin * ln is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((sin * ln) `| Z) . x = (cos . (ln . x)) / x proof let x be Real; ::_thesis: ( x in Z implies ((sin * ln) `| Z) . x = (cos . (ln . x)) / x ) A6: sin is_differentiable_in ln . x by SIN_COS:64; assume A7: x in Z ; ::_thesis: ((sin * ln) `| Z) . x = (cos . (ln . x)) / x then x > 0 by A2; then A8: x in right_open_halfline 0 by Lm3; ln is_differentiable_in x by A2, A7, TAYLOR_1:18; then diff ((sin * ln),x) = (diff (sin,(ln . x))) * (diff (ln,x)) by A6, FDIFF_2:13 .= (cos . (ln . x)) * (diff (ln,x)) by SIN_COS:64 .= (cos . (ln . x)) * (1 / x) by A8, TAYLOR_1:18 .= (cos . (ln . x)) / x by XCMPLX_1:99 ; hence ((sin * ln) `| Z) . x = (cos . (ln . x)) / x by A5, A7, FDIFF_1:def_7; ::_thesis: verum end; hence ( sin * ln is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * ln) `| Z) . x = (cos . (ln . x)) / x ) ) by A1, A3, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_7:33 for Z being open Subset of REAL st Z c= dom (cos * ln) & ( for x being Real st x in Z holds x > 0 ) holds ( cos * ln is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * ln) `| Z) . x = - ((sin . (ln . x)) / x) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cos * ln) & ( for x being Real st x in Z holds x > 0 ) implies ( cos * ln is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * ln) `| Z) . x = - ((sin . (ln . x)) / x) ) ) ) assume that A1: Z c= dom (cos * ln) and A2: for x being Real st x in Z holds x > 0 ; ::_thesis: ( cos * ln is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * ln) `| Z) . x = - ((sin . (ln . x)) / x) ) ) A3: for x being Real st x in Z holds cos * ln is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies cos * ln is_differentiable_in x ) assume x in Z ; ::_thesis: cos * ln is_differentiable_in x then A4: ln is_differentiable_in x by A2, TAYLOR_1:18; cos is_differentiable_in ln . x by SIN_COS:63; hence cos * ln is_differentiable_in x by A4, FDIFF_2:13; ::_thesis: verum end; then A5: cos * ln is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((cos * ln) `| Z) . x = - ((sin . (ln . x)) / x) proof let x be Real; ::_thesis: ( x in Z implies ((cos * ln) `| Z) . x = - ((sin . (ln . x)) / x) ) A6: cos is_differentiable_in ln . x by SIN_COS:63; assume A7: x in Z ; ::_thesis: ((cos * ln) `| Z) . x = - ((sin . (ln . x)) / x) then x > 0 by A2; then A8: x in right_open_halfline 0 by Lm3; ln is_differentiable_in x by A2, A7, TAYLOR_1:18; then diff ((cos * ln),x) = (diff (cos,(ln . x))) * (diff (ln,x)) by A6, FDIFF_2:13 .= (- (sin . (ln . x))) * (diff (ln,x)) by SIN_COS:63 .= (- (sin . (ln . x))) * (1 / x) by A8, TAYLOR_1:18 .= (- (sin . (ln . x))) / x by XCMPLX_1:99 .= - ((sin . (ln . x)) / x) by XCMPLX_1:187 ; hence ((cos * ln) `| Z) . x = - ((sin . (ln . x)) / x) by A5, A7, FDIFF_1:def_7; ::_thesis: verum end; hence ( cos * ln is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * ln) `| Z) . x = - ((sin . (ln . x)) / x) ) ) by A1, A3, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_7:34 for Z being open Subset of REAL st Z c= dom (sin * exp_R) holds ( sin * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * exp_R) `| Z) . x = (exp_R . x) * (cos . (exp_R . x)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sin * exp_R) implies ( sin * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * exp_R) `| Z) . x = (exp_R . x) * (cos . (exp_R . x)) ) ) ) A1: for x being Real st x in Z holds sin * exp_R is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies sin * exp_R is_differentiable_in x ) assume x in Z ; ::_thesis: sin * exp_R is_differentiable_in x ( exp_R is_differentiable_in x & sin is_differentiable_in exp_R . x ) by SIN_COS:64, SIN_COS:65; hence sin * exp_R is_differentiable_in x by FDIFF_2:13; ::_thesis: verum end; assume A2: Z c= dom (sin * exp_R) ; ::_thesis: ( sin * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * exp_R) `| Z) . x = (exp_R . x) * (cos . (exp_R . x)) ) ) then A3: sin * exp_R is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((sin * exp_R) `| Z) . x = (exp_R . x) * (cos . (exp_R . x)) proof let x be Real; ::_thesis: ( x in Z implies ((sin * exp_R) `| Z) . x = (exp_R . x) * (cos . (exp_R . x)) ) ( exp_R is_differentiable_in x & sin is_differentiable_in exp_R . x ) by SIN_COS:64, SIN_COS:65; then A4: diff ((sin * exp_R),x) = (diff (sin,(exp_R . x))) * (diff (exp_R,x)) by FDIFF_2:13 .= (cos . (exp_R . x)) * (diff (exp_R,x)) by SIN_COS:64 .= (exp_R . x) * (cos . (exp_R . x)) by SIN_COS:65 ; assume x in Z ; ::_thesis: ((sin * exp_R) `| Z) . x = (exp_R . x) * (cos . (exp_R . x)) hence ((sin * exp_R) `| Z) . x = (exp_R . x) * (cos . (exp_R . x)) by A3, A4, FDIFF_1:def_7; ::_thesis: verum end; hence ( sin * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * exp_R) `| Z) . x = (exp_R . x) * (cos . (exp_R . x)) ) ) by A2, A1, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_7:35 for Z being open Subset of REAL st Z c= dom (cos * exp_R) holds ( cos * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * exp_R) `| Z) . x = - ((exp_R . x) * (sin . (exp_R . x))) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cos * exp_R) implies ( cos * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * exp_R) `| Z) . x = - ((exp_R . x) * (sin . (exp_R . x))) ) ) ) A1: for x being Real st x in Z holds cos * exp_R is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies cos * exp_R is_differentiable_in x ) assume x in Z ; ::_thesis: cos * exp_R is_differentiable_in x ( exp_R is_differentiable_in x & cos is_differentiable_in exp_R . x ) by SIN_COS:63, SIN_COS:65; hence cos * exp_R is_differentiable_in x by FDIFF_2:13; ::_thesis: verum end; assume A2: Z c= dom (cos * exp_R) ; ::_thesis: ( cos * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * exp_R) `| Z) . x = - ((exp_R . x) * (sin . (exp_R . x))) ) ) then A3: cos * exp_R is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((cos * exp_R) `| Z) . x = - ((exp_R . x) * (sin . (exp_R . x))) proof let x be Real; ::_thesis: ( x in Z implies ((cos * exp_R) `| Z) . x = - ((exp_R . x) * (sin . (exp_R . x))) ) ( exp_R is_differentiable_in x & cos is_differentiable_in exp_R . x ) by SIN_COS:63, SIN_COS:65; then A4: diff ((cos * exp_R),x) = (diff (cos,(exp_R . x))) * (diff (exp_R,x)) by FDIFF_2:13 .= (- (sin . (exp_R . x))) * (diff (exp_R,x)) by SIN_COS:63 .= (- (sin . (exp_R . x))) * (exp_R . x) by SIN_COS:65 .= - ((exp_R . x) * (sin . (exp_R . x))) ; assume x in Z ; ::_thesis: ((cos * exp_R) `| Z) . x = - ((exp_R . x) * (sin . (exp_R . x))) hence ((cos * exp_R) `| Z) . x = - ((exp_R . x) * (sin . (exp_R . x))) by A3, A4, FDIFF_1:def_7; ::_thesis: verum end; hence ( cos * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * exp_R) `| Z) . x = - ((exp_R . x) * (sin . (exp_R . x))) ) ) by A2, A1, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_7:36 for Z being open Subset of REAL st Z c= dom (exp_R * cos) holds ( exp_R * cos is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R * cos) `| Z) . x = - ((exp_R . (cos . x)) * (sin . x)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (exp_R * cos) implies ( exp_R * cos is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R * cos) `| Z) . x = - ((exp_R . (cos . x)) * (sin . x)) ) ) ) A1: for x being Real st x in Z holds exp_R * cos is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies exp_R * cos is_differentiable_in x ) assume x in Z ; ::_thesis: exp_R * cos is_differentiable_in x ( cos is_differentiable_in x & exp_R is_differentiable_in cos . x ) by SIN_COS:63, SIN_COS:65; hence exp_R * cos is_differentiable_in x by FDIFF_2:13; ::_thesis: verum end; assume A2: Z c= dom (exp_R * cos) ; ::_thesis: ( exp_R * cos is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R * cos) `| Z) . x = - ((exp_R . (cos . x)) * (sin . x)) ) ) then A3: exp_R * cos is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((exp_R * cos) `| Z) . x = - ((exp_R . (cos . x)) * (sin . x)) proof let x be Real; ::_thesis: ( x in Z implies ((exp_R * cos) `| Z) . x = - ((exp_R . (cos . x)) * (sin . x)) ) ( cos is_differentiable_in x & exp_R is_differentiable_in cos . x ) by SIN_COS:63, SIN_COS:65; then A4: diff ((exp_R * cos),x) = (diff (exp_R,(cos . x))) * (diff (cos,x)) by FDIFF_2:13 .= (diff (exp_R,(cos . x))) * (- (sin . x)) by SIN_COS:63 .= (exp_R . (cos . x)) * (- (sin . x)) by SIN_COS:65 .= - ((exp_R . (cos . x)) * (sin . x)) ; assume x in Z ; ::_thesis: ((exp_R * cos) `| Z) . x = - ((exp_R . (cos . x)) * (sin . x)) hence ((exp_R * cos) `| Z) . x = - ((exp_R . (cos . x)) * (sin . x)) by A3, A4, FDIFF_1:def_7; ::_thesis: verum end; hence ( exp_R * cos is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R * cos) `| Z) . x = - ((exp_R . (cos . x)) * (sin . x)) ) ) by A2, A1, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_7:37 for Z being open Subset of REAL st Z c= dom (exp_R * sin) holds ( exp_R * sin is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R * sin) `| Z) . x = (exp_R . (sin . x)) * (cos . x) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (exp_R * sin) implies ( exp_R * sin is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R * sin) `| Z) . x = (exp_R . (sin . x)) * (cos . x) ) ) ) A1: for x being Real st x in Z holds exp_R * sin is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies exp_R * sin is_differentiable_in x ) assume x in Z ; ::_thesis: exp_R * sin is_differentiable_in x ( sin is_differentiable_in x & exp_R is_differentiable_in sin . x ) by SIN_COS:64, SIN_COS:65; hence exp_R * sin is_differentiable_in x by FDIFF_2:13; ::_thesis: verum end; assume A2: Z c= dom (exp_R * sin) ; ::_thesis: ( exp_R * sin is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R * sin) `| Z) . x = (exp_R . (sin . x)) * (cos . x) ) ) then A3: exp_R * sin is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((exp_R * sin) `| Z) . x = (exp_R . (sin . x)) * (cos . x) proof let x be Real; ::_thesis: ( x in Z implies ((exp_R * sin) `| Z) . x = (exp_R . (sin . x)) * (cos . x) ) ( sin is_differentiable_in x & exp_R is_differentiable_in sin . x ) by SIN_COS:64, SIN_COS:65; then A4: diff ((exp_R * sin),x) = (diff (exp_R,(sin . x))) * (diff (sin,x)) by FDIFF_2:13 .= (diff (exp_R,(sin . x))) * (cos . x) by SIN_COS:64 .= (exp_R . (sin . x)) * (cos . x) by SIN_COS:65 ; assume x in Z ; ::_thesis: ((exp_R * sin) `| Z) . x = (exp_R . (sin . x)) * (cos . x) hence ((exp_R * sin) `| Z) . x = (exp_R . (sin . x)) * (cos . x) by A3, A4, FDIFF_1:def_7; ::_thesis: verum end; hence ( exp_R * sin is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R * sin) `| Z) . x = (exp_R . (sin . x)) * (cos . x) ) ) by A2, A1, FDIFF_1:9; ::_thesis: verum end; theorem Th38: :: FDIFF_7:38 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) - (sin . x) ) ) 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) - (sin . x) ) ) ) A1: ( sin is_differentiable_on Z & cos is_differentiable_on Z ) by FDIFF_1:26, SIN_COS:67, SIN_COS:68; assume A2: 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) - (sin . x) ) ) now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ ((sin_+_cos)_`|_Z)_._x_=_(cos_._x)_-_(sin_._x) let x be Real; ::_thesis: ( x in Z implies ((sin + cos) `| Z) . x = (cos . x) - (sin . x) ) assume x in Z ; ::_thesis: ((sin + cos) `| Z) . x = (cos . x) - (sin . x) hence ((sin + cos) `| Z) . x = (diff (sin,x)) + (diff (cos,x)) by A2, A1, FDIFF_1:18 .= (cos . x) + (diff (cos,x)) by SIN_COS:64 .= (cos . x) + (- (sin . x)) by SIN_COS:63 .= (cos . x) - (sin . x) ; ::_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) - (sin . x) ) ) by A2, A1, FDIFF_1:18; ::_thesis: verum end; theorem Th39: :: FDIFF_7:39 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) + (sin . x) ) ) 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) + (sin . x) ) ) ) A1: ( sin is_differentiable_on Z & cos is_differentiable_on Z ) by FDIFF_1:26, SIN_COS:67, SIN_COS:68; assume A2: 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) + (sin . x) ) ) now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ ((sin_-_cos)_`|_Z)_._x_=_(cos_._x)_+_(sin_._x) let x be Real; ::_thesis: ( x in Z implies ((sin - cos) `| Z) . x = (cos . x) + (sin . x) ) assume x in Z ; ::_thesis: ((sin - cos) `| Z) . x = (cos . x) + (sin . x) hence ((sin - cos) `| Z) . x = (diff (sin,x)) - (diff (cos,x)) by A2, A1, FDIFF_1:19 .= (cos . x) - (diff (cos,x)) by SIN_COS:64 .= (cos . x) - (- (sin . x)) by SIN_COS:63 .= (cos . x) + (sin . x) ; ::_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) + (sin . x) ) ) by A2, A1, FDIFF_1:19; ::_thesis: verum end; theorem :: FDIFF_7:40 for Z being open Subset of REAL st Z c= dom (exp_R (#) (sin - cos)) holds ( exp_R (#) (sin - cos) is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) (sin - cos)) `| Z) . x = (2 * (exp_R . x)) * (sin . x) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (exp_R (#) (sin - cos)) implies ( exp_R (#) (sin - cos) is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) (sin - cos)) `| Z) . x = (2 * (exp_R . x)) * (sin . x) ) ) ) assume A1: Z c= dom (exp_R (#) (sin - cos)) ; ::_thesis: ( exp_R (#) (sin - cos) is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) (sin - cos)) `| Z) . x = (2 * (exp_R . x)) * (sin . x) ) ) then Z c= (dom (sin - cos)) /\ (dom exp_R) by VALUED_1:def_4; then A2: Z c= dom (sin - cos) by XBOOLE_1:18; then A3: sin - cos is_differentiable_on Z by Th39; 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 (#) (sin - cos)) `| Z) . x = (2 * (exp_R . x)) * (sin . x) proof let x be Real; ::_thesis: ( x in Z implies ((exp_R (#) (sin - cos)) `| Z) . x = (2 * (exp_R . x)) * (sin . x) ) assume A5: x in Z ; ::_thesis: ((exp_R (#) (sin - cos)) `| Z) . x = (2 * (exp_R . x)) * (sin . x) then ((exp_R (#) (sin - cos)) `| Z) . x = (((sin - cos) . x) * (diff (exp_R,x))) + ((exp_R . x) * (diff ((sin - cos),x))) by A1, A3, A4, FDIFF_1:21 .= (((sin . x) - (cos . x)) * (diff (exp_R,x))) + ((exp_R . x) * (diff ((sin - cos),x))) by A2, A5, VALUED_1:13 .= (((sin . x) - (cos . x)) * (exp_R . x)) + ((exp_R . x) * (diff ((sin - cos),x))) by TAYLOR_1:16 .= (((sin . x) - (cos . x)) * (exp_R . x)) + ((exp_R . x) * (((sin - cos) `| Z) . x)) by A3, A5, FDIFF_1:def_7 .= (((sin . x) - (cos . x)) * (exp_R . x)) + ((exp_R . x) * ((cos . x) + (sin . x))) by A2, A5, Th39 .= (2 * (exp_R . x)) * (sin . x) ; hence ((exp_R (#) (sin - cos)) `| Z) . x = (2 * (exp_R . x)) * (sin . x) ; ::_thesis: verum end; hence ( exp_R (#) (sin - cos) is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) (sin - cos)) `| Z) . x = (2 * (exp_R . x)) * (sin . x) ) ) by A1, A3, A4, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_7:41 for Z being open Subset of REAL st Z c= dom (exp_R (#) (sin + cos)) holds ( exp_R (#) (sin + cos) is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) (sin + cos)) `| Z) . x = (2 * (exp_R . x)) * (cos . x) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (exp_R (#) (sin + cos)) implies ( exp_R (#) (sin + cos) is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) (sin + cos)) `| Z) . x = (2 * (exp_R . x)) * (cos . x) ) ) ) assume A1: Z c= dom (exp_R (#) (sin + cos)) ; ::_thesis: ( exp_R (#) (sin + cos) is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) (sin + cos)) `| Z) . x = (2 * (exp_R . x)) * (cos . x) ) ) then Z c= (dom (sin + cos)) /\ (dom exp_R) by VALUED_1:def_4; then A2: Z c= dom (sin + cos) by XBOOLE_1:18; then A3: sin + cos is_differentiable_on Z by Th38; 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 (#) (sin + cos)) `| Z) . x = (2 * (exp_R . x)) * (cos . x) proof let x be Real; ::_thesis: ( x in Z implies ((exp_R (#) (sin + cos)) `| Z) . x = (2 * (exp_R . x)) * (cos . x) ) assume A5: x in Z ; ::_thesis: ((exp_R (#) (sin + cos)) `| Z) . x = (2 * (exp_R . x)) * (cos . x) then ((exp_R (#) (sin + cos)) `| Z) . x = (((sin + cos) . x) * (diff (exp_R,x))) + ((exp_R . x) * (diff ((sin + cos),x))) by A1, A3, A4, FDIFF_1:21 .= (((sin . x) + (cos . x)) * (diff (exp_R,x))) + ((exp_R . x) * (diff ((sin + cos),x))) by VALUED_1:1 .= (((sin . x) + (cos . x)) * (exp_R . x)) + ((exp_R . x) * (diff ((sin + cos),x))) by TAYLOR_1:16 .= (((sin . x) + (cos . x)) * (exp_R . x)) + ((exp_R . x) * (((sin + cos) `| Z) . x)) by A3, A5, FDIFF_1:def_7 .= (((sin . x) + (cos . x)) * (exp_R . x)) + ((exp_R . x) * ((cos . x) - (sin . x))) by A2, A5, Th38 .= (2 * (exp_R . x)) * (cos . x) ; hence ((exp_R (#) (sin + cos)) `| Z) . x = (2 * (exp_R . x)) * (cos . x) ; ::_thesis: verum end; hence ( exp_R (#) (sin + cos) is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) (sin + cos)) `| Z) . x = (2 * (exp_R . x)) * (cos . x) ) ) by A1, A3, A4, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_7:42 for Z being open Subset of REAL st Z c= dom ((sin + cos) / exp_R) holds ( (sin + cos) / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds (((sin + cos) / exp_R) `| Z) . x = - ((2 * (sin . x)) / (exp_R . x)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((sin + cos) / exp_R) implies ( (sin + cos) / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds (((sin + cos) / exp_R) `| Z) . x = - ((2 * (sin . x)) / (exp_R . x)) ) ) ) assume Z c= dom ((sin + cos) / exp_R) ; ::_thesis: ( (sin + cos) / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds (((sin + cos) / exp_R) `| Z) . x = - ((2 * (sin . x)) / (exp_R . x)) ) ) then Z c= (dom (sin + cos)) /\ ((dom exp_R) \ (exp_R " {0})) by RFUNCT_1:def_1; then A1: Z c= dom (sin + cos) by XBOOLE_1:18; then A2: sin + cos is_differentiable_on Z by Th38; A3: ( exp_R is_differentiable_on Z & ( for x being Real st x in Z holds exp_R . x <> 0 ) ) by FDIFF_1:26, SIN_COS:54, TAYLOR_1:16; then A4: (sin + cos) / exp_R is_differentiable_on Z by A2, FDIFF_2:21; for x being Real st x in Z holds (((sin + cos) / exp_R) `| Z) . x = - ((2 * (sin . x)) / (exp_R . x)) proof let x be Real; ::_thesis: ( x in Z implies (((sin + cos) / exp_R) `| Z) . x = - ((2 * (sin . x)) / (exp_R . x)) ) A5: (sin + cos) . x = (sin . x) + (cos . x) by VALUED_1:1; A6: exp_R . x <> 0 by SIN_COS:54; assume A7: x in Z ; ::_thesis: (((sin + cos) / exp_R) `| Z) . x = - ((2 * (sin . x)) / (exp_R . x)) then ( exp_R is_differentiable_in x & sin + cos is_differentiable_in x ) by A2, FDIFF_1:9, SIN_COS:65; then diff (((sin + cos) / exp_R),x) = (((diff ((sin + cos),x)) * (exp_R . x)) - ((diff (exp_R,x)) * ((sin + cos) . x))) / ((exp_R . x) ^2) by A6, FDIFF_2:14 .= (((((sin + cos) `| Z) . x) * (exp_R . x)) - ((diff (exp_R,x)) * ((sin + cos) . x))) / ((exp_R . x) ^2) by A2, A7, FDIFF_1:def_7 .= ((((cos . x) - (sin . x)) * (exp_R . x)) - ((diff (exp_R,x)) * ((sin + cos) . x))) / ((exp_R . x) ^2) by A1, A7, Th38 .= ((((cos . x) - (sin . x)) * (exp_R . x)) - ((exp_R . x) * ((sin . x) + (cos . x)))) / ((exp_R . x) ^2) by A5, SIN_COS:65 .= ((- (2 * (sin . x))) * (exp_R . x)) / ((exp_R . x) * (exp_R . x)) .= (- (2 * (sin . x))) * ((exp_R . x) / ((exp_R . x) * (exp_R . x))) by XCMPLX_1:74 .= (- (2 * (sin . x))) * (((exp_R . x) / (exp_R . x)) / (exp_R . x)) by XCMPLX_1:78 .= (- (2 * (sin . x))) * (1 / (exp_R . x)) by A6, XCMPLX_1:60 .= (- (2 * (sin . x))) / (exp_R . x) by XCMPLX_1:99 .= - ((2 * (sin . x)) / (exp_R . x)) by XCMPLX_1:187 ; hence (((sin + cos) / exp_R) `| Z) . x = - ((2 * (sin . x)) / (exp_R . x)) by A4, A7, FDIFF_1:def_7; ::_thesis: verum end; hence ( (sin + cos) / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds (((sin + cos) / exp_R) `| Z) . x = - ((2 * (sin . x)) / (exp_R . x)) ) ) by A2, A3, FDIFF_2:21; ::_thesis: verum end; theorem :: FDIFF_7:43 for Z being open Subset of REAL st Z c= dom ((sin - cos) / exp_R) holds ( (sin - cos) / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds (((sin - cos) / exp_R) `| Z) . x = (2 * (cos . x)) / (exp_R . x) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((sin - cos) / exp_R) implies ( (sin - cos) / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds (((sin - cos) / exp_R) `| Z) . x = (2 * (cos . x)) / (exp_R . x) ) ) ) assume Z c= dom ((sin - cos) / exp_R) ; ::_thesis: ( (sin - cos) / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds (((sin - cos) / exp_R) `| Z) . x = (2 * (cos . x)) / (exp_R . x) ) ) then Z c= (dom (sin - cos)) /\ ((dom exp_R) \ (exp_R " {0})) by RFUNCT_1:def_1; then A1: Z c= dom (sin - cos) by XBOOLE_1:18; then A2: sin - cos is_differentiable_on Z by Th39; A3: ( exp_R is_differentiable_on Z & ( for x being Real st x in Z holds exp_R . x <> 0 ) ) by FDIFF_1:26, SIN_COS:54, TAYLOR_1:16; then A4: (sin - cos) / exp_R is_differentiable_on Z by A2, FDIFF_2:21; for x being Real st x in Z holds (((sin - cos) / exp_R) `| Z) . x = (2 * (cos . x)) / (exp_R . x) proof let x be Real; ::_thesis: ( x in Z implies (((sin - cos) / exp_R) `| Z) . x = (2 * (cos . x)) / (exp_R . x) ) A5: exp_R . x <> 0 by SIN_COS:54; assume A6: x in Z ; ::_thesis: (((sin - cos) / exp_R) `| Z) . x = (2 * (cos . x)) / (exp_R . x) then A7: (sin - cos) . x = (sin . x) - (cos . x) by A1, VALUED_1:13; ( exp_R is_differentiable_in x & sin - cos is_differentiable_in x ) by A2, A6, FDIFF_1:9, SIN_COS:65; then diff (((sin - cos) / exp_R),x) = (((diff ((sin - cos),x)) * (exp_R . x)) - ((diff (exp_R,x)) * ((sin - cos) . x))) / ((exp_R . x) ^2) by A5, FDIFF_2:14 .= (((((sin - cos) `| Z) . x) * (exp_R . x)) - ((diff (exp_R,x)) * ((sin - cos) . x))) / ((exp_R . x) ^2) by A2, A6, FDIFF_1:def_7 .= ((((cos . x) + (sin . x)) * (exp_R . x)) - ((diff (exp_R,x)) * ((sin - cos) . x))) / ((exp_R . x) ^2) by A1, A6, Th39 .= ((((cos . x) + (sin . x)) * (exp_R . x)) - ((exp_R . x) * ((sin . x) - (cos . x)))) / ((exp_R . x) ^2) by A7, SIN_COS:65 .= ((2 * (cos . x)) * (exp_R . x)) / ((exp_R . x) * (exp_R . x)) .= (2 * (cos . x)) * ((exp_R . x) / ((exp_R . x) * (exp_R . x))) by XCMPLX_1:74 .= (2 * (cos . x)) * (((exp_R . x) / (exp_R . x)) / (exp_R . x)) by XCMPLX_1:78 .= (2 * (cos . x)) * (1 / (exp_R . x)) by A5, XCMPLX_1:60 .= (2 * (cos . x)) / (exp_R . x) by XCMPLX_1:99 ; hence (((sin - cos) / exp_R) `| Z) . x = (2 * (cos . x)) / (exp_R . x) by A4, A6, FDIFF_1:def_7; ::_thesis: verum end; hence ( (sin - cos) / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds (((sin - cos) / exp_R) `| Z) . x = (2 * (cos . x)) / (exp_R . x) ) ) by A2, A3, FDIFF_2:21; ::_thesis: verum end; theorem :: FDIFF_7:44 for Z being open Subset of REAL st Z c= dom (exp_R (#) sin) holds ( exp_R (#) sin is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) sin) `| Z) . x = (exp_R . x) * ((sin . x) + (cos . x)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (exp_R (#) sin) implies ( exp_R (#) sin is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) sin) `| Z) . x = (exp_R . x) * ((sin . x) + (cos . x)) ) ) ) A1: ( sin is_differentiable_on Z & exp_R is_differentiable_on Z ) by FDIFF_1:26, SIN_COS:68, TAYLOR_1:16; assume A2: Z c= dom (exp_R (#) sin) ; ::_thesis: ( exp_R (#) sin is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) sin) `| Z) . x = (exp_R . x) * ((sin . x) + (cos . x)) ) ) now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ ((exp_R_(#)_sin)_`|_Z)_._x_=_(exp_R_._x)_*_((sin_._x)_+_(cos_._x)) let x be Real; ::_thesis: ( x in Z implies ((exp_R (#) sin) `| Z) . x = (exp_R . x) * ((sin . x) + (cos . x)) ) assume x in Z ; ::_thesis: ((exp_R (#) sin) `| Z) . x = (exp_R . x) * ((sin . x) + (cos . x)) hence ((exp_R (#) sin) `| Z) . x = ((sin . x) * (diff (exp_R,x))) + ((exp_R . x) * (diff (sin,x))) by A2, A1, FDIFF_1:21 .= ((sin . x) * (exp_R . x)) + ((exp_R . x) * (diff (sin,x))) by TAYLOR_1:16 .= ((sin . x) * (exp_R . x)) + ((exp_R . x) * (cos . x)) by SIN_COS:64 .= (exp_R . x) * ((sin . x) + (cos . x)) ; ::_thesis: verum end; hence ( exp_R (#) sin is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) sin) `| Z) . x = (exp_R . x) * ((sin . x) + (cos . x)) ) ) by A2, A1, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_7:45 for Z being open Subset of REAL st Z c= dom (exp_R (#) cos) holds ( exp_R (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) cos) `| Z) . x = (exp_R . x) * ((cos . x) - (sin . x)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (exp_R (#) cos) implies ( exp_R (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) cos) `| Z) . x = (exp_R . x) * ((cos . x) - (sin . x)) ) ) ) A1: ( cos is_differentiable_on Z & exp_R is_differentiable_on Z ) by FDIFF_1:26, SIN_COS:67, TAYLOR_1:16; assume A2: Z c= dom (exp_R (#) cos) ; ::_thesis: ( exp_R (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) cos) `| Z) . x = (exp_R . x) * ((cos . x) - (sin . x)) ) ) now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ ((exp_R_(#)_cos)_`|_Z)_._x_=_(exp_R_._x)_*_((cos_._x)_-_(sin_._x)) let x be Real; ::_thesis: ( x in Z implies ((exp_R (#) cos) `| Z) . x = (exp_R . x) * ((cos . x) - (sin . x)) ) assume x in Z ; ::_thesis: ((exp_R (#) cos) `| Z) . x = (exp_R . x) * ((cos . x) - (sin . x)) hence ((exp_R (#) cos) `| Z) . x = ((cos . x) * (diff (exp_R,x))) + ((exp_R . x) * (diff (cos,x))) by A2, A1, FDIFF_1:21 .= ((cos . x) * (exp_R . x)) + ((exp_R . x) * (diff (cos,x))) by TAYLOR_1:16 .= ((cos . x) * (exp_R . x)) + ((exp_R . x) * (- (sin . x))) by SIN_COS:63 .= (exp_R . x) * ((cos . x) - (sin . x)) ; ::_thesis: verum end; hence ( exp_R (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) cos) `| Z) . x = (exp_R . x) * ((cos . x) - (sin . x)) ) ) by A2, A1, FDIFF_1:21; ::_thesis: verum end; theorem Th46: :: FDIFF_7:46 for x being Real st cos . x <> 0 holds ( sin / cos is_differentiable_in x & diff ((sin / cos),x) = 1 / ((cos . x) ^2) ) proof let x be Real; ::_thesis: ( cos . x <> 0 implies ( sin / cos is_differentiable_in x & diff ((sin / cos),x) = 1 / ((cos . x) ^2) ) ) assume A1: cos . x <> 0 ; ::_thesis: ( sin / cos is_differentiable_in x & diff ((sin / cos),x) = 1 / ((cos . x) ^2) ) A2: ( sin is_differentiable_in x & cos is_differentiable_in x ) by SIN_COS:63, SIN_COS:64; then diff ((sin / cos),x) = (((diff (sin,x)) * (cos . x)) - ((diff (cos,x)) * (sin . x))) / ((cos . x) ^2) by A1, FDIFF_2:14 .= (((cos . x) * (cos . x)) - ((diff (cos,x)) * (sin . x))) / ((cos . x) ^2) by SIN_COS:64 .= (((cos . x) * (cos . x)) - ((- (sin . x)) * (sin . x))) / ((cos . x) ^2) by SIN_COS:63 .= (((cos . x) * (cos . x)) + ((sin . x) * (sin . x))) / ((cos . x) ^2) .= 1 / ((cos . x) ^2) by SIN_COS:28 ; hence ( sin / cos is_differentiable_in x & diff ((sin / cos),x) = 1 / ((cos . x) ^2) ) by A2, A1, FDIFF_2:14; ::_thesis: verum end; theorem Th47: :: FDIFF_7:47 for x being Real st sin . x <> 0 holds ( cos / sin is_differentiable_in x & diff ((cos / sin),x) = - (1 / ((sin . x) ^2)) ) proof let x be Real; ::_thesis: ( sin . x <> 0 implies ( cos / sin is_differentiable_in x & diff ((cos / sin),x) = - (1 / ((sin . x) ^2)) ) ) assume A1: sin . x <> 0 ; ::_thesis: ( cos / sin is_differentiable_in x & diff ((cos / sin),x) = - (1 / ((sin . x) ^2)) ) A2: ( sin is_differentiable_in x & cos is_differentiable_in x ) by SIN_COS:63, SIN_COS:64; then diff ((cos / sin),x) = (((diff (cos,x)) * (sin . x)) - ((diff (sin,x)) * (cos . x))) / ((sin . x) ^2) by A1, FDIFF_2:14 .= (((- (sin . x)) * (sin . x)) - ((diff (sin,x)) * (cos . x))) / ((sin . x) ^2) by SIN_COS:63 .= ((- ((sin . x) * (sin . x))) - ((cos . x) * (cos . x))) / ((sin . x) ^2) by SIN_COS:64 .= (- (((cos . x) ^2) + ((sin . x) * (sin . x)))) / ((sin . x) ^2) .= - ((((cos . x) ^2) + ((sin . x) ^2)) / ((sin . x) ^2)) by XCMPLX_1:187 .= - (1 / ((sin . x) ^2)) by SIN_COS:28 ; hence ( cos / sin is_differentiable_in x & diff ((cos / sin),x) = - (1 / ((sin . x) ^2)) ) by A2, A1, FDIFF_2:14; ::_thesis: verum end; theorem :: FDIFF_7:48 for Z being open Subset of REAL st Z c= dom ((#Z 2) * (sin / cos)) & ( for x being Real st x in Z holds cos . x <> 0 ) holds ( (#Z 2) * (sin / cos) is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z 2) * (sin / cos)) `| Z) . x = (2 * (sin . x)) / ((cos . x) #Z 3) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((#Z 2) * (sin / cos)) & ( for x being Real st x in Z holds cos . x <> 0 ) implies ( (#Z 2) * (sin / cos) is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z 2) * (sin / cos)) `| Z) . x = (2 * (sin . x)) / ((cos . x) #Z 3) ) ) ) assume that A1: Z c= dom ((#Z 2) * (sin / cos)) and A2: for x being Real st x in Z holds cos . x <> 0 ; ::_thesis: ( (#Z 2) * (sin / cos) is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z 2) * (sin / cos)) `| Z) . x = (2 * (sin . x)) / ((cos . x) #Z 3) ) ) for y being set st y in Z holds y in dom (sin / cos) by A1, FUNCT_1:11; then A3: Z c= dom (sin / cos) by TARSKI:def_3; A4: for x being Real st x in Z holds (#Z 2) * (sin / cos) is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies (#Z 2) * (sin / cos) is_differentiable_in x ) assume x in Z ; ::_thesis: (#Z 2) * (sin / cos) is_differentiable_in x then cos . x <> 0 by A2; then sin / cos is_differentiable_in x by Th46; hence (#Z 2) * (sin / cos) is_differentiable_in x by TAYLOR_1:3; ::_thesis: verum end; then A5: (#Z 2) * (sin / cos) is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds (((#Z 2) * (sin / cos)) `| Z) . x = (2 * (sin . x)) / ((cos . x) #Z 3) proof let x be Real; ::_thesis: ( x in Z implies (((#Z 2) * (sin / cos)) `| Z) . x = (2 * (sin . x)) / ((cos . x) #Z 3) ) assume A6: x in Z ; ::_thesis: (((#Z 2) * (sin / cos)) `| Z) . x = (2 * (sin . x)) / ((cos . x) #Z 3) then A7: (sin / cos) . x = (sin . x) * ((cos . x) ") by A3, RFUNCT_1:def_1 .= (sin . x) * (1 / (cos . x)) by XCMPLX_1:215 .= (sin . x) / (cos . x) by XCMPLX_1:99 ; A8: cos . x <> 0 by A2, A6; then A9: sin / cos is_differentiable_in x by Th46; (((#Z 2) * (sin / cos)) `| Z) . x = diff (((#Z 2) * (sin / cos)),x) by A5, A6, FDIFF_1:def_7 .= (2 * (((sin / cos) . x) #Z (2 - 1))) * (diff ((sin / cos),x)) by A9, TAYLOR_1:3 .= (2 * (((sin / cos) . x) #Z (2 - 1))) * (1 / ((cos . x) ^2)) by A8, Th46 .= (2 * (((sin / cos) . x) #Z 1)) / ((cos . x) ^2) by XCMPLX_1:99 .= (2 * ((sin . x) / (cos . x))) / ((cos . x) ^2) by A7, PREPOWER:35 .= ((2 * (sin . x)) / (cos . x)) / ((cos . x) ^2) by XCMPLX_1:74 .= (2 * (sin . x)) / ((cos . x) * ((cos . x) ^2)) by XCMPLX_1:78 .= (2 * (sin . x)) / ((cos . x) * ((cos . x) #Z 2)) by Th1 .= (2 * (sin . x)) / (((cos . x) #Z 1) * ((cos . x) #Z 2)) by PREPOWER:35 .= (2 * (sin . x)) / ((cos . x) #Z (1 + 2)) by A2, A6, PREPOWER:44 .= (2 * (sin . x)) / ((cos . x) #Z 3) ; hence (((#Z 2) * (sin / cos)) `| Z) . x = (2 * (sin . x)) / ((cos . x) #Z 3) ; ::_thesis: verum end; hence ( (#Z 2) * (sin / cos) is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z 2) * (sin / cos)) `| Z) . x = (2 * (sin . x)) / ((cos . x) #Z 3) ) ) by A1, A4, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_7:49 for Z being open Subset of REAL st Z c= dom ((#Z 2) * (cos / sin)) & ( for x being Real st x in Z holds sin . x <> 0 ) holds ( (#Z 2) * (cos / sin) is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z 2) * (cos / sin)) `| Z) . x = - ((2 * (cos . x)) / ((sin . x) #Z 3)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((#Z 2) * (cos / sin)) & ( for x being Real st x in Z holds sin . x <> 0 ) implies ( (#Z 2) * (cos / sin) is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z 2) * (cos / sin)) `| Z) . x = - ((2 * (cos . x)) / ((sin . x) #Z 3)) ) ) ) assume that A1: Z c= dom ((#Z 2) * (cos / sin)) and A2: for x being Real st x in Z holds sin . x <> 0 ; ::_thesis: ( (#Z 2) * (cos / sin) is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z 2) * (cos / sin)) `| Z) . x = - ((2 * (cos . x)) / ((sin . x) #Z 3)) ) ) for y being set st y in Z holds y in dom (cos / sin) by A1, FUNCT_1:11; then A3: Z c= dom (cos / sin) by TARSKI:def_3; A4: for x being Real st x in Z holds (#Z 2) * (cos / sin) is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies (#Z 2) * (cos / sin) is_differentiable_in x ) assume x in Z ; ::_thesis: (#Z 2) * (cos / sin) is_differentiable_in x then sin . x <> 0 by A2; then cos / sin is_differentiable_in x by Th47; hence (#Z 2) * (cos / sin) is_differentiable_in x by TAYLOR_1:3; ::_thesis: verum end; then A5: (#Z 2) * (cos / sin) is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds (((#Z 2) * (cos / sin)) `| Z) . x = - ((2 * (cos . x)) / ((sin . x) #Z 3)) proof let x be Real; ::_thesis: ( x in Z implies (((#Z 2) * (cos / sin)) `| Z) . x = - ((2 * (cos . x)) / ((sin . x) #Z 3)) ) assume A6: x in Z ; ::_thesis: (((#Z 2) * (cos / sin)) `| Z) . x = - ((2 * (cos . x)) / ((sin . x) #Z 3)) then A7: (cos / sin) . x = (cos . x) * ((sin . x) ") by A3, RFUNCT_1:def_1 .= (cos . x) * (1 / (sin . x)) by XCMPLX_1:215 .= (cos . x) / (sin . x) by XCMPLX_1:99 ; A8: sin . x <> 0 by A2, A6; then A9: cos / sin is_differentiable_in x by Th47; (((#Z 2) * (cos / sin)) `| Z) . x = diff (((#Z 2) * (cos / sin)),x) by A5, A6, FDIFF_1:def_7 .= (2 * (((cos / sin) . x) #Z (2 - 1))) * (diff ((cos / sin),x)) by A9, TAYLOR_1:3 .= (2 * (((cos / sin) . x) #Z (2 - 1))) * (- (1 / ((sin . x) ^2))) by A8, Th47 .= - ((2 * (((cos / sin) . x) #Z (2 - 1))) * (1 / ((sin . x) ^2))) .= - ((2 * (((cos / sin) . x) #Z 1)) / ((sin . x) ^2)) by XCMPLX_1:99 .= - ((2 * ((cos . x) / (sin . x))) / ((sin . x) ^2)) by A7, PREPOWER:35 .= - (((2 * (cos . x)) / (sin . x)) / ((sin . x) ^2)) by XCMPLX_1:74 .= - ((2 * (cos . x)) / ((sin . x) * ((sin . x) ^2))) by XCMPLX_1:78 .= - ((2 * (cos . x)) / ((sin . x) * ((sin . x) #Z 2))) by Th1 .= - ((2 * (cos . x)) / (((sin . x) #Z 1) * ((sin . x) #Z 2))) by PREPOWER:35 .= - ((2 * (cos . x)) / ((sin . x) #Z (1 + 2))) by A2, A6, PREPOWER:44 .= - ((2 * (cos . x)) / ((sin . x) #Z 3)) ; hence (((#Z 2) * (cos / sin)) `| Z) . x = - ((2 * (cos . x)) / ((sin . x) #Z 3)) ; ::_thesis: verum end; hence ( (#Z 2) * (cos / sin) is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z 2) * (cos / sin)) `| Z) . x = - ((2 * (cos . x)) / ((sin . x) #Z 3)) ) ) by A1, A4, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_7:50 for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((sin / cos) * f) & ( for x being Real st x in Z holds ( f . x = x / 2 & cos . (f . x) <> 0 ) ) holds ( (sin / cos) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((sin / cos) * f) `| Z) . x = 1 / (1 + (cos . x)) ) ) proof let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom ((sin / cos) * f) & ( for x being Real st x in Z holds ( f . x = x / 2 & cos . (f . x) <> 0 ) ) holds ( (sin / cos) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((sin / cos) * f) `| Z) . x = 1 / (1 + (cos . x)) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom ((sin / cos) * f) & ( for x being Real st x in Z holds ( f . x = x / 2 & cos . (f . x) <> 0 ) ) implies ( (sin / cos) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((sin / cos) * f) `| Z) . x = 1 / (1 + (cos . x)) ) ) ) assume that A1: Z c= dom ((sin / cos) * f) and A2: for x being Real st x in Z holds ( f . x = x / 2 & cos . (f . x) <> 0 ) ; ::_thesis: ( (sin / cos) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((sin / cos) * f) `| Z) . x = 1 / (1 + (cos . x)) ) ) A3: for x being Real st x in Z holds f . x = ((1 / 2) * x) + 0 proof let x be Real; ::_thesis: ( x in Z implies f . x = ((1 / 2) * x) + 0 ) assume x in Z ; ::_thesis: f . x = ((1 / 2) * x) + 0 then f . x = x / 2 by A2; hence f . x = ((1 / 2) * x) + 0 ; ::_thesis: verum end; for y being set st y in Z holds y in dom f by A1, FUNCT_1:11; then A4: Z c= dom f by TARSKI:def_3; then A5: f is_differentiable_on Z by A3, FDIFF_1:23; A6: for x being Real st x in Z holds (sin / cos) * f is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies (sin / cos) * f is_differentiable_in x ) assume A7: x in Z ; ::_thesis: (sin / cos) * f is_differentiable_in x then cos . (f . x) <> 0 by A2; then A8: sin / cos is_differentiable_in f . x by Th46; f is_differentiable_in x by A5, A7, FDIFF_1:9; hence (sin / cos) * f is_differentiable_in x by A8, FDIFF_2:13; ::_thesis: verum end; then A9: (sin / cos) * f is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds (((sin / cos) * f) `| Z) . x = 1 / (1 + (cos . x)) proof let x be Real; ::_thesis: ( x in Z implies (((sin / cos) * f) `| Z) . x = 1 / (1 + (cos . x)) ) assume A10: x in Z ; ::_thesis: (((sin / cos) * f) `| Z) . x = 1 / (1 + (cos . x)) then A11: f is_differentiable_in x by A5, FDIFF_1:9; A12: cos . (f . x) <> 0 by A2, A10; then sin / cos is_differentiable_in f . x by Th46; then diff (((sin / cos) * f),x) = (diff ((sin / cos),(f . x))) * (diff (f,x)) by A11, FDIFF_2:13 .= (1 / ((cos . (f . x)) ^2)) * (diff (f,x)) by A12, Th46 .= (diff (f,x)) / ((cos . (f . x)) ^2) by XCMPLX_1:99 .= (diff (f,x)) / ((cos . (x / 2)) ^2) by A2, A10 .= ((f `| Z) . x) / ((cos . (x / 2)) ^2) by A5, A10, FDIFF_1:def_7 .= (1 / 2) / ((cos . (x / 2)) ^2) by A3, A4, A10, FDIFF_1:23 .= 1 / (2 * ((cos . (x / 2)) ^2)) by XCMPLX_1:78 .= 1 / (1 + (cos . x)) by Lm1 ; hence (((sin / cos) * f) `| Z) . x = 1 / (1 + (cos . x)) by A9, A10, FDIFF_1:def_7; ::_thesis: verum end; hence ( (sin / cos) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((sin / cos) * f) `| Z) . x = 1 / (1 + (cos . x)) ) ) by A1, A6, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_7:51 for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((cos / sin) * f) & ( for x being Real st x in Z holds ( f . x = x / 2 & sin . (f . x) <> 0 ) ) holds ( (cos / sin) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((cos / sin) * f) `| Z) . x = - (1 / (1 - (cos . x))) ) ) proof let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom ((cos / sin) * f) & ( for x being Real st x in Z holds ( f . x = x / 2 & sin . (f . x) <> 0 ) ) holds ( (cos / sin) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((cos / sin) * f) `| Z) . x = - (1 / (1 - (cos . x))) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom ((cos / sin) * f) & ( for x being Real st x in Z holds ( f . x = x / 2 & sin . (f . x) <> 0 ) ) implies ( (cos / sin) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((cos / sin) * f) `| Z) . x = - (1 / (1 - (cos . x))) ) ) ) assume that A1: Z c= dom ((cos / sin) * f) and A2: for x being Real st x in Z holds ( f . x = x / 2 & sin . (f . x) <> 0 ) ; ::_thesis: ( (cos / sin) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((cos / sin) * f) `| Z) . x = - (1 / (1 - (cos . x))) ) ) A3: for x being Real st x in Z holds f . x = ((1 / 2) * x) + 0 proof let x be Real; ::_thesis: ( x in Z implies f . x = ((1 / 2) * x) + 0 ) assume x in Z ; ::_thesis: f . x = ((1 / 2) * x) + 0 then f . x = x / 2 by A2; hence f . x = ((1 / 2) * x) + 0 ; ::_thesis: verum end; for y being set st y in Z holds y in dom f by A1, FUNCT_1:11; then A4: Z c= dom f by TARSKI:def_3; then A5: f is_differentiable_on Z by A3, FDIFF_1:23; A6: for x being Real st x in Z holds (cos / sin) * f is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies (cos / sin) * f is_differentiable_in x ) assume A7: x in Z ; ::_thesis: (cos / sin) * f is_differentiable_in x then sin . (f . x) <> 0 by A2; then A8: cos / sin is_differentiable_in f . x by Th47; f is_differentiable_in x by A5, A7, FDIFF_1:9; hence (cos / sin) * f is_differentiable_in x by A8, FDIFF_2:13; ::_thesis: verum end; then A9: (cos / sin) * f is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds (((cos / sin) * f) `| Z) . x = - (1 / (1 - (cos . x))) proof let x be Real; ::_thesis: ( x in Z implies (((cos / sin) * f) `| Z) . x = - (1 / (1 - (cos . x))) ) assume A10: x in Z ; ::_thesis: (((cos / sin) * f) `| Z) . x = - (1 / (1 - (cos . x))) then A11: f is_differentiable_in x by A5, FDIFF_1:9; A12: sin . (f . x) <> 0 by A2, A10; then cos / sin is_differentiable_in f . x by Th47; then diff (((cos / sin) * f),x) = (diff ((cos / sin),(f . x))) * (diff (f,x)) by A11, FDIFF_2:13 .= (- (1 / ((sin . (f . x)) ^2))) * (diff (f,x)) by A12, Th47 .= - ((1 / ((sin . (f . x)) ^2)) * (diff (f,x))) .= - ((diff (f,x)) / ((sin . (f . x)) ^2)) by XCMPLX_1:99 .= - ((diff (f,x)) / ((sin . (x / 2)) ^2)) by A2, A10 .= - (((f `| Z) . x) / ((sin . (x / 2)) ^2)) by A5, A10, FDIFF_1:def_7 .= - ((1 / 2) / ((sin . (x / 2)) ^2)) by A3, A4, A10, FDIFF_1:23 .= - (1 / (2 * ((sin . (x / 2)) ^2))) by XCMPLX_1:78 .= - (1 / (1 - (cos . x))) by Lm2 ; hence (((cos / sin) * f) `| Z) . x = - (1 / (1 - (cos . x))) by A9, A10, FDIFF_1:def_7; ::_thesis: verum end; hence ( (cos / sin) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((cos / sin) * f) `| Z) . x = - (1 / (1 - (cos . x))) ) ) by A1, A6, FDIFF_1:9; ::_thesis: verum end;