sin | ].(- (PI / 2)),(PI / 2).[ c= sin | [.(- (PI / 2)),(PI / 2).] by RELAT_1:75, XXREAL_1:25;
then A1: rng (sin | ].(- (PI / 2)),(PI / 2).[) c= rng (sin | [.(- (PI / 2)),(PI / 2).]) by RELAT_1:11;
A2: rng (sin | ].(- (PI / 2)),(PI / 2).[) = sin .: ].(- (PI / 2)),(PI / 2).[ by RELAT_1:115;
thus sin .: ].(- (PI / 2)),(PI / 2).[ c= ].(- 1),1.[ :: according to XBOOLE_0:def 10 :: thesis: ].(- 1),1.[ c= sin .: ].(- (PI / 2)),(PI / 2).[
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in sin .: ].(- (PI / 2)),(PI / 2).[ or x in ].(- 1),1.[ )
assume A3: x in sin .: ].(- (PI / 2)),(PI / 2).[ ; :: thesis: x in ].(- 1),1.[
then consider a being object such that
A4: a in dom sin and
A5: a in ].(- (PI / 2)),(PI / 2).[ and
A6: sin . 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: sin . a = sin a by SIN_COS:def 17;
A9: now :: thesis: not x = 1
assume x = 1 ; :: thesis: contradiction
then A10: a = (PI / 2) + H1([\(a / (2 * PI))/]) by A6, A8, Th24;
then (PI / 2) + H1([\(a / (2 * PI))/]) < PI / 2 by A5, XXREAL_1:4;
then ((PI / 2) + H1([\(a / (2 * PI))/])) - (PI / 2) < (PI / 2) - (PI / 2) by XREAL_1:9;
then [\(a / (2 * PI))/] < 0 ;
then A11: [\(a / (2 * PI))/] <= - 1 by INT_1:8;
- (PI / 2) < (PI / 2) + H1([\(a / (2 * PI))/]) by A5, A10, XXREAL_1:4;
then (- (PI / 2)) - (PI / 2) < ((PI / 2) + H1([\(a / (2 * PI))/])) - (PI / 2) by XREAL_1:9;
then ((- 1) * PI) / (2 * PI) < [\(a / (2 * PI))/] by A7, XREAL_1:74;
then (- 1) / 2 < [\(a / (2 * PI))/] by XCMPLX_1:91;
hence contradiction by A11, XXREAL_0:2; :: thesis: verum
end;
A12: now :: thesis: not x = - 1
assume x = - 1 ; :: thesis: contradiction
then A13: a = ((3 / 2) * PI) + H1([\(a / (2 * PI))/]) by A6, A8, Th23;
then - (PI / 2) < ((3 / 2) * PI) + H1([\(a / (2 * PI))/]) by A5, XXREAL_1:4;
then (- (PI / 2)) - ((3 / 2) * PI) < (((3 / 2) * PI) + H1([\(a / (2 * PI))/])) - ((3 / 2) * PI) by XREAL_1:9;
then (- (2 * PI)) / (2 * PI) < [\(a / (2 * PI))/] by A7, XREAL_1:74;
then - ((2 * PI) / (2 * PI)) < [\(a / (2 * PI))/] by XCMPLX_1:187;
then - 1 < [\(a / (2 * PI))/] by XCMPLX_1:60;
then A14: (- 1) + 1 <= [\(a / (2 * PI))/] by INT_1:7;
((3 / 2) * PI) + H1([\(a / (2 * PI))/]) < PI / 2 by A5, A13, XXREAL_1:4;
then (((3 / 2) * PI) + H1([\(a / (2 * PI))/])) - ((3 / 2) * PI) < (PI / 2) - ((3 / 2) * PI) by XREAL_1:9;
then [\(a / (2 * PI))/] < (- PI) / (2 * PI) by A7, XREAL_1:74;
hence contradiction by A14, XCMPLX_1:91; :: thesis: verum
end;
x <= 1 by A1, A2, A3, COMPTRIG:30, XXREAL_1:1;
then A15: x < 1 by A9, XXREAL_0:1;
- 1 <= x by A1, A2, A3, COMPTRIG:30, XXREAL_1:1;
then - 1 < x by A12, XXREAL_0:1;
hence x in ].(- 1),1.[ by A15, XXREAL_1:4; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in ].(- 1),1.[ or a in sin .: ].(- (PI / 2)),(PI / 2).[ )
assume A16: a in ].(- 1),1.[ ; :: thesis: a in sin .: ].(- (PI / 2)),(PI / 2).[
then reconsider a = a as Real ;
( - 1 < a & a < 1 ) by A16, XXREAL_1:4;
then a in rng (sin | [.(- (PI / 2)),(PI / 2).]) by COMPTRIG:30, XXREAL_1:1;
then consider x being object such that
A17: x in dom (sin | [.(- (PI / 2)),(PI / 2).]) and
A18: (sin | [.(- (PI / 2)),(PI / 2).]) . x = a by FUNCT_1:def 3;
reconsider x = x as Real by A17;
A19: sin . x = a by A17, A18, FUNCT_1:47;
dom (sin | [.(- (PI / 2)),(PI / 2).]) = [.(- (PI / 2)),(PI / 2).] by RELAT_1:62, SIN_COS:24;
then ( - (PI / 2) <= x & x <= PI / 2 ) by A17, XXREAL_1:1;
then ( ( - (PI / 2) < x & x < PI / 2 ) or - (PI / 2) = x or PI / 2 = x ) by XXREAL_0:1;
then x in ].(- (PI / 2)),(PI / 2).[ by A16, A19, Th7, SIN_COS:76, XXREAL_1:4;
hence a in sin .: ].(- (PI / 2)),(PI / 2).[ by A19, FUNCT_1:def 6, SIN_COS:24; :: thesis: verum