let a be real number ; :: thesis: ( sin a = 0 implies cos a <> 0 )
consider r being real number such that
A1: r = ((2 * PI ) * (- [\(a / (2 * PI ))/])) + a and
A2: ( 0 <= r & r < 2 * PI ) by Th2, COMPTRIG:21;
A3: sin a = sin r by A1, Th9;
A4: cos a = cos r by A1, Th10;
assume ( sin a = 0 & cos a = 0 ) ; :: thesis: contradiction
then ( ( r = 0 or r = PI ) & ( r = PI / 2 or r = (3 / 2) * PI ) ) by A2, A3, A4, COMPTRIG:33, COMPTRIG:34;
hence contradiction by COMPTRIG:21; :: thesis: verum