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