thus A1: cos . (PI / 2) = cos . ((PI / 4) + (PI / 4))
.= ((cos . (PI / 4)) * (cos . (PI / 4))) - ((cos . (PI / 4)) * (cos . (PI / 4))) by Th72, Th73
.= 0 ; :: thesis: ( sin . (PI / 2) = 1 & cos . PI = - 1 & sin . PI = 0 & cos . (PI + (PI / 2)) = 0 & sin . (PI + (PI / 2)) = - 1 & cos . (2 * PI) = 1 & sin . (2 * PI) = 0 )
thus A2: sin . (PI / 2) = sin . ((PI / 4) + (PI / 4))
.= ((cos . (PI / 4)) * (cos . (PI / 4))) + ((sin . (PI / 4)) * (sin . (PI / 4))) by Th72, Th73
.= 1 by Th28 ; :: thesis: ( cos . PI = - 1 & sin . PI = 0 & cos . (PI + (PI / 2)) = 0 & sin . (PI + (PI / 2)) = - 1 & cos . (2 * PI) = 1 & sin . (2 * PI) = 0 )
thus A3: cos . PI = cos . ((PI / 2) + (PI / 2))
.= (0 * 0) - ((sin . (PI / 2)) * (sin . (PI / 2))) by A1, Th73
.= - 1 by A2 ; :: thesis: ( sin . PI = 0 & cos . (PI + (PI / 2)) = 0 & sin . (PI + (PI / 2)) = - 1 & cos . (2 * PI) = 1 & sin . (2 * PI) = 0 )
thus A4: sin . PI = sin . ((PI / 2) + (PI / 2))
.= ((sin . (PI / 2)) * (cos . (PI / 2))) + ((cos . (PI / 2)) * (sin . (PI / 2))) by Th73
.= 0 by A1 ; :: thesis: ( cos . (PI + (PI / 2)) = 0 & sin . (PI + (PI / 2)) = - 1 & cos . (2 * PI) = 1 & sin . (2 * PI) = 0 )
thus cos . (PI + (PI / 2)) = ((cos . PI) * (cos . (PI / 2))) - ((sin . PI) * (sin . (PI / 2))) by Th73
.= 0 by A1, A4 ; :: thesis: ( sin . (PI + (PI / 2)) = - 1 & cos . (2 * PI) = 1 & sin . (2 * PI) = 0 )
thus sin . (PI + (PI / 2)) = ((sin . PI) * (cos . (PI / 2))) + ((cos . PI) * (sin . (PI / 2))) by Th73
.= - 1 by A1, A2, A3 ; :: thesis: ( cos . (2 * PI) = 1 & sin . (2 * PI) = 0 )
thus cos . (2 * PI) = cos . (PI + PI)
.= ((- 1) * (- 1)) - ((sin . PI) * (sin . PI)) by A3, Th73
.= 1 by A4 ; :: thesis: sin . (2 * PI) = 0
thus sin . (2 * PI) = sin . (PI + PI)
.= ((sin . PI) * (cos . PI)) + ((cos . PI) * (sin . PI)) by Th73
.= 0 by A4 ; :: thesis: verum