let a be Real; :: thesis: ( sin a = 0 implies cos a <> 0 )
assume that
A1: sin a = 0 and
A2: cos a = 0 ; :: thesis: contradiction
consider r being Real such that
A3: r = ((2 * PI) * (- [\(a / (2 * PI))/])) + a and
A4: ( 0 <= r & r < 2 * PI ) by Th1, COMPTRIG:5;
A5: cos a = cos r by A3, Th9;
sin a = sin r by A3, Th8;
then ( r = 0 or r = PI ) by A4, A1, COMPTRIG:17;
hence contradiction by A5, A2, COMPTRIG:5, COMPTRIG:18; :: thesis: verum