let n be Element of NAT ; :: thesis: for A being closed-interval Subset of REAL st A = [.(- ((2 * n) * PI )),((2 * n) * PI ).] holds
sin is_orthogonal_with cos ,A
let A be closed-interval Subset of REAL ; :: thesis: ( A = [.(- ((2 * n) * PI )),((2 * n) * PI ).] implies sin is_orthogonal_with cos ,A )
assume A = [.(- ((2 * n) * PI )),((2 * n) * PI ).] ; :: thesis: 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:33
.= (1 / 2) * (((cos . ((2 * n) * PI )) * (cos . ((2 * n) * PI ))) - ((cos . ((2 * n) * PI )) * (cos . ((2 * n) * PI )))) by SIN_COS:33 ;
hence sin is_orthogonal_with cos ,A by Def2; :: thesis: verum