cos | ].0,PI.[ c= cos | [.0,PI.]
by RELAT_1:75, XXREAL_1:25;
then A1:
rng (cos | ].0,PI.[) c= rng (cos | [.0,PI.])
by RELAT_1:11;
A2:
rng (cos | ].0,PI.[) = cos .: ].0,PI.[
by RELAT_1:115;
thus
cos .: ].0,PI.[ c= ].(- 1),1.[
XBOOLE_0:def 10 ].(- 1),1.[ c= cos .: ].0,PI.[proof
let x be
object ;
TARSKI:def 3 ( not x in cos .: ].0,PI.[ or x in ].(- 1),1.[ )
assume A3:
x in cos .: ].0,PI.[
;
x in ].(- 1),1.[
then consider a being
object such that A4:
a in dom cos
and A5:
a in ].0,PI.[
and A6:
cos . a = x
by FUNCT_1:def 6;
reconsider a =
a,
x =
x as
Real by A4, A6;
set i =
[\(a / (2 * PI))/];
A7:
H1(
[\(a / (2 * PI))/])
/ ((2 * PI) * 1) = [\(a / (2 * PI))/] / 1
by XCMPLX_1:91;
A8:
cos . a = cos a
by SIN_COS:def 19;
x <= 1
by A1, A2, A3, COMPTRIG:32, XXREAL_1:1;
then A15:
x < 1
by A9, XXREAL_0:1;
- 1
<= x
by A1, A2, A3, COMPTRIG:32, XXREAL_1:1;
then
- 1
< x
by A12, XXREAL_0:1;
hence
x in ].(- 1),1.[
by A15, XXREAL_1:4;
verum
end;
let a be object ; TARSKI:def 3 ( not a in ].(- 1),1.[ or a in cos .: ].0,PI.[ )
assume A16:
a in ].(- 1),1.[
; a in cos .: ].0,PI.[
then reconsider a = a as Real ;
( - 1 < a & a < 1 )
by A16, XXREAL_1:4;
then
a in rng (cos | [.0,PI.])
by COMPTRIG:32, XXREAL_1:1;
then consider x being object such that
A17:
x in dom (cos | [.0,PI.])
and
A18:
(cos | [.0,PI.]) . x = a
by FUNCT_1:def 3;
reconsider x = x as Real by A17;
A19:
cos . x = a
by A17, A18, FUNCT_1:47;
A20:
dom (cos | [.0,PI.]) = [.0,PI.]
by RELAT_1:62, SIN_COS:24;
then
x <= PI
by A17, XXREAL_1:1;
then
( ( 0 < x & x < PI ) or 0 = x or PI = x )
by A17, A20, XXREAL_0:1, XXREAL_1:1;
then
x in ].0,PI.[
by A16, A19, SIN_COS:30, SIN_COS:76, XXREAL_1:4;
hence
a in cos .: ].0,PI.[
by A19, FUNCT_1:def 6, SIN_COS:24; verum