thus A1: cos . (PI / 2) = cos . ((PI / 4) + (PI / 4))
.= ((cos . (PI / 4)) * (cos . (PI / 4))) - ((cos . (PI / 4)) * (cos . (PI / 4))) by Th78, Th79
.= 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 Th78, Th79
.= 1 by Th31 ; :: 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, Th79
.= - 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 Th79
.= 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 Th79
.= 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 Th79
.= - 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, Th79
.= 1 by A4 ; :: thesis: sin . (2 * PI ) = 0
thus sin . (2 * PI ) = sin . (PI + PI )
.= ((sin . PI ) * (cos . PI )) + ((cos . PI ) * (sin . PI )) by Th79
.= 0 by A4 ; :: thesis: verum