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