A1: sin | [.(PI / 2),((3 / 2) * PI).] is one-to-one ;
let x1, y1 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in K112(()) or not y1 in K112(()) or not () . x1 = () . y1 or x1 = y1 )
set f = CircleMap | [.0,1.[;
A2: [.0,(PI / 2).] c= [.(- (PI / 2)),(PI / 2).] by XXREAL_1:34;
A3: dom () = [.0,1.[ by ;
assume A4: x1 in dom () ; :: thesis: ( not y1 in K112(()) or not () . x1 = () . y1 or x1 = y1 )
then reconsider x = x1 as Real ;
A5: () . x = CircleMap . x by
.= |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]| by Def11 ;
assume A6: y1 in dom () ; :: thesis: ( not () . x1 = () . y1 or x1 = y1 )
then reconsider y = y1 as Real ;
assume A7: (CircleMap | [.0,1.[) . x1 = () . y1 ; :: thesis: x1 = y1
A8: () . y = CircleMap . y by
.= |[(cos ((2 * PI) * y)),(sin ((2 * PI) * y))]| by Def11 ;
then A9: cos ((2 * PI) * x) = cos ((2 * PI) * y) by ;
A10: cos ((2 * PI) * y) = cos . ((2 * PI) * y) by SIN_COS:def 19;
A11: cos ((2 * PI) * x) = cos . ((2 * PI) * x) by SIN_COS:def 19;
A12: sin ((2 * PI) * x) = sin ((2 * PI) * y) by ;
A13: sin ((2 * PI) * y) = sin . ((2 * PI) * y) by SIN_COS:def 17;
A14: sin ((2 * PI) * x) = sin . ((2 * PI) * x) by SIN_COS:def 17;
per cases ( ( 0 <= x & x <= 1 / 4 ) or ( 1 / 4 < x & x <= 1 / 2 ) or ( 1 / 2 < x & x <= 3 / 4 ) or ( 3 / 4 < x & x < 1 ) ) by ;
suppose A15: ( 0 <= x & x <= 1 / 4 ) ; :: thesis: x1 = y1
A16: [.0,(PI / 2).] c= by ;
(2 * PI) * x <= (2 * PI) * (1 / 4) by ;
then A17: (2 * PI) * x in [.0,(((2 * PI) * 1) / 4).] by ;
per cases ( ( 0 <= y & y <= 1 / 4 ) or ( 1 / 4 < y & y < 3 / 4 ) or ( 3 / 4 <= y & y < 1 ) ) by ;
suppose A18: ( 0 <= y & y <= 1 / 4 ) ; :: thesis: x1 = y1
then (2 * PI) * y <= (2 * PI) * (1 / 4) by XREAL_1:64;
then A19: (2 * PI) * y in [.0,(((2 * PI) * 1) / 4).] by ;
set g = sin | [.0,(PI / 2).];
A20: dom (sin | [.0,(PI / 2).]) = [.0,(PI / 2).] by ;
(sin | [.0,(PI / 2).]) . ((2 * PI) * x) = sin . ((2 * PI) * x) by
.= sin . ((2 * PI) * y) by
.= (sin | [.0,(PI / 2).]) . ((2 * PI) * y) by ;
then (2 * PI) * x = (2 * PI) * y by ;
then x = ((2 * PI) * y) / (2 * PI) by XCMPLX_1:89;
hence x1 = y1 by XCMPLX_1:89; :: thesis: verum
end;
suppose A21: ( 1 / 4 < y & y < 3 / 4 ) ; :: thesis: x1 = y1
then A22: (2 * PI) * y < (2 * PI) * (3 / 4) by XREAL_1:68;
(2 * PI) * (1 / 4) < (2 * PI) * y by ;
then (2 * PI) * y in ].(PI / 2),((3 / 2) * PI).[ by ;
hence x1 = y1 by ; :: thesis: verum
end;
suppose A23: ( 3 / 4 <= y & y < 1 ) ; :: thesis: x1 = y1
then A24: (2 * PI) * y < (2 * PI) * 1 by XREAL_1:68;
A25: [.((3 / 2) * PI),(2 * PI).[ c= ].PI,(2 * PI).[ by ;
(2 * PI) * (3 / 4) <= (2 * PI) * y by ;
then (2 * PI) * y in [.((3 / 2) * PI),(2 * PI).[ by ;
hence x1 = y1 by ; :: thesis: verum
end;
end;
end;
suppose A26: ( 1 / 4 < x & x <= 1 / 2 ) ; :: thesis: x1 = y1
then A27: (2 * PI) * x <= (2 * PI) * (1 / 2) by XREAL_1:64;
(2 * PI) * (1 / 4) < (2 * PI) * x by ;
then A28: (2 * PI) * x in ].(PI / 2),((2 * PI) * (1 / 2)).] by ;
A29: ].(PI / 2),PI.] c= ].(PI / 2),((3 / 2) * PI).[ by ;
A30: ].(PI / 2),PI.] c= by XXREAL_1:36;
per cases ( ( 0 <= y & y <= 1 / 4 ) or ( 1 / 4 < y & y <= 1 / 2 ) or ( 1 / 2 < y & y < 1 ) ) by ;
suppose A31: ( 0 <= y & y <= 1 / 4 ) ; :: thesis: x1 = y1
then (2 * PI) * y <= (2 * PI) * (1 / 4) by XREAL_1:64;
then (2 * PI) * y in [.0,((2 * PI) * (1 / 4)).] by ;
hence x1 = y1 by ; :: thesis: verum
end;
suppose A32: ( 1 / 4 < y & y <= 1 / 2 ) ; :: thesis: x1 = y1
then A33: (2 * PI) * y <= (2 * PI) * (1 / 2) by XREAL_1:64;
(2 * PI) * (1 / 4) < (2 * PI) * y by ;
then A34: (2 * PI) * y in ].((2 * PI) * (1 / 4)),((2 * PI) * (1 / 2)).] by ;
set g = sin | ].(PI / 2),PI.];
A35: dom (sin | ].(PI / 2),PI.]) = ].(PI / 2),PI.] by ;
A36: sin | ].(PI / 2),PI.] is one-to-one by ;
(sin | ].(PI / 2),PI.]) . ((2 * PI) * x) = sin . ((2 * PI) * x) by
.= sin . ((2 * PI) * y) by
.= (sin | ].(PI / 2),PI.]) . ((2 * PI) * y) by ;
then (2 * PI) * x = (2 * PI) * y by A28, A34, A36, A35;
then x = ((2 * PI) * y) / (2 * PI) by XCMPLX_1:89;
hence x1 = y1 by XCMPLX_1:89; :: thesis: verum
end;
suppose A37: ( 1 / 2 < y & y < 1 ) ; :: thesis: x1 = y1
then A38: (2 * PI) * y < (2 * PI) * 1 by XREAL_1:68;
(2 * PI) * (1 / 2) < (2 * PI) * y by ;
then (2 * PI) * y in ].PI,(2 * PI).[ by ;
hence x1 = y1 by ; :: thesis: verum
end;
end;
end;
suppose A39: ( 1 / 2 < x & x <= 3 / 4 ) ; :: thesis: x1 = y1
then A40: (2 * PI) * x <= (2 * PI) * (3 / 4) by XREAL_1:64;
(2 * PI) * (1 / 2) < (2 * PI) * x by ;
then A41: (2 * PI) * x in ].PI,((2 * PI) * (3 / 4)).] by ;
A42: ].PI,((3 / 2) * PI).] c= [.(PI / 2),((3 / 2) * PI).] by ;
A43: ].PI,((3 / 2) * PI).] c= ].PI,(2 * PI).[ by ;
per cases ( ( 0 <= y & y <= 1 / 2 ) or ( 1 / 2 < y & y <= 3 / 4 ) or ( 3 / 4 < y & y < 1 ) ) by ;
suppose A44: ( 0 <= y & y <= 1 / 2 ) ; :: thesis: x1 = y1
then (2 * PI) * y <= (2 * PI) * (1 / 2) by XREAL_1:64;
then (2 * PI) * y in by ;
hence x1 = y1 by ; :: thesis: verum
end;
suppose A45: ( 1 / 2 < y & y <= 3 / 4 ) ; :: thesis: x1 = y1
then A46: (2 * PI) * y <= (2 * PI) * (3 / 4) by XREAL_1:64;
(2 * PI) * (1 / 2) < (2 * PI) * y by ;
then A47: (2 * PI) * y in ].PI,((2 * PI) * (3 / 4)).] by ;
set g = sin | ].PI,((3 / 2) * PI).];
A48: dom (sin | ].PI,((3 / 2) * PI).]) = ].PI,((3 / 2) * PI).] by ;
A49: sin | ].PI,((3 / 2) * PI).] is one-to-one by ;
(sin | ].PI,((3 / 2) * PI).]) . ((2 * PI) * x) = sin . ((2 * PI) * x) by
.= sin . ((2 * PI) * y) by
.= (sin | ].PI,((3 / 2) * PI).]) . ((2 * PI) * y) by ;
then (2 * PI) * x = (2 * PI) * y by A41, A47, A49, A48;
then x = ((2 * PI) * y) / (2 * PI) by XCMPLX_1:89;
hence x1 = y1 by XCMPLX_1:89; :: thesis: verum
end;
suppose A50: ( 3 / 4 < y & y < 1 ) ; :: thesis: x1 = y1
then A51: (2 * PI) * y < (2 * PI) * 1 by XREAL_1:68;
(2 * PI) * (3 / 4) < (2 * PI) * y by ;
then (2 * PI) * y in ].((3 / 2) * PI),(2 * PI).[ by ;
hence x1 = y1 by ; :: thesis: verum
end;
end;
end;
suppose A52: ( 3 / 4 < x & x < 1 ) ; :: thesis: x1 = y1
then A53: (2 * PI) * x < (2 * PI) * 1 by XREAL_1:68;
(2 * PI) * (3 / 4) < (2 * PI) * x by ;
then A54: (2 * PI) * x in ].((3 / 2) * PI),(2 * PI).[ by ;
A55: ].((3 / 2) * PI),(2 * PI).[ c= ].PI,(2 * PI).[ by ;
per cases ( ( 0 <= y & y <= 1 / 2 ) or ( 1 / 2 < y & y <= 3 / 4 ) or ( 3 / 4 < y & y < 1 ) ) by ;
suppose A56: ( 0 <= y & y <= 1 / 2 ) ; :: thesis: x1 = y1
then (2 * PI) * y <= (2 * PI) * (1 / 2) by XREAL_1:64;
then (2 * PI) * y in by ;
hence x1 = y1 by ; :: thesis: verum
end;
suppose A57: ( 1 / 2 < y & y <= 3 / 4 ) ; :: thesis: x1 = y1
then A58: (2 * PI) * y <= (2 * PI) * (3 / 4) by XREAL_1:64;
A59: ].PI,((3 / 2) * PI).] c= [.(PI / 2),((3 / 2) * PI).] by ;
(2 * PI) * (1 / 2) < (2 * PI) * y by ;
then (2 * PI) * y in ].PI,((3 / 2) * PI).] by ;
hence x1 = y1 by ; :: thesis: verum
end;
suppose A60: ( 3 / 4 < y & y < 1 ) ; :: thesis: x1 = y1
then A61: (2 * PI) * y < (2 * PI) * 1 by XREAL_1:68;
(2 * PI) * (3 / 4) < (2 * PI) * y by ;
then A62: (2 * PI) * y in ].((3 / 2) * PI),(2 * PI).[ by ;
set g = sin | ].((3 / 2) * PI),(2 * PI).[;
A63: dom (sin | ].((3 / 2) * PI),(2 * PI).[) = ].((3 / 2) * PI),(2 * PI).[ by ;
(sin | ].((3 / 2) * PI),(2 * PI).[) . ((2 * PI) * x) = sin . ((2 * PI) * x) by
.= sin . ((2 * PI) * y) by
.= (sin | ].((3 / 2) * PI),(2 * PI).[) . ((2 * PI) * y) by ;
then (2 * PI) * x = (2 * PI) * y by ;
then x = ((2 * PI) * y) / (2 * PI) by XCMPLX_1:89;
hence x1 = y1 by XCMPLX_1:89; :: thesis: verum
end;
end;
end;
end;