let x be Real; :: thesis: for n being Element of NAT
for A being non empty closed_interval Subset of REAL st A = [.(x - ((2 * n) * PI)),(x + ((2 * n) * PI)).] holds
sin is_orthogonal_with cos ,A
let n be Element of NAT ; :: thesis: for A being non empty closed_interval Subset of REAL st A = [.(x - ((2 * n) * PI)),(x + ((2 * n) * PI)).] holds
sin is_orthogonal_with cos ,A
let A be non empty closed_interval Subset of REAL; :: thesis: ( A = [.(x - ((2 * n) * PI)),(x + ((2 * n) * PI)).] implies sin is_orthogonal_with cos ,A )
assume A = [.(x - ((2 * n) * PI)),(x + ((2 * n) * PI)).] ; :: thesis: sin is_orthogonal_with cos ,A
then A1: ( upper_bound A = x + ((2 * n) * PI) & lower_bound A = x - ((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) - x)) * (cos . (- (((2 * n) * PI) - x)))) - ((cos . (x + ((2 * n) * PI))) * (cos . (x + ((2 * n) * PI))))) by A1, SIN_COS:30
.= (1 / 2) * (((cos . ((- x) + ((2 * n) * PI))) * (cos . ((- x) + ((2 * n) * PI)))) - ((cos . (x + ((2 * n) * PI))) * (cos . (x + ((2 * n) * PI))))) by SIN_COS:30
.= (1 / 2) * (((cos (- x)) * (cos ((- x) + ((2 * n) * PI)))) - ((cos . (x + ((2 * n) * PI))) * (cos . (x + ((2 * n) * PI))))) by INTEGRA8:3
.= (1 / 2) * (((cos (- x)) * (cos (- x))) - ((cos . (x + ((2 * n) * PI))) * (cos . (x + ((2 * n) * PI))))) by INTEGRA8:3
.= (1 / 2) * (((cos x) * (cos (- x))) - ((cos . (x + ((2 * n) * PI))) * (cos . (x + ((2 * n) * PI))))) by SIN_COS:31
.= (1 / 2) * (((cos x) * (cos x)) - ((cos (x + ((2 * n) * PI))) * (cos . (x + ((2 * n) * PI))))) by SIN_COS:31
.= (1 / 2) * (((cos x) * (cos x)) - ((cos x) * (cos (x + ((2 * n) * PI))))) by INTEGRA8:3
.= (1 / 2) * (((cos x) * (cos x)) - ((cos x) * (cos x))) by INTEGRA8:3 ;
hence sin is_orthogonal_with cos ,A ; :: thesis: verum