let n be Element of NAT ; ( n <> 0 implies ( (- (1 / n)) (#) (cos * (AffineMap (n,0))) is_differentiable_on REAL & ( for x being Real holds (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = sin (n * x) ) ) )
assume A1:
n <> 0
; ( (- (1 / n)) (#) (cos * (AffineMap (n,0))) is_differentiable_on REAL & ( for x being Real holds (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = sin (n * x) ) )
A2:
[#] REAL = dom ((- (1 / n)) (#) (cos * (AffineMap (n,0))))
by FUNCT_2:def 1;
A3:
( [#] REAL = dom (cos * (AffineMap (n,0))) & ( for x being Real st x in REAL holds
(AffineMap (n,0)) . x = (n * x) + 0 ) )
by FCONT_1:def 4, FUNCT_2:def 1;
then A4:
cos * (AffineMap (n,0)) is_differentiable_on REAL
by FDIFF_4:38;
hence
(- (1 / n)) (#) (cos * (AffineMap (n,0))) is_differentiable_on REAL
by A2, FDIFF_1:20; for x being Real holds (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = sin (n * x)
A5:
for x being Real st x in REAL holds
(((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = sin (n * x)
proof
let x be
Real;
( x in REAL implies (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = sin (n * x) )
assume A6:
x in REAL
;
(((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = sin (n * x)
then (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x =
(- (1 / n)) * (diff ((cos * (AffineMap (n,0))),x))
by A2, A4, FDIFF_1:20
.=
(- (1 / n)) * (((cos * (AffineMap (n,0))) `| REAL) . x)
by A4, FDIFF_1:def 7, A6
.=
(- (1 / n)) * (- (n * (sin . ((n * x) + 0))))
by A3, FDIFF_4:38, A6
.=
((1 / n) * n) * (sin . ((n * x) + 0))
.=
(n / n) * (sin . ((n * x) + 0))
by XCMPLX_1:99
.=
1
* (sin . ((n * x) + 0))
by A1, XCMPLX_1:60
.=
sin (n * x)
;
hence
(((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = sin (n * x)
;
verum
end;
let x be Real; (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = sin (n * x)
x in REAL
by XREAL_0:def 1;
hence
(((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = sin (n * x)
by A5; verum