:: DIFF_4 semantic presentation begin theorem Th1: :: DIFF_4:1 for x0, x1 being Real st x0 > 0 & x1 > 0 holds (log (number_e,x0)) - (log (number_e,x1)) = log (number_e,(x0 / x1)) proof let x0, x1 be Real; ::_thesis: ( x0 > 0 & x1 > 0 implies (log (number_e,x0)) - (log (number_e,x1)) = log (number_e,(x0 / x1)) ) assume A1: ( x0 > 0 & x1 > 0 ) ; ::_thesis: (log (number_e,x0)) - (log (number_e,x1)) = log (number_e,(x0 / x1)) number_e > 1 by TAYLOR_1:11, XXREAL_0:2; hence (log (number_e,x0)) - (log (number_e,x1)) = log (number_e,(x0 / x1)) by A1, POWER:54; ::_thesis: verum end; theorem :: DIFF_4:2 for x0, x1 being Real st x0 > 0 & x1 > 0 holds (log (number_e,x0)) + (log (number_e,x1)) = log (number_e,(x0 * x1)) proof let x0, x1 be Real; ::_thesis: ( x0 > 0 & x1 > 0 implies (log (number_e,x0)) + (log (number_e,x1)) = log (number_e,(x0 * x1)) ) assume A1: ( x0 > 0 & x1 > 0 ) ; ::_thesis: (log (number_e,x0)) + (log (number_e,x1)) = log (number_e,(x0 * x1)) number_e > 1 by TAYLOR_1:11, XXREAL_0:2; hence (log (number_e,x0)) + (log (number_e,x1)) = log (number_e,(x0 * x1)) by A1, POWER:53; ::_thesis: verum end; theorem Th3: :: DIFF_4:3 for x being Real st x > 0 holds log (number_e,x) = ln . x proof let x be Real; ::_thesis: ( x > 0 implies log (number_e,x) = ln . x ) assume A1: x > 0 ; ::_thesis: log (number_e,x) = ln . x x in right_open_halfline 0 proof x in { g where g is Real : 0 < g } by A1; hence x in right_open_halfline 0 by XXREAL_1:230; ::_thesis: verum end; hence log (number_e,x) = ln . x by TAYLOR_1:def_2; ::_thesis: verum end; theorem Th4: :: DIFF_4:4 for x0, x1 being Real st x0 > 0 & x1 > 0 holds (ln . x0) - (ln . x1) = ln . (x0 / x1) proof let x0, x1 be Real; ::_thesis: ( x0 > 0 & x1 > 0 implies (ln . x0) - (ln . x1) = ln . (x0 / x1) ) assume A1: ( x0 > 0 & x1 > 0 ) ; ::_thesis: (ln . x0) - (ln . x1) = ln . (x0 / x1) A2: log (number_e,(x0 / x1)) = ln . (x0 / x1) proof A3: x0 / x1 in REAL by XREAL_0:def_1; x0 / x1 in right_open_halfline 0 proof x0 / x1 in { g where g is Real : 0 < g } by A1, A3; hence x0 / x1 in right_open_halfline 0 by XXREAL_1:230; ::_thesis: verum end; hence log (number_e,(x0 / x1)) = ln . (x0 / x1) by TAYLOR_1:def_2; ::_thesis: verum end; (ln . x0) - (ln . x1) = (log (number_e,x0)) - (ln . x1) by A1, Th3 .= (log (number_e,x0)) - (log (number_e,x1)) by A1, Th3 .= log (number_e,(x0 / x1)) by A1, Th1 ; hence (ln . x0) - (ln . x1) = ln . (x0 / x1) by A2; ::_thesis: verum end; theorem :: DIFF_4:5 for k, x0, x1, x2, x3 being Real for f being Function of REAL,REAL st ( for x being Real holds f . x = k / (x ^2) ) & x0 <> 0 & x1 <> 0 & x2 <> 0 & x3 <> 0 & x0,x1,x2,x3 are_mutually_different holds [!f,x0,x1,x2,x3!] = (k * (((1 / ((x1 * x2) * x0)) * (((1 / x0) + (1 / x2)) + (1 / x1))) - ((1 / ((x2 * x1) * x3)) * (((1 / x3) + (1 / x1)) + (1 / x2))))) / (x0 - x3) proof let k, x0, x1, x2, x3 be Real; ::_thesis: for f being Function of REAL,REAL st ( for x being Real holds f . x = k / (x ^2) ) & x0 <> 0 & x1 <> 0 & x2 <> 0 & x3 <> 0 & x0,x1,x2,x3 are_mutually_different holds [!f,x0,x1,x2,x3!] = (k * (((1 / ((x1 * x2) * x0)) * (((1 / x0) + (1 / x2)) + (1 / x1))) - ((1 / ((x2 * x1) * x3)) * (((1 / x3) + (1 / x1)) + (1 / x2))))) / (x0 - x3) let f be Function of REAL,REAL; ::_thesis: ( ( for x being Real holds f . x = k / (x ^2) ) & x0 <> 0 & x1 <> 0 & x2 <> 0 & x3 <> 0 & x0,x1,x2,x3 are_mutually_different implies [!f,x0,x1,x2,x3!] = (k * (((1 / ((x1 * x2) * x0)) * (((1 / x0) + (1 / x2)) + (1 / x1))) - ((1 / ((x2 * x1) * x3)) * (((1 / x3) + (1 / x1)) + (1 / x2))))) / (x0 - x3) ) assume that A1: for x being Real holds f . x = k / (x ^2) and A2: ( x0 <> 0 & x1 <> 0 & x2 <> 0 & x3 <> 0 ) and A3: x0,x1,x2,x3 are_mutually_different ; ::_thesis: [!f,x0,x1,x2,x3!] = (k * (((1 / ((x1 * x2) * x0)) * (((1 / x0) + (1 / x2)) + (1 / x1))) - ((1 / ((x2 * x1) * x3)) * (((1 / x3) + (1 / x1)) + (1 / x2))))) / (x0 - x3) ( x0 <> x1 & x0 <> x2 & x1 <> x2 ) by A3, ZFMISC_1:def_6; then x0,x1,x2 are_mutually_different by ZFMISC_1:def_5; then A4: [!f,x0,x1,x2!] = (k / ((x0 * x1) * x2)) * (((1 / x0) + (1 / x1)) + (1 / x2)) by A1, A2, DIFF_3:49 .= (k * (1 / ((x1 * x2) * x0))) * (((1 / x0) + (1 / x2)) + (1 / x1)) ; ( x1 <> x2 & x1 <> x3 & x2 <> x3 ) by A3, ZFMISC_1:def_6; then x1,x2,x3 are_mutually_different by ZFMISC_1:def_5; then [!f,x1,x2,x3!] = (k / ((x1 * x2) * x3)) * (((1 / x1) + (1 / x2)) + (1 / x3)) by A1, A2, DIFF_3:49; hence [!f,x0,x1,x2,x3!] = (k * (((1 / ((x1 * x2) * x0)) * (((1 / x0) + (1 / x2)) + (1 / x1))) - ((1 / ((x2 * x1) * x3)) * (((1 / x3) + (1 / x1)) + (1 / x2))))) / (x0 - x3) by A4; ::_thesis: verum end; theorem :: DIFF_4:6 for x0, x1 being Real st x0 in dom cot & x1 in dom cot holds [!(cot (#) cot),x0,x1!] = - ((((cos x1) ^2) - ((cos x0) ^2)) / ((((sin x0) * (sin x1)) ^2) * (x0 - x1))) proof let x0, x1 be Real; ::_thesis: ( x0 in dom cot & x1 in dom cot implies [!(cot (#) cot),x0,x1!] = - ((((cos x1) ^2) - ((cos x0) ^2)) / ((((sin x0) * (sin x1)) ^2) * (x0 - x1))) ) assume A1: ( x0 in dom cot & x1 in dom cot ) ; ::_thesis: [!(cot (#) cot),x0,x1!] = - ((((cos x1) ^2) - ((cos x0) ^2)) / ((((sin x0) * (sin x1)) ^2) * (x0 - x1))) A2: ( sin x0 <> 0 & sin x1 <> 0 ) by A1, FDIFF_8:2; [!(cot (#) cot),x0,x1!] = (((cot . x0) * (cot . x0)) - ((cot (#) cot) . x1)) / (x0 - x1) by VALUED_1:5 .= (((cot . x0) * (cot . x0)) - ((cot . x1) * (cot . x1))) / (x0 - x1) by VALUED_1:5 .= ((((cos . x0) * ((sin . x0) ")) * (cot . x0)) - ((cot . x1) * (cot . x1))) / (x0 - x1) by A1, RFUNCT_1:def_1 .= ((((cos . x0) * ((sin . x0) ")) * ((cos . x0) * ((sin . x0) "))) - ((cot . x1) * (cot . x1))) / (x0 - x1) by A1, RFUNCT_1:def_1 .= ((((cos . x0) * ((sin . x0) ")) * ((cos . x0) * ((sin . x0) "))) - (((cos . x1) * ((sin . x1) ")) * (cot . x1))) / (x0 - x1) by A1, RFUNCT_1:def_1 .= (((cot x0) ^2) - ((cot x1) ^2)) / (x0 - x1) by A1, RFUNCT_1:def_1 .= (((cot x0) - (cot x1)) * ((cot x0) + (cot x1))) / (x0 - x1) .= ((- ((sin (x0 - x1)) / ((sin x0) * (sin x1)))) * ((cot x0) + (cot x1))) / (x0 - x1) by A2, SIN_COS4:24 .= (- (((sin (x0 - x1)) / ((sin x0) * (sin x1))) * ((cot x0) + (cot x1)))) / (x0 - x1) .= (- (((sin (x0 - x1)) / ((sin x0) * (sin x1))) * ((sin (x0 + x1)) / ((sin x0) * (sin x1))))) / (x0 - x1) by A2, SIN_COS4:23 .= (- (((sin (x0 + x1)) * (sin (x0 - x1))) / (((sin x0) * (sin x1)) ^2))) / (x0 - x1) by XCMPLX_1:76 .= (- ((((cos x1) ^2) - ((cos x0) ^2)) / (((sin x0) * (sin x1)) ^2))) / (x0 - x1) by SIN_COS4:38 .= - (((((cos x1) ^2) - ((cos x0) ^2)) / (((sin x0) * (sin x1)) ^2)) / (x0 - x1)) .= - ((((cos x1) ^2) - ((cos x0) ^2)) / ((((sin x0) * (sin x1)) ^2) * (x0 - x1))) by XCMPLX_1:78 ; hence [!(cot (#) cot),x0,x1!] = - ((((cos x1) ^2) - ((cos x0) ^2)) / ((((sin x0) * (sin x1)) ^2) * (x0 - x1))) ; ::_thesis: verum end; theorem :: DIFF_4:7 for x, h being Real st x in dom cot & x + h in dom cot holds (fD ((cot (#) cot),h)) . x = ((1 / 2) * ((cos (2 * (x + h))) - (cos (2 * x)))) / (((sin (x + h)) * (sin x)) ^2) proof let x, h be Real; ::_thesis: ( x in dom cot & x + h in dom cot implies (fD ((cot (#) cot),h)) . x = ((1 / 2) * ((cos (2 * (x + h))) - (cos (2 * x)))) / (((sin (x + h)) * (sin x)) ^2) ) set f = cot (#) cot; assume A1: ( x in dom cot & x + h in dom cot ) ; ::_thesis: (fD ((cot (#) cot),h)) . x = ((1 / 2) * ((cos (2 * (x + h))) - (cos (2 * x)))) / (((sin (x + h)) * (sin x)) ^2) A2: ( sin x <> 0 & sin (x + h) <> 0 ) by A1, FDIFF_8:2; ( x in dom (cot (#) cot) & x + h in dom (cot (#) cot) ) proof ( x in (dom cot) /\ (dom cot) & x + h in (dom cot) /\ (dom cot) ) by A1; hence ( x in dom (cot (#) cot) & x + h in dom (cot (#) cot) ) by VALUED_1:def_4; ::_thesis: verum end; then (fD ((cot (#) cot),h)) . x = ((cot (#) cot) . (x + h)) - ((cot (#) cot) . x) by DIFF_1:1 .= ((cot . (x + h)) * (cot . (x + h))) - ((cot (#) cot) . x) by VALUED_1:5 .= ((cot . (x + h)) * (cot . (x + h))) - ((cot . x) * (cot . x)) by VALUED_1:5 .= (((cos . (x + h)) * ((sin . (x + h)) ")) * (cot . (x + h))) - ((cot . x) * (cot . x)) by A1, RFUNCT_1:def_1 .= (((cos . (x + h)) * ((sin . (x + h)) ")) * ((cos . (x + h)) * ((sin . (x + h)) "))) - ((cot . x) * (cot . x)) by A1, RFUNCT_1:def_1 .= (((cos . (x + h)) * ((sin . (x + h)) ")) * ((cos . (x + h)) * ((sin . (x + h)) "))) - (((cos . x) * ((sin . x) ")) * (cot . x)) by A1, RFUNCT_1:def_1 .= ((cot (x + h)) ^2) - ((cot x) ^2) by A1, RFUNCT_1:def_1 .= ((cot (x + h)) - (cot x)) * ((cot (x + h)) + (cot x)) .= (- ((sin ((x + h) - x)) / ((sin (x + h)) * (sin x)))) * ((cot (x + h)) + (cot x)) by A2, SIN_COS4:24 .= (- ((sin ((x + h) - x)) / ((sin (x + h)) * (sin x)))) * ((sin ((x + h) + x)) / ((sin (x + h)) * (sin x))) by A2, SIN_COS4:23 .= - (((sin ((x + h) - x)) / ((sin (x + h)) * (sin x))) * ((sin ((x + h) + x)) / ((sin (x + h)) * (sin x)))) .= - (((sin ((2 * x) + h)) * (sin h)) / (((sin (x + h)) * (sin x)) ^2)) by XCMPLX_1:76 .= - ((- ((1 / 2) * ((cos (((2 * x) + h) + h)) - (cos (((2 * x) + h) - h))))) / (((sin (x + h)) * (sin x)) ^2)) by SIN_COS4:29 .= ((1 / 2) * ((cos (2 * (x + h))) - (cos (2 * x)))) / (((sin (x + h)) * (sin x)) ^2) ; hence (fD ((cot (#) cot),h)) . x = ((1 / 2) * ((cos (2 * (x + h))) - (cos (2 * x)))) / (((sin (x + h)) * (sin x)) ^2) ; ::_thesis: verum end; theorem :: DIFF_4:8 for x, h being Real st x in dom cot & x - h in dom cot holds (bD ((cot (#) cot),h)) . x = ((1 / 2) * ((cos (2 * x)) - (cos (2 * (h - x))))) / (((sin x) * (sin (x - h))) ^2) proof let x, h be Real; ::_thesis: ( x in dom cot & x - h in dom cot implies (bD ((cot (#) cot),h)) . x = ((1 / 2) * ((cos (2 * x)) - (cos (2 * (h - x))))) / (((sin x) * (sin (x - h))) ^2) ) set f = cot (#) cot; assume A1: ( x in dom cot & x - h in dom cot ) ; ::_thesis: (bD ((cot (#) cot),h)) . x = ((1 / 2) * ((cos (2 * x)) - (cos (2 * (h - x))))) / (((sin x) * (sin (x - h))) ^2) A2: ( sin x <> 0 & sin (x - h) <> 0 ) by A1, FDIFF_8:2; ( x in dom (cot (#) cot) & x - h in dom (cot (#) cot) ) proof ( x in (dom cot) /\ (dom cot) & x - h in (dom cot) /\ (dom cot) ) by A1; hence ( x in dom (cot (#) cot) & x - h in dom (cot (#) cot) ) by VALUED_1:def_4; ::_thesis: verum end; then (bD ((cot (#) cot),h)) . x = ((cot (#) cot) . x) - ((cot (#) cot) . (x - h)) by DIFF_1:38 .= ((cot . x) * (cot . x)) - ((cot (#) cot) . (x - h)) by VALUED_1:5 .= ((cot . x) * (cot . x)) - ((cot . (x - h)) * (cot . (x - h))) by VALUED_1:5 .= (((cos . x) * ((sin . x) ")) * (cot . x)) - ((cot . (x - h)) * (cot . (x - h))) by A1, RFUNCT_1:def_1 .= (((cos . x) * ((sin . x) ")) * ((cos . x) * ((sin . x) "))) - ((cot . (x - h)) * (cot . (x - h))) by A1, RFUNCT_1:def_1 .= (((cos . x) * ((sin . x) ")) * ((cos . x) * ((sin . x) "))) - (((cos . (x - h)) * ((sin . (x - h)) ")) * (cot . (x - h))) by A1, RFUNCT_1:def_1 .= ((cot x) ^2) - ((cot (x - h)) ^2) by A1, RFUNCT_1:def_1 .= ((cot x) - (cot (x - h))) * ((cot x) + (cot (x - h))) .= (- ((sin (x - (x - h))) / ((sin x) * (sin (x - h))))) * ((cot x) + (cot (x - h))) by A2, SIN_COS4:24 .= - (((sin (x - (x - h))) / ((sin x) * (sin (x - h)))) * ((cot x) + (cot (x - h)))) .= - (((sin h) / ((sin x) * (sin (x - h)))) * ((sin (x + (x - h))) / ((sin x) * (sin (x - h))))) by A2, SIN_COS4:23 .= - (((sin h) * (sin ((2 * x) - h))) / (((sin x) * (sin (x - h))) ^2)) by XCMPLX_1:76 .= - ((- ((1 / 2) * ((cos (h + ((2 * x) - h))) - (cos (h - ((2 * x) - h)))))) / (((sin x) * (sin (x - h))) ^2)) by SIN_COS4:29 .= ((1 / 2) * ((cos (2 * x)) - (cos (2 * (h - x))))) / (((sin x) * (sin (x - h))) ^2) ; hence (bD ((cot (#) cot),h)) . x = ((1 / 2) * ((cos (2 * x)) - (cos (2 * (h - x))))) / (((sin x) * (sin (x - h))) ^2) ; ::_thesis: verum end; theorem :: DIFF_4:9 for x, h being Real st x + (h / 2) in dom cot & x - (h / 2) in dom cot holds (cD ((cot (#) cot),h)) . x = ((1 / 2) * ((cos (h + (2 * x))) - (cos (h - (2 * x))))) / (((sin (x + (h / 2))) * (sin (x - (h / 2)))) ^2) proof let x, h be Real; ::_thesis: ( x + (h / 2) in dom cot & x - (h / 2) in dom cot implies (cD ((cot (#) cot),h)) . x = ((1 / 2) * ((cos (h + (2 * x))) - (cos (h - (2 * x))))) / (((sin (x + (h / 2))) * (sin (x - (h / 2)))) ^2) ) set f = cot (#) cot; assume A1: ( x + (h / 2) in dom cot & x - (h / 2) in dom cot ) ; ::_thesis: (cD ((cot (#) cot),h)) . x = ((1 / 2) * ((cos (h + (2 * x))) - (cos (h - (2 * x))))) / (((sin (x + (h / 2))) * (sin (x - (h / 2)))) ^2) A2: ( sin (x + (h / 2)) <> 0 & sin (x - (h / 2)) <> 0 ) by A1, FDIFF_8:2; ( x + (h / 2) in dom (cot (#) cot) & x - (h / 2) in dom (cot (#) cot) ) proof ( x + (h / 2) in (dom cot) /\ (dom cot) & x - (h / 2) in (dom cot) /\ (dom cot) ) by A1; hence ( x + (h / 2) in dom (cot (#) cot) & x - (h / 2) in dom (cot (#) cot) ) by VALUED_1:def_4; ::_thesis: verum end; then (cD ((cot (#) cot),h)) . x = ((cot (#) cot) . (x + (h / 2))) - ((cot (#) cot) . (x - (h / 2))) by DIFF_1:39 .= ((cot . (x + (h / 2))) * (cot . (x + (h / 2)))) - ((cot (#) cot) . (x - (h / 2))) by VALUED_1:5 .= ((cot . (x + (h / 2))) * (cot . (x + (h / 2)))) - ((cot . (x - (h / 2))) * (cot . (x - (h / 2)))) by VALUED_1:5 .= (((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) ")) * (cot . (x + (h / 2)))) - ((cot . (x - (h / 2))) * (cot . (x - (h / 2)))) by A1, RFUNCT_1:def_1 .= (((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) ")) * ((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) "))) - ((cot . (x - (h / 2))) * (cot . (x - (h / 2)))) by A1, RFUNCT_1:def_1 .= (((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) ")) * ((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) "))) - (((cos . (x - (h / 2))) * ((sin . (x - (h / 2))) ")) * (cot . (x - (h / 2)))) by A1, RFUNCT_1:def_1 .= ((cot (x + (h / 2))) ^2) - ((cot (x - (h / 2))) ^2) by A1, RFUNCT_1:def_1 .= ((cot (x + (h / 2))) - (cot (x - (h / 2)))) * ((cot (x + (h / 2))) + (cot (x - (h / 2)))) .= (- ((sin ((x + (h / 2)) - (x - (h / 2)))) / ((sin (x + (h / 2))) * (sin (x - (h / 2)))))) * ((cot (x + (h / 2))) + (cot (x - (h / 2)))) by A2, SIN_COS4:24 .= (- ((sin h) / ((sin (x + (h / 2))) * (sin (x - (h / 2)))))) * ((sin ((x + (h / 2)) + (x - (h / 2)))) / ((sin (x + (h / 2))) * (sin (x - (h / 2))))) by A2, SIN_COS4:23 .= - (((sin h) / ((sin (x + (h / 2))) * (sin (x - (h / 2))))) * ((sin ((x + (h / 2)) + (x - (h / 2)))) / ((sin (x + (h / 2))) * (sin (x - (h / 2)))))) .= - (((sin h) * (sin (2 * x))) / (((sin (x + (h / 2))) * (sin (x - (h / 2)))) ^2)) by XCMPLX_1:76 .= - ((- ((1 / 2) * ((cos (h + (2 * x))) - (cos (h - (2 * x)))))) / (((sin (x + (h / 2))) * (sin (x - (h / 2)))) ^2)) by SIN_COS4:29 .= ((1 / 2) * ((cos (h + (2 * x))) - (cos (h - (2 * x))))) / (((sin (x + (h / 2))) * (sin (x - (h / 2)))) ^2) ; hence (cD ((cot (#) cot),h)) . x = ((1 / 2) * ((cos (h + (2 * x))) - (cos (h - (2 * x))))) / (((sin (x + (h / 2))) * (sin (x - (h / 2)))) ^2) ; ::_thesis: verum end; theorem :: DIFF_4:10 for x0, x1 being Real st x0 in dom cosec & x1 in dom cosec holds [!(cosec (#) cosec),x0,x1!] = (4 * ((sin (x1 + x0)) * (sin (x1 - x0)))) / ((((cos (x0 + x1)) - (cos (x0 - x1))) ^2) * (x0 - x1)) proof let x0, x1 be Real; ::_thesis: ( x0 in dom cosec & x1 in dom cosec implies [!(cosec (#) cosec),x0,x1!] = (4 * ((sin (x1 + x0)) * (sin (x1 - x0)))) / ((((cos (x0 + x1)) - (cos (x0 - x1))) ^2) * (x0 - x1)) ) assume A1: ( x0 in dom cosec & x1 in dom cosec ) ; ::_thesis: [!(cosec (#) cosec),x0,x1!] = (4 * ((sin (x1 + x0)) * (sin (x1 - x0)))) / ((((cos (x0 + x1)) - (cos (x0 - x1))) ^2) * (x0 - x1)) A2: ( sin . x0 <> 0 & sin . x1 <> 0 ) by A1, RFUNCT_1:3; [!(cosec (#) cosec),x0,x1!] = (((cosec . x0) * (cosec . x0)) - ((cosec (#) cosec) . x1)) / (x0 - x1) by VALUED_1:5 .= (((cosec . x0) * (cosec . x0)) - ((cosec . x1) * (cosec . x1))) / (x0 - x1) by VALUED_1:5 .= ((((sin . x0) ") * (cosec . x0)) - ((cosec . x1) * (cosec . x1))) / (x0 - x1) by A1, RFUNCT_1:def_2 .= ((((sin . x0) ") * ((sin . x0) ")) - ((cosec . x1) * (cosec . x1))) / (x0 - x1) by A1, RFUNCT_1:def_2 .= ((((sin . x0) ") * ((sin . x0) ")) - (((sin . x1) ") * (cosec . x1))) / (x0 - x1) by A1, RFUNCT_1:def_2 .= ((((sin . x0) ") ^2) - (((sin . x1) ") ^2)) / (x0 - x1) by A1, RFUNCT_1:def_2 .= (((1 / (sin . x0)) - (1 / (sin . x1))) * ((1 / (sin . x0)) + (1 / (sin . x1)))) / (x0 - x1) .= ((((1 * (sin . x1)) - (1 * (sin . x0))) / ((sin . x0) * (sin . x1))) * ((1 / (sin . x0)) + (1 / (sin . x1)))) / (x0 - x1) by A2, XCMPLX_1:130 .= ((((sin . x1) - (sin . x0)) / ((sin . x0) * (sin . x1))) * (((sin . x1) + (sin . x0)) / ((sin . x0) * (sin . x1)))) / (x0 - x1) by A2, XCMPLX_1:116 .= ((((sin . x1) - (sin . x0)) * ((sin . x1) + (sin . x0))) / (((sin . x0) * (sin . x1)) * ((sin . x0) * (sin . x1)))) / (x0 - x1) by XCMPLX_1:76 .= ((((sin x1) * (sin x1)) - ((sin x0) * (sin x0))) / (((sin x0) * (sin x1)) ^2)) / (x0 - x1) .= (((sin (x1 + x0)) * (sin (x1 - x0))) / (((sin x0) * (sin x1)) ^2)) / (x0 - x1) by SIN_COS4:37 .= (((sin (x1 + x0)) * (sin (x1 - x0))) / ((- ((1 / 2) * ((cos (x0 + x1)) - (cos (x0 - x1))))) ^2)) / (x0 - x1) by SIN_COS4:29 .= ((1 * ((sin (x1 + x0)) * (sin (x1 - x0)))) / ((1 / 4) * (((cos (x0 + x1)) - (cos (x0 - x1))) ^2))) / (x0 - x1) .= ((1 / (1 / 4)) * (((sin (x1 + x0)) * (sin (x1 - x0))) / (((cos (x0 + x1)) - (cos (x0 - x1))) ^2))) / (x0 - x1) by XCMPLX_1:76 .= ((4 * ((sin (x1 + x0)) * (sin (x1 - x0)))) / (((cos (x0 + x1)) - (cos (x0 - x1))) ^2)) / (x0 - x1) .= (4 * ((sin (x1 + x0)) * (sin (x1 - x0)))) / ((((cos (x0 + x1)) - (cos (x0 - x1))) ^2) * (x0 - x1)) by XCMPLX_1:78 ; hence [!(cosec (#) cosec),x0,x1!] = (4 * ((sin (x1 + x0)) * (sin (x1 - x0)))) / ((((cos (x0 + x1)) - (cos (x0 - x1))) ^2) * (x0 - x1)) ; ::_thesis: verum end; theorem :: DIFF_4:11 for x, h being Real st x in dom cosec & x + h in dom cosec holds (fD ((cosec (#) cosec),h)) . x = - (((4 * (sin ((2 * x) + h))) * (sin h)) / (((cos ((2 * x) + h)) - (cos h)) ^2)) proof let x, h be Real; ::_thesis: ( x in dom cosec & x + h in dom cosec implies (fD ((cosec (#) cosec),h)) . x = - (((4 * (sin ((2 * x) + h))) * (sin h)) / (((cos ((2 * x) + h)) - (cos h)) ^2)) ) set f = cosec (#) cosec; assume A1: ( x in dom cosec & x + h in dom cosec ) ; ::_thesis: (fD ((cosec (#) cosec),h)) . x = - (((4 * (sin ((2 * x) + h))) * (sin h)) / (((cos ((2 * x) + h)) - (cos h)) ^2)) A2: ( sin . x <> 0 & sin . (x + h) <> 0 ) by A1, RFUNCT_1:3; ( x in dom (cosec (#) cosec) & x + h in dom (cosec (#) cosec) ) proof ( x in (dom cosec) /\ (dom cosec) & x + h in (dom cosec) /\ (dom cosec) ) by A1; hence ( x in dom (cosec (#) cosec) & x + h in dom (cosec (#) cosec) ) by VALUED_1:def_4; ::_thesis: verum end; then (fD ((cosec (#) cosec),h)) . x = ((cosec (#) cosec) . (x + h)) - ((cosec (#) cosec) . x) by DIFF_1:1 .= ((cosec . (x + h)) * (cosec . (x + h))) - ((cosec (#) cosec) . x) by VALUED_1:5 .= ((cosec . (x + h)) * (cosec . (x + h))) - ((cosec . x) * (cosec . x)) by VALUED_1:5 .= (((sin . (x + h)) ") * (cosec . (x + h))) - ((cosec . x) * (cosec . x)) by A1, RFUNCT_1:def_2 .= (((sin . (x + h)) ") * ((sin . (x + h)) ")) - ((cosec . x) * (cosec . x)) by A1, RFUNCT_1:def_2 .= (((sin . (x + h)) ") * ((sin . (x + h)) ")) - (((sin . x) ") * (cosec . x)) by A1, RFUNCT_1:def_2 .= (((sin . (x + h)) ") ^2) - (((sin . x) ") ^2) by A1, RFUNCT_1:def_2 .= ((1 / (sin . (x + h))) - (1 / (sin . x))) * ((1 / (sin . (x + h))) + (1 / (sin . x))) .= (((1 * (sin . x)) - (1 * (sin . (x + h)))) / ((sin . (x + h)) * (sin . x))) * ((1 / (sin . (x + h))) + (1 / (sin . x))) by A2, XCMPLX_1:130 .= (((sin . x) - (sin . (x + h))) / ((sin . (x + h)) * (sin . x))) * (((sin . x) + (sin . (x + h))) / ((sin . (x + h)) * (sin . x))) by A2, XCMPLX_1:116 .= (((sin . x) - (sin . (x + h))) * ((sin . x) + (sin . (x + h)))) / (((sin . (x + h)) * (sin . x)) * ((sin . (x + h)) * (sin . x))) by XCMPLX_1:76 .= (((sin x) * (sin x)) - ((sin (x + h)) * (sin (x + h)))) / (((sin (x + h)) * (sin x)) ^2) .= ((sin (x + (x + h))) * (sin (x - (x + h)))) / (((sin (x + h)) * (sin x)) ^2) by SIN_COS4:37 .= ((sin ((2 * x) + h)) * (sin (- h))) / ((- ((1 / 2) * ((cos ((x + h) + x)) - (cos ((x + h) - x))))) ^2) by SIN_COS4:29 .= ((sin ((2 * x) + h)) * (- (sin h))) / ((1 / 4) * (((cos ((2 * x) + h)) - (cos h)) ^2)) by SIN_COS:31 .= - ((1 * ((sin ((2 * x) + h)) * (sin h))) / ((1 / 4) * (((cos ((2 * x) + h)) - (cos h)) ^2))) .= - ((1 / (1 / 4)) * (((sin ((2 * x) + h)) * (sin h)) / (((cos ((2 * x) + h)) - (cos h)) ^2))) by XCMPLX_1:76 .= - (((4 * (sin ((2 * x) + h))) * (sin h)) / (((cos ((2 * x) + h)) - (cos h)) ^2)) ; hence (fD ((cosec (#) cosec),h)) . x = - (((4 * (sin ((2 * x) + h))) * (sin h)) / (((cos ((2 * x) + h)) - (cos h)) ^2)) ; ::_thesis: verum end; theorem :: DIFF_4:12 for x, h being Real st x in dom cosec & x - h in dom cosec holds (bD ((cosec (#) cosec),h)) . x = - (((4 * (sin ((2 * x) - h))) * (sin h)) / (((cos ((2 * x) - h)) - (cos h)) ^2)) proof let x, h be Real; ::_thesis: ( x in dom cosec & x - h in dom cosec implies (bD ((cosec (#) cosec),h)) . x = - (((4 * (sin ((2 * x) - h))) * (sin h)) / (((cos ((2 * x) - h)) - (cos h)) ^2)) ) set f = cosec (#) cosec; assume A1: ( x in dom cosec & x - h in dom cosec ) ; ::_thesis: (bD ((cosec (#) cosec),h)) . x = - (((4 * (sin ((2 * x) - h))) * (sin h)) / (((cos ((2 * x) - h)) - (cos h)) ^2)) A2: ( sin . x <> 0 & sin . (x - h) <> 0 ) by A1, RFUNCT_1:3; ( x in dom (cosec (#) cosec) & x - h in dom (cosec (#) cosec) ) proof ( x in (dom cosec) /\ (dom cosec) & x - h in (dom cosec) /\ (dom cosec) ) by A1; hence ( x in dom (cosec (#) cosec) & x - h in dom (cosec (#) cosec) ) by VALUED_1:def_4; ::_thesis: verum end; then (bD ((cosec (#) cosec),h)) . x = ((cosec (#) cosec) . x) - ((cosec (#) cosec) . (x - h)) by DIFF_1:38 .= ((cosec . x) * (cosec . x)) - ((cosec (#) cosec) . (x - h)) by VALUED_1:5 .= ((cosec . x) * (cosec . x)) - ((cosec . (x - h)) * (cosec . (x - h))) by VALUED_1:5 .= (((sin . x) ") * (cosec . x)) - ((cosec . (x - h)) * (cosec . (x - h))) by A1, RFUNCT_1:def_2 .= (((sin . x) ") * ((sin . x) ")) - ((cosec . (x - h)) * (cosec . (x - h))) by A1, RFUNCT_1:def_2 .= (((sin . x) ") * ((sin . x) ")) - (((sin . (x - h)) ") * (cosec . (x - h))) by A1, RFUNCT_1:def_2 .= (((sin . x) ") ^2) - (((sin . (x - h)) ") ^2) by A1, RFUNCT_1:def_2 .= ((1 / (sin . x)) - (1 / (sin . (x - h)))) * ((1 / (sin . x)) + (1 / (sin . (x - h)))) .= (((1 * (sin . (x - h))) - (1 * (sin . x))) / ((sin . x) * (sin . (x - h)))) * ((1 / (sin . x)) + (1 / (sin . (x - h)))) by A2, XCMPLX_1:130 .= (((sin . (x - h)) - (sin . x)) / ((sin . x) * (sin . (x - h)))) * (((sin . (x - h)) + (sin . x)) / ((sin . x) * (sin . (x - h)))) by A2, XCMPLX_1:116 .= (((sin . (x - h)) - (sin . x)) * ((sin . (x - h)) + (sin . x))) / (((sin . x) * (sin . (x - h))) * ((sin . x) * (sin . (x - h)))) by XCMPLX_1:76 .= (((sin (x - h)) * (sin (x - h))) - ((sin x) * (sin x))) / (((sin x) * (sin (x - h))) ^2) .= ((sin ((x - h) + x)) * (sin ((x - h) - x))) / (((sin x) * (sin (x - h))) ^2) by SIN_COS4:37 .= ((sin ((2 * x) - h)) * (sin (- h))) / ((- ((1 / 2) * ((cos (x + (x - h))) - (cos (x - (x - h)))))) ^2) by SIN_COS4:29 .= ((sin ((2 * x) - h)) * (- (sin h))) / ((1 / 4) * (((cos ((2 * x) - h)) - (cos h)) ^2)) by SIN_COS:31 .= - ((1 * ((sin ((2 * x) - h)) * (sin h))) / ((1 / 4) * (((cos ((2 * x) - h)) - (cos h)) ^2))) .= - ((1 / (1 / 4)) * (((sin ((2 * x) - h)) * (sin h)) / (((cos ((2 * x) - h)) - (cos h)) ^2))) by XCMPLX_1:76 .= - (((4 * (sin ((2 * x) - h))) * (sin h)) / (((cos ((2 * x) - h)) - (cos h)) ^2)) ; hence (bD ((cosec (#) cosec),h)) . x = - (((4 * (sin ((2 * x) - h))) * (sin h)) / (((cos ((2 * x) - h)) - (cos h)) ^2)) ; ::_thesis: verum end; theorem :: DIFF_4:13 for x, h being Real st x + (h / 2) in dom cosec & x - (h / 2) in dom cosec holds (cD ((cosec (#) cosec),h)) . x = - (((4 * (sin (2 * x))) * (sin h)) / (((cos (2 * x)) - (cos h)) ^2)) proof let x, h be Real; ::_thesis: ( x + (h / 2) in dom cosec & x - (h / 2) in dom cosec implies (cD ((cosec (#) cosec),h)) . x = - (((4 * (sin (2 * x))) * (sin h)) / (((cos (2 * x)) - (cos h)) ^2)) ) set f = cosec (#) cosec; assume A1: ( x + (h / 2) in dom cosec & x - (h / 2) in dom cosec ) ; ::_thesis: (cD ((cosec (#) cosec),h)) . x = - (((4 * (sin (2 * x))) * (sin h)) / (((cos (2 * x)) - (cos h)) ^2)) A2: ( sin . (x + (h / 2)) <> 0 & sin . (x - (h / 2)) <> 0 ) by A1, RFUNCT_1:3; ( x + (h / 2) in dom (cosec (#) cosec) & x - (h / 2) in dom (cosec (#) cosec) ) proof ( x + (h / 2) in (dom cosec) /\ (dom cosec) & x - (h / 2) in (dom cosec) /\ (dom cosec) ) by A1; hence ( x + (h / 2) in dom (cosec (#) cosec) & x - (h / 2) in dom (cosec (#) cosec) ) by VALUED_1:def_4; ::_thesis: verum end; then (cD ((cosec (#) cosec),h)) . x = ((cosec (#) cosec) . (x + (h / 2))) - ((cosec (#) cosec) . (x - (h / 2))) by DIFF_1:39 .= ((cosec . (x + (h / 2))) * (cosec . (x + (h / 2)))) - ((cosec (#) cosec) . (x - (h / 2))) by VALUED_1:5 .= ((cosec . (x + (h / 2))) * (cosec . (x + (h / 2)))) - ((cosec . (x - (h / 2))) * (cosec . (x - (h / 2)))) by VALUED_1:5 .= (((sin . (x + (h / 2))) ") * (cosec . (x + (h / 2)))) - ((cosec . (x - (h / 2))) * (cosec . (x - (h / 2)))) by A1, RFUNCT_1:def_2 .= (((sin . (x + (h / 2))) ") * ((sin . (x + (h / 2))) ")) - ((cosec . (x - (h / 2))) * (cosec . (x - (h / 2)))) by A1, RFUNCT_1:def_2 .= (((sin . (x + (h / 2))) ") * ((sin . (x + (h / 2))) ")) - (((sin . (x - (h / 2))) ") * (cosec . (x - (h / 2)))) by A1, RFUNCT_1:def_2 .= (((sin . (x + (h / 2))) ") ^2) - (((sin . (x - (h / 2))) ") ^2) by A1, RFUNCT_1:def_2 .= ((1 / (sin . (x + (h / 2)))) - (1 / (sin . (x - (h / 2))))) * ((1 / (sin . (x + (h / 2)))) + (1 / (sin . (x - (h / 2))))) .= (((1 * (sin . (x - (h / 2)))) - (1 * (sin . (x + (h / 2))))) / ((sin . (x + (h / 2))) * (sin . (x - (h / 2))))) * ((1 / (sin . (x + (h / 2)))) + (1 / (sin . (x - (h / 2))))) by A2, XCMPLX_1:130 .= (((sin . (x - (h / 2))) - (sin . (x + (h / 2)))) / ((sin . (x + (h / 2))) * (sin . (x - (h / 2))))) * (((sin . (x - (h / 2))) + (sin . (x + (h / 2)))) / ((sin . (x + (h / 2))) * (sin . (x - (h / 2))))) by A2, XCMPLX_1:116 .= (((sin . (x - (h / 2))) - (sin . (x + (h / 2)))) * ((sin . (x - (h / 2))) + (sin . (x + (h / 2))))) / (((sin . (x + (h / 2))) * (sin . (x - (h / 2)))) * ((sin . (x + (h / 2))) * (sin . (x - (h / 2))))) by XCMPLX_1:76 .= (((sin (x - (h / 2))) * (sin (x - (h / 2)))) - ((sin (x + (h / 2))) * (sin (x + (h / 2))))) / (((sin (x + (h / 2))) * (sin (x - (h / 2)))) ^2) .= ((sin ((x - (h / 2)) + (x + (h / 2)))) * (sin ((x - (h / 2)) - (x + (h / 2))))) / (((sin (x + (h / 2))) * (sin (x - (h / 2)))) ^2) by SIN_COS4:37 .= ((sin (2 * x)) * (sin (- h))) / ((- ((1 / 2) * ((cos ((x + (h / 2)) + (x - (h / 2)))) - (cos ((x + (h / 2)) - (x - (h / 2))))))) ^2) by SIN_COS4:29 .= ((sin (2 * x)) * (- (sin h))) / ((1 / 4) * (((cos (2 * x)) - (cos h)) ^2)) by SIN_COS:31 .= - ((1 * ((sin (2 * x)) * (sin h))) / ((1 / 4) * (((cos (2 * x)) - (cos h)) ^2))) .= - ((1 / (1 / 4)) * (((sin (2 * x)) * (sin h)) / (((cos (2 * x)) - (cos h)) ^2))) by XCMPLX_1:76 .= - (((4 * (sin (2 * x))) * (sin h)) / (((cos (2 * x)) - (cos h)) ^2)) ; hence (cD ((cosec (#) cosec),h)) . x = - (((4 * (sin (2 * x))) * (sin h)) / (((cos (2 * x)) - (cos h)) ^2)) ; ::_thesis: verum end; theorem :: DIFF_4:14 for x0, x1 being Real st x0 in dom sec & x1 in dom sec holds [!(sec (#) sec),x0,x1!] = (4 * ((sin (x0 + x1)) * (sin (x0 - x1)))) / ((((cos (x0 + x1)) + (cos (x0 - x1))) ^2) * (x0 - x1)) proof let x0, x1 be Real; ::_thesis: ( x0 in dom sec & x1 in dom sec implies [!(sec (#) sec),x0,x1!] = (4 * ((sin (x0 + x1)) * (sin (x0 - x1)))) / ((((cos (x0 + x1)) + (cos (x0 - x1))) ^2) * (x0 - x1)) ) assume A1: ( x0 in dom sec & x1 in dom sec ) ; ::_thesis: [!(sec (#) sec),x0,x1!] = (4 * ((sin (x0 + x1)) * (sin (x0 - x1)))) / ((((cos (x0 + x1)) + (cos (x0 - x1))) ^2) * (x0 - x1)) A2: ( cos . x0 <> 0 & cos . x1 <> 0 ) by A1, RFUNCT_1:3; [!(sec (#) sec),x0,x1!] = (((sec . x0) * (sec . x0)) - ((sec (#) sec) . x1)) / (x0 - x1) by VALUED_1:5 .= (((sec . x0) * (sec . x0)) - ((sec . x1) * (sec . x1))) / (x0 - x1) by VALUED_1:5 .= ((((cos . x0) ") * (sec . x0)) - ((sec . x1) * (sec . x1))) / (x0 - x1) by A1, RFUNCT_1:def_2 .= ((((cos . x0) ") * ((cos . x0) ")) - ((sec . x1) * (sec . x1))) / (x0 - x1) by A1, RFUNCT_1:def_2 .= ((((cos . x0) ") * ((cos . x0) ")) - (((cos . x1) ") * (sec . x1))) / (x0 - x1) by A1, RFUNCT_1:def_2 .= ((((cos . x0) ") ^2) - (((cos . x1) ") ^2)) / (x0 - x1) by A1, RFUNCT_1:def_2 .= (((1 / (cos . x0)) - (1 / (cos . x1))) * ((1 / (cos . x0)) + (1 / (cos . x1)))) / (x0 - x1) .= ((((1 * (cos . x1)) - (1 * (cos . x0))) / ((cos . x0) * (cos . x1))) * ((1 / (cos . x0)) + (1 / (cos . x1)))) / (x0 - x1) by A2, XCMPLX_1:130 .= ((((cos . x1) - (cos . x0)) / ((cos . x0) * (cos . x1))) * (((cos . x1) + (cos . x0)) / ((cos . x0) * (cos . x1)))) / (x0 - x1) by A2, XCMPLX_1:116 .= ((((cos . x1) - (cos . x0)) * ((cos . x1) + (cos . x0))) / (((cos . x0) * (cos . x1)) * ((cos . x0) * (cos . x1)))) / (x0 - x1) by XCMPLX_1:76 .= ((((cos x1) * (cos x1)) - ((cos x0) * (cos x0))) / (((cos x0) * (cos x1)) ^2)) / (x0 - x1) .= (((sin (x0 + x1)) * (sin (x0 - x1))) / (((cos x0) * (cos x1)) ^2)) / (x0 - x1) by SIN_COS4:38 .= (((sin (x0 + x1)) * (sin (x0 - x1))) / (((1 / 2) * ((cos (x0 + x1)) + (cos (x0 - x1)))) ^2)) / (x0 - x1) by SIN_COS4:32 .= ((1 * ((sin (x0 + x1)) * (sin (x0 - x1)))) / ((1 / 4) * (((cos (x0 + x1)) + (cos (x0 - x1))) ^2))) / (x0 - x1) .= ((1 / (1 / 4)) * (((sin (x0 + x1)) * (sin (x0 - x1))) / (((cos (x0 + x1)) + (cos (x0 - x1))) ^2))) / (x0 - x1) by XCMPLX_1:76 .= ((4 * ((sin (x0 + x1)) * (sin (x0 - x1)))) / (((cos (x0 + x1)) + (cos (x0 - x1))) ^2)) / (x0 - x1) .= (4 * ((sin (x0 + x1)) * (sin (x0 - x1)))) / ((((cos (x0 + x1)) + (cos (x0 - x1))) ^2) * (x0 - x1)) by XCMPLX_1:78 ; hence [!(sec (#) sec),x0,x1!] = (4 * ((sin (x0 + x1)) * (sin (x0 - x1)))) / ((((cos (x0 + x1)) + (cos (x0 - x1))) ^2) * (x0 - x1)) ; ::_thesis: verum end; theorem :: DIFF_4:15 for x, h being Real st x in dom sec & x + h in dom sec holds (fD ((sec (#) sec),h)) . x = ((4 * (sin ((2 * x) + h))) * (sin h)) / (((cos ((2 * x) + h)) + (cos h)) ^2) proof let x, h be Real; ::_thesis: ( x in dom sec & x + h in dom sec implies (fD ((sec (#) sec),h)) . x = ((4 * (sin ((2 * x) + h))) * (sin h)) / (((cos ((2 * x) + h)) + (cos h)) ^2) ) set f = sec (#) sec; assume A1: ( x in dom sec & x + h in dom sec ) ; ::_thesis: (fD ((sec (#) sec),h)) . x = ((4 * (sin ((2 * x) + h))) * (sin h)) / (((cos ((2 * x) + h)) + (cos h)) ^2) A2: ( cos . x <> 0 & cos . (x + h) <> 0 ) by A1, RFUNCT_1:3; ( x in dom (sec (#) sec) & x + h in dom (sec (#) sec) ) proof ( x in (dom sec) /\ (dom sec) & x + h in (dom sec) /\ (dom sec) ) by A1; hence ( x in dom (sec (#) sec) & x + h in dom (sec (#) sec) ) by VALUED_1:def_4; ::_thesis: verum end; then (fD ((sec (#) sec),h)) . x = ((sec (#) sec) . (x + h)) - ((sec (#) sec) . x) by DIFF_1:1 .= ((sec . (x + h)) * (sec . (x + h))) - ((sec (#) sec) . x) by VALUED_1:5 .= ((sec . (x + h)) * (sec . (x + h))) - ((sec . x) * (sec . x)) by VALUED_1:5 .= (((cos . (x + h)) ") * (sec . (x + h))) - ((sec . x) * (sec . x)) by A1, RFUNCT_1:def_2 .= (((cos . (x + h)) ") * ((cos . (x + h)) ")) - ((sec . x) * (sec . x)) by A1, RFUNCT_1:def_2 .= (((cos . (x + h)) ") * ((cos . (x + h)) ")) - (((cos . x) ") * (sec . x)) by A1, RFUNCT_1:def_2 .= (((cos . (x + h)) ") ^2) - (((cos . x) ") ^2) by A1, RFUNCT_1:def_2 .= ((1 / (cos . (x + h))) - (1 / (cos . x))) * ((1 / (cos . (x + h))) + (1 / (cos . x))) .= (((1 * (cos . x)) - (1 * (cos . (x + h)))) / ((cos . (x + h)) * (cos . x))) * ((1 / (cos . (x + h))) + (1 / (cos . x))) by A2, XCMPLX_1:130 .= (((cos . x) - (cos . (x + h))) / ((cos . (x + h)) * (cos . x))) * (((cos . x) + (cos . (x + h))) / ((cos . (x + h)) * (cos . x))) by A2, XCMPLX_1:116 .= (((cos . x) - (cos . (x + h))) * ((cos . x) + (cos . (x + h)))) / (((cos . (x + h)) * (cos . x)) * ((cos . (x + h)) * (cos . x))) by XCMPLX_1:76 .= (((cos x) * (cos x)) - ((cos (x + h)) * (cos (x + h)))) / (((cos (x + h)) * (cos x)) ^2) .= ((sin ((x + h) + x)) * (sin ((x + h) - x))) / (((cos (x + h)) * (cos x)) ^2) by SIN_COS4:38 .= ((sin ((2 * x) + h)) * (sin h)) / (((1 / 2) * ((cos ((x + h) + x)) + (cos ((x + h) - x)))) ^2) by SIN_COS4:32 .= (1 * ((sin ((2 * x) + h)) * (sin h))) / ((1 / 4) * (((cos ((2 * x) + h)) + (cos h)) ^2)) .= (1 / (1 / 4)) * (((sin ((2 * x) + h)) * (sin h)) / (((cos ((2 * x) + h)) + (cos h)) ^2)) by XCMPLX_1:76 .= ((4 * (sin ((2 * x) + h))) * (sin h)) / (((cos ((2 * x) + h)) + (cos h)) ^2) ; hence (fD ((sec (#) sec),h)) . x = ((4 * (sin ((2 * x) + h))) * (sin h)) / (((cos ((2 * x) + h)) + (cos h)) ^2) ; ::_thesis: verum end; theorem :: DIFF_4:16 for x, h being Real st x in dom sec & x - h in dom sec holds (bD ((sec (#) sec),h)) . x = ((4 * (sin ((2 * x) - h))) * (sin h)) / (((cos ((2 * x) - h)) + (cos h)) ^2) proof let x, h be Real; ::_thesis: ( x in dom sec & x - h in dom sec implies (bD ((sec (#) sec),h)) . x = ((4 * (sin ((2 * x) - h))) * (sin h)) / (((cos ((2 * x) - h)) + (cos h)) ^2) ) set f = sec (#) sec; assume A1: ( x in dom sec & x - h in dom sec ) ; ::_thesis: (bD ((sec (#) sec),h)) . x = ((4 * (sin ((2 * x) - h))) * (sin h)) / (((cos ((2 * x) - h)) + (cos h)) ^2) A2: ( cos . x <> 0 & cos . (x - h) <> 0 ) by A1, RFUNCT_1:3; ( x in dom (sec (#) sec) & x - h in dom (sec (#) sec) ) proof ( x in (dom sec) /\ (dom sec) & x - h in (dom sec) /\ (dom sec) ) by A1; hence ( x in dom (sec (#) sec) & x - h in dom (sec (#) sec) ) by VALUED_1:def_4; ::_thesis: verum end; then (bD ((sec (#) sec),h)) . x = ((sec (#) sec) . x) - ((sec (#) sec) . (x - h)) by DIFF_1:38 .= ((sec . x) * (sec . x)) - ((sec (#) sec) . (x - h)) by VALUED_1:5 .= ((sec . x) * (sec . x)) - ((sec . (x - h)) * (sec . (x - h))) by VALUED_1:5 .= (((cos . x) ") * (sec . x)) - ((sec . (x - h)) * (sec . (x - h))) by A1, RFUNCT_1:def_2 .= (((cos . x) ") * ((cos . x) ")) - ((sec . (x - h)) * (sec . (x - h))) by A1, RFUNCT_1:def_2 .= (((cos . x) ") * ((cos . x) ")) - (((cos . (x - h)) ") * (sec . (x - h))) by A1, RFUNCT_1:def_2 .= (((cos . x) ") ^2) - (((cos . (x - h)) ") ^2) by A1, RFUNCT_1:def_2 .= ((1 / (cos . x)) - (1 / (cos . (x - h)))) * ((1 / (cos . x)) + (1 / (cos . (x - h)))) .= (((1 * (cos . (x - h))) - (1 * (cos . x))) / ((cos . x) * (cos . (x - h)))) * ((1 / (cos . x)) + (1 / (cos . (x - h)))) by A2, XCMPLX_1:130 .= (((cos . (x - h)) - (cos . x)) / ((cos . x) * (cos . (x - h)))) * (((cos . (x - h)) + (cos . x)) / ((cos . x) * (cos . (x - h)))) by A2, XCMPLX_1:116 .= (((cos . (x - h)) - (cos . x)) * ((cos . (x - h)) + (cos . x))) / (((cos . x) * (cos . (x - h))) * ((cos . x) * (cos . (x - h)))) by XCMPLX_1:76 .= (((cos (x - h)) * (cos (x - h))) - ((cos x) * (cos x))) / (((cos x) * (cos (x - h))) ^2) .= ((sin (x + (x - h))) * (sin (x - (x - h)))) / (((cos x) * (cos (x - h))) ^2) by SIN_COS4:38 .= ((sin ((2 * x) - h)) * (sin h)) / (((1 / 2) * ((cos (x + (x - h))) + (cos (x - (x - h))))) ^2) by SIN_COS4:32 .= (1 * ((sin ((2 * x) - h)) * (sin h))) / ((1 / 4) * (((cos ((2 * x) - h)) + (cos h)) ^2)) .= (1 / (1 / 4)) * (((sin ((2 * x) - h)) * (sin h)) / (((cos ((2 * x) - h)) + (cos h)) ^2)) by XCMPLX_1:76 .= ((4 * (sin ((2 * x) - h))) * (sin h)) / (((cos ((2 * x) - h)) + (cos h)) ^2) ; hence (bD ((sec (#) sec),h)) . x = ((4 * (sin ((2 * x) - h))) * (sin h)) / (((cos ((2 * x) - h)) + (cos h)) ^2) ; ::_thesis: verum end; theorem :: DIFF_4:17 for x, h being Real st x + (h / 2) in dom sec & x - (h / 2) in dom sec holds (cD ((sec (#) sec),h)) . x = ((4 * (sin (2 * x))) * (sin h)) / (((cos (2 * x)) + (cos h)) ^2) proof let x, h be Real; ::_thesis: ( x + (h / 2) in dom sec & x - (h / 2) in dom sec implies (cD ((sec (#) sec),h)) . x = ((4 * (sin (2 * x))) * (sin h)) / (((cos (2 * x)) + (cos h)) ^2) ) set f = sec (#) sec; assume A1: ( x + (h / 2) in dom sec & x - (h / 2) in dom sec ) ; ::_thesis: (cD ((sec (#) sec),h)) . x = ((4 * (sin (2 * x))) * (sin h)) / (((cos (2 * x)) + (cos h)) ^2) A2: ( cos . (x + (h / 2)) <> 0 & cos . (x - (h / 2)) <> 0 ) by A1, RFUNCT_1:3; ( x + (h / 2) in dom (sec (#) sec) & x - (h / 2) in dom (sec (#) sec) ) proof ( x + (h / 2) in (dom sec) /\ (dom sec) & x - (h / 2) in (dom sec) /\ (dom sec) ) by A1; hence ( x + (h / 2) in dom (sec (#) sec) & x - (h / 2) in dom (sec (#) sec) ) by VALUED_1:def_4; ::_thesis: verum end; then (cD ((sec (#) sec),h)) . x = ((sec (#) sec) . (x + (h / 2))) - ((sec (#) sec) . (x - (h / 2))) by DIFF_1:39 .= ((sec . (x + (h / 2))) * (sec . (x + (h / 2)))) - ((sec (#) sec) . (x - (h / 2))) by VALUED_1:5 .= ((sec . (x + (h / 2))) * (sec . (x + (h / 2)))) - ((sec . (x - (h / 2))) * (sec . (x - (h / 2)))) by VALUED_1:5 .= (((cos . (x + (h / 2))) ") * (sec . (x + (h / 2)))) - ((sec . (x - (h / 2))) * (sec . (x - (h / 2)))) by A1, RFUNCT_1:def_2 .= (((cos . (x + (h / 2))) ") * ((cos . (x + (h / 2))) ")) - ((sec . (x - (h / 2))) * (sec . (x - (h / 2)))) by A1, RFUNCT_1:def_2 .= (((cos . (x + (h / 2))) ") * ((cos . (x + (h / 2))) ")) - (((cos . (x - (h / 2))) ") * (sec . (x - (h / 2)))) by A1, RFUNCT_1:def_2 .= (((cos . (x + (h / 2))) ") ^2) - (((cos . (x - (h / 2))) ") ^2) by A1, RFUNCT_1:def_2 .= ((1 / (cos . (x + (h / 2)))) - (1 / (cos . (x - (h / 2))))) * ((1 / (cos . (x + (h / 2)))) + (1 / (cos . (x - (h / 2))))) .= (((1 * (cos . (x - (h / 2)))) - (1 * (cos . (x + (h / 2))))) / ((cos . (x + (h / 2))) * (cos . (x - (h / 2))))) * ((1 / (cos . (x + (h / 2)))) + (1 / (cos . (x - (h / 2))))) by A2, XCMPLX_1:130 .= (((cos . (x - (h / 2))) - (cos . (x + (h / 2)))) / ((cos . (x + (h / 2))) * (cos . (x - (h / 2))))) * (((cos . (x - (h / 2))) + (cos . (x + (h / 2)))) / ((cos . (x + (h / 2))) * (cos . (x - (h / 2))))) by A2, XCMPLX_1:116 .= (((cos . (x - (h / 2))) - (cos . (x + (h / 2)))) * ((cos . (x - (h / 2))) + (cos . (x + (h / 2))))) / (((cos . (x + (h / 2))) * (cos . (x - (h / 2)))) * ((cos . (x + (h / 2))) * (cos . (x - (h / 2))))) by XCMPLX_1:76 .= (((cos (x - (h / 2))) * (cos (x - (h / 2)))) - ((cos (x + (h / 2))) * (cos (x + (h / 2))))) / (((cos (x + (h / 2))) * (cos (x - (h / 2)))) ^2) .= ((sin ((x + (h / 2)) + (x - (h / 2)))) * (sin ((x + (h / 2)) - (x - (h / 2))))) / (((cos (x + (h / 2))) * (cos (x - (h / 2)))) ^2) by SIN_COS4:38 .= ((sin (2 * x)) * (sin h)) / (((1 / 2) * ((cos ((x + (h / 2)) + (x - (h / 2)))) + (cos ((x + (h / 2)) - (x - (h / 2)))))) ^2) by SIN_COS4:32 .= (1 * ((sin (2 * x)) * (sin h))) / ((1 / 4) * (((cos (2 * x)) + (cos h)) ^2)) .= (1 / (1 / 4)) * (((sin (2 * x)) * (sin h)) / (((cos (2 * x)) + (cos h)) ^2)) by XCMPLX_1:76 .= ((4 * (sin (2 * x))) * (sin h)) / (((cos (2 * x)) + (cos h)) ^2) ; hence (cD ((sec (#) sec),h)) . x = ((4 * (sin (2 * x))) * (sin h)) / (((cos (2 * x)) + (cos h)) ^2) ; ::_thesis: verum end; theorem :: DIFF_4:18 for x0, x1 being Real st x0 in (dom cosec) /\ (dom sec) & x1 in (dom cosec) /\ (dom sec) holds [!(cosec (#) sec),x0,x1!] = ((4 * ((cos (x1 + x0)) * (sin (x1 - x0)))) / ((sin (2 * x0)) * (sin (2 * x1)))) / (x0 - x1) proof let x0, x1 be Real; ::_thesis: ( x0 in (dom cosec) /\ (dom sec) & x1 in (dom cosec) /\ (dom sec) implies [!(cosec (#) sec),x0,x1!] = ((4 * ((cos (x1 + x0)) * (sin (x1 - x0)))) / ((sin (2 * x0)) * (sin (2 * x1)))) / (x0 - x1) ) assume A1: ( x0 in (dom cosec) /\ (dom sec) & x1 in (dom cosec) /\ (dom sec) ) ; ::_thesis: [!(cosec (#) sec),x0,x1!] = ((4 * ((cos (x1 + x0)) * (sin (x1 - x0)))) / ((sin (2 * x0)) * (sin (2 * x1)))) / (x0 - x1) A2: ( x0 in dom cosec & x0 in dom sec ) by A1, XBOOLE_0:def_4; A3: ( x1 in dom cosec & x1 in dom sec ) by A1, XBOOLE_0:def_4; A4: ( sin . x0 <> 0 & cos . x0 <> 0 ) by A2, RFUNCT_1:3; A5: ( sin . x1 <> 0 & cos . x1 <> 0 ) by A3, RFUNCT_1:3; [!(cosec (#) sec),x0,x1!] = (((cosec . x0) * (sec . x0)) - ((cosec (#) sec) . x1)) / (x0 - x1) by VALUED_1:5 .= (((cosec . x0) * (sec . x0)) - ((cosec . x1) * (sec . x1))) / (x0 - x1) by VALUED_1:5 .= ((((sin . x0) ") * (sec . x0)) - ((cosec . x1) * (sec . x1))) / (x0 - x1) by A2, RFUNCT_1:def_2 .= ((((sin . x0) ") * ((cos . x0) ")) - ((cosec . x1) * (sec . x1))) / (x0 - x1) by A2, RFUNCT_1:def_2 .= ((((sin . x0) ") * ((cos . x0) ")) - (((sin . x1) ") * (sec . x1))) / (x0 - x1) by A3, RFUNCT_1:def_2 .= ((((sin . x0) ") * ((cos . x0) ")) - (((sin . x1) ") * ((cos . x1) "))) / (x0 - x1) by A3, RFUNCT_1:def_2 .= ((((sin . x0) * (cos . x0)) ") - (((sin . x1) ") * ((cos . x1) "))) / (x0 - x1) by XCMPLX_1:204 .= ((1 / ((sin . x0) * (cos . x0))) - (1 / ((sin . x1) * (cos . x1)))) / (x0 - x1) by XCMPLX_1:204 .= (((1 * ((sin . x1) * (cos . x1))) - (1 * ((sin . x0) * (cos . x0)))) / (((sin . x0) * (cos . x0)) * ((sin . x1) * (cos . x1)))) / (x0 - x1) by A4, A5, XCMPLX_1:130 .= (((cos (x1 + x0)) * (sin (x1 - x0))) / (((1 / 2) * ((2 * (sin x0)) * (cos x0))) * ((1 / 2) * ((2 * (sin x1)) * (cos x1))))) / (x0 - x1) by SIN_COS4:40 .= (((cos (x1 + x0)) * (sin (x1 - x0))) / (((1 / 2) * (sin (2 * x0))) * ((1 / 2) * ((2 * (sin x1)) * (cos x1))))) / (x0 - x1) by SIN_COS5:5 .= (((cos (x1 + x0)) * (sin (x1 - x0))) / (((1 / 2) * (sin (2 * x0))) * ((1 / 2) * (sin (2 * x1))))) / (x0 - x1) by SIN_COS5:5 .= (((cos (x1 + x0)) * (sin (x1 - x0))) / ((((sin (2 * x0)) * (sin (2 * x1))) * 1) / 4)) / (x0 - x1) .= ((1 / (1 / 4)) * (((cos (x1 + x0)) * (sin (x1 - x0))) / ((sin (2 * x0)) * (sin (2 * x1))))) / (x0 - x1) by XCMPLX_1:103 .= ((4 * ((cos (x1 + x0)) * (sin (x1 - x0)))) / ((sin (2 * x0)) * (sin (2 * x1)))) / (x0 - x1) ; hence [!(cosec (#) sec),x0,x1!] = ((4 * ((cos (x1 + x0)) * (sin (x1 - x0)))) / ((sin (2 * x0)) * (sin (2 * x1)))) / (x0 - x1) ; ::_thesis: verum end; theorem :: DIFF_4:19 for x, h being Real st x + h in (dom cosec) /\ (dom sec) & x in (dom cosec) /\ (dom sec) holds (fD ((cosec (#) sec),h)) . x = - (4 * (((cos ((2 * x) + h)) * (sin h)) / ((sin (2 * (x + h))) * (sin (2 * x))))) proof let x, h be Real; ::_thesis: ( x + h in (dom cosec) /\ (dom sec) & x in (dom cosec) /\ (dom sec) implies (fD ((cosec (#) sec),h)) . x = - (4 * (((cos ((2 * x) + h)) * (sin h)) / ((sin (2 * (x + h))) * (sin (2 * x))))) ) set f = cosec (#) sec; assume A1: ( x + h in (dom cosec) /\ (dom sec) & x in (dom cosec) /\ (dom sec) ) ; ::_thesis: (fD ((cosec (#) sec),h)) . x = - (4 * (((cos ((2 * x) + h)) * (sin h)) / ((sin (2 * (x + h))) * (sin (2 * x))))) A2: ( x + h in dom cosec & x + h in dom sec ) by A1, XBOOLE_0:def_4; A3: ( x in dom cosec & x in dom sec ) by A1, XBOOLE_0:def_4; A4: ( sin . (x + h) <> 0 & cos . (x + h) <> 0 ) by A2, RFUNCT_1:3; A5: ( sin . x <> 0 & cos . x <> 0 ) by A3, RFUNCT_1:3; ( x in dom (cosec (#) sec) & x + h in dom (cosec (#) sec) ) by A1, VALUED_1:def_4; then (fD ((cosec (#) sec),h)) . x = ((cosec (#) sec) . (x + h)) - ((cosec (#) sec) . x) by DIFF_1:1 .= ((cosec . (x + h)) * (sec . (x + h))) - ((cosec (#) sec) . x) by VALUED_1:5 .= ((cosec . (x + h)) * (sec . (x + h))) - ((cosec . x) * (sec . x)) by VALUED_1:5 .= (((sin . (x + h)) ") * (sec . (x + h))) - ((cosec . x) * (sec . x)) by A2, RFUNCT_1:def_2 .= (((sin . (x + h)) ") * ((cos . (x + h)) ")) - ((cosec . x) * (sec . x)) by A2, RFUNCT_1:def_2 .= (((sin . (x + h)) ") * ((cos . (x + h)) ")) - (((sin . x) ") * (sec . x)) by A3, RFUNCT_1:def_2 .= (((sin . (x + h)) ") * ((cos . (x + h)) ")) - (((sin . x) ") * ((cos . x) ")) by A3, RFUNCT_1:def_2 .= (((sin . (x + h)) * (cos . (x + h))) ") - (((sin . x) ") * ((cos . x) ")) by XCMPLX_1:204 .= (1 / ((sin . (x + h)) * (cos . (x + h)))) - (1 / ((sin . x) * (cos . x))) by XCMPLX_1:204 .= ((1 * ((sin . x) * (cos . x))) - (1 * ((sin . (x + h)) * (cos . (x + h))))) / (((sin . (x + h)) * (cos . (x + h))) * ((sin . x) * (cos . x))) by A4, A5, XCMPLX_1:130 .= ((cos (x + (x + h))) * (sin (x - (x + h)))) / (((sin (x + h)) * (cos (x + h))) * ((sin x) * (cos x))) by SIN_COS4:40 .= ((cos ((2 * x) + h)) * (sin (- h))) / (((1 * (sin (x + h))) * (cos (x + h))) * ((1 * (sin x)) * (cos x))) .= ((cos ((2 * x) + h)) * (- (sin h))) / (((((1 / 2) * 2) * (sin (x + h))) * (cos (x + h))) * ((((1 / 2) * 2) * (sin x)) * (cos x))) by SIN_COS:31 .= (- ((cos ((2 * x) + h)) * (sin h))) / (((1 / 2) * ((2 * (sin (x + h))) * (cos (x + h)))) * ((1 / 2) * ((2 * (sin x)) * (cos x)))) .= (- ((cos ((2 * x) + h)) * (sin h))) / (((1 / 2) * (sin (2 * (x + h)))) * ((1 / 2) * ((2 * (sin x)) * (cos x)))) by SIN_COS5:5 .= (- ((cos ((2 * x) + h)) * (sin h))) / (((1 / 2) * (sin (2 * (x + h)))) * ((1 / 2) * (sin (2 * x)))) by SIN_COS5:5 .= - (((cos ((2 * x) + h)) * (sin h)) / (((sin (2 * (x + h))) * (sin (2 * x))) * (1 / 4))) .= - ((1 / (1 / 4)) * (((cos ((2 * x) + h)) * (sin h)) / ((sin (2 * (x + h))) * (sin (2 * x))))) by XCMPLX_1:103 .= - (4 * (((cos ((2 * x) + h)) * (sin h)) / ((sin (2 * (x + h))) * (sin (2 * x))))) ; hence (fD ((cosec (#) sec),h)) . x = - (4 * (((cos ((2 * x) + h)) * (sin h)) / ((sin (2 * (x + h))) * (sin (2 * x))))) ; ::_thesis: verum end; theorem :: DIFF_4:20 for x, h being Real st x - h in (dom cosec) /\ (dom sec) & x in (dom cosec) /\ (dom sec) holds (bD ((cosec (#) sec),h)) . x = - (4 * (((cos ((2 * x) - h)) * (sin h)) / ((sin (2 * x)) * (sin (2 * (x - h)))))) proof let x, h be Real; ::_thesis: ( x - h in (dom cosec) /\ (dom sec) & x in (dom cosec) /\ (dom sec) implies (bD ((cosec (#) sec),h)) . x = - (4 * (((cos ((2 * x) - h)) * (sin h)) / ((sin (2 * x)) * (sin (2 * (x - h)))))) ) set f = cosec (#) sec; assume A1: ( x - h in (dom cosec) /\ (dom sec) & x in (dom cosec) /\ (dom sec) ) ; ::_thesis: (bD ((cosec (#) sec),h)) . x = - (4 * (((cos ((2 * x) - h)) * (sin h)) / ((sin (2 * x)) * (sin (2 * (x - h)))))) A2: ( x - h in dom cosec & x - h in dom sec ) by A1, XBOOLE_0:def_4; A3: ( x in dom cosec & x in dom sec ) by A1, XBOOLE_0:def_4; A4: ( sin . (x - h) <> 0 & cos . (x - h) <> 0 ) by A2, RFUNCT_1:3; A5: ( sin . x <> 0 & cos . x <> 0 ) by A3, RFUNCT_1:3; ( x in dom (cosec (#) sec) & x - h in dom (cosec (#) sec) ) by A1, VALUED_1:def_4; then (bD ((cosec (#) sec),h)) . x = ((cosec (#) sec) . x) - ((cosec (#) sec) . (x - h)) by DIFF_1:38 .= ((cosec . x) * (sec . x)) - ((cosec (#) sec) . (x - h)) by VALUED_1:5 .= ((cosec . x) * (sec . x)) - ((cosec . (x - h)) * (sec . (x - h))) by VALUED_1:5 .= (((sin . x) ") * (sec . x)) - ((cosec . (x - h)) * (sec . (x - h))) by A3, RFUNCT_1:def_2 .= (((sin . x) ") * ((cos . x) ")) - ((cosec . (x - h)) * (sec . (x - h))) by A3, RFUNCT_1:def_2 .= (((sin . x) ") * ((cos . x) ")) - (((sin . (x - h)) ") * (sec . (x - h))) by A2, RFUNCT_1:def_2 .= (((sin . x) ") * ((cos . x) ")) - (((sin . (x - h)) ") * ((cos . (x - h)) ")) by A2, RFUNCT_1:def_2 .= (((sin . x) * (cos . x)) ") - (((sin . (x - h)) ") * ((cos . (x - h)) ")) by XCMPLX_1:204 .= (1 / ((sin . x) * (cos . x))) - (1 / ((sin . (x - h)) * (cos . (x - h)))) by XCMPLX_1:204 .= ((1 * ((sin . (x - h)) * (cos . (x - h)))) - (1 * ((sin . x) * (cos . x)))) / (((sin . x) * (cos . x)) * ((sin . (x - h)) * (cos . (x - h)))) by A4, A5, XCMPLX_1:130 .= ((cos ((x - h) + x)) * (sin ((x - h) - x))) / (((sin x) * (cos x)) * ((sin (x - h)) * (cos (x - h)))) by SIN_COS4:40 .= ((cos ((2 * x) - h)) * (- (sin h))) / (((((1 / 2) * 2) * (sin x)) * (cos x)) * ((((1 / 2) * 2) * (sin (x - h))) * (cos (x - h)))) by SIN_COS:31 .= (- ((cos ((2 * x) - h)) * (sin h))) / (((1 / 2) * ((2 * (sin x)) * (cos x))) * ((1 / 2) * ((2 * (sin (x - h))) * (cos (x - h))))) .= (- ((cos ((2 * x) - h)) * (sin h))) / (((1 / 2) * (sin (2 * x))) * ((1 / 2) * ((2 * (sin (x - h))) * (cos (x - h))))) by SIN_COS5:5 .= (- ((cos ((2 * x) - h)) * (sin h))) / (((1 / 2) * (sin (2 * x))) * ((1 / 2) * (sin (2 * (x - h))))) by SIN_COS5:5 .= - (((cos ((2 * x) - h)) * (sin h)) / (((sin (2 * x)) * (sin (2 * (x - h)))) * (1 / 4))) .= - ((1 / (1 / 4)) * (((cos ((2 * x) - h)) * (sin h)) / ((sin (2 * x)) * (sin (2 * (x - h)))))) by XCMPLX_1:103 .= - (4 * (((cos ((2 * x) - h)) * (sin h)) / ((sin (2 * x)) * (sin (2 * (x - h)))))) ; hence (bD ((cosec (#) sec),h)) . x = - (4 * (((cos ((2 * x) - h)) * (sin h)) / ((sin (2 * x)) * (sin (2 * (x - h)))))) ; ::_thesis: verum end; theorem :: DIFF_4:21 for x, h being Real st x + (h / 2) in (dom cosec) /\ (dom sec) & x - (h / 2) in (dom cosec) /\ (dom sec) holds (cD ((cosec (#) sec),h)) . x = - (4 * (((cos (2 * x)) * (sin h)) / ((sin ((2 * x) + h)) * (sin ((2 * x) - h))))) proof let x, h be Real; ::_thesis: ( x + (h / 2) in (dom cosec) /\ (dom sec) & x - (h / 2) in (dom cosec) /\ (dom sec) implies (cD ((cosec (#) sec),h)) . x = - (4 * (((cos (2 * x)) * (sin h)) / ((sin ((2 * x) + h)) * (sin ((2 * x) - h))))) ) set f = cosec (#) sec; assume A1: ( x + (h / 2) in (dom cosec) /\ (dom sec) & x - (h / 2) in (dom cosec) /\ (dom sec) ) ; ::_thesis: (cD ((cosec (#) sec),h)) . x = - (4 * (((cos (2 * x)) * (sin h)) / ((sin ((2 * x) + h)) * (sin ((2 * x) - h))))) A2: ( x + (h / 2) in dom cosec & x + (h / 2) in dom sec ) by A1, XBOOLE_0:def_4; A3: ( x - (h / 2) in dom cosec & x - (h / 2) in dom sec ) by A1, XBOOLE_0:def_4; A4: ( sin . (x + (h / 2)) <> 0 & cos . (x + (h / 2)) <> 0 ) by A2, RFUNCT_1:3; A5: ( sin . (x - (h / 2)) <> 0 & cos . (x - (h / 2)) <> 0 ) by A3, RFUNCT_1:3; ( x + (h / 2) in dom (cosec (#) sec) & x - (h / 2) in dom (cosec (#) sec) ) by A1, VALUED_1:def_4; then (cD ((cosec (#) sec),h)) . x = ((cosec (#) sec) . (x + (h / 2))) - ((cosec (#) sec) . (x - (h / 2))) by DIFF_1:39 .= ((cosec . (x + (h / 2))) * (sec . (x + (h / 2)))) - ((cosec (#) sec) . (x - (h / 2))) by VALUED_1:5 .= ((cosec . (x + (h / 2))) * (sec . (x + (h / 2)))) - ((cosec . (x - (h / 2))) * (sec . (x - (h / 2)))) by VALUED_1:5 .= (((sin . (x + (h / 2))) ") * (sec . (x + (h / 2)))) - ((cosec . (x - (h / 2))) * (sec . (x - (h / 2)))) by A2, RFUNCT_1:def_2 .= (((sin . (x + (h / 2))) ") * ((cos . (x + (h / 2))) ")) - ((cosec . (x - (h / 2))) * (sec . (x - (h / 2)))) by A2, RFUNCT_1:def_2 .= (((sin . (x + (h / 2))) ") * ((cos . (x + (h / 2))) ")) - (((sin . (x - (h / 2))) ") * (sec . (x - (h / 2)))) by A3, RFUNCT_1:def_2 .= (((sin . (x + (h / 2))) ") * ((cos . (x + (h / 2))) ")) - (((sin . (x - (h / 2))) ") * ((cos . (x - (h / 2))) ")) by A3, RFUNCT_1:def_2 .= (((sin . (x + (h / 2))) * (cos . (x + (h / 2)))) ") - (((sin . (x - (h / 2))) ") * ((cos . (x - (h / 2))) ")) by XCMPLX_1:204 .= (1 / ((sin . (x + (h / 2))) * (cos . (x + (h / 2))))) - (1 / ((sin . (x - (h / 2))) * (cos . (x - (h / 2))))) by XCMPLX_1:204 .= ((1 * ((sin . (x - (h / 2))) * (cos . (x - (h / 2))))) - (1 * ((sin . (x + (h / 2))) * (cos . (x + (h / 2)))))) / (((sin . (x + (h / 2))) * (cos . (x + (h / 2)))) * ((sin . (x - (h / 2))) * (cos . (x - (h / 2))))) by A4, A5, XCMPLX_1:130 .= ((cos ((x - (h / 2)) + (x + (h / 2)))) * (sin ((x - (h / 2)) - (x + (h / 2))))) / (((sin (x + (h / 2))) * (cos (x + (h / 2)))) * ((sin (x - (h / 2))) * (cos (x - (h / 2))))) by SIN_COS4:40 .= ((cos (2 * x)) * (sin (- h))) / (((1 * (sin (x + (h / 2)))) * (cos (x + (h / 2)))) * ((1 * (sin (x - (h / 2)))) * (cos (x - (h / 2))))) .= ((cos (2 * x)) * (- (sin h))) / (((((1 / 2) * 2) * (sin (x + (h / 2)))) * (cos (x + (h / 2)))) * ((((1 / 2) * 2) * (sin (x - (h / 2)))) * (cos (x - (h / 2))))) by SIN_COS:31 .= (- ((cos (2 * x)) * (sin h))) / (((1 / 2) * ((2 * (sin (x + (h / 2)))) * (cos (x + (h / 2))))) * ((1 / 2) * ((2 * (sin (x - (h / 2)))) * (cos (x - (h / 2)))))) .= (- ((cos (2 * x)) * (sin h))) / (((1 / 2) * (sin (2 * (x + (h / 2))))) * ((1 / 2) * ((2 * (sin (x - (h / 2)))) * (cos (x - (h / 2)))))) by SIN_COS5:5 .= (- ((cos (2 * x)) * (sin h))) / (((1 / 2) * (sin (2 * (x + (h / 2))))) * ((1 / 2) * (sin (2 * (x - (h / 2)))))) by SIN_COS5:5 .= - (((cos (2 * x)) * (sin h)) / (((sin ((2 * x) + h)) * (sin ((2 * x) - h))) * (1 / 4))) .= - ((1 / (1 / 4)) * (((cos (2 * x)) * (sin h)) / ((sin ((2 * x) + h)) * (sin ((2 * x) - h))))) by XCMPLX_1:103 .= - (4 * (((cos (2 * x)) * (sin h)) / ((sin ((2 * x) + h)) * (sin ((2 * x) - h))))) ; hence (cD ((cosec (#) sec),h)) . x = - (4 * (((cos (2 * x)) * (sin h)) / ((sin ((2 * x) + h)) * (sin ((2 * x) - h))))) ; ::_thesis: verum end; theorem :: DIFF_4:22 for x0, x1 being Real st x0 in dom tan & x1 in dom tan holds [!((tan (#) tan) (#) cos),x0,x1!] = [!(tan (#) sin),x0,x1!] proof let x0, x1 be Real; ::_thesis: ( x0 in dom tan & x1 in dom tan implies [!((tan (#) tan) (#) cos),x0,x1!] = [!(tan (#) sin),x0,x1!] ) assume A1: ( x0 in dom tan & x1 in dom tan ) ; ::_thesis: [!((tan (#) tan) (#) cos),x0,x1!] = [!(tan (#) sin),x0,x1!] [!((tan (#) tan) (#) cos),x0,x1!] = ((((tan (#) tan) . x0) * (cos . x0)) - (((tan (#) tan) (#) cos) . x1)) / (x0 - x1) by VALUED_1:5 .= ((((tan . x0) * (tan . x0)) * (cos . x0)) - (((tan (#) tan) (#) cos) . x1)) / (x0 - x1) by VALUED_1:5 .= ((((tan . x0) * (tan . x0)) * (cos . x0)) - (((tan (#) tan) . x1) * (cos . x1))) / (x0 - x1) by VALUED_1:5 .= ((((tan . x0) * (tan . x0)) * (cos . x0)) - (((tan . x1) * (tan . x1)) * (cos . x1))) / (x0 - x1) by VALUED_1:5 .= (((((sin . x0) * ((cos . x0) ")) * (tan . x0)) * (cos . x0)) - (((tan . x1) * (tan . x1)) * (cos . x1))) / (x0 - x1) by A1, RFUNCT_1:def_1 .= (((((sin . x0) * ((cos . x0) ")) * (tan . x0)) * (cos . x0)) - ((((sin . x1) * ((cos . x1) ")) * (tan . x1)) * (cos . x1))) / (x0 - x1) by A1, RFUNCT_1:def_1 .= ((((sin . x0) * ((cos . x0) * (1 / (cos . x0)))) * (tan . x0)) - (((sin . x1) * ((cos . x1) * (1 / (cos . x1)))) * (tan . x1))) / (x0 - x1) .= ((((sin . x0) * 1) * (tan . x0)) - (((sin . x1) * ((cos . x1) * (1 / (cos . x1)))) * (tan . x1))) / (x0 - x1) by A1, FDIFF_8:1, XCMPLX_1:106 .= ((((sin . x0) * 1) * (tan . x0)) - (((sin . x1) * 1) * (tan . x1))) / (x0 - x1) by A1, FDIFF_8:1, XCMPLX_1:106 .= (((tan (#) sin) . x0) - ((tan . x1) * (sin . x1))) / (x0 - x1) by VALUED_1:5 .= [!(tan (#) sin),x0,x1!] by VALUED_1:5 ; hence [!((tan (#) tan) (#) cos),x0,x1!] = [!(tan (#) sin),x0,x1!] ; ::_thesis: verum end; theorem :: DIFF_4:23 for x, h being Real st x in dom tan & x + h in dom tan holds (fD (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . (x + h)) - ((tan (#) sin) . x) proof let x, h be Real; ::_thesis: ( x in dom tan & x + h in dom tan implies (fD (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . (x + h)) - ((tan (#) sin) . x) ) set f = (tan (#) tan) (#) cos; assume A1: ( x in dom tan & x + h in dom tan ) ; ::_thesis: (fD (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . (x + h)) - ((tan (#) sin) . x) ( x in dom ((tan (#) tan) (#) cos) & x + h in dom ((tan (#) tan) (#) cos) ) proof set f1 = tan (#) tan; set f2 = cos ; A2: ( x in dom (tan (#) tan) & x + h in dom (tan (#) tan) ) proof ( x in (dom tan) /\ (dom tan) & x + h in (dom tan) /\ (dom tan) ) by A1; hence ( x in dom (tan (#) tan) & x + h in dom (tan (#) tan) ) by VALUED_1:def_4; ::_thesis: verum end; ( x in (dom (tan (#) tan)) /\ (dom cos) & x + h in (dom (tan (#) tan)) /\ (dom cos) ) by A2, SIN_COS:24, XBOOLE_0:def_4; hence ( x in dom ((tan (#) tan) (#) cos) & x + h in dom ((tan (#) tan) (#) cos) ) by VALUED_1:def_4; ::_thesis: verum end; then (fD (((tan (#) tan) (#) cos),h)) . x = (((tan (#) tan) (#) cos) . (x + h)) - (((tan (#) tan) (#) cos) . x) by DIFF_1:1 .= (((tan (#) tan) . (x + h)) * (cos . (x + h))) - (((tan (#) tan) (#) cos) . x) by VALUED_1:5 .= (((tan . (x + h)) * (tan . (x + h))) * (cos . (x + h))) - (((tan (#) tan) (#) cos) . x) by VALUED_1:5 .= (((tan . (x + h)) * (tan . (x + h))) * (cos . (x + h))) - (((tan (#) tan) . x) * (cos . x)) by VALUED_1:5 .= (((tan . (x + h)) * (tan . (x + h))) * (cos . (x + h))) - (((tan . x) * (tan . x)) * (cos . x)) by VALUED_1:5 .= ((((sin . (x + h)) * ((cos . (x + h)) ")) * (tan . (x + h))) * (cos . (x + h))) - (((tan . x) * (tan . x)) * (cos . x)) by A1, RFUNCT_1:def_1 .= ((((sin . (x + h)) * ((cos . (x + h)) ")) * (tan . (x + h))) * (cos . (x + h))) - ((((sin . x) * ((cos . x) ")) * (tan . x)) * (cos . x)) by A1, RFUNCT_1:def_1 .= (((sin . (x + h)) * (tan . (x + h))) * ((cos . (x + h)) * (1 / (cos . (x + h))))) - (((sin . x) * (tan . x)) * ((cos . x) * (1 / (cos . x)))) .= (((sin . (x + h)) * (tan . (x + h))) * 1) - (((sin . x) * (tan . x)) * ((cos . x) * (1 / (cos . x)))) by A1, FDIFF_8:1, XCMPLX_1:106 .= (((sin . (x + h)) * (tan . (x + h))) * 1) - (((sin . x) * (tan . x)) * 1) by A1, FDIFF_8:1, XCMPLX_1:106 .= ((tan (#) sin) . (x + h)) - ((tan . x) * (sin . x)) by VALUED_1:5 .= ((tan (#) sin) . (x + h)) - ((tan (#) sin) . x) by VALUED_1:5 ; hence (fD (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . (x + h)) - ((tan (#) sin) . x) ; ::_thesis: verum end; theorem :: DIFF_4:24 for x, h being Real st x in dom tan & x - h in dom tan holds (bD (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . x) - ((tan (#) sin) . (x - h)) proof let x, h be Real; ::_thesis: ( x in dom tan & x - h in dom tan implies (bD (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . x) - ((tan (#) sin) . (x - h)) ) set f = (tan (#) tan) (#) cos; assume A1: ( x in dom tan & x - h in dom tan ) ; ::_thesis: (bD (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . x) - ((tan (#) sin) . (x - h)) ( x in dom ((tan (#) tan) (#) cos) & x - h in dom ((tan (#) tan) (#) cos) ) proof set f1 = tan (#) tan; set f2 = cos ; A2: ( x in dom (tan (#) tan) & x - h in dom (tan (#) tan) ) proof ( x in (dom tan) /\ (dom tan) & x - h in (dom tan) /\ (dom tan) ) by A1; hence ( x in dom (tan (#) tan) & x - h in dom (tan (#) tan) ) by VALUED_1:def_4; ::_thesis: verum end; ( x in (dom (tan (#) tan)) /\ (dom cos) & x - h in (dom (tan (#) tan)) /\ (dom cos) ) by A2, SIN_COS:24, XBOOLE_0:def_4; hence ( x in dom ((tan (#) tan) (#) cos) & x - h in dom ((tan (#) tan) (#) cos) ) by VALUED_1:def_4; ::_thesis: verum end; then (bD (((tan (#) tan) (#) cos),h)) . x = (((tan (#) tan) (#) cos) . x) - (((tan (#) tan) (#) cos) . (x - h)) by DIFF_1:38 .= (((tan (#) tan) . x) * (cos . x)) - (((tan (#) tan) (#) cos) . (x - h)) by VALUED_1:5 .= (((tan . x) * (tan . x)) * (cos . x)) - (((tan (#) tan) (#) cos) . (x - h)) by VALUED_1:5 .= (((tan . x) * (tan . x)) * (cos . x)) - (((tan (#) tan) . (x - h)) * (cos . (x - h))) by VALUED_1:5 .= (((tan . x) * (tan . x)) * (cos . x)) - (((tan . (x - h)) * (tan . (x - h))) * (cos . (x - h))) by VALUED_1:5 .= ((((sin . x) * ((cos . x) ")) * (tan . x)) * (cos . x)) - (((tan . (x - h)) * (tan . (x - h))) * (cos . (x - h))) by A1, RFUNCT_1:def_1 .= ((((sin . x) * ((cos . x) ")) * (tan . x)) * (cos . x)) - ((((sin . (x - h)) * ((cos . (x - h)) ")) * (tan . (x - h))) * (cos . (x - h))) by A1, RFUNCT_1:def_1 .= (((sin . x) * (tan . x)) * ((cos . x) * (1 / (cos . x)))) - (((sin . (x - h)) * (tan . (x - h))) * ((cos . (x - h)) * (1 / (cos . (x - h))))) .= (((sin . x) * (tan . x)) * 1) - (((sin . (x - h)) * (tan . (x - h))) * ((cos . (x - h)) * (1 / (cos . (x - h))))) by A1, FDIFF_8:1, XCMPLX_1:106 .= (((sin . x) * (tan . x)) * 1) - (((sin . (x - h)) * (tan . (x - h))) * 1) by A1, FDIFF_8:1, XCMPLX_1:106 .= ((tan (#) sin) . x) - ((tan . (x - h)) * (sin . (x - h))) by VALUED_1:5 .= ((tan (#) sin) . x) - ((tan (#) sin) . (x - h)) by VALUED_1:5 ; hence (bD (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . x) - ((tan (#) sin) . (x - h)) ; ::_thesis: verum end; theorem :: DIFF_4:25 for x, h being Real st x + (h / 2) in dom tan & x - (h / 2) in dom tan holds (cD (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . (x + (h / 2))) - ((tan (#) sin) . (x - (h / 2))) proof let x, h be Real; ::_thesis: ( x + (h / 2) in dom tan & x - (h / 2) in dom tan implies (cD (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . (x + (h / 2))) - ((tan (#) sin) . (x - (h / 2))) ) set f = (tan (#) tan) (#) cos; assume A1: ( x + (h / 2) in dom tan & x - (h / 2) in dom tan ) ; ::_thesis: (cD (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . (x + (h / 2))) - ((tan (#) sin) . (x - (h / 2))) ( x + (h / 2) in dom ((tan (#) tan) (#) cos) & x - (h / 2) in dom ((tan (#) tan) (#) cos) ) proof set f1 = tan (#) tan; set f2 = cos ; A2: ( x + (h / 2) in dom (tan (#) tan) & x - (h / 2) in dom (tan (#) tan) ) proof ( x + (h / 2) in (dom tan) /\ (dom tan) & x - (h / 2) in (dom tan) /\ (dom tan) ) by A1; hence ( x + (h / 2) in dom (tan (#) tan) & x - (h / 2) in dom (tan (#) tan) ) by VALUED_1:def_4; ::_thesis: verum end; ( x + (h / 2) in (dom (tan (#) tan)) /\ (dom cos) & x - (h / 2) in (dom (tan (#) tan)) /\ (dom cos) ) by A2, SIN_COS:24, XBOOLE_0:def_4; hence ( x + (h / 2) in dom ((tan (#) tan) (#) cos) & x - (h / 2) in dom ((tan (#) tan) (#) cos) ) by VALUED_1:def_4; ::_thesis: verum end; then (cD (((tan (#) tan) (#) cos),h)) . x = (((tan (#) tan) (#) cos) . (x + (h / 2))) - (((tan (#) tan) (#) cos) . (x - (h / 2))) by DIFF_1:39 .= (((tan (#) tan) . (x + (h / 2))) * (cos . (x + (h / 2)))) - (((tan (#) tan) (#) cos) . (x - (h / 2))) by VALUED_1:5 .= (((tan . (x + (h / 2))) * (tan . (x + (h / 2)))) * (cos . (x + (h / 2)))) - (((tan (#) tan) (#) cos) . (x - (h / 2))) by VALUED_1:5 .= (((tan . (x + (h / 2))) * (tan . (x + (h / 2)))) * (cos . (x + (h / 2)))) - (((tan (#) tan) . (x - (h / 2))) * (cos . (x - (h / 2)))) by VALUED_1:5 .= (((tan . (x + (h / 2))) * (tan . (x + (h / 2)))) * (cos . (x + (h / 2)))) - (((tan . (x - (h / 2))) * (tan . (x - (h / 2)))) * (cos . (x - (h / 2)))) by VALUED_1:5 .= ((((sin . (x + (h / 2))) * ((cos . (x + (h / 2))) ")) * (tan . (x + (h / 2)))) * (cos . (x + (h / 2)))) - (((tan . (x - (h / 2))) * (tan . (x - (h / 2)))) * (cos . (x - (h / 2)))) by A1, RFUNCT_1:def_1 .= ((((sin . (x + (h / 2))) * ((cos . (x + (h / 2))) ")) * (tan . (x + (h / 2)))) * (cos . (x + (h / 2)))) - ((((sin . (x - (h / 2))) * ((cos . (x - (h / 2))) ")) * (tan . (x - (h / 2)))) * (cos . (x - (h / 2)))) by A1, RFUNCT_1:def_1 .= (((sin . (x + (h / 2))) * (tan . (x + (h / 2)))) * ((cos . (x + (h / 2))) * (1 / (cos . (x + (h / 2)))))) - (((sin . (x - (h / 2))) * (tan . (x - (h / 2)))) * ((cos . (x - (h / 2))) * (1 / (cos . (x - (h / 2)))))) .= (((sin . (x + (h / 2))) * (tan . (x + (h / 2)))) * 1) - (((sin . (x - (h / 2))) * (tan . (x - (h / 2)))) * ((cos . (x - (h / 2))) * (1 / (cos . (x - (h / 2)))))) by A1, FDIFF_8:1, XCMPLX_1:106 .= (((sin . (x + (h / 2))) * (tan . (x + (h / 2)))) * 1) - (((sin . (x - (h / 2))) * (tan . (x - (h / 2)))) * 1) by A1, FDIFF_8:1, XCMPLX_1:106 .= ((tan (#) sin) . (x + (h / 2))) - ((tan . (x - (h / 2))) * (sin . (x - (h / 2)))) by VALUED_1:5 .= ((tan (#) sin) . (x + (h / 2))) - ((tan (#) sin) . (x - (h / 2))) by VALUED_1:5 ; hence (cD (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . (x + (h / 2))) - ((tan (#) sin) . (x - (h / 2))) ; ::_thesis: verum end; theorem :: DIFF_4:26 for x0, x1 being Real st x0 in dom cot & x1 in dom cot holds [!((cot (#) cot) (#) sin),x0,x1!] = [!(cot (#) cos),x0,x1!] proof let x0, x1 be Real; ::_thesis: ( x0 in dom cot & x1 in dom cot implies [!((cot (#) cot) (#) sin),x0,x1!] = [!(cot (#) cos),x0,x1!] ) assume A1: ( x0 in dom cot & x1 in dom cot ) ; ::_thesis: [!((cot (#) cot) (#) sin),x0,x1!] = [!(cot (#) cos),x0,x1!] [!((cot (#) cot) (#) sin),x0,x1!] = ((((cot (#) cot) . x0) * (sin . x0)) - (((cot (#) cot) (#) sin) . x1)) / (x0 - x1) by VALUED_1:5 .= ((((cot . x0) * (cot . x0)) * (sin . x0)) - (((cot (#) cot) (#) sin) . x1)) / (x0 - x1) by VALUED_1:5 .= ((((cot . x0) * (cot . x0)) * (sin . x0)) - (((cot (#) cot) . x1) * (sin . x1))) / (x0 - x1) by VALUED_1:5 .= ((((cot . x0) * (cot . x0)) * (sin . x0)) - (((cot . x1) * (cot . x1)) * (sin . x1))) / (x0 - x1) by VALUED_1:5 .= (((((cos . x0) * ((sin . x0) ")) * (cot . x0)) * (sin . x0)) - (((cot . x1) * (cot . x1)) * (sin . x1))) / (x0 - x1) by A1, RFUNCT_1:def_1 .= (((((cos . x0) * ((sin . x0) ")) * (cot . x0)) * (sin . x0)) - ((((cos . x1) * ((sin . x1) ")) * (cot . x1)) * (sin . x1))) / (x0 - x1) by A1, RFUNCT_1:def_1 .= ((((cot . x0) * (cos . x0)) * ((sin . x0) * (1 / (sin . x0)))) - (((cot . x1) * (cos . x1)) * ((sin . x1) * (1 / (sin . x1))))) / (x0 - x1) .= ((((cot . x0) * (cos . x0)) * 1) - (((cot . x1) * (cos . x1)) * ((sin . x1) * (1 / (sin . x1))))) / (x0 - x1) by A1, FDIFF_8:2, XCMPLX_1:106 .= ((((cot . x0) * (cos . x0)) * 1) - (((cot . x1) * (cos . x1)) * 1)) / (x0 - x1) by A1, FDIFF_8:2, XCMPLX_1:106 .= (((cot (#) cos) . x0) - ((cot . x1) * (cos . x1))) / (x0 - x1) by VALUED_1:5 .= [!(cot (#) cos),x0,x1!] by VALUED_1:5 ; hence [!((cot (#) cot) (#) sin),x0,x1!] = [!(cot (#) cos),x0,x1!] ; ::_thesis: verum end; theorem :: DIFF_4:27 for x, h being Real st x in dom cot & x + h in dom cot holds (fD (((cot (#) cot) (#) sin),h)) . x = ((cot (#) cos) . (x + h)) - ((cot (#) cos) . x) proof let x, h be Real; ::_thesis: ( x in dom cot & x + h in dom cot implies (fD (((cot (#) cot) (#) sin),h)) . x = ((cot (#) cos) . (x + h)) - ((cot (#) cos) . x) ) set f = (cot (#) cot) (#) sin; assume A1: ( x in dom cot & x + h in dom cot ) ; ::_thesis: (fD (((cot (#) cot) (#) sin),h)) . x = ((cot (#) cos) . (x + h)) - ((cot (#) cos) . x) ( x in dom ((cot (#) cot) (#) sin) & x + h in dom ((cot (#) cot) (#) sin) ) proof set f1 = cot (#) cot; set f2 = sin ; A2: ( x in dom (cot (#) cot) & x + h in dom (cot (#) cot) ) proof ( x in (dom cot) /\ (dom cot) & x + h in (dom cot) /\ (dom cot) ) by A1; hence ( x in dom (cot (#) cot) & x + h in dom (cot (#) cot) ) by VALUED_1:def_4; ::_thesis: verum end; ( x in (dom (cot (#) cot)) /\ (dom sin) & x + h in (dom (cot (#) cot)) /\ (dom sin) ) by A2, SIN_COS:24, XBOOLE_0:def_4; hence ( x in dom ((cot (#) cot) (#) sin) & x + h in dom ((cot (#) cot) (#) sin) ) by VALUED_1:def_4; ::_thesis: verum end; then (fD (((cot (#) cot) (#) sin),h)) . x = (((cot (#) cot) (#) sin) . (x + h)) - (((cot (#) cot) (#) sin) . x) by DIFF_1:1 .= (((cot (#) cot) . (x + h)) * (sin . (x + h))) - (((cot (#) cot) (#) sin) . x) by VALUED_1:5 .= (((cot . (x + h)) * (cot . (x + h))) * (sin . (x + h))) - (((cot (#) cot) (#) sin) . x) by VALUED_1:5 .= (((cot . (x + h)) * (cot . (x + h))) * (sin . (x + h))) - (((cot (#) cot) . x) * (sin . x)) by VALUED_1:5 .= (((cot . (x + h)) * (cot . (x + h))) * (sin . (x + h))) - (((cot . x) * (cot . x)) * (sin . x)) by VALUED_1:5 .= ((((cos . (x + h)) * ((sin . (x + h)) ")) * (cot . (x + h))) * (sin . (x + h))) - (((cot . x) * (cot . x)) * (sin . x)) by A1, RFUNCT_1:def_1 .= ((((cos . (x + h)) * ((sin . (x + h)) ")) * (cot . (x + h))) * (sin . (x + h))) - ((((cos . x) * ((sin . x) ")) * (cot . x)) * (sin . x)) by A1, RFUNCT_1:def_1 .= (((cot . (x + h)) * (cos . (x + h))) * ((sin . (x + h)) * (1 / (sin . (x + h))))) - (((cot . x) * (cos . x)) * ((sin . x) * (1 / (sin . x)))) .= (((cot . (x + h)) * (cos . (x + h))) * 1) - (((cot . x) * (cos . x)) * ((sin . x) * (1 / (sin . x)))) by A1, FDIFF_8:2, XCMPLX_1:106 .= (((cot . (x + h)) * (cos . (x + h))) * 1) - (((cot . x) * (cos . x)) * 1) by A1, FDIFF_8:2, XCMPLX_1:106 .= ((cot (#) cos) . (x + h)) - ((cot . x) * (cos . x)) by VALUED_1:5 .= ((cot (#) cos) . (x + h)) - ((cot (#) cos) . x) by VALUED_1:5 ; hence (fD (((cot (#) cot) (#) sin),h)) . x = ((cot (#) cos) . (x + h)) - ((cot (#) cos) . x) ; ::_thesis: verum end; theorem :: DIFF_4:28 for x, h being Real st x in dom cot & x - h in dom cot holds (bD (((cot (#) cot) (#) sin),h)) . x = ((cot (#) cos) . x) - ((cot (#) cos) . (x - h)) proof let x, h be Real; ::_thesis: ( x in dom cot & x - h in dom cot implies (bD (((cot (#) cot) (#) sin),h)) . x = ((cot (#) cos) . x) - ((cot (#) cos) . (x - h)) ) set f = (cot (#) cot) (#) sin; assume A1: ( x in dom cot & x - h in dom cot ) ; ::_thesis: (bD (((cot (#) cot) (#) sin),h)) . x = ((cot (#) cos) . x) - ((cot (#) cos) . (x - h)) ( x in dom ((cot (#) cot) (#) sin) & x - h in dom ((cot (#) cot) (#) sin) ) proof set f1 = cot (#) cot; set f2 = sin ; A2: ( x in dom (cot (#) cot) & x - h in dom (cot (#) cot) ) proof ( x in (dom cot) /\ (dom cot) & x - h in (dom cot) /\ (dom cot) ) by A1; hence ( x in dom (cot (#) cot) & x - h in dom (cot (#) cot) ) by VALUED_1:def_4; ::_thesis: verum end; ( x in (dom (cot (#) cot)) /\ (dom sin) & x - h in (dom (cot (#) cot)) /\ (dom sin) ) by A2, SIN_COS:24, XBOOLE_0:def_4; hence ( x in dom ((cot (#) cot) (#) sin) & x - h in dom ((cot (#) cot) (#) sin) ) by VALUED_1:def_4; ::_thesis: verum end; then (bD (((cot (#) cot) (#) sin),h)) . x = (((cot (#) cot) (#) sin) . x) - (((cot (#) cot) (#) sin) . (x - h)) by DIFF_1:38 .= (((cot (#) cot) . x) * (sin . x)) - (((cot (#) cot) (#) sin) . (x - h)) by VALUED_1:5 .= (((cot . x) * (cot . x)) * (sin . x)) - (((cot (#) cot) (#) sin) . (x - h)) by VALUED_1:5 .= (((cot . x) * (cot . x)) * (sin . x)) - (((cot (#) cot) . (x - h)) * (sin . (x - h))) by VALUED_1:5 .= (((cot . x) * (cot . x)) * (sin . x)) - (((cot . (x - h)) * (cot . (x - h))) * (sin . (x - h))) by VALUED_1:5 .= ((((cos . x) * ((sin . x) ")) * (cot . x)) * (sin . x)) - (((cot . (x - h)) * (cot . (x - h))) * (sin . (x - h))) by A1, RFUNCT_1:def_1 .= ((((cos . x) * ((sin . x) ")) * (cot . x)) * (sin . x)) - ((((cos . (x - h)) * ((sin . (x - h)) ")) * (cot . (x - h))) * (sin . (x - h))) by A1, RFUNCT_1:def_1 .= (((cot . x) * (cos . x)) * ((sin . x) * (1 / (sin . x)))) - (((cot . (x - h)) * (cos . (x - h))) * ((sin . (x - h)) * (1 / (sin . (x - h))))) .= (((cot . x) * (cos . x)) * 1) - (((cot . (x - h)) * (cos . (x - h))) * ((sin . (x - h)) * (1 / (sin . (x - h))))) by A1, FDIFF_8:2, XCMPLX_1:106 .= (((cot . x) * (cos . x)) * 1) - (((cot . (x - h)) * (cos . (x - h))) * 1) by A1, FDIFF_8:2, XCMPLX_1:106 .= ((cot (#) cos) . x) - ((cot . (x - h)) * (cos . (x - h))) by VALUED_1:5 .= ((cot (#) cos) . x) - ((cot (#) cos) . (x - h)) by VALUED_1:5 ; hence (bD (((cot (#) cot) (#) sin),h)) . x = ((cot (#) cos) . x) - ((cot (#) cos) . (x - h)) ; ::_thesis: verum end; theorem :: DIFF_4:29 for x, h being Real st x + (h / 2) in dom cot & x - (h / 2) in dom cot holds (cD (((cot (#) cot) (#) sin),h)) . x = ((cot (#) cos) . (x + (h / 2))) - ((cot (#) cos) . (x - (h / 2))) proof let x, h be Real; ::_thesis: ( x + (h / 2) in dom cot & x - (h / 2) in dom cot implies (cD (((cot (#) cot) (#) sin),h)) . x = ((cot (#) cos) . (x + (h / 2))) - ((cot (#) cos) . (x - (h / 2))) ) set f = (cot (#) cot) (#) sin; assume A1: ( x + (h / 2) in dom cot & x - (h / 2) in dom cot ) ; ::_thesis: (cD (((cot (#) cot) (#) sin),h)) . x = ((cot (#) cos) . (x + (h / 2))) - ((cot (#) cos) . (x - (h / 2))) ( x + (h / 2) in dom ((cot (#) cot) (#) sin) & x - (h / 2) in dom ((cot (#) cot) (#) sin) ) proof set f1 = cot (#) cot; set f2 = sin ; A2: ( x + (h / 2) in dom (cot (#) cot) & x - (h / 2) in dom (cot (#) cot) ) proof ( x + (h / 2) in (dom cot) /\ (dom cot) & x - (h / 2) in (dom cot) /\ (dom cot) ) by A1; hence ( x + (h / 2) in dom (cot (#) cot) & x - (h / 2) in dom (cot (#) cot) ) by VALUED_1:def_4; ::_thesis: verum end; ( x + (h / 2) in (dom (cot (#) cot)) /\ (dom sin) & x - (h / 2) in (dom (cot (#) cot)) /\ (dom sin) ) by A2, SIN_COS:24, XBOOLE_0:def_4; hence ( x + (h / 2) in dom ((cot (#) cot) (#) sin) & x - (h / 2) in dom ((cot (#) cot) (#) sin) ) by VALUED_1:def_4; ::_thesis: verum end; then (cD (((cot (#) cot) (#) sin),h)) . x = (((cot (#) cot) (#) sin) . (x + (h / 2))) - (((cot (#) cot) (#) sin) . (x - (h / 2))) by DIFF_1:39 .= (((cot (#) cot) . (x + (h / 2))) * (sin . (x + (h / 2)))) - (((cot (#) cot) (#) sin) . (x - (h / 2))) by VALUED_1:5 .= (((cot . (x + (h / 2))) * (cot . (x + (h / 2)))) * (sin . (x + (h / 2)))) - (((cot (#) cot) (#) sin) . (x - (h / 2))) by VALUED_1:5 .= (((cot . (x + (h / 2))) * (cot . (x + (h / 2)))) * (sin . (x + (h / 2)))) - (((cot (#) cot) . (x - (h / 2))) * (sin . (x - (h / 2)))) by VALUED_1:5 .= (((cot . (x + (h / 2))) * (cot . (x + (h / 2)))) * (sin . (x + (h / 2)))) - (((cot . (x - (h / 2))) * (cot . (x - (h / 2)))) * (sin . (x - (h / 2)))) by VALUED_1:5 .= ((((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) ")) * (cot . (x + (h / 2)))) * (sin . (x + (h / 2)))) - (((cot . (x - (h / 2))) * (cot . (x - (h / 2)))) * (sin . (x - (h / 2)))) by A1, RFUNCT_1:def_1 .= ((((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) ")) * (cot . (x + (h / 2)))) * (sin . (x + (h / 2)))) - ((((cos . (x - (h / 2))) * ((sin . (x - (h / 2))) ")) * (cot . (x - (h / 2)))) * (sin . (x - (h / 2)))) by A1, RFUNCT_1:def_1 .= (((cot . (x + (h / 2))) * (cos . (x + (h / 2)))) * ((sin . (x + (h / 2))) * (1 / (sin . (x + (h / 2)))))) - (((cot . (x - (h / 2))) * (cos . (x - (h / 2)))) * ((sin . (x - (h / 2))) * (1 / (sin . (x - (h / 2)))))) .= (((cot . (x + (h / 2))) * (cos . (x + (h / 2)))) * 1) - (((cot . (x - (h / 2))) * (cos . (x - (h / 2)))) * ((sin . (x - (h / 2))) * (1 / (sin . (x - (h / 2)))))) by A1, FDIFF_8:2, XCMPLX_1:106 .= (((cot . (x + (h / 2))) * (cos . (x + (h / 2)))) * 1) - (((cot . (x - (h / 2))) * (cos . (x - (h / 2)))) * 1) by A1, FDIFF_8:2, XCMPLX_1:106 .= ((cot (#) cos) . (x + (h / 2))) - ((cot . (x - (h / 2))) * (cos . (x - (h / 2)))) by VALUED_1:5 .= ((cot (#) cos) . (x + (h / 2))) - ((cot (#) cos) . (x - (h / 2))) by VALUED_1:5 ; hence (cD (((cot (#) cot) (#) sin),h)) . x = ((cot (#) cos) . (x + (h / 2))) - ((cot (#) cos) . (x - (h / 2))) ; ::_thesis: verum end; theorem :: DIFF_4:30 for x0, x1 being Real st x0 > 0 & x1 > 0 holds [!ln,x0,x1!] = (ln . (x0 / x1)) / (x0 - x1) by Th4; theorem :: DIFF_4:31 for x, h being Real st x > 0 & x + h > 0 holds (fD (ln,h)) . x = ln . (1 + (h / x)) proof let x, h be Real; ::_thesis: ( x > 0 & x + h > 0 implies (fD (ln,h)) . x = ln . (1 + (h / x)) ) set f = ln ; assume A1: ( x > 0 & x + h > 0 ) ; ::_thesis: (fD (ln,h)) . x = ln . (1 + (h / x)) A2: x in right_open_halfline 0 proof x in { g where g is Real : 0 < g } by A1; hence x in right_open_halfline 0 by XXREAL_1:230; ::_thesis: verum end; A3: x + h in right_open_halfline 0 proof x + h in { g where g is Real : 0 < g } by A1; hence x + h in right_open_halfline 0 by XXREAL_1:230; ::_thesis: verum end; (fD (ln,h)) . x = (ln . (x + h)) - (ln . x) by A2, A3, DIFF_1:1, TAYLOR_1:18 .= ln . ((x + h) / x) by A1, Th4 .= ln . ((x / x) + (h / x)) .= ln . (1 + (h / x)) by A1, XCMPLX_1:60 ; hence (fD (ln,h)) . x = ln . (1 + (h / x)) ; ::_thesis: verum end; theorem :: DIFF_4:32 for x, h being Real st x > 0 & x - h > 0 holds (bD (ln,h)) . x = ln . (1 + (h / (x - h))) proof let x, h be Real; ::_thesis: ( x > 0 & x - h > 0 implies (bD (ln,h)) . x = ln . (1 + (h / (x - h))) ) set f = ln ; assume A1: ( x > 0 & x - h > 0 ) ; ::_thesis: (bD (ln,h)) . x = ln . (1 + (h / (x - h))) A2: x in right_open_halfline 0 proof x in { g where g is Real : 0 < g } by A1; hence x in right_open_halfline 0 by XXREAL_1:230; ::_thesis: verum end; A3: x - h in right_open_halfline 0 proof x - h in { g where g is Real : 0 < g } by A1; hence x - h in right_open_halfline 0 by XXREAL_1:230; ::_thesis: verum end; (bD (ln,h)) . x = (ln . x) - (ln . (x - h)) by A2, A3, DIFF_1:38, TAYLOR_1:18 .= ln . (x / (x - h)) by A1, Th4 .= ln . (((x - h) / (x - h)) + (h / (x - h))) .= ln . (1 + (h / (x - h))) by A1, XCMPLX_1:60 ; hence (bD (ln,h)) . x = ln . (1 + (h / (x - h))) ; ::_thesis: verum end; theorem :: DIFF_4:33 for x, h being Real st x + (h / 2) > 0 & x - (h / 2) > 0 holds (cD (ln,h)) . x = ln . (1 + (h / (x - (h / 2)))) proof let x, h be Real; ::_thesis: ( x + (h / 2) > 0 & x - (h / 2) > 0 implies (cD (ln,h)) . x = ln . (1 + (h / (x - (h / 2)))) ) set f = ln ; assume A1: ( x + (h / 2) > 0 & x - (h / 2) > 0 ) ; ::_thesis: (cD (ln,h)) . x = ln . (1 + (h / (x - (h / 2)))) A2: x + (h / 2) in right_open_halfline 0 proof x + (h / 2) in { g where g is Real : 0 < g } by A1; hence x + (h / 2) in right_open_halfline 0 by XXREAL_1:230; ::_thesis: verum end; A3: x - (h / 2) in right_open_halfline 0 proof x - (h / 2) in { g where g is Real : 0 < g } by A1; hence x - (h / 2) in right_open_halfline 0 by XXREAL_1:230; ::_thesis: verum end; (cD (ln,h)) . x = (ln . (x + (h / 2))) - (ln . (x - (h / 2))) by A2, A3, DIFF_1:39, TAYLOR_1:18 .= ln . (((x - (h / 2)) + h) / (x - (h / 2))) by A1, Th4 .= ln . (((x - (h / 2)) / (x - (h / 2))) + (h / (x - (h / 2)))) .= ln . (1 + (h / (x - (h / 2)))) by A1, XCMPLX_1:60 ; hence (cD (ln,h)) . x = ln . (1 + (h / (x - (h / 2)))) ; ::_thesis: verum end; theorem :: DIFF_4:34 for h, k being real number holds exp_R (h - k) = (exp_R h) / (exp_R k) proof let h, k be real number ; ::_thesis: exp_R (h - k) = (exp_R h) / (exp_R k) exp_R (h - k) = (exp_R h) * (exp_R (- k)) by SIN_COS:50 .= (exp_R h) * (1 / (exp_R k)) by TAYLOR_1:4 .= (exp_R h) / (exp_R k) ; hence exp_R (h - k) = (exp_R h) / (exp_R k) ; ::_thesis: verum end; theorem :: DIFF_4:35 for h, x being Real for f being Function of REAL,REAL holds (fD (f,h)) . x = ((Shift (f,h)) . x) - (f . x) proof let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds (fD (f,h)) . x = ((Shift (f,h)) . x) - (f . x) let f be Function of REAL,REAL; ::_thesis: (fD (f,h)) . x = ((Shift (f,h)) . x) - (f . x) (fD (f,h)) . x = ((fdif (f,h)) . 1) . x by DIFF_3:7 .= ((Shift (f,h)) . x) - (f . x) by DIFF_1:11 ; hence (fD (f,h)) . x = ((Shift (f,h)) . x) - (f . x) ; ::_thesis: verum end; theorem :: DIFF_4:36 for h, x0, x1 being Real for f, g being Function of REAL,REAL st ( for x being Real holds f . x = (fD (g,h)) . x ) holds [!f,x0,x1!] = [!g,(x0 + h),(x1 + h)!] - [!g,x0,x1!] proof let h, x0, x1 be Real; ::_thesis: for f, g being Function of REAL,REAL st ( for x being Real holds f . x = (fD (g,h)) . x ) holds [!f,x0,x1!] = [!g,(x0 + h),(x1 + h)!] - [!g,x0,x1!] let f, g be Function of REAL,REAL; ::_thesis: ( ( for x being Real holds f . x = (fD (g,h)) . x ) implies [!f,x0,x1!] = [!g,(x0 + h),(x1 + h)!] - [!g,x0,x1!] ) assume A1: for x being Real holds f . x = (fD (g,h)) . x ; ::_thesis: [!f,x0,x1!] = [!g,(x0 + h),(x1 + h)!] - [!g,x0,x1!] [!f,x0,x1!] = (((fD (g,h)) . x0) - (f . x1)) / (x0 - x1) by A1 .= (((fD (g,h)) . x0) - ((fD (g,h)) . x1)) / (x0 - x1) by A1 .= (((g . (x0 + h)) - (g . x0)) - ((fD (g,h)) . x1)) / (x0 - x1) by DIFF_1:3 .= (((g . (x0 + h)) - (g . x0)) - ((g . (x1 + h)) - (g . x1))) / (x0 - x1) by DIFF_1:3 .= [!g,(x0 + h),(x1 + h)!] - [!g,x0,x1!] ; hence [!f,x0,x1!] = [!g,(x0 + h),(x1 + h)!] - [!g,x0,x1!] ; ::_thesis: verum end; theorem :: DIFF_4:37 for h, x being Real for f being Function of REAL,REAL holds (fD ((fD (f,h)),h)) . x = ((fD (f,(2 * h))) . x) - (2 * ((fD (f,h)) . x)) proof let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds (fD ((fD (f,h)),h)) . x = ((fD (f,(2 * h))) . x) - (2 * ((fD (f,h)) . x)) let f be Function of REAL,REAL; ::_thesis: (fD ((fD (f,h)),h)) . x = ((fD (f,(2 * h))) . x) - (2 * ((fD (f,h)) . x)) (fD ((fD (f,h)),h)) . x = ((fD (f,h)) . (x + h)) - ((fD (f,h)) . x) by DIFF_1:3 .= ((f . ((x + h) + h)) - (f . (x + h))) - ((fD (f,h)) . x) by DIFF_1:3 .= ((f . ((x + h) + h)) - (f . (x + h))) - ((f . (x + h)) - (f . x)) by DIFF_1:3 .= ((f . (x + (2 * h))) - (f . x)) - ((2 * (f . (x + h))) - (2 * (f . x))) .= ((fD (f,(2 * h))) . x) - (2 * ((f . (x + h)) - (f . x))) by DIFF_1:3 .= ((fD (f,(2 * h))) . x) - (2 * ((fD (f,h)) . x)) by DIFF_1:3 ; hence (fD ((fD (f,h)),h)) . x = ((fD (f,(2 * h))) . x) - (2 * ((fD (f,h)) . x)) ; ::_thesis: verum end; theorem :: DIFF_4:38 for h, x being Real for f being Function of REAL,REAL holds (bD ((fD (f,h)),h)) . x = ((fD (f,h)) . x) - ((bD (f,h)) . x) proof let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds (bD ((fD (f,h)),h)) . x = ((fD (f,h)) . x) - ((bD (f,h)) . x) let f be Function of REAL,REAL; ::_thesis: (bD ((fD (f,h)),h)) . x = ((fD (f,h)) . x) - ((bD (f,h)) . x) (bD ((fD (f,h)),h)) . x = ((fD (f,h)) . x) - ((fD (f,h)) . (x - h)) by DIFF_1:4 .= ((fD (f,h)) . x) - ((f . ((x - h) + h)) - (f . (x - h))) by DIFF_1:3 .= ((fD (f,h)) . x) - ((bD (f,h)) . x) by DIFF_1:4 ; hence (bD ((fD (f,h)),h)) . x = ((fD (f,h)) . x) - ((bD (f,h)) . x) ; ::_thesis: verum end; theorem :: DIFF_4:39 for h, x being Real for f being Function of REAL,REAL holds (cD ((fD (f,h)),h)) . x = ((fD (f,h)) . (x + (h / 2))) - ((cD (f,h)) . x) proof let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds (cD ((fD (f,h)),h)) . x = ((fD (f,h)) . (x + (h / 2))) - ((cD (f,h)) . x) let f be Function of REAL,REAL; ::_thesis: (cD ((fD (f,h)),h)) . x = ((fD (f,h)) . (x + (h / 2))) - ((cD (f,h)) . x) (cD ((fD (f,h)),h)) . x = ((fD (f,h)) . (x + (h / 2))) - ((fD (f,h)) . (x - (h / 2))) by DIFF_1:5 .= ((fD (f,h)) . (x + (h / 2))) - ((f . ((x - (h / 2)) + h)) - (f . (x - (h / 2)))) by DIFF_1:3 .= ((fD (f,h)) . (x + (h / 2))) - ((cD (f,h)) . x) by DIFF_1:5 ; hence (cD ((fD (f,h)),h)) . x = ((fD (f,h)) . (x + (h / 2))) - ((cD (f,h)) . x) ; ::_thesis: verum end; theorem Th40: :: DIFF_4:40 for h, x being Real for f being Function of REAL,REAL holds ((fdif (f,h)) . 1) . x = (((fdif (f,h)) . 0) . (x + h)) - (((fdif (f,h)) . 0) . x) proof let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds ((fdif (f,h)) . 1) . x = (((fdif (f,h)) . 0) . (x + h)) - (((fdif (f,h)) . 0) . x) let f be Function of REAL,REAL; ::_thesis: ((fdif (f,h)) . 1) . x = (((fdif (f,h)) . 0) . (x + h)) - (((fdif (f,h)) . 0) . x) ((fdif (f,h)) . 1) . x = (fD (f,h)) . x by DIFF_3:7 .= (f . (x + h)) - (f . x) by DIFF_1:3 .= (((fdif (f,h)) . 0) . (x + h)) - (f . x) by DIFF_1:def_6 .= (((fdif (f,h)) . 0) . (x + h)) - (((fdif (f,h)) . 0) . x) by DIFF_1:def_6 ; hence ((fdif (f,h)) . 1) . x = (((fdif (f,h)) . 0) . (x + h)) - (((fdif (f,h)) . 0) . x) ; ::_thesis: verum end; theorem :: DIFF_4:41 for n being Element of NAT for h, x being Real for f being Function of REAL,REAL holds ((fdif (f,h)) . (n + 1)) . x = (((fdif (f,h)) . n) . (x + h)) - (((fdif (f,h)) . n) . x) proof let n be Element of NAT ; ::_thesis: for h, x being Real for f being Function of REAL,REAL holds ((fdif (f,h)) . (n + 1)) . x = (((fdif (f,h)) . n) . (x + h)) - (((fdif (f,h)) . n) . x) let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds ((fdif (f,h)) . (n + 1)) . x = (((fdif (f,h)) . n) . (x + h)) - (((fdif (f,h)) . n) . x) let f be Function of REAL,REAL; ::_thesis: ((fdif (f,h)) . (n + 1)) . x = (((fdif (f,h)) . n) . (x + h)) - (((fdif (f,h)) . n) . x) defpred S1[ Element of NAT ] means ((fdif (f,h)) . (\$1 + 1)) . x = (((fdif (f,h)) . \$1) . (x + h)) - (((fdif (f,h)) . \$1) . x); A1: for i being Element of NAT st S1[i] holds S1[i + 1] proof let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] ) assume ((fdif (f,h)) . (i + 1)) . x = (((fdif (f,h)) . i) . (x + h)) - (((fdif (f,h)) . i) . x) ; ::_thesis: S1[i + 1] A2: (fdif (f,h)) . (i + 1) is Function of REAL,REAL by DIFF_1:2; ((fdif (f,h)) . (i + 2)) . x = ((fdif (f,h)) . ((i + 1) + 1)) . x .= (fD (((fdif (f,h)) . (i + 1)),h)) . x by DIFF_1:def_6 .= (((fdif (f,h)) . (i + 1)) . (x + h)) - (((fdif (f,h)) . (i + 1)) . x) by A2, DIFF_1:3 ; hence S1[i + 1] ; ::_thesis: verum end; A3: S1[ 0 ] by Th40; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1); hence ((fdif (f,h)) . (n + 1)) . x = (((fdif (f,h)) . n) . (x + h)) - (((fdif (f,h)) . n) . x) ; ::_thesis: verum end; theorem :: DIFF_4:42 for h, x being Real for f being Function of REAL,REAL holds (bD (f,h)) . x = (f . x) - ((Shift (f,(- h))) . x) proof let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds (bD (f,h)) . x = (f . x) - ((Shift (f,(- h))) . x) let f be Function of REAL,REAL; ::_thesis: (bD (f,h)) . x = (f . x) - ((Shift (f,(- h))) . x) (bD (f,h)) . x = ((bdif (f,h)) . 1) . x by DIFF_3:11 .= (f . x) - ((Shift (f,(- h))) . x) by DIFF_1:18 ; hence (bD (f,h)) . x = (f . x) - ((Shift (f,(- h))) . x) ; ::_thesis: verum end; theorem :: DIFF_4:43 for h, x0, x1 being Real for f, g being Function of REAL,REAL st ( for x being Real holds f . x = (bD (g,h)) . x ) holds [!f,x0,x1!] = [!g,x0,x1!] - [!g,(x0 - h),(x1 - h)!] proof let h, x0, x1 be Real; ::_thesis: for f, g being Function of REAL,REAL st ( for x being Real holds f . x = (bD (g,h)) . x ) holds [!f,x0,x1!] = [!g,x0,x1!] - [!g,(x0 - h),(x1 - h)!] let f, g be Function of REAL,REAL; ::_thesis: ( ( for x being Real holds f . x = (bD (g,h)) . x ) implies [!f,x0,x1!] = [!g,x0,x1!] - [!g,(x0 - h),(x1 - h)!] ) assume A1: for x being Real holds f . x = (bD (g,h)) . x ; ::_thesis: [!f,x0,x1!] = [!g,x0,x1!] - [!g,(x0 - h),(x1 - h)!] [!f,x0,x1!] = (((bD (g,h)) . x0) - (f . x1)) / (x0 - x1) by A1 .= (((bD (g,h)) . x0) - ((bD (g,h)) . x1)) / (x0 - x1) by A1 .= (((g . x0) - (g . (x0 - h))) - ((bD (g,h)) . x1)) / (x0 - x1) by DIFF_1:4 .= (((g . x0) - (g . (x0 - h))) - ((g . x1) - (g . (x1 - h)))) / (x0 - x1) by DIFF_1:4 .= [!g,x0,x1!] - [!g,(x0 - h),(x1 - h)!] ; hence [!f,x0,x1!] = [!g,x0,x1!] - [!g,(x0 - h),(x1 - h)!] ; ::_thesis: verum end; theorem :: DIFF_4:44 for h, x being Real for f being Function of REAL,REAL holds (fD ((bD (f,h)),h)) . x = ((fD (f,h)) . x) - ((bD (f,h)) . x) proof let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds (fD ((bD (f,h)),h)) . x = ((fD (f,h)) . x) - ((bD (f,h)) . x) let f be Function of REAL,REAL; ::_thesis: (fD ((bD (f,h)),h)) . x = ((fD (f,h)) . x) - ((bD (f,h)) . x) (fD ((bD (f,h)),h)) . x = ((bD (f,h)) . (x + h)) - ((bD (f,h)) . x) by DIFF_1:3 .= ((f . (x + h)) - (f . ((x + h) - h))) - ((bD (f,h)) . x) by DIFF_1:4 .= ((fD (f,h)) . x) - ((bD (f,h)) . x) by DIFF_1:3 ; hence (fD ((bD (f,h)),h)) . x = ((fD (f,h)) . x) - ((bD (f,h)) . x) ; ::_thesis: verum end; theorem :: DIFF_4:45 for h, x being Real for f being Function of REAL,REAL holds (bD ((bD (f,h)),h)) . x = (2 * ((bD (f,h)) . x)) - ((bD (f,(2 * h))) . x) proof let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds (bD ((bD (f,h)),h)) . x = (2 * ((bD (f,h)) . x)) - ((bD (f,(2 * h))) . x) let f be Function of REAL,REAL; ::_thesis: (bD ((bD (f,h)),h)) . x = (2 * ((bD (f,h)) . x)) - ((bD (f,(2 * h))) . x) (bD ((bD (f,h)),h)) . x = ((bD (f,h)) . x) - ((bD (f,h)) . (x - h)) by DIFF_1:4 .= ((f . x) - (f . (x - h))) - ((bD (f,h)) . (x - h)) by DIFF_1:4 .= ((f . x) - (f . (x - h))) - ((f . (x - h)) - (f . ((x - h) - h))) by DIFF_1:4 .= (2 * ((f . x) - (f . (x - h)))) - ((f . x) - (f . (x - (2 * h)))) .= (2 * ((bD (f,h)) . x)) - ((f . x) - (f . (x - (2 * h)))) by DIFF_1:4 .= (2 * ((bD (f,h)) . x)) - ((bD (f,(2 * h))) . x) by DIFF_1:4 ; hence (bD ((bD (f,h)),h)) . x = (2 * ((bD (f,h)) . x)) - ((bD (f,(2 * h))) . x) ; ::_thesis: verum end; theorem :: DIFF_4:46 for h, x being Real for f being Function of REAL,REAL holds (cD ((bD (f,h)),h)) . x = ((cD (f,h)) . x) - ((bD (f,h)) . (x - (h / 2))) proof let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds (cD ((bD (f,h)),h)) . x = ((cD (f,h)) . x) - ((bD (f,h)) . (x - (h / 2))) let f be Function of REAL,REAL; ::_thesis: (cD ((bD (f,h)),h)) . x = ((cD (f,h)) . x) - ((bD (f,h)) . (x - (h / 2))) (cD ((bD (f,h)),h)) . x = ((bD (f,h)) . (x + (h / 2))) - ((bD (f,h)) . (x - (h / 2))) by DIFF_1:5 .= ((f . (x + (h / 2))) - (f . ((x + (h / 2)) - h))) - ((bD (f,h)) . (x - (h / 2))) by DIFF_1:4 .= ((cD (f,h)) . x) - ((bD (f,h)) . (x - (h / 2))) by DIFF_1:5 ; hence (cD ((bD (f,h)),h)) . x = ((cD (f,h)) . x) - ((bD (f,h)) . (x - (h / 2))) ; ::_thesis: verum end; theorem Th47: :: DIFF_4:47 for h, x being Real for f being Function of REAL,REAL holds ((bdif (f,h)) . 1) . x = (((bdif (f,h)) . 0) . x) - (((bdif (f,h)) . 0) . (x - h)) proof let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds ((bdif (f,h)) . 1) . x = (((bdif (f,h)) . 0) . x) - (((bdif (f,h)) . 0) . (x - h)) let f be Function of REAL,REAL; ::_thesis: ((bdif (f,h)) . 1) . x = (((bdif (f,h)) . 0) . x) - (((bdif (f,h)) . 0) . (x - h)) ((bdif (f,h)) . 1) . x = (bD (f,h)) . x by DIFF_3:11 .= (f . x) - (f . (x - h)) by DIFF_1:4 .= (((bdif (f,h)) . 0) . x) - (f . (x - h)) by DIFF_1:def_7 .= (((bdif (f,h)) . 0) . x) - (((bdif (f,h)) . 0) . (x - h)) by DIFF_1:def_7 ; hence ((bdif (f,h)) . 1) . x = (((bdif (f,h)) . 0) . x) - (((bdif (f,h)) . 0) . (x - h)) ; ::_thesis: verum end; theorem :: DIFF_4:48 for n being Element of NAT for h, x being Real for f being Function of REAL,REAL holds ((bdif (f,h)) . (n + 1)) . x = (((bdif (f,h)) . n) . x) - (((bdif (f,h)) . n) . (x - h)) proof let n be Element of NAT ; ::_thesis: for h, x being Real for f being Function of REAL,REAL holds ((bdif (f,h)) . (n + 1)) . x = (((bdif (f,h)) . n) . x) - (((bdif (f,h)) . n) . (x - h)) let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds ((bdif (f,h)) . (n + 1)) . x = (((bdif (f,h)) . n) . x) - (((bdif (f,h)) . n) . (x - h)) let f be Function of REAL,REAL; ::_thesis: ((bdif (f,h)) . (n + 1)) . x = (((bdif (f,h)) . n) . x) - (((bdif (f,h)) . n) . (x - h)) defpred S1[ Element of NAT ] means ((bdif (f,h)) . (\$1 + 1)) . x = (((bdif (f,h)) . \$1) . x) - (((bdif (f,h)) . \$1) . (x - h)); A1: for i being Element of NAT st S1[i] holds S1[i + 1] proof let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] ) assume ((bdif (f,h)) . (i + 1)) . x = (((bdif (f,h)) . i) . x) - (((bdif (f,h)) . i) . (x - h)) ; ::_thesis: S1[i + 1] A2: (bdif (f,h)) . (i + 1) is Function of REAL,REAL by DIFF_1:12; ((bdif (f,h)) . (i + 2)) . x = ((bdif (f,h)) . ((i + 1) + 1)) . x .= (bD (((bdif (f,h)) . (i + 1)),h)) . x by DIFF_1:def_7 .= (((bdif (f,h)) . (i + 1)) . x) - (((bdif (f,h)) . (i + 1)) . (x - h)) by A2, DIFF_1:4 ; hence S1[i + 1] ; ::_thesis: verum end; A3: S1[ 0 ] by Th47; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1); hence ((bdif (f,h)) . (n + 1)) . x = (((bdif (f,h)) . n) . x) - (((bdif (f,h)) . n) . (x - h)) ; ::_thesis: verum end; theorem :: DIFF_4:49 for h, x being Real for f being Function of REAL,REAL holds (cD (f,h)) . x = ((Shift (f,(h / 2))) . x) - ((Shift (f,(- (h / 2)))) . x) proof let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds (cD (f,h)) . x = ((Shift (f,(h / 2))) . x) - ((Shift (f,(- (h / 2)))) . x) let f be Function of REAL,REAL; ::_thesis: (cD (f,h)) . x = ((Shift (f,(h / 2))) . x) - ((Shift (f,(- (h / 2)))) . x) (cD (f,h)) . x = ((cdif (f,h)) . 1) . x by DIFF_3:16 .= ((Shift (f,(h / 2))) . x) - ((Shift (f,(- (h / 2)))) . x) by DIFF_1:25 ; hence (cD (f,h)) . x = ((Shift (f,(h / 2))) . x) - ((Shift (f,(- (h / 2)))) . x) ; ::_thesis: verum end; theorem :: DIFF_4:50 for h, x0, x1 being Real for f, g being Function of REAL,REAL st ( for x being Real holds f . x = (cD (g,h)) . x ) holds [!f,x0,x1!] = [!g,(x0 + (h / 2)),(x1 + (h / 2))!] - [!g,(x0 - (h / 2)),(x1 - (h / 2))!] proof let h, x0, x1 be Real; ::_thesis: for f, g being Function of REAL,REAL st ( for x being Real holds f . x = (cD (g,h)) . x ) holds [!f,x0,x1!] = [!g,(x0 + (h / 2)),(x1 + (h / 2))!] - [!g,(x0 - (h / 2)),(x1 - (h / 2))!] let f, g be Function of REAL,REAL; ::_thesis: ( ( for x being Real holds f . x = (cD (g,h)) . x ) implies [!f,x0,x1!] = [!g,(x0 + (h / 2)),(x1 + (h / 2))!] - [!g,(x0 - (h / 2)),(x1 - (h / 2))!] ) assume A1: for x being Real holds f . x = (cD (g,h)) . x ; ::_thesis: [!f,x0,x1!] = [!g,(x0 + (h / 2)),(x1 + (h / 2))!] - [!g,(x0 - (h / 2)),(x1 - (h / 2))!] [!f,x0,x1!] = (((cD (g,h)) . x0) - (f . x1)) / (x0 - x1) by A1 .= (((cD (g,h)) . x0) - ((cD (g,h)) . x1)) / (x0 - x1) by A1 .= (((g . (x0 + (h / 2))) - (g . (x0 - (h / 2)))) - ((cD (g,h)) . x1)) / (x0 - x1) by DIFF_1:5 .= (((g . (x0 + (h / 2))) - (g . (x0 - (h / 2)))) - ((g . (x1 + (h / 2))) - (g . (x1 - (h / 2))))) / (x0 - x1) by DIFF_1:5 .= [!g,(x0 + (h / 2)),(x1 + (h / 2))!] - [!g,(x0 - (h / 2)),(x1 - (h / 2))!] ; hence [!f,x0,x1!] = [!g,(x0 + (h / 2)),(x1 + (h / 2))!] - [!g,(x0 - (h / 2)),(x1 - (h / 2))!] ; ::_thesis: verum end; theorem :: DIFF_4:51 for h, x being Real for f being Function of REAL,REAL holds (fD ((cD (f,h)),h)) . x = ((fD (f,h)) . (x + (h / 2))) - ((cD (f,h)) . x) proof let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds (fD ((cD (f,h)),h)) . x = ((fD (f,h)) . (x + (h / 2))) - ((cD (f,h)) . x) let f be Function of REAL,REAL; ::_thesis: (fD ((cD (f,h)),h)) . x = ((fD (f,h)) . (x + (h / 2))) - ((cD (f,h)) . x) (fD ((cD (f,h)),h)) . x = ((cD (f,h)) . (x + h)) - ((cD (f,h)) . x) by DIFF_1:3 .= ((f . ((x + h) + (h / 2))) - (f . ((x + h) - (h / 2)))) - ((cD (f,h)) . x) by DIFF_1:5 .= ((f . ((x + (h / 2)) + h)) - (f . (x + (h / 2)))) - ((cD (f,h)) . x) .= ((fD (f,h)) . (x + (h / 2))) - ((cD (f,h)) . x) by DIFF_1:3 ; hence (fD ((cD (f,h)),h)) . x = ((fD (f,h)) . (x + (h / 2))) - ((cD (f,h)) . x) ; ::_thesis: verum end; theorem :: DIFF_4:52 for h, x being Real for f being Function of REAL,REAL holds (bD ((cD (f,h)),h)) . x = ((cD (f,h)) . x) - ((bD (f,h)) . (x - (h / 2))) proof let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds (bD ((cD (f,h)),h)) . x = ((cD (f,h)) . x) - ((bD (f,h)) . (x - (h / 2))) let f be Function of REAL,REAL; ::_thesis: (bD ((cD (f,h)),h)) . x = ((cD (f,h)) . x) - ((bD (f,h)) . (x - (h / 2))) (bD ((cD (f,h)),h)) . x = ((cD (f,h)) . x) - ((cD (f,h)) . (x - h)) by DIFF_1:4 .= ((cD (f,h)) . x) - ((f . ((x - h) + (h / 2))) - (f . ((x - h) - (h / 2)))) by DIFF_1:5 .= ((cD (f,h)) . x) - ((f . (x - (h / 2))) - (f . ((x - (h / 2)) - h))) .= ((cD (f,h)) . x) - ((bD (f,h)) . (x - (h / 2))) by DIFF_1:4 ; hence (bD ((cD (f,h)),h)) . x = ((cD (f,h)) . x) - ((bD (f,h)) . (x - (h / 2))) ; ::_thesis: verum end; theorem :: DIFF_4:53 for h, x being Real for f being Function of REAL,REAL holds (cD ((cD (f,h)),h)) . x = ((fD (f,h)) . x) - ((bD (f,h)) . x) proof let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds (cD ((cD (f,h)),h)) . x = ((fD (f,h)) . x) - ((bD (f,h)) . x) let f be Function of REAL,REAL; ::_thesis: (cD ((cD (f,h)),h)) . x = ((fD (f,h)) . x) - ((bD (f,h)) . x) (cD ((cD (f,h)),h)) . x = ((cD (f,h)) . (x + (h / 2))) - ((cD (f,h)) . (x - (h / 2))) by DIFF_1:5 .= ((f . ((x + (h / 2)) + (h / 2))) - (f . ((x + (h / 2)) - (h / 2)))) - ((cD (f,h)) . (x - (h / 2))) by DIFF_1:5 .= ((f . ((x + (h / 2)) + (h / 2))) - (f . ((x + (h / 2)) - (h / 2)))) - ((f . ((x - (h / 2)) + (h / 2))) - (f . ((x - (h / 2)) - (h / 2)))) by DIFF_1:5 .= ((f . (x + h)) - (f . x)) - ((f . x) - (f . (x - h))) .= ((fD (f,h)) . x) - ((f . x) - (f . (x - h))) by DIFF_1:3 .= ((fD (f,h)) . x) - ((bD (f,h)) . x) by DIFF_1:4 ; hence (cD ((cD (f,h)),h)) . x = ((fD (f,h)) . x) - ((bD (f,h)) . x) ; ::_thesis: verum end; theorem Th54: :: DIFF_4:54 for h, x being Real for f being Function of REAL,REAL holds ((cdif (f,h)) . 1) . x = (((cdif (f,h)) . 0) . (x + (h / 2))) - (((cdif (f,h)) . 0) . (x - (h / 2))) proof let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds ((cdif (f,h)) . 1) . x = (((cdif (f,h)) . 0) . (x + (h / 2))) - (((cdif (f,h)) . 0) . (x - (h / 2))) let f be Function of REAL,REAL; ::_thesis: ((cdif (f,h)) . 1) . x = (((cdif (f,h)) . 0) . (x + (h / 2))) - (((cdif (f,h)) . 0) . (x - (h / 2))) ((cdif (f,h)) . 1) . x = (cD (f,h)) . x by DIFF_3:16 .= (f . (x + (h / 2))) - (f . (x - (h / 2))) by DIFF_1:5 .= (((cdif (f,h)) . 0) . (x + (h / 2))) - (f . (x - (h / 2))) by DIFF_1:def_8 .= (((cdif (f,h)) . 0) . (x + (h / 2))) - (((cdif (f,h)) . 0) . (x - (h / 2))) by DIFF_1:def_8 ; hence ((cdif (f,h)) . 1) . x = (((cdif (f,h)) . 0) . (x + (h / 2))) - (((cdif (f,h)) . 0) . (x - (h / 2))) ; ::_thesis: verum end; theorem :: DIFF_4:55 for n being Element of NAT for h, x being Real for f being Function of REAL,REAL holds ((cdif (f,h)) . (n + 1)) . x = (((cdif (f,h)) . n) . (x + (h / 2))) - (((cdif (f,h)) . n) . (x - (h / 2))) proof let n be Element of NAT ; ::_thesis: for h, x being Real for f being Function of REAL,REAL holds ((cdif (f,h)) . (n + 1)) . x = (((cdif (f,h)) . n) . (x + (h / 2))) - (((cdif (f,h)) . n) . (x - (h / 2))) let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds ((cdif (f,h)) . (n + 1)) . x = (((cdif (f,h)) . n) . (x + (h / 2))) - (((cdif (f,h)) . n) . (x - (h / 2))) let f be Function of REAL,REAL; ::_thesis: ((cdif (f,h)) . (n + 1)) . x = (((cdif (f,h)) . n) . (x + (h / 2))) - (((cdif (f,h)) . n) . (x - (h / 2))) defpred S1[ Element of NAT ] means ((cdif (f,h)) . (\$1 + 1)) . x = (((cdif (f,h)) . \$1) . (x + (h / 2))) - (((cdif (f,h)) . \$1) . (x - (h / 2))); A1: for i being Element of NAT st S1[i] holds S1[i + 1] proof let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] ) assume ((cdif (f,h)) . (i + 1)) . x = (((cdif (f,h)) . i) . (x + (h / 2))) - (((cdif (f,h)) . i) . (x - (h / 2))) ; ::_thesis: S1[i + 1] A2: (cdif (f,h)) . (i + 1) is Function of REAL,REAL by DIFF_1:19; ((cdif (f,h)) . (i + 2)) . x = ((cdif (f,h)) . ((i + 1) + 1)) . x .= (cD (((cdif (f,h)) . (i + 1)),h)) . x by DIFF_1:def_8 .= (((cdif (f,h)) . (i + 1)) . (x + (h / 2))) - (((cdif (f,h)) . (i + 1)) . (x - (h / 2))) by A2, DIFF_1:5 ; hence S1[i + 1] ; ::_thesis: verum end; A3: S1[ 0 ] by Th54; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1); hence ((cdif (f,h)) . (n + 1)) . x = (((cdif (f,h)) . n) . (x + (h / 2))) - (((cdif (f,h)) . n) . (x - (h / 2))) ; ::_thesis: verum end; theorem :: DIFF_4:56 for x0, x1 being Real st x0 in dom tan & x1 in dom tan holds [!((tan (#) tan) (#) sin),x0,x1!] = ((((sin x0) |^ 3) * ((cos x1) ^2)) - (((sin x1) |^ 3) * ((cos x0) ^2))) / ((((cos x0) ^2) * ((cos x1) ^2)) * (x0 - x1)) proof let x0, x1 be Real; ::_thesis: ( x0 in dom tan & x1 in dom tan implies [!((tan (#) tan) (#) sin),x0,x1!] = ((((sin x0) |^ 3) * ((cos x1) ^2)) - (((sin x1) |^ 3) * ((cos x0) ^2))) / ((((cos x0) ^2) * ((cos x1) ^2)) * (x0 - x1)) ) assume A1: ( x0 in dom tan & x1 in dom tan ) ; ::_thesis: [!((tan (#) tan) (#) sin),x0,x1!] = ((((sin x0) |^ 3) * ((cos x1) ^2)) - (((sin x1) |^ 3) * ((cos x0) ^2))) / ((((cos x0) ^2) * ((cos x1) ^2)) * (x0 - x1)) A2: ( cos x0 <> 0 & cos x1 <> 0 ) by A1, FDIFF_8:1; [!((tan (#) tan) (#) sin),x0,x1!] = ((((tan (#) tan) . x0) * (sin . x0)) - (((tan (#) tan) (#) sin) . x1)) / (x0 - x1) by VALUED_1:5 .= ((((tan . x0) * (tan . x0)) * (sin . x0)) - (((tan (#) tan) (#) sin) . x1)) / (x0 - x1) by VALUED_1:5 .= ((((tan . x0) * (tan . x0)) * (sin . x0)) - (((tan (#) tan) . x1) * (sin . x1))) / (x0 - x1) by VALUED_1:5 .= ((((tan . x0) * (tan . x0)) * (sin . x0)) - (((tan . x1) * (tan . x1)) * (sin . x1))) / (x0 - x1) by VALUED_1:5 .= (((((sin . x0) * ((cos . x0) ")) * (tan . x0)) * (sin . x0)) - (((tan . x1) * (tan . x1)) * (sin . x1))) / (x0 - x1) by A1, RFUNCT_1:def_1 .= (((((sin . x0) * ((cos . x0) ")) * ((sin . x0) * ((cos . x0) "))) * (sin . x0)) - (((tan . x1) * (tan . x1)) * (sin . x1))) / (x0 - x1) by A1, RFUNCT_1:def_1 .= (((((sin . x0) * ((cos . x0) ")) * ((sin . x0) * ((cos . x0) "))) * (sin . x0)) - ((((sin . x1) * ((cos . x1) ")) * (tan . x1)) * (sin . x1))) / (x0 - x1) by A1, RFUNCT_1:def_1 .= (((((sin . x0) * ((cos . x0) ")) * ((sin . x0) * ((cos . x0) "))) * (sin . x0)) - ((((sin . x1) * ((cos . x1) ")) * ((sin . x1) * ((cos . x1) "))) * (sin . x1))) / (x0 - x1) by A1, RFUNCT_1:def_1 .= ((((((sin . x0) * (sin . x0)) * (sin . x0)) * ((cos . x0) ")) * ((cos . x0) ")) - (((((sin . x1) * (sin . x1)) * (sin . x1)) * ((cos . x1) ")) * ((cos . x1) "))) / (x0 - x1) .= (((((((sin . x0) |^ 1) * (sin . x0)) * (sin . x0)) * ((cos . x0) ")) * ((cos . x0) ")) - (((((sin . x1) * (sin . x1)) * (sin . x1)) * ((cos . x1) ")) * ((cos . x1) "))) / (x0 - x1) by NEWTON:5 .= ((((((sin . x0) |^ (1 + 1)) * (sin . x0)) * ((cos . x0) ")) * ((cos . x0) ")) - (((((sin . x1) * (sin . x1)) * (sin . x1)) * ((cos . x1) ")) * ((cos . x1) "))) / (x0 - x1) by NEWTON:6 .= (((((sin . x0) |^ (2 + 1)) * ((cos . x0) ")) * ((cos . x0) ")) - (((((sin . x1) * (sin . x1)) * (sin . x1)) * ((cos . x1) ")) * ((cos . x1) "))) / (x0 - x1) by NEWTON:6 .= (((((sin . x0) |^ 3) * ((cos . x0) ")) * ((cos . x0) ")) - ((((((sin . x1) |^ 1) * (sin . x1)) * (sin . x1)) * ((cos . x1) ")) * ((cos . x1) "))) / (x0 - x1) by NEWTON:5 .= (((((sin . x0) |^ 3) * ((cos . x0) ")) * ((cos . x0) ")) - (((((sin . x1) |^ (1 + 1)) * (sin . x1)) * ((cos . x1) ")) * ((cos . x1) "))) / (x0 - x1) by NEWTON:6 .= (((((sin . x0) |^ 3) * ((cos . x0) ")) * ((cos . x0) ")) - ((((sin . x1) |^ (2 + 1)) * ((cos . x1) ")) * ((cos . x1) "))) / (x0 - x1) by NEWTON:6 .= ((((sin . x0) |^ 3) * (((cos . x0) ") * ((cos . x0) "))) - ((((sin . x1) |^ 3) * ((cos . x1) ")) * ((cos . x1) "))) / (x0 - x1) .= ((((sin . x0) |^ 3) * (((cos . x0) * (cos . x0)) ")) - (((sin . x1) |^ 3) * (((cos . x1) ") * ((cos . x1) ")))) / (x0 - x1) by XCMPLX_1:204 .= ((((sin . x0) |^ 3) / ((cos . x0) ^2)) - (((sin . x1) |^ 3) / ((cos . x1) ^2))) / (x0 - x1) by XCMPLX_1:204 .= (((((sin x0) |^ 3) * ((cos x1) ^2)) - (((sin x1) |^ 3) * ((cos x0) ^2))) / (((cos x0) ^2) * ((cos x1) ^2))) / (x0 - x1) by A2, XCMPLX_1:130 .= ((((sin x0) |^ 3) * ((cos x1) ^2)) - (((sin x1) |^ 3) * ((cos x0) ^2))) / ((((cos x0) ^2) * ((cos x1) ^2)) * (x0 - x1)) by XCMPLX_1:78 ; hence [!((tan (#) tan) (#) sin),x0,x1!] = ((((sin x0) |^ 3) * ((cos x1) ^2)) - (((sin x1) |^ 3) * ((cos x0) ^2))) / ((((cos x0) ^2) * ((cos x1) ^2)) * (x0 - x1)) ; ::_thesis: verum end; theorem :: DIFF_4:57 for x, h being Real st x in dom tan & x + h in dom tan holds (fD (((tan (#) tan) (#) sin),h)) . x = (((sin . (x + h)) |^ 3) * (((cos . (x + h)) ") |^ 2)) - (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) proof let x, h be Real; ::_thesis: ( x in dom tan & x + h in dom tan implies (fD (((tan (#) tan) (#) sin),h)) . x = (((sin . (x + h)) |^ 3) * (((cos . (x + h)) ") |^ 2)) - (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) ) set f = (tan (#) tan) (#) sin; assume A1: ( x in dom tan & x + h in dom tan ) ; ::_thesis: (fD (((tan (#) tan) (#) sin),h)) . x = (((sin . (x + h)) |^ 3) * (((cos . (x + h)) ") |^ 2)) - (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) ( x in dom ((tan (#) tan) (#) sin) & x + h in dom ((tan (#) tan) (#) sin) ) proof set f1 = tan (#) tan; set f2 = sin ; A2: ( x in dom (tan (#) tan) & x + h in dom (tan (#) tan) ) proof ( x in (dom tan) /\ (dom tan) & x + h in (dom tan) /\ (dom tan) ) by A1; hence ( x in dom (tan (#) tan) & x + h in dom (tan (#) tan) ) by VALUED_1:def_4; ::_thesis: verum end; ( x in (dom (tan (#) tan)) /\ (dom sin) & x + h in (dom (tan (#) tan)) /\ (dom sin) ) by A2, SIN_COS:24, XBOOLE_0:def_4; hence ( x in dom ((tan (#) tan) (#) sin) & x + h in dom ((tan (#) tan) (#) sin) ) by VALUED_1:def_4; ::_thesis: verum end; then (fD (((tan (#) tan) (#) sin),h)) . x = (((tan (#) tan) (#) sin) . (x + h)) - (((tan (#) tan) (#) sin) . x) by DIFF_1:1 .= (((tan (#) tan) . (x + h)) * (sin . (x + h))) - (((tan (#) tan) (#) sin) . x) by VALUED_1:5 .= (((tan (#) tan) . (x + h)) * (sin . (x + h))) - (((tan (#) tan) . x) * (sin . x)) by VALUED_1:5 .= (((tan . (x + h)) * (tan . (x + h))) * (sin . (x + h))) - (((tan (#) tan) . x) * (sin . x)) by VALUED_1:5 .= (((tan . (x + h)) * (tan . (x + h))) * (sin . (x + h))) - (((tan . x) * (tan . x)) * (sin . x)) by VALUED_1:5 .= ((((sin . (x + h)) * ((cos . (x + h)) ")) * (tan . (x + h))) * (sin . (x + h))) - (((tan . x) * (tan . x)) * (sin . x)) by A1, RFUNCT_1:def_1 .= ((((sin . (x + h)) * ((cos . (x + h)) ")) * ((sin . (x + h)) * ((cos . (x + h)) "))) * (sin . (x + h))) - (((tan . x) * (tan . x)) * (sin . x)) by A1, RFUNCT_1:def_1 .= ((((sin . (x + h)) * ((cos . (x + h)) ")) * ((sin . (x + h)) * ((cos . (x + h)) "))) * (sin . (x + h))) - ((((sin . x) * ((cos . x) ")) * (tan . x)) * (sin . x)) by A1, RFUNCT_1:def_1 .= ((((sin . (x + h)) * ((cos . (x + h)) ")) * ((sin . (x + h)) * ((cos . (x + h)) "))) * (sin . (x + h))) - ((((sin . x) * ((cos . x) ")) * ((sin . x) * ((cos . x) "))) * (sin . x)) by A1, RFUNCT_1:def_1 .= ((((sin . (x + h)) * (sin . (x + h))) * (sin . (x + h))) * (((cos . (x + h)) ") * ((cos . (x + h)) "))) - ((((sin . x) * (sin . x)) * (sin . x)) * (((cos . x) ") * ((cos . x) "))) .= (((((sin . (x + h)) |^ 1) * (sin . (x + h))) * (sin . (x + h))) * (((cos . (x + h)) ") * ((cos . (x + h)) "))) - ((((sin . x) * (sin . x)) * (sin . x)) * (((cos . x) ") * ((cos . x) "))) by NEWTON:5 .= ((((sin . (x + h)) |^ (1 + 1)) * (sin . (x + h))) * (((cos . (x + h)) ") * ((cos . (x + h)) "))) - ((((sin . x) * (sin . x)) * (sin . x)) * (((cos . x) ") * ((cos . x) "))) by NEWTON:6 .= (((sin . (x + h)) |^ (2 + 1)) * (((cos . (x + h)) ") * ((cos . (x + h)) "))) - ((((sin . x) * (sin . x)) * (sin . x)) * (((cos . x) ") * ((cos . x) "))) by NEWTON:6 .= (((sin . (x + h)) |^ 3) * ((((cos . (x + h)) ") |^ 1) * ((cos . (x + h)) "))) - ((((sin . x) * (sin . x)) * (sin . x)) * (((cos . x) ") * ((cos . x) "))) by NEWTON:5 .= (((sin . (x + h)) |^ 3) * (((cos . (x + h)) ") |^ (1 + 1))) - ((((sin . x) * (sin . x)) * (sin . x)) * (((cos . x) ") * ((cos . x) "))) by NEWTON:6 .= (((sin . (x + h)) |^ 3) * (((cos . (x + h)) ") |^ 2)) - (((((sin . x) |^ 1) * (sin . x)) * (sin . x)) * (((cos . x) ") * ((cos . x) "))) by NEWTON:5 .= (((sin . (x + h)) |^ 3) * (((cos . (x + h)) ") |^ 2)) - ((((sin . x) |^ (1 + 1)) * (sin . x)) * (((cos . x) ") * ((cos . x) "))) by NEWTON:6 .= (((sin . (x + h)) |^ 3) * (((cos . (x + h)) ") |^ 2)) - (((sin . x) |^ (2 + 1)) * (((cos . x) ") * ((cos . x) "))) by NEWTON:6 .= (((sin . (x + h)) |^ 3) * (((cos . (x + h)) ") |^ 2)) - (((sin . x) |^ 3) * ((((cos . x) ") |^ 1) * ((cos . x) "))) by NEWTON:5 .= (((sin . (x + h)) |^ 3) * (((cos . (x + h)) ") |^ 2)) - (((sin . x) |^ 3) * (((cos . x) ") |^ (1 + 1))) by NEWTON:6 .= (((sin . (x + h)) |^ 3) * (((cos . (x + h)) ") |^ 2)) - (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) ; hence (fD (((tan (#) tan) (#) sin),h)) . x = (((sin . (x + h)) |^ 3) * (((cos . (x + h)) ") |^ 2)) - (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) ; ::_thesis: verum end; theorem :: DIFF_4:58 for x, h being Real st x in dom tan & x - h in dom tan holds (bD (((tan (#) tan) (#) sin),h)) . x = (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) - (((sin . (x - h)) |^ 3) * (((cos . (x - h)) ") |^ 2)) proof let x, h be Real; ::_thesis: ( x in dom tan & x - h in dom tan implies (bD (((tan (#) tan) (#) sin),h)) . x = (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) - (((sin . (x - h)) |^ 3) * (((cos . (x - h)) ") |^ 2)) ) set f = (tan (#) tan) (#) sin; assume A1: ( x in dom tan & x - h in dom tan ) ; ::_thesis: (bD (((tan (#) tan) (#) sin),h)) . x = (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) - (((sin . (x - h)) |^ 3) * (((cos . (x - h)) ") |^ 2)) ( x in dom ((tan (#) tan) (#) sin) & x - h in dom ((tan (#) tan) (#) sin) ) proof set f1 = tan (#) tan; set f2 = sin ; A2: ( x in dom (tan (#) tan) & x - h in dom (tan (#) tan) ) proof ( x in (dom tan) /\ (dom tan) & x - h in (dom tan) /\ (dom tan) ) by A1; hence ( x in dom (tan (#) tan) & x - h in dom (tan (#) tan) ) by VALUED_1:def_4; ::_thesis: verum end; ( x in (dom (tan (#) tan)) /\ (dom sin) & x - h in (dom (tan (#) tan)) /\ (dom sin) ) by A2, SIN_COS:24, XBOOLE_0:def_4; hence ( x in dom ((tan (#) tan) (#) sin) & x - h in dom ((tan (#) tan) (#) sin) ) by VALUED_1:def_4; ::_thesis: verum end; then (bD (((tan (#) tan) (#) sin),h)) . x = (((tan (#) tan) (#) sin) . x) - (((tan (#) tan) (#) sin) . (x - h)) by DIFF_1:38 .= (((tan (#) tan) . x) * (sin . x)) - (((tan (#) tan) (#) sin) . (x - h)) by VALUED_1:5 .= (((tan (#) tan) . x) * (sin . x)) - (((tan (#) tan) . (x - h)) * (sin . (x - h))) by VALUED_1:5 .= (((tan . x) * (tan . x)) * (sin . x)) - (((tan (#) tan) . (x - h)) * (sin . (x - h))) by VALUED_1:5 .= (((tan . x) * (tan . x)) * (sin . x)) - (((tan . (x - h)) * (tan . (x - h))) * (sin . (x - h))) by VALUED_1:5 .= ((((sin . x) * ((cos . x) ")) * (tan . x)) * (sin . x)) - (((tan . (x - h)) * (tan . (x - h))) * (sin . (x - h))) by A1, RFUNCT_1:def_1 .= ((((sin . x) * ((cos . x) ")) * ((sin . x) * ((cos . x) "))) * (sin . x)) - (((tan . (x - h)) * (tan . (x - h))) * (sin . (x - h))) by A1, RFUNCT_1:def_1 .= ((((sin . x) * ((cos . x) ")) * ((sin . x) * ((cos . x) "))) * (sin . x)) - ((((sin . (x - h)) * ((cos . (x - h)) ")) * (tan . (x - h))) * (sin . (x - h))) by A1, RFUNCT_1:def_1 .= ((((sin . x) * ((cos . x) ")) * ((sin . x) * ((cos . x) "))) * (sin . x)) - ((((sin . (x - h)) * ((cos . (x - h)) ")) * ((sin . (x - h)) * ((cos . (x - h)) "))) * (sin . (x - h))) by A1, RFUNCT_1:def_1 .= ((((sin . x) * (sin . x)) * (sin . x)) * (((cos . x) ") * ((cos . x) "))) - ((((sin . (x - h)) * (sin . (x - h))) * (sin . (x - h))) * (((cos . (x - h)) ") * ((cos . (x - h)) "))) .= (((((sin . x) |^ 1) * (sin . x)) * (sin . x)) * (((cos . x) ") * ((cos . x) "))) - ((((sin . (x - h)) * (sin . (x - h))) * (sin . (x - h))) * (((cos . (x - h)) ") * ((cos . (x - h)) "))) by NEWTON:5 .= ((((sin . x) |^ (1 + 1)) * (sin . x)) * (((cos . x) ") * ((cos . x) "))) - ((((sin . (x - h)) * (sin . (x - h))) * (sin . (x - h))) * (((cos . (x - h)) ") * ((cos . (x - h)) "))) by NEWTON:6 .= (((sin . x) |^ (2 + 1)) * (((cos . x) ") * ((cos . x) "))) - ((((sin . (x - h)) * (sin . (x - h))) * (sin . (x - h))) * (((cos . (x - h)) ") * ((cos . (x - h)) "))) by NEWTON:6 .= (((sin . x) |^ 3) * ((((cos . x) ") |^ 1) * ((cos . x) "))) - ((((sin . (x - h)) * (sin . (x - h))) * (sin . (x - h))) * (((cos . (x - h)) ") * ((cos . (x - h)) "))) by NEWTON:5 .= (((sin . x) |^ 3) * (((cos . x) ") |^ (1 + 1))) - ((((sin . (x - h)) * (sin . (x - h))) * (sin . (x - h))) * (((cos . (x - h)) ") * ((cos . (x - h)) "))) by NEWTON:6 .= (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) - (((((sin . (x - h)) |^ 1) * (sin . (x - h))) * (sin . (x - h))) * (((cos . (x - h)) ") * ((cos . (x - h)) "))) by NEWTON:5 .= (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) - ((((sin . (x - h)) |^ (1 + 1)) * (sin . (x - h))) * (((cos . (x - h)) ") * ((cos . (x - h)) "))) by NEWTON:6 .= (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) - (((sin . (x - h)) |^ (2 + 1)) * (((cos . (x - h)) ") * ((cos . (x - h)) "))) by NEWTON:6 .= (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) - (((sin . (x - h)) |^ 3) * ((((cos . (x - h)) ") |^ 1) * ((cos . (x - h)) "))) by NEWTON:5 .= (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) - (((sin . (x - h)) |^ 3) * (((cos . (x - h)) ") |^ (1 + 1))) by NEWTON:6 .= (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) - (((sin . (x - h)) |^ 3) * (((cos . (x - h)) ") |^ 2)) ; hence (bD (((tan (#) tan) (#) sin),h)) . x = (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) - (((sin . (x - h)) |^ 3) * (((cos . (x - h)) ") |^ 2)) ; ::_thesis: verum end; theorem :: DIFF_4:59 for x, h being Real st x + (h / 2) in dom tan & x - (h / 2) in dom tan holds (cD (((tan (#) tan) (#) sin),h)) . x = (((sin . (x + (h / 2))) |^ 3) * (((cos . (x + (h / 2))) ") |^ 2)) - (((sin . (x - (h / 2))) |^ 3) * (((cos . (x - (h / 2))) ") |^ 2)) proof let x, h be Real; ::_thesis: ( x + (h / 2) in dom tan & x - (h / 2) in dom tan implies (cD (((tan (#) tan) (#) sin),h)) . x = (((sin . (x + (h / 2))) |^ 3) * (((cos . (x + (h / 2))) ") |^ 2)) - (((sin . (x - (h / 2))) |^ 3) * (((cos . (x - (h / 2))) ") |^ 2)) ) set f = (tan (#) tan) (#) sin; assume A1: ( x + (h / 2) in dom tan & x - (h / 2) in dom tan ) ; ::_thesis: (cD (((tan (#) tan) (#) sin),h)) . x = (((sin . (x + (h / 2))) |^ 3) * (((cos . (x + (h / 2))) ") |^ 2)) - (((sin . (x - (h / 2))) |^ 3) * (((cos . (x - (h / 2))) ") |^ 2)) ( x + (h / 2) in dom ((tan (#) tan) (#) sin) & x - (h / 2) in dom ((tan (#) tan) (#) sin) ) proof set f1 = tan (#) tan; set f2 = sin ; A2: ( x + (h / 2) in dom (tan (#) tan) & x - (h / 2) in dom (tan (#) tan) ) proof ( x + (h / 2) in (dom tan) /\ (dom tan) & x - (h / 2) in (dom tan) /\ (dom tan) ) by A1; hence ( x + (h / 2) in dom (tan (#) tan) & x - (h / 2) in dom (tan (#) tan) ) by VALUED_1:def_4; ::_thesis: verum end; ( x + (h / 2) in (dom (tan (#) tan)) /\ (dom sin) & x - (h / 2) in (dom (tan (#) tan)) /\ (dom sin) ) by A2, SIN_COS:24, XBOOLE_0:def_4; hence ( x + (h / 2) in dom ((tan (#) tan) (#) sin) & x - (h / 2) in dom ((tan (#) tan) (#) sin) ) by VALUED_1:def_4; ::_thesis: verum end; then (cD (((tan (#) tan) (#) sin),h)) . x = (((tan (#) tan) (#) sin) . (x + (h / 2))) - (((tan (#) tan) (#) sin) . (x - (h / 2))) by DIFF_1:39 .= (((tan (#) tan) . (x + (h / 2))) * (sin . (x + (h / 2)))) - (((tan (#) tan) (#) sin) . (x - (h / 2))) by VALUED_1:5 .= (((tan (#) tan) . (x + (h / 2))) * (sin . (x + (h / 2)))) - (((tan (#) tan) . (x - (h / 2))) * (sin . (x - (h / 2)))) by VALUED_1:5 .= (((tan . (x + (h / 2))) * (tan . (x + (h / 2)))) * (sin . (x + (h / 2)))) - (((tan (#) tan) . (x - (h / 2))) * (sin . (x - (h / 2)))) by VALUED_1:5 .= (((tan . (x + (h / 2))) * (tan . (x + (h / 2)))) * (sin . (x + (h / 2)))) - (((tan . (x - (h / 2))) * (tan . (x - (h / 2)))) * (sin . (x - (h / 2)))) by VALUED_1:5 .= ((((sin . (x + (h / 2))) * ((cos . (x + (h / 2))) ")) * (tan . (x + (h / 2)))) * (sin . (x + (h / 2)))) - (((tan . (x - (h / 2))) * (tan . (x - (h / 2)))) * (sin . (x - (h / 2)))) by A1, RFUNCT_1:def_1 .= ((((sin . (x + (h / 2))) * ((cos . (x + (h / 2))) ")) * ((sin . (x + (h / 2))) * ((cos . (x + (h / 2))) "))) * (sin . (x + (h / 2)))) - (((tan . (x - (h / 2))) * (tan . (x - (h / 2)))) * (sin . (x - (h / 2)))) by A1, RFUNCT_1:def_1 .= ((((sin . (x + (h / 2))) * ((cos . (x + (h / 2))) ")) * ((sin . (x + (h / 2))) * ((cos . (x + (h / 2))) "))) * (sin . (x + (h / 2)))) - ((((sin . (x - (h / 2))) * ((cos . (x - (h / 2))) ")) * (tan . (x - (h / 2)))) * (sin . (x - (h / 2)))) by A1, RFUNCT_1:def_1 .= ((((sin . (x + (h / 2))) * ((cos . (x + (h / 2))) ")) * ((sin . (x + (h / 2))) * ((cos . (x + (h / 2))) "))) * (sin . (x + (h / 2)))) - ((((sin . (x - (h / 2))) * ((cos . (x - (h / 2))) ")) * ((sin . (x - (h / 2))) * ((cos . (x - (h / 2))) "))) * (sin . (x - (h / 2)))) by A1, RFUNCT_1:def_1 .= ((((sin . (x + (h / 2))) * (sin . (x + (h / 2)))) * (sin . (x + (h / 2)))) * (((cos . (x + (h / 2))) ") * ((cos . (x + (h / 2))) "))) - ((((sin . (x - (h / 2))) * (sin . (x - (h / 2)))) * (sin . (x - (h / 2)))) * (((cos . (x - (h / 2))) ") * ((cos . (x - (h / 2))) "))) .= (((((sin . (x + (h / 2))) |^ 1) * (sin . (x + (h / 2)))) * (sin . (x + (h / 2)))) * (((cos . (x + (h / 2))) ") * ((cos . (x + (h / 2))) "))) - ((((sin . (x - (h / 2))) * (sin . (x - (h / 2)))) * (sin . (x - (h / 2)))) * (((cos . (x - (h / 2))) ") * ((cos . (x - (h / 2))) "))) by NEWTON:5 .= ((((sin . (x + (h / 2))) |^ (1 + 1)) * (sin . (x + (h / 2)))) * (((cos . (x + (h / 2))) ") * ((cos . (x + (h / 2))) "))) - ((((sin . (x - (h / 2))) * (sin . (x - (h / 2)))) * (sin . (x - (h / 2)))) * (((cos . (x - (h / 2))) ") * ((cos . (x - (h / 2))) "))) by NEWTON:6 .= (((sin . (x + (h / 2))) |^ (2 + 1)) * (((cos . (x + (h / 2))) ") * ((cos . (x + (h / 2))) "))) - ((((sin . (x - (h / 2))) * (sin . (x - (h / 2)))) * (sin . (x - (h / 2)))) * (((cos . (x - (h / 2))) ") * ((cos . (x - (h / 2))) "))) by NEWTON:6 .= (((sin . (x + (h / 2))) |^ 3) * ((((cos . (x + (h / 2))) ") |^ 1) * ((cos . (x + (h / 2))) "))) - ((((sin . (x - (h / 2))) * (sin . (x - (h / 2)))) * (sin . (x - (h / 2)))) * (((cos . (x - (h / 2))) ") * ((cos . (x - (h / 2))) "))) by NEWTON:5 .= (((sin . (x + (h / 2))) |^ 3) * (((cos . (x + (h / 2))) ") |^ (1 + 1))) - ((((sin . (x - (h / 2))) * (sin . (x - (h / 2)))) * (sin . (x - (h / 2)))) * (((cos . (x - (h / 2))) ") * ((cos . (x - (h / 2))) "))) by NEWTON:6 .= (((sin . (x + (h / 2))) |^ 3) * (((cos . (x + (h / 2))) ") |^ 2)) - (((((sin . (x - (h / 2))) |^ 1) * (sin . (x - (h / 2)))) * (sin . (x - (h / 2)))) * (((cos . (x - (h / 2))) ") * ((cos . (x - (h / 2))) "))) by NEWTON:5 .= (((sin . (x + (h / 2))) |^ 3) * (((cos . (x + (h / 2))) ") |^ 2)) - ((((sin . (x - (h / 2))) |^ (1 + 1)) * (sin . (x - (h / 2)))) * (((cos . (x - (h / 2))) ") * ((cos . (x - (h / 2))) "))) by NEWTON:6 .= (((sin . (x + (h / 2))) |^ 3) * (((cos . (x + (h / 2))) ") |^ 2)) - (((sin . (x - (h / 2))) |^ (2 + 1)) * (((cos . (x - (h / 2))) ") * ((cos . (x - (h / 2))) "))) by NEWTON:6 .= (((sin . (x + (h / 2))) |^ 3) * (((cos . (x + (h / 2))) ") |^ 2)) - (((sin . (x - (h / 2))) |^ 3) * ((((cos . (x - (h / 2))) ") |^ 1) * ((cos . (x - (h / 2))) "))) by NEWTON:5 .= (((sin . (x + (h / 2))) |^ 3) * (((cos . (x + (h / 2))) ") |^ 2)) - (((sin . (x - (h / 2))) |^ 3) * (((cos . (x - (h / 2))) ") |^ (1 + 1))) by NEWTON:6 .= (((sin . (x + (h / 2))) |^ 3) * (((cos . (x + (h / 2))) ") |^ 2)) - (((sin . (x - (h / 2))) |^ 3) * (((cos . (x - (h / 2))) ") |^ 2)) ; hence (cD (((tan (#) tan) (#) sin),h)) . x = (((sin . (x + (h / 2))) |^ 3) * (((cos . (x + (h / 2))) ") |^ 2)) - (((sin . (x - (h / 2))) |^ 3) * (((cos . (x - (h / 2))) ") |^ 2)) ; ::_thesis: verum end; theorem :: DIFF_4:60 for x0, x1 being Real st x0 in dom cot & x1 in dom cot holds [!((cot (#) cot) (#) cos),x0,x1!] = ((((cos x0) |^ 3) * ((sin x1) ^2)) - (((cos x1) |^ 3) * ((sin x0) ^2))) / ((((sin x0) ^2) * ((sin x1) ^2)) * (x0 - x1)) proof let x0, x1 be Real; ::_thesis: ( x0 in dom cot & x1 in dom cot implies [!((cot (#) cot) (#) cos),x0,x1!] = ((((cos x0) |^ 3) * ((sin x1) ^2)) - (((cos x1) |^ 3) * ((sin x0) ^2))) / ((((sin x0) ^2) * ((sin x1) ^2)) * (x0 - x1)) ) assume A1: ( x0 in dom cot & x1 in dom cot ) ; ::_thesis: [!((cot (#) cot) (#) cos),x0,x1!] = ((((cos x0) |^ 3) * ((sin x1) ^2)) - (((cos x1) |^ 3) * ((sin x0) ^2))) / ((((sin x0) ^2) * ((sin x1) ^2)) * (x0 - x1)) A2: ( sin x0 <> 0 & sin x1 <> 0 ) by A1, FDIFF_8:2; [!((cot (#) cot) (#) cos),x0,x1!] = ((((cot (#) cot) . x0) * (cos . x0)) - (((cot (#) cot) (#) cos) . x1)) / (x0 - x1) by VALUED_1:5 .= ((((cot . x0) * (cot . x0)) * (cos . x0)) - (((cot (#) cot) (#) cos) . x1)) / (x0 - x1) by VALUED_1:5 .= ((((cot . x0) * (cot . x0)) * (cos . x0)) - (((cot (#) cot) . x1) * (cos . x1))) / (x0 - x1) by VALUED_1:5 .= ((((cot . x0) * (cot . x0)) * (cos . x0)) - (((cot . x1) * (cot . x1)) * (cos . x1))) / (x0 - x1) by VALUED_1:5 .= (((((cos . x0) * ((sin . x0) ")) * (cot . x0)) * (cos . x0)) - (((cot . x1) * (cot . x1)) * (cos . x1))) / (x0 - x1) by A1, RFUNCT_1:def_1 .= (((((cos . x0) * ((sin . x0) ")) * ((cos . x0) * ((sin . x0) "))) * (cos . x0)) - (((cot . x1) * (cot . x1)) * (cos . x1))) / (x0 - x1) by A1, RFUNCT_1:def_1 .= (((((cos . x0) * ((sin . x0) ")) * ((cos . x0) * ((sin . x0) "))) * (cos . x0)) - ((((cos . x1) * ((sin . x1) ")) * (cot . x1)) * (cos . x1))) / (x0 - x1) by A1, RFUNCT_1:def_1 .= (((((cos . x0) * ((sin . x0) ")) * ((cos . x0) * ((sin . x0) "))) * (cos . x0)) - ((((cos . x1) * ((sin . x1) ")) * ((cos . x1) * ((sin . x1) "))) * (cos . x1))) / (x0 - x1) by A1, RFUNCT_1:def_1 .= ((((((cos . x0) * (cos . x0)) * (cos . x0)) * ((sin . x0) ")) * ((sin . x0) ")) - (((((cos . x1) * (cos . x1)) * (cos . x1)) * ((sin . x1) ")) * ((sin . x1) "))) / (x0 - x1) .= (((((((cos . x0) |^ 1) * (cos . x0)) * (cos . x0)) * ((sin . x0) ")) * ((sin . x0) ")) - (((((cos . x1) * (cos . x1)) * (cos . x1)) * ((sin . x1) ")) * ((sin . x1) "))) / (x0 - x1) by NEWTON:5 .= ((((((cos . x0) |^ (1 + 1)) * (cos . x0)) * ((sin . x0) ")) * ((sin . x0) ")) - (((((cos . x1) * (cos . x1)) * (cos . x1)) * ((sin . x1) ")) * ((sin . x1) "))) / (x0 - x1) by NEWTON:6 .= (((((cos . x0) |^ (2 + 1)) * ((sin . x0) ")) * ((sin . x0) ")) - (((((cos . x1) * (cos . x1)) * (cos . x1)) * ((sin . x1) ")) * ((sin . x1) "))) / (x0 - x1) by NEWTON:6 .= (((((cos . x0) |^ 3) * ((sin . x0) ")) * ((sin . x0) ")) - ((((((cos . x1) |^ 1) * (cos . x1)) * (cos . x1)) * ((sin . x1) ")) * ((sin . x1) "))) / (x0 - x1) by NEWTON:5 .= (((((cos . x0) |^ 3) * ((sin . x0) ")) * ((sin . x0) ")) - (((((cos . x1) |^ (1 + 1)) * (cos . x1)) * ((sin . x1) ")) * ((sin . x1) "))) / (x0 - x1) by NEWTON:6 .= (((((cos . x0) |^ 3) * ((sin . x0) ")) * ((sin . x0) ")) - ((((cos . x1) |^ (2 + 1)) * ((sin . x1) ")) * ((sin . x1) "))) / (x0 - x1) by NEWTON:6 .= ((((cos . x0) |^ 3) * (((sin . x0) ") * ((sin . x0) "))) - ((((cos . x1) |^ 3) * ((sin . x1) ")) * ((sin . x1) "))) / (x0 - x1) .= ((((cos . x0) |^ 3) * (((sin . x0) * (sin . x0)) ")) - (((cos . x1) |^ 3) * (((sin . x1) ") * ((sin . x1) ")))) / (x0 - x1) by XCMPLX_1:204 .= ((((cos . x0) |^ 3) / ((sin . x0) ^2)) - (((cos . x1) |^ 3) / ((sin . x1) ^2))) / (x0 - x1) by XCMPLX_1:204 .= (((((cos x0) |^ 3) * ((sin x1) ^2)) - (((cos x1) |^ 3) * ((sin x0) ^2))) / (((sin x0) ^2) * ((sin x1) ^2))) / (x0 - x1) by A2, XCMPLX_1:130 .= ((((cos x0) |^ 3) * ((sin x1) ^2)) - (((cos x1) |^ 3) * ((sin x0) ^2))) / ((((sin x0) ^2) * ((sin x1) ^2)) * (x0 - x1)) by XCMPLX_1:78 ; hence [!((cot (#) cot) (#) cos),x0,x1!] = ((((cos x0) |^ 3) * ((sin x1) ^2)) - (((cos x1) |^ 3) * ((sin x0) ^2))) / ((((sin x0) ^2) * ((sin x1) ^2)) * (x0 - x1)) ; ::_thesis: verum end; theorem :: DIFF_4:61 for x, h being Real st x in dom cot & x + h in dom cot holds (fD (((cot (#) cot) (#) cos),h)) . x = (((cos . (x + h)) |^ 3) * (((sin . (x + h)) ") |^ 2)) - (((cos . x) |^ 3) * (((sin . x) ") |^ 2)) proof let x, h be Real; ::_thesis: ( x in dom cot & x + h in dom cot implies (fD (((cot (#) cot) (#) cos),h)) . x = (((cos . (x + h)) |^ 3) * (((sin . (x + h)) ") |^ 2)) - (((cos . x) |^ 3) * (((sin . x) ") |^ 2)) ) set f = (cot (#) cot) (#) cos; assume A1: ( x in dom cot & x + h in dom cot ) ; ::_thesis: (fD (((cot (#) cot) (#) cos),h)) . x = (((cos . (x + h)) |^ 3) * (((sin . (x + h)) ") |^ 2)) - (((cos . x) |^ 3) * (((sin . x) ") |^ 2)) ( x in dom ((cot (#) cot) (#) cos) & x + h in dom ((cot (#) cot) (#) cos) ) proof set f1 = cot (#) cot; set f2 = cos ; A2: ( x in dom (cot (#) cot) & x + h in dom (cot (#) cot) ) proof ( x in (dom cot) /\ (dom cot) & x + h in (dom cot) /\ (dom cot) ) by A1; hence ( x in dom (cot (#) cot) & x + h in dom (cot (#) cot) ) by VALUED_1:def_4; ::_thesis: verum end; ( x in (dom (cot (#) cot)) /\ (dom cos) & x + h in (dom (cot (#) cot)) /\ (dom cos) ) by A2, SIN_COS:24, XBOOLE_0:def_4; hence ( x in dom ((cot (#) cot) (#) cos) & x + h in dom ((cot (#) cot) (#) cos) ) by VALUED_1:def_4; ::_thesis: verum end; then (fD (((cot (#) cot) (#) cos),h)) . x = (((cot (#) cot) (#) cos) . (x + h)) - (((cot (#) cot) (#) cos) . x) by DIFF_1:1 .= (((cot (#) cot) . (x + h)) * (cos . (x + h))) - (((cot (#) cot) (#) cos) . x) by VALUED_1:5 .= (((cot (#) cot) . (x + h)) * (cos . (x + h))) - (((cot (#) cot) . x) * (cos . x)) by VALUED_1:5 .= (((cot . (x + h)) * (cot . (x + h))) * (cos . (x + h))) - (((cot (#) cot) . x) * (cos . x)) by VALUED_1:5 .= (((cot . (x + h)) * (cot . (x + h))) * (cos . (x + h))) - (((cot . x) * (cot . x)) * (cos . x)) by VALUED_1:5 .= ((((cos . (x + h)) * ((sin . (x + h)) ")) * (cot . (x + h))) * (cos . (x + h))) - (((cot . x) * (cot . x)) * (cos . x)) by A1, RFUNCT_1:def_1 .= ((((cos . (x + h)) * ((sin . (x + h)) ")) * ((cos . (x + h)) * ((sin . (x + h)) "))) * (cos . (x + h))) - (((cot . x) * (cot . x)) * (cos . x)) by A1, RFUNCT_1:def_1 .= ((((cos . (x + h)) * ((sin . (x + h)) ")) * ((cos . (x + h)) * ((sin . (x + h)) "))) * (cos . (x + h))) - ((((cos . x) * ((sin . x) ")) * (cot . x)) * (cos . x)) by A1, RFUNCT_1:def_1 .= ((((cos . (x + h)) * ((sin . (x + h)) ")) * ((cos . (x + h)) * ((sin . (x + h)) "))) * (cos . (x + h))) - ((((cos . x) * ((sin . x) ")) * ((cos . x) * ((sin . x) "))) * (cos . x)) by A1, RFUNCT_1:def_1 .= ((((cos . (x + h)) * (cos . (x + h))) * (cos . (x + h))) * (((sin . (x + h)) ") * ((sin . (x + h)) "))) - ((((cos . x) * (cos . x)) * (cos . x)) * (((sin . x) ") * ((sin . x) "))) .= (((((cos . (x + h)) |^ 1) * (cos . (x + h))) * (cos . (x + h))) * (((sin . (x + h)) ") * ((sin . (x + h)) "))) - ((((cos . x) * (cos . x)) * (cos . x)) * (((sin . x) ") * ((sin . x) "))) by NEWTON:5 .= ((((cos . (x + h)) |^ (1 + 1)) * (cos . (x + h))) * (((sin . (x + h)) ") * ((sin . (x + h)) "))) - ((((cos . x) * (cos . x)) * (cos . x)) * (((sin . x) ") * ((sin . x) "))) by NEWTON:6 .= (((cos . (x + h)) |^ (2 + 1)) * (((sin . (x + h)) ") * ((sin . (x + h)) "))) - ((((cos . x) * (cos . x)) * (cos . x)) * (((sin . x) ") * ((sin . x) "))) by NEWTON:6 .= (((cos . (x + h)) |^ 3) * ((((sin . (x + h)) ") |^ 1) * ((sin . (x + h)) "))) - ((((cos . x) * (cos . x)) * (cos . x)) * (((sin . x) ") * ((sin . x) "))) by NEWTON:5 .= (((cos . (x + h)) |^ 3) * (((sin . (x + h)) ") |^ (1 + 1))) - ((((cos . x) * (cos . x)) * (cos . x)) * (((sin . x) ") * ((sin . x) "))) by NEWTON:6 .= (((cos . (x + h)) |^ 3) * (((sin . (x + h)) ") |^ 2)) - (((((cos . x) |^ 1) * (cos . x)) * (cos . x)) * (((sin . x) ") * ((sin . x) "))) by NEWTON:5 .= (((cos . (x + h)) |^ 3) * (((sin . (x + h)) ") |^ 2)) - ((((cos . x) |^ (1 + 1)) * (cos . x)) * (((sin . x) ") * ((sin . x) "))) by NEWTON:6 .= (((cos . (x + h)) |^ 3) * (((sin . (x + h)) ") |^ 2)) - (((cos . x) |^ (2 + 1)) * (((sin . x) ") * ((sin . x) "))) by NEWTON:6 .= (((cos . (x + h)) |^ 3) * (((sin . (x + h)) ") |^ 2)) - (((cos . x) |^ 3) * ((((sin . x) ") |^ 1) * ((sin . x) "))) by NEWTON:5 .= (((cos . (x + h)) |^ 3) * (((sin . (x + h)) ") |^ 2)) - (((cos . x) |^ 3) * (((sin . x) ") |^ (1 + 1))) by NEWTON:6 .= (((cos . (x + h)) |^ 3) * (((sin . (x + h)) ") |^ 2)) - (((cos . x) |^ 3) * (((sin . x) ") |^ 2)) ; hence (fD (((cot (#) cot) (#) cos),h)) . x = (((cos . (x + h)) |^ 3) * (((sin . (x + h)) ") |^ 2)) - (((cos . x) |^ 3) * (((sin . x) ") |^ 2)) ; ::_thesis: verum end; theorem :: DIFF_4:62 for x, h being Real st x in dom cot & x - h in dom cot holds (bD (((cot (#) cot) (#) cos),h)) . x = (((cos . x) |^ 3) * (((sin . x) ") |^ 2)) - (((cos . (x - h)) |^ 3) * (((sin . (x - h)) ") |^ 2)) proof let x, h be Real; ::_thesis: ( x in dom cot & x - h in dom cot implies (bD (((cot (#) cot) (#) cos),h)) . x = (((cos . x) |^ 3) * (((sin . x) ") |^ 2)) - (((cos . (x - h)) |^ 3) * (((sin . (x - h)) ") |^ 2)) ) set f = (cot (#) cot) (#) cos; assume A1: ( x in dom cot & x - h in dom cot ) ; ::_thesis: (bD (((cot (#) cot) (#) cos),h)) . x = (((cos . x) |^ 3) * (((sin . x) ") |^ 2)) - (((cos . (x - h)) |^ 3) * (((sin . (x - h)) ") |^ 2)) ( x in dom ((cot (#) cot) (#) cos) & x - h in dom ((cot (#) cot) (#) cos) ) proof set f1 = cot (#) cot; set f2 = cos ; A2: ( x in dom (cot (#) cot) & x - h in dom (cot (#) cot) ) proof ( x in (dom cot) /\ (dom cot) & x - h in (dom cot) /\ (dom cot) ) by A1; hence ( x in dom (cot (#) cot) & x - h in dom (cot (#) cot) ) by VALUED_1:def_4; ::_thesis: verum end; ( x in (dom (cot (#) cot)) /\ (dom cos) & x - h in (dom (cot (#) cot)) /\ (dom cos) ) by A2, SIN_COS:24, XBOOLE_0:def_4; hence ( x in dom ((cot (#) cot) (#) cos) & x - h in dom ((cot (#) cot) (#) cos) ) by VALUED_1:def_4; ::_thesis: verum end; then (bD (((cot (#) cot) (#) cos),h)) . x = (((cot (#) cot) (#) cos) . x) - (((cot (#) cot) (#) cos) . (x - h)) by DIFF_1:38 .= (((cot (#) cot) . x) * (cos . x)) - (((cot (#) cot) (#) cos) . (x - h)) by VALUED_1:5 .= (((cot (#) cot) . x) * (cos . x)) - (((cot (#) cot) . (x - h)) * (cos . (x - h))) by VALUED_1:5 .= (((cot . x) * (cot . x)) * (cos . x)) - (((cot (#) cot) . (x - h)) * (cos . (x - h))) by VALUED_1:5 .= (((cot . x) * (cot . x)) * (cos . x)) - (((cot . (x - h)) * (cot . (x - h))) * (cos . (x - h))) by VALUED_1:5 .= ((((cos . x) * ((sin . x) ")) * (cot . x)) * (cos . x)) - (((cot . (x - h)) * (cot . (x - h))) * (cos . (x - h))) by A1, RFUNCT_1:def_1 .= ((((cos . x) * ((sin . x) ")) * ((cos . x) * ((sin . x) "))) * (cos . x)) - (((cot . (x - h)) * (cot . (x - h))) * (cos . (x - h))) by A1, RFUNCT_1:def_1 .= ((((cos . x) * ((sin . x) ")) * ((cos . x) * ((sin . x) "))) * (cos . x)) - ((((cos . (x - h)) * ((sin . (x - h)) ")) * (cot . (x - h))) * (cos . (x - h))) by A1, RFUNCT_1:def_1 .= ((((cos . x) * ((sin . x) ")) * ((cos . x) * ((sin . x) "))) * (cos . x)) - ((((cos . (x - h)) * ((sin . (x - h)) ")) * ((cos . (x - h)) * ((sin . (x - h)) "))) * (cos . (x - h))) by A1, RFUNCT_1:def_1 .= ((((cos . x) * (cos . x)) * (cos . x)) * (((sin . x) ") * ((sin . x) "))) - ((((cos . (x - h)) * (cos . (x - h))) * (cos . (x - h))) * (((sin . (x - h)) ") * ((sin . (x - h)) "))) .= (((((cos . x) |^ 1) * (cos . x)) * (cos . x)) * (((sin . x) ") * ((sin . x) "))) - ((((cos . (x - h)) * (cos . (x - h))) * (cos . (x - h))) * (((sin . (x - h)) ") * ((sin . (x - h)) "))) by NEWTON:5 .= ((((cos . x) |^ (1 + 1)) * (cos . x)) * (((sin . x) ") * ((sin . x) "))) - ((((cos . (x - h)) * (cos . (x - h))) * (cos . (x - h))) * (((sin . (x - h)) ") * ((sin . (x - h)) "))) by NEWTON:6 .= (((cos . x) |^ (2 + 1)) * (((sin . x) ") * ((sin . x) "))) - ((((cos . (x - h)) * (cos . (x - h))) * (cos . (x - h))) * (((sin . (x - h)) ") * ((sin . (x - h)) "))) by NEWTON:6 .= (((cos . x) |^ 3) * ((((sin . x) ") |^ 1) * ((sin . x) "))) - ((((cos . (x - h)) * (cos . (x - h))) * (cos . (x - h))) * (((sin . (x - h)) ") * ((sin . (x - h)) "))) by NEWTON:5 .= (((cos . x) |^ 3) * (((sin . x) ") |^ (1 + 1))) - ((((cos . (x - h)) * (cos . (x - h))) * (cos . (x - h))) * (((sin . (x - h)) ") * ((sin . (x - h)) "))) by NEWTON:6 .= (((cos . x) |^ 3) * (((sin . x) ") |^ 2)) - (((((cos . (x - h)) |^ 1) * (cos . (x - h))) * (cos . (x - h))) * (((sin . (x - h)) ") * ((sin . (x - h)) "))) by NEWTON:5 .= (((cos . x) |^ 3) * (((sin . x) ") |^ 2)) - ((((cos . (x - h)) |^ (1 + 1)) * (cos . (x - h))) * (((sin . (x - h)) ") * ((sin . (x - h)) "))) by NEWTON:6 .= (((cos . x) |^ 3) * (((sin . x) ") |^ 2)) - (((cos . (x - h)) |^ (2 + 1)) * (((sin . (x - h)) ") * ((sin . (x - h)) "))) by NEWTON:6 .= (((cos . x) |^ 3) * (((sin . x) ") |^ 2)) - (((cos . (x - h)) |^ 3) * ((((sin . (x - h)) ") |^ 1) * ((sin . (x - h)) "))) by NEWTON:5 .= (((cos . x) |^ 3) * (((sin . x) ") |^ 2)) - (((cos . (x - h)) |^ 3) * (((sin . (x - h)) ") |^ (1 + 1))) by NEWTON:6 .= (((cos . x) |^ 3) * (((sin . x) ") |^ 2)) - (((cos . (x - h)) |^ 3) * (((sin . (x - h)) ") |^ 2)) ; hence (bD (((cot (#) cot) (#) cos),h)) . x = (((cos . x) |^ 3) * (((sin . x) ") |^ 2)) - (((cos . (x - h)) |^ 3) * (((sin . (x - h)) ") |^ 2)) ; ::_thesis: verum end; theorem :: DIFF_4:63 for x, h being Real st x + (h / 2) in dom cot & x - (h / 2) in dom cot holds (cD (((cot (#) cot) (#) cos),h)) . x = (((cos . (x + (h / 2))) |^ 3) * (((sin . (x + (h / 2))) ") |^ 2)) - (((cos . (x - (h / 2))) |^ 3) * (((sin . (x - (h / 2))) ") |^ 2)) proof let x, h be Real; ::_thesis: ( x + (h / 2) in dom cot & x - (h / 2) in dom cot implies (cD (((cot (#) cot) (#) cos),h)) . x = (((cos . (x + (h / 2))) |^ 3) * (((sin . (x + (h / 2))) ") |^ 2)) - (((cos . (x - (h / 2))) |^ 3) * (((sin . (x - (h / 2))) ") |^ 2)) ) set f = (cot (#) cot) (#) cos; assume A1: ( x + (h / 2) in dom cot & x - (h / 2) in dom cot ) ; ::_thesis: (cD (((cot (#) cot) (#) cos),h)) . x = (((cos . (x + (h / 2))) |^ 3) * (((sin . (x + (h / 2))) ") |^ 2)) - (((cos . (x - (h / 2))) |^ 3) * (((sin . (x - (h / 2))) ") |^ 2)) ( x + (h / 2) in dom ((cot (#) cot) (#) cos) & x - (h / 2) in dom ((cot (#) cot) (#) cos) ) proof set f1 = cot (#) cot; set f2 = cos ; A2: ( x + (h / 2) in dom (cot (#) cot) & x - (h / 2) in dom (cot (#) cot) ) proof ( x + (h / 2) in (dom cot) /\ (dom cot) & x - (h / 2) in (dom cot) /\ (dom cot) ) by A1; hence ( x + (h / 2) in dom (cot (#) cot) & x - (h / 2) in dom (cot (#) cot) ) by VALUED_1:def_4; ::_thesis: verum end; ( x + (h / 2) in (dom (cot (#) cot)) /\ (dom cos) & x - (h / 2) in (dom (cot (#) cot)) /\ (dom cos) ) by A2, SIN_COS:24, XBOOLE_0:def_4; hence ( x + (h / 2) in dom ((cot (#) cot) (#) cos) & x - (h / 2) in dom ((cot (#) cot) (#) cos) ) by VALUED_1:def_4; ::_thesis: verum end; then (cD (((cot (#) cot) (#) cos),h)) . x = (((cot (#) cot) (#) cos) . (x + (h / 2))) - (((cot (#) cot) (#) cos) . (x - (h / 2))) by DIFF_1:39 .= (((cot (#) cot) . (x + (h / 2))) * (cos . (x + (h / 2)))) - (((cot (#) cot) (#) cos) . (x - (h / 2))) by VALUED_1:5 .= (((cot (#) cot) . (x + (h / 2))) * (cos . (x + (h / 2)))) - (((cot (#) cot) . (x - (h / 2))) * (cos . (x - (h / 2)))) by VALUED_1:5 .= (((cot . (x + (h / 2))) * (cot . (x + (h / 2)))) * (cos . (x + (h / 2)))) - (((cot (#) cot) . (x - (h / 2))) * (cos . (x - (h / 2)))) by VALUED_1:5 .= (((cot . (x + (h / 2))) * (cot . (x + (h / 2)))) * (cos . (x + (h / 2)))) - (((cot . (x - (h / 2))) * (cot . (x - (h / 2)))) * (cos . (x - (h / 2)))) by VALUED_1:5 .= ((((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) ")) * (cot . (x + (h / 2)))) * (cos . (x + (h / 2)))) - (((cot . (x - (h / 2))) * (cot . (x - (h / 2)))) * (cos . (x - (h / 2)))) by A1, RFUNCT_1:def_1 .= ((((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) ")) * ((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) "))) * (cos . (x + (h / 2)))) - (((cot . (x - (h / 2))) * (cot . (x - (h / 2)))) * (cos . (x - (h / 2)))) by A1, RFUNCT_1:def_1 .= ((((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) ")) * ((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) "))) * (cos . (x + (h / 2)))) - ((((cos . (x - (h / 2))) * ((sin . (x - (h / 2))) ")) * (cot . (x - (h / 2)))) * (cos . (x - (h / 2)))) by A1, RFUNCT_1:def_1 .= ((((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) ")) * ((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) "))) * (cos . (x + (h / 2)))) - ((((cos . (x - (h / 2))) * ((sin . (x - (h / 2))) ")) * ((cos . (x - (h / 2))) * ((sin . (x - (h / 2))) "))) * (cos . (x - (h / 2)))) by A1, RFUNCT_1:def_1 .= ((((cos . (x + (h / 2))) * (cos . (x + (h / 2)))) * (cos . (x + (h / 2)))) * (((sin . (x + (h / 2))) ") * ((sin . (x + (h / 2))) "))) - ((((cos . (x - (h / 2))) * (cos . (x - (h / 2)))) * (cos . (x - (h / 2)))) * (((sin . (x - (h / 2))) ") * ((sin . (x - (h / 2))) "))) .= (((((cos . (x + (h / 2))) |^ 1) * (cos . (x + (h / 2)))) * (cos . (x + (h / 2)))) * (((sin . (x + (h / 2))) ") * ((sin . (x + (h / 2))) "))) - ((((cos . (x - (h / 2))) * (cos . (x - (h / 2)))) * (cos . (x - (h / 2)))) * (((sin . (x - (h / 2))) ") * ((sin . (x - (h / 2))) "))) by NEWTON:5 .= ((((cos . (x + (h / 2))) |^ (1 + 1)) * (cos . (x + (h / 2)))) * (((sin . (x + (h / 2))) ") * ((sin . (x + (h / 2))) "))) - ((((cos . (x - (h / 2))) * (cos . (x - (h / 2)))) * (cos . (x - (h / 2)))) * (((sin . (x - (h / 2))) ") * ((sin . (x - (h / 2))) "))) by NEWTON:6 .= (((cos . (x + (h / 2))) |^ (2 + 1)) * (((sin . (x + (h / 2))) ") * ((sin . (x + (h / 2))) "))) - ((((cos . (x - (h / 2))) * (cos . (x - (h / 2)))) * (cos . (x - (h / 2)))) * (((sin . (x - (h / 2))) ") * ((sin . (x - (h / 2))) "))) by NEWTON:6 .= (((cos . (x + (h / 2))) |^ 3) * ((((sin . (x + (h / 2))) ") |^ 1) * ((sin . (x + (h / 2))) "))) - ((((cos . (x - (h / 2))) * (cos . (x - (h / 2)))) * (cos . (x - (h / 2)))) * (((sin . (x - (h / 2))) ") * ((sin . (x - (h / 2))) "))) by NEWTON:5 .= (((cos . (x + (h / 2))) |^ 3) * (((sin . (x + (h / 2))) ") |^ (1 + 1))) - ((((cos . (x - (h / 2))) * (cos . (x - (h / 2)))) * (cos . (x - (h / 2)))) * (((sin . (x - (h / 2))) ") * ((sin . (x - (h / 2))) "))) by NEWTON:6 .= (((cos . (x + (h / 2))) |^ 3) * (((sin . (x + (h / 2))) ") |^ 2)) - (((((cos . (x - (h / 2))) |^ 1) * (cos . (x - (h / 2)))) * (cos . (x - (h / 2)))) * (((sin . (x - (h / 2))) ") * ((sin . (x - (h / 2))) "))) by NEWTON:5 .= (((cos . (x + (h / 2))) |^ 3) * (((sin . (x + (h / 2))) ") |^ 2)) - ((((cos . (x - (h / 2))) |^ (1 + 1)) * (cos . (x - (h / 2)))) * (((sin . (x - (h / 2))) ") * ((sin . (x - (h / 2))) "))) by NEWTON:6 .= (((cos . (x + (h / 2))) |^ 3) * (((sin . (x + (h / 2))) ") |^ 2)) - (((cos . (x - (h / 2))) |^ (2 + 1)) * (((sin . (x - (h / 2))) ") * ((sin . (x - (h / 2))) "))) by NEWTON:6 .= (((cos . (x + (h / 2))) |^ 3) * (((sin . (x + (h / 2))) ") |^ 2)) - (((cos . (x - (h / 2))) |^ 3) * ((((sin . (x - (h / 2))) ") |^ 1) * ((sin . (x - (h / 2))) "))) by NEWTON:5 .= (((cos . (x + (h / 2))) |^ 3) * (((sin . (x + (h / 2))) ") |^ 2)) - (((cos . (x - (h / 2))) |^ 3) * (((sin . (x - (h / 2))) ") |^ (1 + 1))) by NEWTON:6 .= (((cos . (x + (h / 2))) |^ 3) * (((sin . (x + (h / 2))) ") |^ 2)) - (((cos . (x - (h / 2))) |^ 3) * (((sin . (x - (h / 2))) ") |^ 2)) ; hence (cD (((cot (#) cot) (#) cos),h)) . x = (((cos . (x + (h / 2))) |^ 3) * (((sin . (x + (h / 2))) ") |^ 2)) - (((cos . (x - (h / 2))) |^ 3) * (((sin . (x - (h / 2))) ") |^ 2)) ; ::_thesis: verum end;