let n, m be Element of NAT ; :: thesis: ( m + n <> 0 & m - n <> 0 implies ( (- ((1 / (2 * (m + n))) (#) (cos * (AffineMap ((m + n),0))))) - ((1 / (2 * (m - n))) (#) (cos * (AffineMap ((m - n),0)))) is_differentiable_on REAL & ( for x being Real holds (((- ((1 / (2 * (m + n))) (#) (cos * (AffineMap ((m + n),0))))) - ((1 / (2 * (m - n))) (#) (cos * (AffineMap ((m - n),0))))) `| REAL) . x = (sin . (m * x)) * (cos . (n * x)) ) ) )
assume that
A1: m + n <> 0 and
A2: m - n <> 0 ; :: thesis: ( (- ((1 / (2 * (m + n))) (#) (cos * (AffineMap ((m + n),0))))) - ((1 / (2 * (m - n))) (#) (cos * (AffineMap ((m - n),0)))) is_differentiable_on REAL & ( for x being Real holds (((- ((1 / (2 * (m + n))) (#) (cos * (AffineMap ((m + n),0))))) - ((1 / (2 * (m - n))) (#) (cos * (AffineMap ((m - n),0))))) `| REAL) . x = (sin . (m * x)) * (cos . (n * x)) ) )
A3: ( dom (cos * (AffineMap ((m + n),0))) = [#] REAL & ( for x being Real st x in REAL holds
(AffineMap ((m + n),0)) . x = ((m + n) * x) + 0 ) ) by FCONT_1:def 4, FUNCT_2:def 1;
then A4: cos * (AffineMap ((m + n),0)) is_differentiable_on REAL by FDIFF_4:38;
A5: for x being Real st x in REAL holds
((- ((1 / (2 * (m + n))) (#) (cos * (AffineMap ((m + n),0))))) `| REAL) . x = (1 / 2) * (sin ((m + n) * x))
proof
let x be Real; :: thesis: ( x in REAL implies ((- ((1 / (2 * (m + n))) (#) (cos * (AffineMap ((m + n),0))))) `| REAL) . x = (1 / 2) * (sin ((m + n) * x)) )
assume A6: x in REAL ; :: thesis: ((- ((1 / (2 * (m + n))) (#) (cos * (AffineMap ((m + n),0))))) `| REAL) . x = (1 / 2) * (sin ((m + n) * x))
A7: dom (((- 1) / (2 * (m + n))) (#) (cos * (AffineMap ((m + n),0)))) = [#] REAL by FUNCT_2:def 1;
((- ((1 / (2 * (m + n))) (#) (cos * (AffineMap ((m + n),0))))) `| REAL) . x = ((((- 1) * (1 / (2 * (m + n)))) (#) (cos * (AffineMap ((m + n),0)))) `| REAL) . x by RFUNCT_1:17
.= (((- (1 / (2 * (m + n)))) (#) (cos * (AffineMap ((m + n),0)))) `| REAL) . x
.= ((((- 1) / (2 * (m + n))) (#) (cos * (AffineMap ((m + n),0)))) `| REAL) . x by XCMPLX_1:187
.= ((- 1) / (2 * (m + n))) * (diff ((cos * (AffineMap ((m + n),0))),x)) by A4, A7, FDIFF_1:20, A6
.= ((- 1) / (2 * (m + n))) * (((cos * (AffineMap ((m + n),0))) `| REAL) . x) by A4, FDIFF_1:def 7, A6
.= ((- 1) / (2 * (m + n))) * (- ((m + n) * (sin . (((m + n) * x) + 0)))) by A3, FDIFF_4:38, A6
.= ((- ((- 1) / (2 * (m + n)))) * (m + n)) * (sin . (((m + n) * x) + 0))
.= ((1 / (2 * (m + n))) * (m + n)) * (sin . (((m + n) * x) + 0)) by XCMPLX_1:190
.= ((1 * (m + n)) / (2 * (m + n))) * (sin . (((m + n) * x) + 0)) by XCMPLX_1:74
.= (1 / 2) * (sin ((m + n) * x)) by A1, XCMPLX_1:91 ;
hence ((- ((1 / (2 * (m + n))) (#) (cos * (AffineMap ((m + n),0))))) `| REAL) . x = (1 / 2) * (sin ((m + n) * x)) ; :: thesis: verum
end;
A8: dom (- ((1 / (2 * (m + n))) (#) (cos * (AffineMap ((m + n),0))))) = [#] REAL by FUNCT_2:def 1;
dom ((1 / (2 * (m + n))) (#) (cos * (AffineMap ((m + n),0)))) = [#] REAL by FUNCT_2:def 1;
then ( - ((1 / (2 * (m + n))) (#) (cos * (AffineMap ((m + n),0)))) = (- 1) (#) ((1 / (2 * (m + n))) (#) (cos * (AffineMap ((m + n),0)))) & (1 / (2 * (m + n))) (#) (cos * (AffineMap ((m + n),0))) is_differentiable_on REAL ) by A4, FDIFF_1:20;
then A9: - ((1 / (2 * (m + n))) (#) (cos * (AffineMap ((m + n),0)))) is_differentiable_on REAL by A8, FDIFF_1:20;
A10: REAL = dom ((- ((1 / (2 * (m + n))) (#) (cos * (AffineMap ((m + n),0))))) - ((1 / (2 * (m - n))) (#) (cos * (AffineMap ((m - n),0))))) by FUNCT_2:def 1;
A11: ( dom (cos * (AffineMap ((m - n),0))) = [#] REAL & ( for x being Real st x in REAL holds
(AffineMap ((m - n),0)) . x = ((m - n) * x) + 0 ) ) by FCONT_1:def 4, FUNCT_2:def 1;
then A12: cos * (AffineMap ((m - n),0)) is_differentiable_on REAL by FDIFF_4:38;
A13: dom ((1 / (2 * (m - n))) (#) (cos * (AffineMap ((m - n),0)))) = [#] REAL by FUNCT_2:def 1;
then A14: (1 / (2 * (m - n))) (#) (cos * (AffineMap ((m - n),0))) is_differentiable_on REAL by A12, FDIFF_1:20;
hence (- ((1 / (2 * (m + n))) (#) (cos * (AffineMap ((m + n),0))))) - ((1 / (2 * (m - n))) (#) (cos * (AffineMap ((m - n),0)))) is_differentiable_on REAL by A8, A10, A9, FDIFF_1:19; :: thesis: for x being Real holds (((- ((1 / (2 * (m + n))) (#) (cos * (AffineMap ((m + n),0))))) - ((1 / (2 * (m - n))) (#) (cos * (AffineMap ((m - n),0))))) `| REAL) . x = (sin . (m * x)) * (cos . (n * x))
A15: for x being Real st x in REAL holds
(((1 / (2 * (m - n))) (#) (cos * (AffineMap ((m - n),0)))) `| REAL) . x = - ((1 / 2) * (sin ((m - n) * x)))
proof
let x be Real; :: thesis: ( x in REAL implies (((1 / (2 * (m - n))) (#) (cos * (AffineMap ((m - n),0)))) `| REAL) . x = - ((1 / 2) * (sin ((m - n) * x))) )
assume A16: x in REAL ; :: thesis: (((1 / (2 * (m - n))) (#) (cos * (AffineMap ((m - n),0)))) `| REAL) . x = - ((1 / 2) * (sin ((m - n) * x)))
(((1 / (2 * (m - n))) (#) (cos * (AffineMap ((m - n),0)))) `| REAL) . x = (1 / (2 * (m - n))) * (diff ((cos * (AffineMap ((m - n),0))),x)) by A13, A12, FDIFF_1:20, A16
.= (1 / (2 * (m - n))) * (((cos * (AffineMap ((m - n),0))) `| REAL) . x) by A12, FDIFF_1:def 7, A16
.= (1 / (2 * (m - n))) * (- ((m - n) * (sin . (((m - n) * x) + 0)))) by A11, FDIFF_4:38, A16
.= ((- (1 / (2 * (m - n)))) * (m - n)) * (sin . (((m - n) * x) + 0))
.= (((- 1) / (2 * (m - n))) * (m - n)) * (sin . (((m - n) * x) + 0)) by XCMPLX_1:187
.= (((- 1) * (m - n)) / (2 * (m - n))) * (sin . (((m - n) * x) + 0)) by XCMPLX_1:74
.= ((- 1) / 2) * (sin ((m - n) * x)) by A2, XCMPLX_1:91 ;
hence (((1 / (2 * (m - n))) (#) (cos * (AffineMap ((m - n),0)))) `| REAL) . x = - ((1 / 2) * (sin ((m - n) * x))) ; :: thesis: verum
end;
A17: for x being Real st x in REAL holds
(((- ((1 / (2 * (m + n))) (#) (cos * (AffineMap ((m + n),0))))) - ((1 / (2 * (m - n))) (#) (cos * (AffineMap ((m - n),0))))) `| REAL) . x = (sin . (m * x)) * (cos . (n * x))
proof
let x be Real; :: thesis: ( x in REAL implies (((- ((1 / (2 * (m + n))) (#) (cos * (AffineMap ((m + n),0))))) - ((1 / (2 * (m - n))) (#) (cos * (AffineMap ((m - n),0))))) `| REAL) . x = (sin . (m * x)) * (cos . (n * x)) )
assume A18: x in REAL ; :: thesis: (((- ((1 / (2 * (m + n))) (#) (cos * (AffineMap ((m + n),0))))) - ((1 / (2 * (m - n))) (#) (cos * (AffineMap ((m - n),0))))) `| REAL) . x = (sin . (m * x)) * (cos . (n * x))
(((- ((1 / (2 * (m + n))) (#) (cos * (AffineMap ((m + n),0))))) - ((1 / (2 * (m - n))) (#) (cos * (AffineMap ((m - n),0))))) `| REAL) . x = (diff ((- ((1 / (2 * (m + n))) (#) (cos * (AffineMap ((m + n),0))))),x)) - (diff (((1 / (2 * (m - n))) (#) (cos * (AffineMap ((m - n),0)))),x)) by A8, A10, A9, A14, FDIFF_1:19, A18
.= (((- ((1 / (2 * (m + n))) (#) (cos * (AffineMap ((m + n),0))))) `| REAL) . x) - (diff (((1 / (2 * (m - n))) (#) (cos * (AffineMap ((m - n),0)))),x)) by A9, FDIFF_1:def 7, A18
.= (((- ((1 / (2 * (m + n))) (#) (cos * (AffineMap ((m + n),0))))) `| REAL) . x) - ((((1 / (2 * (m - n))) (#) (cos * (AffineMap ((m - n),0)))) `| REAL) . x) by A14, FDIFF_1:def 7, A18
.= ((1 / 2) * (sin ((m + n) * x))) - ((((1 / (2 * (m - n))) (#) (cos * (AffineMap ((m - n),0)))) `| REAL) . x) by A5, A18
.= ((1 / 2) * (sin ((m + n) * x))) - (- ((1 / 2) * (sin ((m - n) * x)))) by A15, A18
.= (1 / 2) * ((sin ((m + n) * x)) + (sin ((m - n) * x)))
.= (1 / 2) * (2 * ((cos ((((m + n) * x) - ((m - n) * x)) / 2)) * (sin ((((m + n) * x) + ((m - n) * x)) / 2)))) by SIN_COS4:15
.= (sin . (m * x)) * (cos . (n * x)) ;
hence (((- ((1 / (2 * (m + n))) (#) (cos * (AffineMap ((m + n),0))))) - ((1 / (2 * (m - n))) (#) (cos * (AffineMap ((m - n),0))))) `| REAL) . x = (sin . (m * x)) * (cos . (n * x)) ; :: thesis: verum
end;
let x be Real; :: thesis: (((- ((1 / (2 * (m + n))) (#) (cos * (AffineMap ((m + n),0))))) - ((1 / (2 * (m - n))) (#) (cos * (AffineMap ((m - n),0))))) `| REAL) . x = (sin . (m * x)) * (cos . (n * x))
x in REAL by XREAL_0:def 1;
hence (((- ((1 / (2 * (m + n))) (#) (cos * (AffineMap ((m + n),0))))) - ((1 / (2 * (m - n))) (#) (cos * (AffineMap ((m - n),0))))) `| REAL) . x = (sin . (m * x)) * (cos . (n * x)) by A17; :: thesis: verum