let n be Element of NAT ; ( n <> 0 implies ( ((1 / (n ^2)) (#) (cos * (AffineMap (n,0)))) + ((AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0)))) is_differentiable_on REAL & ( for x being Real holds ((((1 / (n ^2)) (#) (cos * (AffineMap (n,0)))) + ((AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0))))) `| REAL) . x = x * (cos . (n * x)) ) ) )
A1:
dom (((1 / (n ^2)) (#) (cos * (AffineMap (n,0)))) + ((AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0))))) = [#] REAL
by FUNCT_2:def 1;
A2:
( dom (AffineMap ((1 / n),0)) = REAL & ( for x being Real st x in REAL holds
(AffineMap ((1 / n),0)) . x = ((1 / n) * x) + 0 ) )
by FUNCT_2:def 1, JORDAN16:def 3;
then A3:
AffineMap ((1 / n),0) is_differentiable_on REAL
by A1, FDIFF_1:31;
A4:
for x being Real st x in REAL holds
(AffineMap (n,0)) . x = (n * x) + 0
by JORDAN16:def 3;
A5:
dom (cos * (AffineMap (n,0))) = [#] REAL
by FUNCT_2:def 1;
then A6:
cos * (AffineMap (n,0)) is_differentiable_on REAL
by A4, FDIFF_4:38;
A7:
dom ((1 / (n ^2)) (#) (cos * (AffineMap (n,0)))) = REAL
by FUNCT_2:def 1;
then A8:
(1 / (n ^2)) (#) (cos * (AffineMap (n,0))) is_differentiable_on REAL
by A1, A6, FDIFF_1:28;
assume A9:
n <> 0
; ( ((1 / (n ^2)) (#) (cos * (AffineMap (n,0)))) + ((AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0)))) is_differentiable_on REAL & ( for x being Real holds ((((1 / (n ^2)) (#) (cos * (AffineMap (n,0)))) + ((AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0))))) `| REAL) . x = x * (cos . (n * x)) ) )
A10:
for x being Real st x in REAL holds
(((1 / (n ^2)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = - ((1 / n) * (sin (n * x)))
proof
let x be
Real;
( x in REAL implies (((1 / (n ^2)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = - ((1 / n) * (sin (n * x))) )
assume
x in REAL
;
(((1 / (n ^2)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = - ((1 / n) * (sin (n * x)))
(((1 / (n ^2)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x =
(1 / (n ^2)) * (diff ((cos * (AffineMap (n,0))),x))
by A7, A1, A6, FDIFF_1:28
.=
(1 / (n ^2)) * (((cos * (AffineMap (n,0))) `| REAL) . x)
by A6, FDIFF_1:def 8
.=
(1 / (n ^2)) * (- (n * (sin . ((n * x) + 0))))
by A5, A4, FDIFF_4:38
.=
((- 1) * (n * (1 / (n * n)))) * (sin . ((n * x) + 0))
.=
((- 1) * (n / ((n * n) / 1))) * (sin . ((n * x) + 0))
by XCMPLX_1:80
.=
((- 1) * ((n * 1) / (n * n))) * (sin . ((n * x) + 0))
.=
((- 1) * (1 / n)) * (sin . ((n * x) + 0))
by A9, XCMPLX_1:92
;
hence
(((1 / (n ^2)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = - ((1 / n) * (sin (n * x)))
;
verum
end;
A11:
dom (sin * (AffineMap (n,0))) = [#] REAL
by FUNCT_2:def 1;
then A12:
sin * (AffineMap (n,0)) is_differentiable_on REAL
by A4, FDIFF_4:37;
A13:
dom ((AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0)))) = REAL
by FUNCT_2:def 1;
then A14:
(AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0))) is_differentiable_on REAL
by A1, A3, A12, FDIFF_1:29;
A15:
for x being Real st x in REAL holds
(((AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = ((1 / n) * (sin . (n * x))) + (x * (cos . (n * x)))
proof
let x be
Real;
( x in REAL implies (((AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = ((1 / n) * (sin . (n * x))) + (x * (cos . (n * x))) )
assume
x in REAL
;
(((AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = ((1 / n) * (sin . (n * x))) + (x * (cos . (n * x)))
(((AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0)))) `| REAL) . x =
(((sin * (AffineMap (n,0))) . x) * (diff ((AffineMap ((1 / n),0)),x))) + (((AffineMap ((1 / n),0)) . x) * (diff ((sin * (AffineMap (n,0))),x)))
by A13, A1, A3, A12, FDIFF_1:29
.=
(((sin * (AffineMap (n,0))) . x) * (((AffineMap ((1 / n),0)) `| REAL) . x)) + (((AffineMap ((1 / n),0)) . x) * (diff ((sin * (AffineMap (n,0))),x)))
by A3, FDIFF_1:def 8
.=
(((sin * (AffineMap (n,0))) . x) * (1 / n)) + (((AffineMap ((1 / n),0)) . x) * (diff ((sin * (AffineMap (n,0))),x)))
by A1, A2, FDIFF_1:31
.=
(((sin * (AffineMap (n,0))) . x) * (1 / n)) + (((AffineMap ((1 / n),0)) . x) * (((sin * (AffineMap (n,0))) `| REAL) . x))
by A12, FDIFF_1:def 8
.=
(((sin * (AffineMap (n,0))) . x) * (1 / n)) + (((AffineMap ((1 / n),0)) . x) * (n * (cos . ((n * x) + 0))))
by A11, A4, FDIFF_4:37
.=
(((sin * (AffineMap (n,0))) . x) * (1 / n)) + ((((1 / n) * x) + 0) * (n * (cos . ((n * x) + 0))))
by JORDAN16:def 3
.=
((sin . ((AffineMap (n,0)) . x)) * (1 / n)) + (((1 / n) * x) * (n * (cos . ((n * x) + 0))))
by A11, FUNCT_1:22
.=
((1 / n) * (sin . (n * x))) + ((((1 / n) * n) * x) * (cos . (n * x)))
by JORDAN16:def 3
.=
((1 / n) * (sin . (n * x))) + ((1 * x) * (cos . (n * x)))
by A9, XCMPLX_1:88
.=
((1 / n) * (sin . (n * x))) + (x * (cos . (n * x)))
;
hence
(((AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = ((1 / n) * (sin . (n * x))) + (x * (cos . (n * x)))
;
verum
end;
for x being Real st x in REAL holds
((((1 / (n ^2)) (#) (cos * (AffineMap (n,0)))) + ((AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0))))) `| REAL) . x = x * (cos . (n * x))
proof
let x be
Real;
( x in REAL implies ((((1 / (n ^2)) (#) (cos * (AffineMap (n,0)))) + ((AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0))))) `| REAL) . x = x * (cos . (n * x)) )
assume
x in REAL
;
((((1 / (n ^2)) (#) (cos * (AffineMap (n,0)))) + ((AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0))))) `| REAL) . x = x * (cos . (n * x))
((((1 / (n ^2)) (#) (cos * (AffineMap (n,0)))) + ((AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0))))) `| REAL) . x =
(diff (((1 / (n ^2)) (#) (cos * (AffineMap (n,0)))),x)) + (diff (((AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0)))),x))
by A1, A8, A14, FDIFF_1:26
.=
((((1 / (n ^2)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x) + (diff (((AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0)))),x))
by A8, FDIFF_1:def 8
.=
(- ((1 / n) * (sin (n * x)))) + (diff (((AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0)))),x))
by A10
.=
(- ((1 / n) * (sin (n * x)))) + ((((AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0)))) `| REAL) . x)
by A14, FDIFF_1:def 8
.=
(- ((1 / n) * (sin (n * x)))) + (((1 / n) * (sin . (n * x))) + (x * (cos . (n * x))))
by A15
.=
x * (cos . (n * x))
;
hence
((((1 / (n ^2)) (#) (cos * (AffineMap (n,0)))) + ((AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0))))) `| REAL) . x = x * (cos . (n * x))
;
verum
end;
hence
( ((1 / (n ^2)) (#) (cos * (AffineMap (n,0)))) + ((AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0)))) is_differentiable_on REAL & ( for x being Real holds ((((1 / (n ^2)) (#) (cos * (AffineMap (n,0)))) + ((AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0))))) `| REAL) . x = x * (cos . (n * x)) ) )
by A1, A8, A14, FDIFF_1:26; verum