let th be Real; :: thesis: ( sin . (th + (2 * PI)) = sin . th & cos . (th + (2 * PI)) = cos . th & sin . ((PI / 2) - th) = cos . th & cos . ((PI / 2) - th) = sin . th & sin . ((PI / 2) + th) = cos . th & cos . ((PI / 2) + th) = - (sin . th) & sin . (PI + th) = - (sin . th) & cos . (PI + th) = - (cos . th) )
thus sin . (th + (2 * PI)) = ((sin . th) * 1) + ((cos . th) * 0) by Th73, Th75
.= sin . th ; :: thesis: ( cos . (th + (2 * PI)) = cos . th & sin . ((PI / 2) - th) = cos . th & cos . ((PI / 2) - th) = sin . th & sin . ((PI / 2) + th) = cos . th & cos . ((PI / 2) + th) = - (sin . th) & sin . (PI + th) = - (sin . th) & cos . (PI + th) = - (cos . th) )
thus cos . (th + (2 * PI)) = ((cos . th) * 1) - ((sin . th) * 0) by Th73, Th75
.= cos . th ; :: thesis: ( sin . ((PI / 2) - th) = cos . th & cos . ((PI / 2) - th) = sin . th & sin . ((PI / 2) + th) = cos . th & cos . ((PI / 2) + th) = - (sin . th) & sin . (PI + th) = - (sin . th) & cos . (PI + th) = - (cos . th) )
thus sin . ((PI / 2) - th) = ((sin . (PI / 2)) * (cos . (- th))) + ((cos . (PI / 2)) * (sin . (- th))) by Th73
.= cos . th by Th30, Th75 ; :: thesis: ( cos . ((PI / 2) - th) = sin . th & sin . ((PI / 2) + th) = cos . th & cos . ((PI / 2) + th) = - (sin . th) & sin . (PI + th) = - (sin . th) & cos . (PI + th) = - (cos . th) )
thus cos . ((PI / 2) - th) = ((cos . (PI / 2)) * (cos . (- th))) - ((sin . (PI / 2)) * (sin . (- th))) by Th73
.= 0 - (1 * (- (sin . th))) by Th30, Th75
.= sin . th ; :: thesis: ( sin . ((PI / 2) + th) = cos . th & cos . ((PI / 2) + th) = - (sin . th) & sin . (PI + th) = - (sin . th) & cos . (PI + th) = - (cos . th) )
thus sin . ((PI / 2) + th) = (1 * (cos . th)) + (0 * (sin . th)) by Th73, Th75
.= cos . th ; :: thesis: ( cos . ((PI / 2) + th) = - (sin . th) & sin . (PI + th) = - (sin . th) & cos . (PI + th) = - (cos . th) )
thus cos . ((PI / 2) + th) = ((cos . (PI / 2)) * (cos . th)) - ((sin . (PI / 2)) * (sin . th)) by Th73
.= - (sin . th) by Th75 ; :: thesis: ( sin . (PI + th) = - (sin . th) & cos . (PI + th) = - (cos . th) )
thus sin . (PI + th) = ((sin . PI) * (cos . th)) + ((cos . PI) * (sin . th)) by Th73
.= - (sin . th) by Th75 ; :: thesis: cos . (PI + th) = - (cos . th)
thus cos . (PI + th) = ((- 1) * (cos . th)) - (0 * (sin . th)) by Th73, Th75
.= - (cos . th) ; :: thesis: verum