let n be Element of NAT ; for A being non empty closed_interval Subset of REAL st A = [.(- ((2 * n) * PI)),((2 * n) * PI).] holds
sin is_orthogonal_with cos ,A
let A be non empty closed_interval Subset of REAL; ( A = [.(- ((2 * n) * PI)),((2 * n) * PI).] implies sin is_orthogonal_with cos ,A )
assume
A = [.(- ((2 * n) * PI)),((2 * n) * PI).]
; sin is_orthogonal_with cos ,A
then A1:
( upper_bound A = (2 * n) * PI & lower_bound A = - ((2 * n) * PI) )
by INTEGRA8:37;
|||(sin,cos,A)||| =
(1 / 2) * (((cos . (lower_bound A)) * (cos . (lower_bound A))) - ((cos . (upper_bound A)) * (cos . (upper_bound A))))
by INTEGRA8:90
.=
(1 / 2) * (((cos . ((2 * n) * PI)) * (cos . (- ((2 * n) * PI)))) - ((cos . ((2 * n) * PI)) * (cos . ((2 * n) * PI))))
by A1, SIN_COS:30
.=
(1 / 2) * (((cos . ((2 * n) * PI)) * (cos . ((2 * n) * PI))) - ((cos . ((2 * n) * PI)) * (cos . ((2 * n) * PI))))
by SIN_COS:30
;
hence
sin is_orthogonal_with cos ,A
; verum