let r, s be Real; :: thesis: ( cos r = cos s implies ex i being Integer st
( r = s + ((2 * PI) * i) or r = (- s) + ((2 * PI) * i) ) )
assume A1: cos r = cos s ; :: thesis: ex i being Integer st
( r = s + ((2 * PI) * i) or r = (- s) + ((2 * PI) * i) )
A2: (cos r) - (cos s) = - (2 * ((sin ((r + s) / 2)) * (sin ((r - s) / 2)))) by SIN_COS4:18;
per cases ( sin ((r - s) / 2) = 0 or sin ((r + s) / 2) = 0 ) by A1, A2;
suppose sin ((r - s) / 2) = 0 ; :: thesis: ex i being Integer st
( r = s + ((2 * PI) * i) or r = (- s) + ((2 * PI) * i) )
hence ex i being Integer st
( r = s + ((2 * PI) * i) or r = (- s) + ((2 * PI) * i) ) by Lm5; :: thesis: verum
end;
suppose sin ((r + s) / 2) = 0 ; :: thesis: ex i being Integer st
( r = s + ((2 * PI) * i) or r = (- s) + ((2 * PI) * i) )
then consider i being Integer such that
A3: (r + s) / 2 = PI * i by Th7;
(r + s) - s = ((2 * PI) * i) - s by A3;
hence ex i being Integer st
( r = s + ((2 * PI) * i) or r = (- s) + ((2 * PI) * i) ) ; :: thesis: verum
end;
end;