A1:
sin | [.(PI / 2),((3 / 2) * PI).] is one-to-one
;
let x1, y1 be object ; FUNCT_1:def 4 ( 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.[)
; ( 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.[)
; ( 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
; 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 )
;
x1 = y1A16:
[.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 )
;
x1 = y1then
(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;
verum end; suppose A23:
( 3
/ 4
<= y &
y < 1 )
;
x1 = y1then 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;
verum end; end; end; suppose A26:
( 1
/ 4
< x &
x <= 1
/ 2 )
;
x1 = y1then 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 A32:
( 1
/ 4
< y &
y <= 1
/ 2 )
;
x1 = y1then 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;
verum end; end; end; suppose A39:
( 1
/ 2
< x &
x <= 3
/ 4 )
;
x1 = y1then 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 A45:
( 1
/ 2
< y &
y <= 3
/ 4 )
;
x1 = y1then 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;
verum end; end; end; suppose A52:
( 3
/ 4
< x &
x < 1 )
;
x1 = y1then 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 A57:
( 1
/ 2
< y &
y <= 3
/ 4 )
;
x1 = y1then 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;
verum end; suppose A60:
( 3
/ 4
< y &
y < 1 )
;
x1 = y1then 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;
verum end; end; end; end;