:: SIN_COS6 semantic presentation

begin


theorem Th1: :: SIN_COS6:1
for r, s being real number st 0 <= r & r < s holds
[\(r / s)/] = 0
proof
let r, s be real number ; ::_thesis: ( 0 <= r & r < s implies [\(r / s)/] = 0 )
assume A1: ( 0 <= r & r < s ) ; ::_thesis: [\(r / s)/] = 0
then  r / s < s / s by XREAL_1:74;
then  (r / s) - 1 < (s / s) - 1 by XREAL_1:9;
then  (r / s) - 1 < 1 - 1 by A1, XCMPLX_1:60;
hence  [\(r / s)/] = 0 by A1, INT_1:def_6; ::_thesis: verum
end;

theorem Th2: :: SIN_COS6:2
for f being Function
for X, Y being set st f | X is one-to-one & Y c= X holds
f | Y is one-to-one
proof
let f be Function; ::_thesis: for X, Y being set st f | X is one-to-one & Y c= X holds
f | Y is one-to-one
let X, Y be set ; ::_thesis: ( f | X is one-to-one & Y c= X implies f | Y is one-to-one )
assume that
A1: f | X is one-to-one and
A2: Y c= X ; ::_thesis: f | Y is one-to-one
let x, y be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x in dom (f | Y) or not y in dom (f | Y) or not (f | Y) . x = (f | Y) . y or x = y )
A3: dom (f | Y) = (dom f) /\ Y by RELAT_1:61;
assume A4: x in dom (f | Y) ; ::_thesis: ( not y in dom (f | Y) or not (f | Y) . x = (f | Y) . y or x = y )
then A5: x in Y by A3, XBOOLE_0:def_4;
 x in dom f by A3, A4, XBOOLE_0:def_4;
then  x in (dom f) /\ X by A2, A5, XBOOLE_0:def_4;
then A6: x in dom (f | X) by RELAT_1:61;
assume A7: y in dom (f | Y) ; ::_thesis: ( not (f | Y) . x = (f | Y) . y or x = y )
then A8: y in Y by A3, XBOOLE_0:def_4;
 y in dom f by A3, A7, XBOOLE_0:def_4;
then  y in (dom f) /\ X by A2, A8, XBOOLE_0:def_4;
then A9: y in dom (f | X) by RELAT_1:61;
assume A10: (f | Y) . x = (f | Y) . y ; ::_thesis: x = y
(f | X) . x = f . x by A2, A5, FUNCT_1:49
.= (f | Y) . x by A5, FUNCT_1:49
.= f . y by A8, A10, FUNCT_1:49
.= (f | X) . y by A2, A8, FUNCT_1:49 ;
hence  x = y by A1, A6, A9, FUNCT_1:def_4; ::_thesis: verum
end;

begin

theorem Th3: :: SIN_COS6:3
for r being real number holds - 1 <= sin r
proof
let r be real number ; ::_thesis: - 1 <= sin r
 sin . r in [.(- 1),1.] by COMPTRIG:27;
then  sin r in [.(- 1),1.] by SIN_COS:def_17;
hence  - 1 <= sin r by XXREAL_1:1; ::_thesis: verum
end;

theorem Th4: :: SIN_COS6:4
for r being real number holds sin r <= 1
proof
let r be real number ; ::_thesis: sin r <= 1
 sin . r in [.(- 1),1.] by COMPTRIG:27;
then  sin r in [.(- 1),1.] by SIN_COS:def_17;
hence  sin r <= 1 by XXREAL_1:1; ::_thesis: verum
end;

theorem Th5: :: SIN_COS6:5
for r being real number holds - 1 <= cos r
proof
let r be real number ; ::_thesis: - 1 <= cos r
 cos . r in [.(- 1),1.] by COMPTRIG:27;
then  cos r in [.(- 1),1.] by SIN_COS:def_19;
hence  - 1 <= cos r by XXREAL_1:1; ::_thesis: verum
end;

theorem Th6: :: SIN_COS6:6
for r being real number holds cos r <= 1
proof
let r be real number ; ::_thesis: cos r <= 1
 cos . r in [.(- 1),1.] by COMPTRIG:27;
then  cos r in [.(- 1),1.] by SIN_COS:def_19;
hence  cos r <= 1 by XXREAL_1:1; ::_thesis: verum
end;

deffunc H1( Integer) ->  Element of REAL = (2 * PI) * $1;

Lm1:  [.((- (PI / 2)) + H1( 0 )),((PI / 2) + H1( 0 )).] = [.(- (PI / 2)),(PI / 2).]
;

Lm2:  [.((PI / 2) + H1( 0 )),(((3 / 2) * PI) + H1( 0 )).] = [.(PI / 2),((3 / 2) * PI).]
;

Lm3:  [.H1( 0 ),(PI + H1( 0 )).] = [.0,PI.]
;

Lm4:  [.(PI + H1( 0 )),((2 * PI) + H1( 0 )).] = [.PI,(2 * PI).]
;

Lm5:  for r, s being real number st (r ^2) + (s ^2) = 1 holds
( - 1 <= r & r <= 1 )
proof
let r, s be real number ; ::_thesis: ( (r ^2) + (s ^2) = 1 implies ( - 1 <= r & r <= 1 ) )
 s ^2 >= 0 by XREAL_1:63;
then  - (s ^2) <= - 0 ;
then  (r ^2) - ((r ^2) + (s ^2)) <= 0 ;
hence  ( (r ^2) + (s ^2) = 1 implies ( - 1 <= r & r <= 1 ) ) by SQUARE_1:43; ::_thesis: verum
end;

registration
cluster PI  ->  positive ;
coherence
 PI is positive
proof
 PI in ].0,4.[ by SIN_COS:def_28;
hence  PI > 0 by XXREAL_1:4; :: according to XXREAL_0:def_6 ::_thesis: verum
end;
end;

Lm6:  PI / 2 < PI / 1
by XREAL_1:76;

Lm7:  1 * PI < (3 / 2) * PI
by XREAL_1:68;

Lm8:  0 + H1(1) < (PI / 2) + H1(1)
by XREAL_1:6;

Lm9:  (3 / 2) * PI < 2 * PI
by XREAL_1:68;

Lm10:  1 * PI < 2 * PI
by XREAL_1:68;

theorem Th7: :: SIN_COS6:7
( sin (- (PI / 2)) = - 1 & sin . (- (PI / 2)) = - 1 )
proof
sin . (- (PI / 2)) = sin . ((- (PI / 2)) + (2 * PI)) by SIN_COS:78
.= - 1 by SIN_COS:76 ;
hence  ( sin (- (PI / 2)) = - 1 & sin . (- (PI / 2)) = - 1 ) by SIN_COS:def_17; ::_thesis: verum
end;

theorem Th8: :: SIN_COS6:8
for r being real number
for i being integer number holds sin . r = sin . (r + ((2 * PI) * i))
proof
let r be real number ; ::_thesis: for i being integer number holds sin . r = sin . (r + ((2 * PI) * i))
let i be integer number ; ::_thesis: sin . r = sin . (r + ((2 * PI) * i))
thus sin . r = sin r by SIN_COS:def_17
.= sin (r + ((2 * PI) * i)) by COMPLEX2:8
.= sin . (r + ((2 * PI) * i)) by SIN_COS:def_17 ; ::_thesis: verum
end;

theorem Th9: :: SIN_COS6:9
( cos (- (PI / 2)) = 0 & cos . (- (PI / 2)) = 0 )
proof
cos . (- (PI / 2)) = cos . ((- (PI / 2)) + (2 * PI)) by SIN_COS:78
.= 0 by SIN_COS:76 ;
hence  ( cos (- (PI / 2)) = 0 & cos . (- (PI / 2)) = 0 ) by SIN_COS:def_19; ::_thesis: verum
end;

theorem Th10: :: SIN_COS6:10
for r being real number
for i being integer number holds cos . r = cos . (r + ((2 * PI) * i))
proof
let r be real number ; ::_thesis: for i being integer number holds cos . r = cos . (r + ((2 * PI) * i))
let i be integer number ; ::_thesis: cos . r = cos . (r + ((2 * PI) * i))
thus cos . r = cos r by SIN_COS:def_19
.= cos (r + ((2 * PI) * i)) by COMPLEX2:9
.= cos . (r + ((2 * PI) * i)) by SIN_COS:def_19 ; ::_thesis: verum
end;

theorem Th11: :: SIN_COS6:11
for r being real number
for i being integer number st (2 * PI) * i < r & r < PI + ((2 * PI) * i) holds
sin r > 0
proof
let r be real number ; ::_thesis: for i being integer number st (2 * PI) * i < r & r < PI + ((2 * PI) * i) holds
sin r > 0
let i be integer number ; ::_thesis: ( (2 * PI) * i < r & r < PI + ((2 * PI) * i) implies sin r > 0 )
assume  ( H1(i) < r & r < PI + H1(i) ) ; ::_thesis: sin r > 0
then  ( H1(i) - H1(i) < r - H1(i) & r - H1(i) < (PI + H1(i)) - H1(i) ) by XREAL_1:9;
then  r - H1(i) in ].0,PI.[ by XXREAL_1:4;
then  sin . (r + H1( - i)) > 0 by COMPTRIG:7;
then  sin . r > 0 by Th8;
hence  sin r > 0 by SIN_COS:def_17; ::_thesis: verum
end;

theorem Th12: :: SIN_COS6:12
for r being real number
for i being integer number st PI + ((2 * PI) * i) < r & r < (2 * PI) + ((2 * PI) * i) holds
sin r < 0
proof
let r be real number ; ::_thesis: for i being integer number st PI + ((2 * PI) * i) < r & r < (2 * PI) + ((2 * PI) * i) holds
sin r < 0
let i be integer number ; ::_thesis: ( PI + ((2 * PI) * i) < r & r < (2 * PI) + ((2 * PI) * i) implies sin r < 0 )
assume  ( PI + H1(i) < r & r < (2 * PI) + H1(i) ) ; ::_thesis: sin r < 0
then  ( (PI + H1(i)) - H1(i) < r - H1(i) & r - H1(i) < ((2 * PI) + H1(i)) - H1(i) ) by XREAL_1:9;
then  r - H1(i) in ].PI,(2 * PI).[ by XXREAL_1:4;
then  sin . (r + H1( - i)) < 0 by COMPTRIG:9;
then  sin . r < 0 by Th8;
hence  sin r < 0 by SIN_COS:def_17; ::_thesis: verum
end;

theorem Th13: :: SIN_COS6:13
for r being real number
for i being integer number st (- (PI / 2)) + ((2 * PI) * i) < r & r < (PI / 2) + ((2 * PI) * i) holds
cos r > 0
proof
let r be real number ; ::_thesis: for i being integer number st (- (PI / 2)) + ((2 * PI) * i) < r & r < (PI / 2) + ((2 * PI) * i) holds
cos r > 0
let i be integer number ; ::_thesis: ( (- (PI / 2)) + ((2 * PI) * i) < r & r < (PI / 2) + ((2 * PI) * i) implies cos r > 0 )
assume that
A1: (- (PI / 2)) + H1(i) < r and
A2: r < (PI / 2) + H1(i) ; ::_thesis: cos r > 0
 r + (PI / 2) < ((PI / 2) + H1(i)) + (PI / 2) by A2, XREAL_1:6;
then A3: r + (PI / 2) < PI + H1(i) ;
A4: sin (r + (PI / 2)) = cos r by SIN_COS:79;
 ((- (PI / 2)) + H1(i)) + (PI / 2) < r + (PI / 2) by A1, XREAL_1:6;
hence  cos r > 0 by A3, A4, Th11; ::_thesis: verum
end;

theorem Th14: :: SIN_COS6:14
for r being real number
for i being integer number st (PI / 2) + ((2 * PI) * i) < r & r < ((3 / 2) * PI) + ((2 * PI) * i) holds
cos r < 0
proof
let r be real number ; ::_thesis: for i being integer number st (PI / 2) + ((2 * PI) * i) < r & r < ((3 / 2) * PI) + ((2 * PI) * i) holds
cos r < 0
let i be integer number ; ::_thesis: ( (PI / 2) + ((2 * PI) * i) < r & r < ((3 / 2) * PI) + ((2 * PI) * i) implies cos r < 0 )
assume that
A1: (PI / 2) + H1(i) < r and
A2: r < ((3 / 2) * PI) + H1(i) ; ::_thesis: cos r < 0
 ((PI / 2) + H1(i)) + (PI / 2) < r + (PI / 2) by A1, XREAL_1:6;
then A3: PI + H1(i) < r + (PI / 2) ;
 r + (PI / 2) < (((3 / 2) * PI) + H1(i)) + (PI / 2) by A2, XREAL_1:6;
then A4: r + (PI / 2) < (2 * PI) + H1(i) ;
 sin (r + (PI / 2)) = cos r by SIN_COS:79;
hence  cos r < 0 by A3, A4, Th12; ::_thesis: verum
end;

theorem Th15: :: SIN_COS6:15
for r being real number
for i being integer number st ((3 / 2) * PI) + ((2 * PI) * i) < r & r < (2 * PI) + ((2 * PI) * i) holds
cos r > 0
proof
let r be real number ; ::_thesis: for i being integer number st ((3 / 2) * PI) + ((2 * PI) * i) < r & r < (2 * PI) + ((2 * PI) * i) holds
cos r > 0
let i be integer number ; ::_thesis: ( ((3 / 2) * PI) + ((2 * PI) * i) < r & r < (2 * PI) + ((2 * PI) * i) implies cos r > 0 )
assume that
A1: ((3 / 2) * PI) + H1(i) < r and
A2: r < (2 * PI) + H1(i) ; ::_thesis: cos r > 0
 (((3 / 2) * PI) + H1(i)) - PI < r - PI by A1, XREAL_1:9;
then A3: (PI / 2) + H1(i) < r - PI ;
 ( PI + H1(i) < ((3 / 2) * PI) + H1(i) & r - PI < ((2 * PI) + H1(i)) - PI ) by A2, COMPTRIG:5, XREAL_1:6, XREAL_1:9;
then A4: r - PI < ((3 / 2) * PI) + H1(i) by XXREAL_0:2;
cos (r - PI) = cos (- (PI - r))
.= cos (PI + (- r)) by SIN_COS:31
.= - (cos (- r)) by SIN_COS:79
.= - (cos r) by SIN_COS:31 ;
hence  cos r > 0 by A3, A4, Th14; ::_thesis: verum
end;

theorem :: SIN_COS6:16
for r being real number
for i being integer number st (2 * PI) * i <= r & r <= PI + ((2 * PI) * i) holds
sin r >= 0
proof
let r be real number ; ::_thesis: for i being integer number st (2 * PI) * i <= r & r <= PI + ((2 * PI) * i) holds
sin r >= 0
let i be integer number ; ::_thesis: ( (2 * PI) * i <= r & r <= PI + ((2 * PI) * i) implies sin r >= 0 )
assume A1: ( (2 * PI) * i <= r & r <= PI + ((2 * PI) * i) ) ; ::_thesis: sin r >= 0
percases ( ( (2 * PI) * i < r & r < PI + ((2 * PI) * i) ) or (2 * PI) * i = r or r = PI + ((2 * PI) * i) ) by A1, XXREAL_0:1;
suppose ( (2 * PI) * i < r & r < PI + ((2 * PI) * i) ) ; ::_thesis: sin r >= 0
hence  sin r >= 0 by Th11; ::_thesis: verum
end;
supposeA2: (2 * PI) * i = r ; ::_thesis: sin r >= 0
 sin (0 + ((2 * PI) * i)) = sin 0 by COMPLEX2:8;
hence  sin r >= 0 by A2, SIN_COS:31; ::_thesis: verum
end;
suppose r = PI + ((2 * PI) * i) ; ::_thesis: sin r >= 0
hence  sin r >= 0 by COMPLEX2:8, SIN_COS:77; ::_thesis: verum
end;
end;
end;

theorem :: SIN_COS6:17
for r being real number
for i being integer number st PI + ((2 * PI) * i) <= r & r <= (2 * PI) + ((2 * PI) * i) holds
sin r <= 0
proof
let r be real number ; ::_thesis: for i being integer number st PI + ((2 * PI) * i) <= r & r <= (2 * PI) + ((2 * PI) * i) holds
sin r <= 0
let i be integer number ; ::_thesis: ( PI + ((2 * PI) * i) <= r & r <= (2 * PI) + ((2 * PI) * i) implies sin r <= 0 )
assume  ( PI + ((2 * PI) * i) <= r & r <= (2 * PI) + ((2 * PI) * i) ) ; ::_thesis: sin r <= 0
then  ( ( PI + ((2 * PI) * i) < r & r < (2 * PI) + ((2 * PI) * i) ) or PI + ((2 * PI) * i) = r or r = (2 * PI) + ((2 * PI) * i) ) by XXREAL_0:1;
hence  sin r <= 0 by Th12, COMPLEX2:8, SIN_COS:77; ::_thesis: verum
end;

theorem :: SIN_COS6:18
for r being real number
for i being integer number st (- (PI / 2)) + ((2 * PI) * i) <= r & r <= (PI / 2) + ((2 * PI) * i) holds
cos r >= 0
proof
let r be real number ; ::_thesis: for i being integer number st (- (PI / 2)) + ((2 * PI) * i) <= r & r <= (PI / 2) + ((2 * PI) * i) holds
cos r >= 0
let i be integer number ; ::_thesis: ( (- (PI / 2)) + ((2 * PI) * i) <= r & r <= (PI / 2) + ((2 * PI) * i) implies cos r >= 0 )
assume  ( (- (PI / 2)) + ((2 * PI) * i) <= r & r <= (PI / 2) + ((2 * PI) * i) ) ; ::_thesis: cos r >= 0
then  ( ( (- (PI / 2)) + ((2 * PI) * i) < r & r < (PI / 2) + ((2 * PI) * i) ) or (- (PI / 2)) + ((2 * PI) * i) = r or r = (PI / 2) + ((2 * PI) * i) ) by XXREAL_0:1;
hence  cos r >= 0 by Th9, Th13, COMPLEX2:9, SIN_COS:77; ::_thesis: verum
end;

theorem :: SIN_COS6:19
for r being real number
for i being integer number st (PI / 2) + ((2 * PI) * i) <= r & r <= ((3 / 2) * PI) + ((2 * PI) * i) holds
cos r <= 0
proof
let r be real number ; ::_thesis: for i being integer number st (PI / 2) + ((2 * PI) * i) <= r & r <= ((3 / 2) * PI) + ((2 * PI) * i) holds
cos r <= 0
let i be integer number ; ::_thesis: ( (PI / 2) + ((2 * PI) * i) <= r & r <= ((3 / 2) * PI) + ((2 * PI) * i) implies cos r <= 0 )
assume  ( (PI / 2) + ((2 * PI) * i) <= r & r <= ((3 / 2) * PI) + ((2 * PI) * i) ) ; ::_thesis: cos r <= 0
then  ( ( (PI / 2) + ((2 * PI) * i) < r & r < ((3 / 2) * PI) + ((2 * PI) * i) ) or (PI / 2) + ((2 * PI) * i) = r or r = ((3 / 2) * PI) + ((2 * PI) * i) ) by XXREAL_0:1;
hence  cos r <= 0 by Th14, COMPLEX2:9, SIN_COS:77; ::_thesis: verum
end;

theorem :: SIN_COS6:20
for r being real number
for i being integer number st ((3 / 2) * PI) + ((2 * PI) * i) <= r & r <= (2 * PI) + ((2 * PI) * i) holds
cos r >= 0
proof
let r be real number ; ::_thesis: for i being integer number st ((3 / 2) * PI) + ((2 * PI) * i) <= r & r <= (2 * PI) + ((2 * PI) * i) holds
cos r >= 0
let i be integer number ; ::_thesis: ( ((3 / 2) * PI) + ((2 * PI) * i) <= r & r <= (2 * PI) + ((2 * PI) * i) implies cos r >= 0 )
assume A1: ( ((3 / 2) * PI) + ((2 * PI) * i) <= r & r <= (2 * PI) + ((2 * PI) * i) ) ; ::_thesis: cos r >= 0
percases ( ( ((3 / 2) * PI) + ((2 * PI) * i) < r & r < (2 * PI) + ((2 * PI) * i) ) or ((3 / 2) * PI) + ((2 * PI) * i) = r or r = (2 * PI) + ((2 * PI) * i) ) by A1, XXREAL_0:1;
suppose ( ((3 / 2) * PI) + ((2 * PI) * i) < r & r < (2 * PI) + ((2 * PI) * i) ) ; ::_thesis: cos r >= 0
hence  cos r >= 0 by Th15; ::_thesis: verum
end;
suppose ((3 / 2) * PI) + ((2 * PI) * i) = r ; ::_thesis: cos r >= 0
hence  cos r >= 0 by COMPLEX2:9, SIN_COS:77; ::_thesis: verum
end;
suppose r = (2 * PI) + ((2 * PI) * i) ; ::_thesis: cos r >= 0
hence  cos r >= 0 by COMPLEX2:9, SIN_COS:77; ::_thesis: verum
end;
end;
end;

theorem Th21: :: SIN_COS6:21
for r being real number
for i being integer number st (2 * PI) * i <= r & r < (2 * PI) + ((2 * PI) * i) & sin r = 0 & not r = (2 * PI) * i holds
r = PI + ((2 * PI) * i)
proof
let r be real number ; ::_thesis: for i being integer number st (2 * PI) * i <= r & r < (2 * PI) + ((2 * PI) * i) & sin r = 0 & not r = (2 * PI) * i holds
r = PI + ((2 * PI) * i)
let i be integer number ; ::_thesis: ( (2 * PI) * i <= r & r < (2 * PI) + ((2 * PI) * i) & sin r = 0 & not r = (2 * PI) * i implies r = PI + ((2 * PI) * i) )
assume A1: ( H1(i) <= r & r < (2 * PI) + H1(i) ) ; ::_thesis: ( not sin r = 0 or r = (2 * PI) * i or r = PI + ((2 * PI) * i) )
assume A2: sin r = 0 ; ::_thesis: ( r = (2 * PI) * i or r = PI + ((2 * PI) * i) )
then A3: ( r <= PI + H1(i) or (2 * PI) + H1(i) <= r ) by Th12;
 ( r <= H1(i) or r >= PI + H1(i) ) by A2, Th11;
hence  ( r = (2 * PI) * i or r = PI + ((2 * PI) * i) ) by A1, A3, XXREAL_0:1; ::_thesis: verum
end;

theorem Th22: :: SIN_COS6:22
for r being real number
for i being integer number st (2 * PI) * i <= r & r < (2 * PI) + ((2 * PI) * i) & cos r = 0 & not r = (PI / 2) + ((2 * PI) * i) holds
r = ((3 / 2) * PI) + ((2 * PI) * i)
proof
let r be real number ; ::_thesis: for i being integer number st (2 * PI) * i <= r & r < (2 * PI) + ((2 * PI) * i) & cos r = 0 & not r = (PI / 2) + ((2 * PI) * i) holds
r = ((3 / 2) * PI) + ((2 * PI) * i)
let i be integer number ; ::_thesis: ( (2 * PI) * i <= r & r < (2 * PI) + ((2 * PI) * i) & cos r = 0 & not r = (PI / 2) + ((2 * PI) * i) implies r = ((3 / 2) * PI) + ((2 * PI) * i) )
assume that
A1: H1(i) <= r and
A2: r < (2 * PI) + H1(i) ; ::_thesis: ( not cos r = 0 or r = (PI / 2) + ((2 * PI) * i) or r = ((3 / 2) * PI) + ((2 * PI) * i) )
A3: (- (PI / 2)) + H1(i) < 0 + H1(i) by XREAL_1:6;
assume A4: cos r = 0 ; ::_thesis: ( r = (PI / 2) + ((2 * PI) * i) or r = ((3 / 2) * PI) + ((2 * PI) * i) )
then A5: ( (PI / 2) + H1(i) >= r or r >= ((3 / 2) * PI) + H1(i) ) by Th14;
 ( (- (PI / 2)) + H1(i) >= r or r >= (PI / 2) + H1(i) ) by A4, Th13;
then  ( r = (PI / 2) + H1(i) or r = ((3 / 2) * PI) + H1(i) or r > ((3 / 2) * PI) + H1(i) ) by A1, A5, A3, XXREAL_0:1, XXREAL_0:2;
hence  ( r = (PI / 2) + ((2 * PI) * i) or r = ((3 / 2) * PI) + ((2 * PI) * i) ) by A2, A4, Th15; ::_thesis: verum
end;

theorem Th23: :: SIN_COS6:23
for r being real number st sin r = - 1 holds
r = ((3 / 2) * PI) + ((2 * PI) * [\(r / (2 * PI))/])
proof
let r be real number ; ::_thesis: ( sin r = - 1 implies r = ((3 / 2) * PI) + ((2 * PI) * [\(r / (2 * PI))/]) )
set i = [\(r / (2 * PI))/];
consider w being real number  such that
A1: w = ((2 * PI) * (- [\(r / (2 * PI))/])) + r and
A2: ( 0 <= w & w < 2 * PI ) by COMPLEX2:1;
assume A3: sin r = - 1 ; ::_thesis: r = ((3 / 2) * PI) + ((2 * PI) * [\(r / (2 * PI))/])
then  ((cos r) * (cos r)) + ((- 1) * (- 1)) = 1 by SIN_COS:29;
then A4: cos r = 0 ;
 ( 0 + H1([\(r / (2 * PI))/]) <= w + H1([\(r / (2 * PI))/]) & w + H1([\(r / (2 * PI))/]) < (2 * PI) + H1([\(r / (2 * PI))/]) ) by A2, XREAL_1:6;
then  ( r = (PI / 2) + H1([\(r / (2 * PI))/]) or r = ((3 / 2) * PI) + H1([\(r / (2 * PI))/]) ) by A1, A4, Th22;
hence  r = ((3 / 2) * PI) + ((2 * PI) * [\(r / (2 * PI))/]) by A3, COMPLEX2:8, SIN_COS:77; ::_thesis: verum
end;

theorem Th24: :: SIN_COS6:24
for r being real number st sin r = 1 holds
r = (PI / 2) + ((2 * PI) * [\(r / (2 * PI))/])
proof
let r be real number ; ::_thesis: ( sin r = 1 implies r = (PI / 2) + ((2 * PI) * [\(r / (2 * PI))/]) )
set i = [\(r / (2 * PI))/];
consider w being real number  such that
A1: w = ((2 * PI) * (- [\(r / (2 * PI))/])) + r and
A2: ( 0 <= w & w < 2 * PI ) by COMPLEX2:1;
assume A3: sin r = 1 ; ::_thesis: r = (PI / 2) + ((2 * PI) * [\(r / (2 * PI))/])
then  ((cos r) * (cos r)) + (1 * 1) = 1 by SIN_COS:29;
then A4: cos r = 0 ;
 ( 0 + H1([\(r / (2 * PI))/]) <= w + H1([\(r / (2 * PI))/]) & w + H1([\(r / (2 * PI))/]) < (2 * PI) + H1([\(r / (2 * PI))/]) ) by A2, XREAL_1:6;
then  ( r = (PI / 2) + H1([\(r / (2 * PI))/]) or r = ((3 / 2) * PI) + H1([\(r / (2 * PI))/]) ) by A1, A4, Th22;
hence  r = (PI / 2) + ((2 * PI) * [\(r / (2 * PI))/]) by A3, COMPLEX2:8, SIN_COS:77; ::_thesis: verum
end;

theorem Th25: :: SIN_COS6:25
for r being real number st cos r = - 1 holds
r = PI + ((2 * PI) * [\(r / (2 * PI))/])
proof
let r be real number ; ::_thesis: ( cos r = - 1 implies r = PI + ((2 * PI) * [\(r / (2 * PI))/]) )
set i = [\(r / (2 * PI))/];
consider w being real number  such that
A1: w = ((2 * PI) * (- [\(r / (2 * PI))/])) + r and
A2: ( 0 <= w & w < 2 * PI ) by COMPLEX2:1;
assume A3: cos r = - 1 ; ::_thesis: r = PI + ((2 * PI) * [\(r / (2 * PI))/])
then  ((sin r) * (sin r)) + ((- 1) * (- 1)) = 1 by SIN_COS:29;
then A4: sin r = 0 ;
 ( 0 + H1([\(r / (2 * PI))/]) <= w + H1([\(r / (2 * PI))/]) & w + H1([\(r / (2 * PI))/]) < (2 * PI) + H1([\(r / (2 * PI))/]) ) by A2, XREAL_1:6;
then  ( r = 0 + H1([\(r / (2 * PI))/]) or r = PI + H1([\(r / (2 * PI))/]) ) by A1, A4, Th21;
hence  r = PI + ((2 * PI) * [\(r / (2 * PI))/]) by A3, COMPLEX2:9, SIN_COS:31; ::_thesis: verum
end;

theorem Th26: :: SIN_COS6:26
for r being real number st cos r = 1 holds
r = (2 * PI) * [\(r / (2 * PI))/]
proof
let r be real number ; ::_thesis: ( cos r = 1 implies r = (2 * PI) * [\(r / (2 * PI))/] )
set i = [\(r / (2 * PI))/];
consider w being real number  such that
A1: w = ((2 * PI) * (- [\(r / (2 * PI))/])) + r and
A2: ( 0 <= w & w < 2 * PI ) by COMPLEX2:1;
assume A3: cos r = 1 ; ::_thesis: r = (2 * PI) * [\(r / (2 * PI))/]
then  ((sin r) * (sin r)) + (1 * 1) = 1 by SIN_COS:29;
then A4: sin r = 0 ;
 ( 0 + H1([\(r / (2 * PI))/]) <= w + H1([\(r / (2 * PI))/]) & w + H1([\(r / (2 * PI))/]) < (2 * PI) + H1([\(r / (2 * PI))/]) ) by A2, XREAL_1:6;
then  ( r = 0 + H1([\(r / (2 * PI))/]) or r = PI + H1([\(r / (2 * PI))/]) ) by A1, A4, Th21;
hence  r = (2 * PI) * [\(r / (2 * PI))/] by A3, COMPLEX2:9, SIN_COS:77; ::_thesis: verum
end;

theorem Th27: :: SIN_COS6:27
for r being real number st 0 <= r & r <= 2 * PI & sin r = - 1 holds
r = (3 / 2) * PI
proof
let r be real number ; ::_thesis: ( 0 <= r & r <= 2 * PI & sin r = - 1 implies r = (3 / 2) * PI )
assume that
A1: 0 <= r and
A2: r <= 2 * PI and
A3: sin r = - 1 ; ::_thesis: r = (3 / 2) * PI
A4: ( r = 2 * PI or r < 2 * PI ) by A2, XXREAL_0:1;
thus r = ((3 / 2) * PI) + ((2 * PI) * [\(r / (2 * PI))/]) by A3, Th23
.= ((3 / 2) * PI) + ((2 * PI) * 0) by A1, A3, A4, Th1, SIN_COS:77
.= (3 / 2) * PI ; ::_thesis: verum
end;

theorem Th28: :: SIN_COS6:28
for r being real number st 0 <= r & r <= 2 * PI & sin r = 1 holds
r = PI / 2
proof
let r be real number ; ::_thesis: ( 0 <= r & r <= 2 * PI & sin r = 1 implies r = PI / 2 )
assume that
A1: 0 <= r and
A2: r <= 2 * PI and
A3: sin r = 1 ; ::_thesis: r = PI / 2
A4: ( r = 2 * PI or r < 2 * PI ) by A2, XXREAL_0:1;
thus r = (PI / 2) + ((2 * PI) * [\(r / (2 * PI))/]) by A3, Th24
.= (PI / 2) + ((2 * PI) * 0) by A1, A3, A4, Th1, SIN_COS:77
.= PI / 2 ; ::_thesis: verum
end;

theorem Th29: :: SIN_COS6:29
for r being real number st 0 <= r & r <= 2 * PI & cos r = - 1 holds
r = PI
proof
let r be real number ; ::_thesis: ( 0 <= r & r <= 2 * PI & cos r = - 1 implies r = PI )
assume that
A1: 0 <= r and
A2: r <= 2 * PI and
A3: cos r = - 1 ; ::_thesis: r = PI
A4: ( r = 2 * PI or r < 2 * PI ) by A2, XXREAL_0:1;
thus r = PI + ((2 * PI) * [\(r / (2 * PI))/]) by A3, Th25
.= PI + ((2 * PI) * 0) by A1, A3, A4, Th1, SIN_COS:77
.= PI ; ::_thesis: verum
end;

theorem Th30: :: SIN_COS6:30
for r being real number st 0 <= r & r < PI / 2 holds
sin r < 1
proof
let r be real number ; ::_thesis: ( 0 <= r & r < PI / 2 implies sin r < 1 )
assume that
A1: 0 <= r and
A2: r < PI / 2 and
A3: sin r >= 1 ; ::_thesis: contradiction
A4: sin r <= 1 by Th4;
 (1 / 2) * PI <= 2 * PI by XREAL_1:64;
then  r < 2 * PI by A2, XXREAL_0:2;
hence  contradiction by A1, A2, A3, A4, Th28, XXREAL_0:1; ::_thesis: verum
end;

theorem Th31: :: SIN_COS6:31
for r being real number st 0 <= r & r < (3 / 2) * PI holds
sin r > - 1
proof
let r be real number ; ::_thesis: ( 0 <= r & r < (3 / 2) * PI implies sin r > - 1 )
assume that
A1: 0 <= r and
A2: r < (3 / 2) * PI and
A3: sin r <= - 1 ; ::_thesis: contradiction
A4: sin r >= - 1 by Th3;
 r <= 2 * PI by A2, Lm9, XXREAL_0:2;
hence  contradiction by A1, A2, A3, A4, Th27, XXREAL_0:1; ::_thesis: verum
end;

theorem Th32: :: SIN_COS6:32
for r being real number st (3 / 2) * PI < r & r <= 2 * PI holds
sin r > - 1
proof
let r be real number ; ::_thesis: ( (3 / 2) * PI < r & r <= 2 * PI implies sin r > - 1 )
assume A1: ( (3 / 2) * PI < r & r <= 2 * PI & sin r <= - 1 ) ; ::_thesis: contradiction
 sin r >= - 1 by Th3;
hence  contradiction by A1, Th27, XXREAL_0:1; ::_thesis: verum
end;

theorem Th33: :: SIN_COS6:33
for r being real number st PI / 2 < r & r <= 2 * PI holds
sin r < 1
proof
let r be real number ; ::_thesis: ( PI / 2 < r & r <= 2 * PI implies sin r < 1 )
assume A1: ( PI / 2 < r & r <= 2 * PI & sin r >= 1 ) ; ::_thesis: contradiction
 sin r <= 1 by Th4;
hence  contradiction by A1, Th28, XXREAL_0:1; ::_thesis: verum
end;

theorem Th34: :: SIN_COS6:34
for r being real number st 0 < r & r < 2 * PI holds
cos r < 1
proof
let r be real number ; ::_thesis: ( 0 < r & r < 2 * PI implies cos r < 1 )
assume  ( 0 < r & r < 2 * PI ) ; ::_thesis: cos r < 1
then A1: cos r <> 1 by COMPTRIG:61;
 cos r <= 1 by Th6;
hence  cos r < 1 by A1, XXREAL_0:1; ::_thesis: verum
end;

theorem Th35: :: SIN_COS6:35
for r being real number st 0 <= r & r < PI holds
cos r > - 1
proof
let r be real number ; ::_thesis: ( 0 <= r & r < PI implies cos r > - 1 )
assume that
A1: 0 <= r and
A2: r < PI ; ::_thesis: cos r > - 1
A3: cos r >= - 1 by Th5;
 r <= 2 * PI by A2, Lm10, XXREAL_0:2;
hence  cos r > - 1 by A1, A2, A3, Th29, XXREAL_0:1; ::_thesis: verum
end;

theorem Th36: :: SIN_COS6:36
for r being real number st PI < r & r <= 2 * PI holds
cos r > - 1
proof
let r be real number ; ::_thesis: ( PI < r & r <= 2 * PI implies cos r > - 1 )
assume A1: ( PI < r & r <= 2 * PI ) ; ::_thesis: cos r > - 1
 cos r >= - 1 by Th5;
hence  cos r > - 1 by A1, Th29, XXREAL_0:1; ::_thesis: verum
end;

theorem :: SIN_COS6:37
for r being real number
for i being integer number st (2 * PI) * i <= r & r < (PI / 2) + ((2 * PI) * i) holds
sin r < 1
proof
let r be real number ; ::_thesis: for i being integer number st (2 * PI) * i <= r & r < (PI / 2) + ((2 * PI) * i) holds
sin r < 1
let i be integer number ; ::_thesis: ( (2 * PI) * i <= r & r < (PI / 2) + ((2 * PI) * i) implies sin r < 1 )
assume that
A1: ( H1(i) <= r & r < (PI / 2) + H1(i) ) and
A2: sin r >= 1 ; ::_thesis: contradiction
A3: ( H1(i) - H1(i) <= r - H1(i) & r - H1(i) < ((PI / 2) + H1(i)) - H1(i) ) by A1, XREAL_1:9;
A4: sin r <= 1 by Th4;
sin (r - H1(i)) = sin (r + H1( - i))
.= sin r by COMPLEX2:8
.= 1 by A2, A4, XXREAL_0:1 ;
hence  contradiction by A3, Th30; ::_thesis: verum
end;

theorem :: SIN_COS6:38
for r being real number
for i being integer number st (2 * PI) * i <= r & r < ((3 / 2) * PI) + ((2 * PI) * i) holds
sin r > - 1
proof
let r be real number ; ::_thesis: for i being integer number st (2 * PI) * i <= r & r < ((3 / 2) * PI) + ((2 * PI) * i) holds
sin r > - 1
let i be integer number ; ::_thesis: ( (2 * PI) * i <= r & r < ((3 / 2) * PI) + ((2 * PI) * i) implies sin r > - 1 )
assume that
A1: ( H1(i) <= r & r < ((3 / 2) * PI) + H1(i) ) and
A2: sin r <= - 1 ; ::_thesis: contradiction
A3: ( H1(i) - H1(i) <= r - H1(i) & r - H1(i) < (((3 / 2) * PI) + H1(i)) - H1(i) ) by A1, XREAL_1:9;
A4: sin r >= - 1 by Th3;
sin (r - H1(i)) = sin (r + H1( - i))
.= sin r by COMPLEX2:8
.= - 1 by A2, A4, XXREAL_0:1 ;
hence  contradiction by A3, Th31; ::_thesis: verum
end;

theorem :: SIN_COS6:39
for r being real number
for i being integer number st ((3 / 2) * PI) + ((2 * PI) * i) < r & r <= (2 * PI) + ((2 * PI) * i) holds
sin r > - 1
proof
let r be real number ; ::_thesis: for i being integer number st ((3 / 2) * PI) + ((2 * PI) * i) < r & r <= (2 * PI) + ((2 * PI) * i) holds
sin r > - 1
let i be integer number ; ::_thesis: ( ((3 / 2) * PI) + ((2 * PI) * i) < r & r <= (2 * PI) + ((2 * PI) * i) implies sin r > - 1 )
assume that
A1: ( ((3 / 2) * PI) + H1(i) < r & r <= (2 * PI) + H1(i) ) and
A2: sin r <= - 1 ; ::_thesis: contradiction
A3: ( (((3 / 2) * PI) + H1(i)) - H1(i) < r - H1(i) & r - H1(i) <= ((2 * PI) + H1(i)) - H1(i) ) by A1, XREAL_1:9;
A4: sin r >= - 1 by Th3;
sin (r - H1(i)) = sin (r + H1( - i))
.= sin r by COMPLEX2:8
.= - 1 by A2, A4, XXREAL_0:1 ;
hence  contradiction by A3, Th32; ::_thesis: verum
end;

theorem :: SIN_COS6:40
for r being real number
for i being integer number st (PI / 2) + ((2 * PI) * i) < r & r <= (2 * PI) + ((2 * PI) * i) holds
sin r < 1
proof
let r be real number ; ::_thesis: for i being integer number st (PI / 2) + ((2 * PI) * i) < r & r <= (2 * PI) + ((2 * PI) * i) holds
sin r < 1
let i be integer number ; ::_thesis: ( (PI / 2) + ((2 * PI) * i) < r & r <= (2 * PI) + ((2 * PI) * i) implies sin r < 1 )
assume that
A1: ( (PI / 2) + H1(i) < r & r <= (2 * PI) + H1(i) ) and
A2: sin r >= 1 ; ::_thesis: contradiction
A3: ( ((PI / 2) + H1(i)) - H1(i) < r - H1(i) & r - H1(i) <= ((2 * PI) + H1(i)) - H1(i) ) by A1, XREAL_1:9;
A4: sin r <= 1 by Th4;
sin (r - H1(i)) = sin (r + H1( - i))
.= sin r by COMPLEX2:8
.= 1 by A2, A4, XXREAL_0:1 ;
hence  contradiction by A3, Th33; ::_thesis: verum
end;

theorem :: SIN_COS6:41
for r being real number
for i being integer number st (2 * PI) * i < r & r < (2 * PI) + ((2 * PI) * i) holds
cos r < 1
proof
let r be real number ; ::_thesis: for i being integer number st (2 * PI) * i < r & r < (2 * PI) + ((2 * PI) * i) holds
cos r < 1
let i be integer number ; ::_thesis: ( (2 * PI) * i < r & r < (2 * PI) + ((2 * PI) * i) implies cos r < 1 )
assume that
A1: ( H1(i) < r & r < (2 * PI) + H1(i) ) and
A2: cos r >= 1 ; ::_thesis: contradiction
A3: ( H1(i) - H1(i) < r - H1(i) & r - H1(i) < ((2 * PI) + H1(i)) - H1(i) ) by A1, XREAL_1:9;
A4: cos r <= 1 by Th6;
cos (r - H1(i)) = cos (r + H1( - i))
.= cos r by COMPLEX2:9
.= 1 by A2, A4, XXREAL_0:1 ;
hence  contradiction by A3, Th34; ::_thesis: verum
end;

theorem :: SIN_COS6:42
for r being real number
for i being integer number st (2 * PI) * i <= r & r < PI + ((2 * PI) * i) holds
cos r > - 1
proof
let r be real number ; ::_thesis: for i being integer number st (2 * PI) * i <= r & r < PI + ((2 * PI) * i) holds
cos r > - 1
let i be integer number ; ::_thesis: ( (2 * PI) * i <= r & r < PI + ((2 * PI) * i) implies cos r > - 1 )
assume that
A1: ( H1(i) <= r & r < PI + H1(i) ) and
A2: cos r <= - 1 ; ::_thesis: contradiction
A3: ( H1(i) - H1(i) <= r - H1(i) & r - H1(i) < (PI + H1(i)) - H1(i) ) by A1, XREAL_1:9;
A4: cos r >= - 1 by Th5;
cos (r - H1(i)) = cos (r + H1( - i))
.= cos r by COMPLEX2:9
.= - 1 by A2, A4, XXREAL_0:1 ;
hence  contradiction by A3, Th35; ::_thesis: verum
end;

theorem :: SIN_COS6:43
for r being real number
for i being integer number st PI + ((2 * PI) * i) < r & r <= (2 * PI) + ((2 * PI) * i) holds
cos r > - 1
proof
let r be real number ; ::_thesis: for i being integer number st PI + ((2 * PI) * i) < r & r <= (2 * PI) + ((2 * PI) * i) holds
cos r > - 1
let i be integer number ; ::_thesis: ( PI + ((2 * PI) * i) < r & r <= (2 * PI) + ((2 * PI) * i) implies cos r > - 1 )
assume that
A1: ( PI + H1(i) < r & r <= (2 * PI) + H1(i) ) and
A2: cos r <= - 1 ; ::_thesis: contradiction
A3: ( (PI + H1(i)) - H1(i) < r - H1(i) & r - H1(i) <= ((2 * PI) + H1(i)) - H1(i) ) by A1, XREAL_1:9;
A4: cos r >= - 1 by Th5;
cos (r - H1(i)) = cos (r + H1( - i))
.= cos r by COMPLEX2:9
.= - 1 by A2, A4, XXREAL_0:1 ;
hence  contradiction by A3, Th36; ::_thesis: verum
end;

theorem :: SIN_COS6:44
for r being real number st cos ((2 * PI) * r) = 1 holds
r in INT
proof
let r be real number ; ::_thesis: ( cos ((2 * PI) * r) = 1 implies r in INT )
reconsider d = 2 as real positive number ;
assume A1: cos ((2 * PI) * r) = 1 ; ::_thesis: r in INT
assume  not r in INT ; ::_thesis: contradiction
then  not r is integer by INT_1:def_2;
then reconsider t = frac r as real positive number by INT_1:46;
set s = [\r/];
A2: ( r = [\r/] + t & (d * PI) * t < (d * PI) * 1 ) by INT_1:42, INT_1:43, XREAL_1:68;
cos ((2 * PI) * ([\r/] + t)) = cos (((2 * PI) * [\r/]) + ((2 * PI) * t))
.= cos ((2 * PI) * t) by COMPLEX2:9 ;
hence  contradiction by A1, A2, Th34; ::_thesis: verum
end;

theorem Th45: :: SIN_COS6:45
sin .: [.(- (PI / 2)),(PI / 2).] = [.(- 1),1.] by COMPTRIG:30, RELAT_1:115;

theorem Th46: :: SIN_COS6:46
sin .: ].(- (PI / 2)),(PI / 2).[ = ].(- 1),1.[
proof
 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 set ; :: 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 set  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 set ; :: 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 set  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
end;

theorem :: SIN_COS6:47
sin .: [.(PI / 2),((3 / 2) * PI).] = [.(- 1),1.] by COMPTRIG:31, RELAT_1:115;

theorem :: SIN_COS6:48
sin .: ].(PI / 2),((3 / 2) * PI).[ = ].(- 1),1.[
proof
 sin | ].(PI / 2),((3 / 2) * PI).[ c= sin | [.(PI / 2),((3 / 2) * PI).] by RELAT_1:75, XXREAL_1:25;
then A1: rng (sin | ].(PI / 2),((3 / 2) * PI).[) c= rng (sin | [.(PI / 2),((3 / 2) * PI).]) by RELAT_1:11;
A2: rng (sin | ].(PI / 2),((3 / 2) * PI).[) = sin .: ].(PI / 2),((3 / 2) * PI).[ by RELAT_1:115;
thus  sin .: ].(PI / 2),((3 / 2) * PI).[ c= ].(- 1),1.[ :: according to XBOOLE_0:def_10 ::_thesis: ].(- 1),1.[ c= sin .: ].(PI / 2),((3 / 2) * PI).[
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in sin .: ].(PI / 2),((3 / 2) * PI).[ or x in ].(- 1),1.[ )
assume A3: x in sin .: ].(PI / 2),((3 / 2) * PI).[ ; ::_thesis: x in ].(- 1),1.[
then consider a being set  such that
A4: a in dom sin and
A5: a in ].(PI / 2),((3 / 2) * PI).[ 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 < (PI / 2) + H1([\(a / (2 * PI))/]) by A5, XXREAL_1:4;
then  (PI / 2) - (PI / 2) < ((PI / 2) + H1([\(a / (2 * PI))/])) - (PI / 2) by XREAL_1:9;
then  0 < [\(a / (2 * PI))/] ;
then A11: 0 + 1 <= [\(a / (2 * PI))/] by INT_1:7;
 (PI / 2) + H1([\(a / (2 * PI))/]) < (3 / 2) * PI by A5, A10, XXREAL_1:4;
then  ((PI / 2) + H1([\(a / (2 * PI))/])) - (PI / 2) < ((3 / 2) * PI) - (PI / 2) by XREAL_1:9;
then  [\(a / (2 * PI))/] < (1 * PI) / (2 * PI) by A7, XREAL_1:74;
then  [\(a / (2 * PI))/] < 1 / 2 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  ((3 / 2) * PI) + H1([\(a / (2 * PI))/]) < (3 / 2) * PI by A5, XXREAL_1:4;
then  (((3 / 2) * PI) + H1([\(a / (2 * PI))/])) - ((3 / 2) * PI) < ((3 / 2) * PI) - ((3 / 2) * PI) by XREAL_1:9;
then  [\(a / (2 * PI))/] < 0 ;
then A14: [\(a / (2 * PI))/] <= - 1 by INT_1:8;
 PI / 2 < ((3 / 2) * PI) + H1([\(a / (2 * PI))/]) by A5, A13, XXREAL_1:4;
then  (PI / 2) - ((3 / 2) * PI) < (((3 / 2) * PI) + H1([\(a / (2 * PI))/])) - ((3 / 2) * PI) 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 A14, XXREAL_0:2; ::_thesis: verum
end;
 x <= 1 by A1, A2, A3, COMPTRIG:31, XXREAL_1:1;
then A15: x < 1 by A9, XXREAL_0:1;
 - 1 <= x by A1, A2, A3, COMPTRIG:31, 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not a in ].(- 1),1.[ or a in sin .: ].(PI / 2),((3 / 2) * PI).[ )
assume A16: a in ].(- 1),1.[ ; ::_thesis: a in sin .: ].(PI / 2),((3 / 2) * PI).[
then reconsider a = a as Real ;
 ( - 1 < a & a < 1 ) by A16, XXREAL_1:4;
then  a in rng (sin | [.(PI / 2),((3 / 2) * PI).]) by COMPTRIG:31, XXREAL_1:1;
then consider x being set  such that
A17: x in dom (sin | [.(PI / 2),((3 / 2) * PI).]) and
A18: (sin | [.(PI / 2),((3 / 2) * PI).]) . 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),((3 / 2) * PI).]) = [.(PI / 2),((3 / 2) * PI).] by RELAT_1:62, SIN_COS:24;
then  ( PI / 2 <= x & x <= (3 / 2) * PI ) by A17, XXREAL_1:1;
then  ( ( PI / 2 < x & x < (3 / 2) * PI ) or PI / 2 = x or (3 / 2) * PI = x ) by XXREAL_0:1;
then  x in ].(PI / 2),((3 / 2) * PI).[ by A16, A19, SIN_COS:76, XXREAL_1:4;
hence  a in sin .: ].(PI / 2),((3 / 2) * PI).[ by A19, FUNCT_1:def_6, SIN_COS:24; ::_thesis: verum
end;

theorem Th49: :: SIN_COS6:49
cos .: [.0,PI.] = [.(- 1),1.] by COMPTRIG:32, RELAT_1:115;

theorem Th50: :: SIN_COS6:50
cos .: ].0,PI.[ = ].(- 1),1.[
proof
 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.[ :: according to XBOOLE_0:def_10 ::_thesis: ].(- 1),1.[ c= cos .: ].0,PI.[
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in cos .: ].0,PI.[ or x in ].(- 1),1.[ )
assume A3: x in cos .: ].0,PI.[ ; ::_thesis: x in ].(- 1),1.[
then consider a being set  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;
A9: now__::_thesis:_not_x_=_1
assume  x = 1 ; ::_thesis: contradiction
then A10: a = H1([\(a / (2 * PI))/]) by A6, A8, Th26;
then  H1([\(a / (2 * PI))/]) < PI by A5, XXREAL_1:4;
then  [\(a / (2 * PI))/] < (1 * PI) / (2 * PI) by A7, XREAL_1:74;
then A11: [\(a / (2 * PI))/] < 1 / 2 by XCMPLX_1:91;
 0 < [\(a / (2 * PI))/] by A5, A10, XXREAL_1:4;
then  0 + 1 <= [\(a / (2 * PI))/] by INT_1:7;
hence  contradiction by A11, XXREAL_0:2; ::_thesis: verum
end;
A12: now__::_thesis:_not_x_=_-_1
assume  x = - 1 ; ::_thesis: contradiction
then A13: a = PI + H1([\(a / (2 * PI))/]) by A6, A8, Th25;
then  0 < PI + H1([\(a / (2 * PI))/]) by A5, XXREAL_1:4;
then  0 - PI < (PI + H1([\(a / (2 * PI))/])) - PI by XREAL_1:9;
then  (- PI) / (2 * PI) < H1([\(a / (2 * PI))/]) / (2 * PI) by XREAL_1:74;
then  - ((1 * PI) / (2 * PI)) < [\(a / (2 * PI))/] by A7, XCMPLX_1:187;
then A14: - (1 / 2) < [\(a / (2 * PI))/] by XCMPLX_1:91;
 PI + H1([\(a / (2 * PI))/]) < PI by A5, A13, XXREAL_1:4;
then  (PI + H1([\(a / (2 * PI))/])) - PI < PI - PI by XREAL_1:9;
then  [\(a / (2 * PI))/] < 0 ;
then  [\(a / (2 * PI))/] <= - 1 by INT_1:8;
hence  contradiction by A14, XXREAL_0:2; ::_thesis: verum
end;
 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; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in ].(- 1),1.[ or a in cos .: ].0,PI.[ )
assume A16: a in ].(- 1),1.[ ; ::_thesis: 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 set  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; ::_thesis: verum
end;

theorem :: SIN_COS6:51
cos .: [.PI,(2 * PI).] = [.(- 1),1.] by COMPTRIG:33, RELAT_1:115;

theorem :: SIN_COS6:52
cos .: ].PI,(2 * PI).[ = ].(- 1),1.[
proof
 cos | ].PI,(2 * PI).[ c= cos | [.PI,(2 * PI).] by RELAT_1:75, XXREAL_1:25;
then A1: rng (cos | ].PI,(2 * PI).[) c= rng (cos | [.PI,(2 * PI).]) by RELAT_1:11;
A2: rng (cos | ].PI,(2 * PI).[) = cos .: ].PI,(2 * PI).[ by RELAT_1:115;
thus  cos .: ].PI,(2 * PI).[ c= ].(- 1),1.[ :: according to XBOOLE_0:def_10 ::_thesis: ].(- 1),1.[ c= cos .: ].PI,(2 * PI).[
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in cos .: ].PI,(2 * PI).[ or x in ].(- 1),1.[ )
assume A3: x in cos .: ].PI,(2 * PI).[ ; ::_thesis: x in ].(- 1),1.[
then consider a being set  such that
A4: a in dom cos and
A5: a in ].PI,(2 * 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;
A9: now__::_thesis:_not_x_=_1
assume  x = 1 ; ::_thesis: contradiction
then A10: a = H1([\(a / (2 * PI))/]) by A6, A8, Th26;
then  H1([\(a / (2 * PI))/]) < 2 * PI by A5, XXREAL_1:4;
then  [\(a / (2 * PI))/] < (2 * PI) / (2 * PI) by A7, XREAL_1:74;
then A11: [\(a / (2 * PI))/] < 1 + 0 by XCMPLX_1:60;
 PI < H1([\(a / (2 * PI))/]) by A5, A10, XXREAL_1:4;
hence  contradiction by A7, A11, INT_1:7; ::_thesis: verum
end;
A12: now__::_thesis:_not_x_=_-_1
assume  x = - 1 ; ::_thesis: contradiction
then A13: a = PI + H1([\(a / (2 * PI))/]) by A6, A8, Th25;
then  PI < PI + H1([\(a / (2 * PI))/]) by A5, XXREAL_1:4;
then  PI - PI < (PI + H1([\(a / (2 * PI))/])) - PI by XREAL_1:9;
then  0 / (2 * PI) < [\(a / (2 * PI))/] ;
then A14: 0 + 1 <= [\(a / (2 * PI))/] by INT_1:7;
 PI + H1([\(a / (2 * PI))/]) < 2 * PI by A5, A13, XXREAL_1:4;
then  (PI + H1([\(a / (2 * PI))/])) - PI < (2 * PI) - PI by XREAL_1:9;
then  [\(a / (2 * PI))/] < (1 * PI) / (2 * PI) by A7, XREAL_1:74;
then  [\(a / (2 * PI))/] <= 1 / 2 by XCMPLX_1:91;
hence  contradiction by A14, XXREAL_0:2; ::_thesis: verum
end;
 x <= 1 by A1, A2, A3, COMPTRIG:33, XXREAL_1:1;
then A15: x < 1 by A9, XXREAL_0:1;
 - 1 <= x by A1, A2, A3, COMPTRIG:33, 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not a in ].(- 1),1.[ or a in cos .: ].PI,(2 * PI).[ )
assume A16: a in ].(- 1),1.[ ; ::_thesis: a in cos .: ].PI,(2 * PI).[
then reconsider a = a as Real ;
 ( - 1 < a & a < 1 ) by A16, XXREAL_1:4;
then  a in rng (cos | [.PI,(2 * PI).]) by COMPTRIG:33, XXREAL_1:1;
then consider x being set  such that
A17: x in dom (cos | [.PI,(2 * PI).]) and
A18: (cos | [.PI,(2 * 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;
 dom (cos | [.PI,(2 * PI).]) = [.PI,(2 * PI).] by RELAT_1:62, SIN_COS:24;
then  ( PI <= x & x <= 2 * PI ) by A17, XXREAL_1:1;
then  ( ( PI < x & x < 2 * PI ) or PI = x or 2 * PI = x ) by XXREAL_0:1;
then  x in ].PI,(2 * PI).[ by A16, A19, SIN_COS:76, XXREAL_1:4;
hence  a in cos .: ].PI,(2 * PI).[ by A19, FUNCT_1:def_6, SIN_COS:24; ::_thesis: verum
end;

Lm11: now__::_thesis:_for_i_being_integer_number_
for_r,_p1,_p2_being_real_number_st_r_in_[.(p1_+_H1(i)),(p2_+_H1(i)).]_holds_
r_+_(2_*_PI)_in_[.(p1_+_H1(i_+_1)),(p2_+_H1(i_+_1)).]
let i be integer number ; ::_thesis: for r, p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] holds
r + (2 * PI) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).]
let r be real number ; ::_thesis: for p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] holds
r + (2 * PI) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).]
let p1, p2 be real number ; ::_thesis: ( r in [.(p1 + H1(i)),(p2 + H1(i)).] implies r + (2 * PI) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).] )
assume A1: r in [.(p1 + H1(i)),(p2 + H1(i)).] ; ::_thesis: r + (2 * PI) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).]
then  r <= p2 + H1(i) by XXREAL_1:1;
then A2: r + (2 * PI) <= (p2 + H1(i)) + (2 * PI) by XREAL_1:6;
 p1 + H1(i) <= r by A1, XXREAL_1:1;
then  (p1 + H1(i)) + (2 * PI) <= r + (2 * PI) by XREAL_1:6;
hence  r + (2 * PI) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).] by A2, XXREAL_1:1; ::_thesis: verum
end;

Lm12: now__::_thesis:_for_i_being_integer_number_
for_r,_p1,_p2_being_real_number_st_r_in_[.(p1_+_H1(i)),(p2_+_H1(i)).]_/\_REAL_holds_
r_+_(2_*_PI)_in_[.(p1_+_H1(i_+_1)),(p2_+_H1(i_+_1)).]_/\_REAL
let i be integer number ; ::_thesis: for r, p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] /\ REAL holds
r + (2 * PI) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).] /\ REAL
let r be real number ; ::_thesis: for p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] /\ REAL holds
r + (2 * PI) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).] /\ REAL
let p1, p2 be real number ; ::_thesis: ( r in [.(p1 + H1(i)),(p2 + H1(i)).] /\ REAL implies r + (2 * PI) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).] /\ REAL )
assume  r in [.(p1 + H1(i)),(p2 + H1(i)).] /\ REAL ; ::_thesis: r + (2 * PI) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).] /\ REAL
then  r in [.(p1 + H1(i)),(p2 + H1(i)).] by XBOOLE_0:def_4;
then  r + (2 * PI) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).] by Lm11;
hence  r + (2 * PI) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).] /\ REAL by XBOOLE_0:def_4; ::_thesis: verum
end;

Lm13: now__::_thesis:_for_i_being_integer_number_
for_r,_p1,_p2_being_real_number_st_r_in_[.(p1_+_H1(i)),(p2_+_H1(i)).]_holds_
r_-_(2_*_PI)_in_[.(p1_+_H1(i_-_1)),(p2_+_H1(i_-_1)).]
let i be integer number ; ::_thesis: for r, p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] holds
r - (2 * PI) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).]
let r be real number ; ::_thesis: for p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] holds
r - (2 * PI) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).]
let p1, p2 be real number ; ::_thesis: ( r in [.(p1 + H1(i)),(p2 + H1(i)).] implies r - (2 * PI) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).] )
assume A1: r in [.(p1 + H1(i)),(p2 + H1(i)).] ; ::_thesis: r - (2 * PI) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).]
then  r <= p2 + H1(i) by XXREAL_1:1;
then A2: r - (2 * PI) <= (p2 + H1(i)) - (2 * PI) by XREAL_1:9;
 p1 + H1(i) <= r by A1, XXREAL_1:1;
then  (p1 + H1(i)) - (2 * PI) <= r - (2 * PI) by XREAL_1:9;
hence  r - (2 * PI) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).] by A2, XXREAL_1:1; ::_thesis: verum
end;

Lm14: now__::_thesis:_for_i_being_integer_number_
for_r,_p1,_p2_being_real_number_st_r_in_[.(p1_+_H1(i)),(p2_+_H1(i)).]_/\_REAL_holds_
r_-_(2_*_PI)_in_[.(p1_+_H1(i_-_1)),(p2_+_H1(i_-_1)).]_/\_REAL
let i be integer number ; ::_thesis: for r, p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] /\ REAL holds
r - (2 * PI) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).] /\ REAL
let r be real number ; ::_thesis: for p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] /\ REAL holds
r - (2 * PI) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).] /\ REAL
let p1, p2 be real number ; ::_thesis: ( r in [.(p1 + H1(i)),(p2 + H1(i)).] /\ REAL implies r - (2 * PI) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).] /\ REAL )
assume  r in [.(p1 + H1(i)),(p2 + H1(i)).] /\ REAL ; ::_thesis: r - (2 * PI) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).] /\ REAL
then  r in [.(p1 + H1(i)),(p2 + H1(i)).] by XBOOLE_0:def_4;
then  r - (2 * PI) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).] by Lm13;
hence  r - (2 * PI) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).] /\ REAL by XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th53: :: SIN_COS6:53
for i being integer number holds sin | [.((- (PI / 2)) + ((2 * PI) * i)),((PI / 2) + ((2 * PI) * i)).] is increasing
proof
let i be integer number ; ::_thesis: sin | [.((- (PI / 2)) + ((2 * PI) * i)),((PI / 2) + ((2 * PI) * i)).] is increasing
defpred S1[ Integer] means sin | [.((- (PI / 2)) + H1($1)),((PI / 2) + H1($1)).] is increasing ;
A1: for i being integer number st S1[i] holds
( S1[i - 1] & S1[i + 1] )
proof
let i be integer number ; ::_thesis: ( S1[i] implies ( S1[i - 1] & S1[i + 1] ) )
assume A2: S1[i] ; ::_thesis: ( S1[i - 1] & S1[i + 1] )
set Z = [.((- (PI / 2)) + H1((i - 1) + 1)),((PI / 2) + H1((i - 1) + 1)).];
thus  S1[i - 1] ::_thesis: S1[i + 1]
proof
set Y = [.((- (PI / 2)) + H1(i - 1)),((PI / 2) + H1(i - 1)).];
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_[.((-_(PI_/_2))_+_H1(i_-_1)),((PI_/_2)_+_H1(i_-_1)).]_/\_(dom_sin)_&_r2_in_[.((-_(PI_/_2))_+_H1(i_-_1)),((PI_/_2)_+_H1(i_-_1)).]_/\_(dom_sin)_&_r1_<_r2_holds_
sin_._r1_<_sin_._r2
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in [.((- (PI / 2)) + H1(i - 1)),((PI / 2) + H1(i - 1)).] /\ (dom sin) & r2 in [.((- (PI / 2)) + H1(i - 1)),((PI / 2) + H1(i - 1)).] /\ (dom sin) & r1 < r2 implies sin . r1 < sin . r2 )
assume  ( r1 in [.((- (PI / 2)) + H1(i - 1)),((PI / 2) + H1(i - 1)).] /\ (dom sin) & r2 in [.((- (PI / 2)) + H1(i - 1)),((PI / 2) + H1(i - 1)).] /\ (dom sin) ) ; ::_thesis: ( r1 < r2 implies sin . r1 < sin . r2 )
then A3: ( r1 + (2 * PI) in [.((- (PI / 2)) + H1((i - 1) + 1)),((PI / 2) + H1((i - 1) + 1)).] /\ (dom sin) & r2 + (2 * PI) in [.((- (PI / 2)) + H1((i - 1) + 1)),((PI / 2) + H1((i - 1) + 1)).] /\ (dom sin) ) by Lm12, SIN_COS:24;
assume  r1 < r2 ; ::_thesis: sin . r1 < sin . r2
then  r1 + (2 * PI) < r2 + (2 * PI) by XREAL_1:6;
then  sin . (r1 + (2 * PI)) < sin . (r2 + ((2 * PI) * 1)) by A2, A3, RFUNCT_2:20;
then  sin . (r1 + ((2 * PI) * 1)) < sin . r2 by Th8;
hence  sin . r1 < sin . r2 by Th8; ::_thesis: verum
end;
hence  S1[i - 1] by RFUNCT_2:20; ::_thesis: verum
end;
set Y = [.((- (PI / 2)) + H1(i + 1)),((PI / 2) + H1(i + 1)).];
A4: [.((- (PI / 2)) + H1((i - 1) + 1)),((PI / 2) + H1((i - 1) + 1)).] = [.((- (PI / 2)) + H1((i + 1) - 1)),((PI / 2) + H1((i + 1) - 1)).] ;
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_[.((-_(PI_/_2))_+_H1(i_+_1)),((PI_/_2)_+_H1(i_+_1)).]_/\_(dom_sin)_&_r2_in_[.((-_(PI_/_2))_+_H1(i_+_1)),((PI_/_2)_+_H1(i_+_1)).]_/\_(dom_sin)_&_r1_<_r2_holds_
sin_._r1_<_sin_._r2
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in [.((- (PI / 2)) + H1(i + 1)),((PI / 2) + H1(i + 1)).] /\ (dom sin) & r2 in [.((- (PI / 2)) + H1(i + 1)),((PI / 2) + H1(i + 1)).] /\ (dom sin) & r1 < r2 implies sin . r1 < sin . r2 )
assume  ( r1 in [.((- (PI / 2)) + H1(i + 1)),((PI / 2) + H1(i + 1)).] /\ (dom sin) & r2 in [.((- (PI / 2)) + H1(i + 1)),((PI / 2) + H1(i + 1)).] /\ (dom sin) ) ; ::_thesis: ( r1 < r2 implies sin . r1 < sin . r2 )
then A5: ( r1 - (2 * PI) in [.((- (PI / 2)) + H1((i - 1) + 1)),((PI / 2) + H1((i - 1) + 1)).] /\ (dom sin) & r2 - (2 * PI) in [.((- (PI / 2)) + H1((i - 1) + 1)),((PI / 2) + H1((i - 1) + 1)).] /\ (dom sin) ) by A4, Lm14, SIN_COS:24;
assume  r1 < r2 ; ::_thesis: sin . r1 < sin . r2
then  r1 - (2 * PI) < r2 - (2 * PI) by XREAL_1:9;
then  sin . (r1 - (2 * PI)) < sin . (r2 + ((2 * PI) * (- 1))) by A2, A5, RFUNCT_2:20;
then  sin . (r1 + ((2 * PI) * (- 1))) < sin . r2 by Th8;
hence  sin . r1 < sin . r2 by Th8; ::_thesis: verum
end;
hence  S1[i + 1] by RFUNCT_2:20; ::_thesis: verum
end;
A6: S1[ 0 ] by COMPTRIG:23;
 for i being integer number holds S1[i] from INT_1:sch_4(A6, A1);
hence  sin | [.((- (PI / 2)) + ((2 * PI) * i)),((PI / 2) + ((2 * PI) * i)).] is increasing ; ::_thesis: verum
end;

theorem Th54: :: SIN_COS6:54
for i being integer number holds sin | [.((PI / 2) + ((2 * PI) * i)),(((3 / 2) * PI) + ((2 * PI) * i)).] is decreasing
proof
let i be integer number ; ::_thesis: sin | [.((PI / 2) + ((2 * PI) * i)),(((3 / 2) * PI) + ((2 * PI) * i)).] is decreasing
defpred S1[ Integer] means sin | [.((PI / 2) + H1($1)),(((3 / 2) * PI) + H1($1)).] is decreasing ;
A1: for i being integer number st S1[i] holds
( S1[i - 1] & S1[i + 1] )
proof
let i be integer number ; ::_thesis: ( S1[i] implies ( S1[i - 1] & S1[i + 1] ) )
assume A2: S1[i] ; ::_thesis: ( S1[i - 1] & S1[i + 1] )
set Z = [.((PI / 2) + H1((i - 1) + 1)),(((3 / 2) * PI) + H1((i - 1) + 1)).];
thus  S1[i - 1] ::_thesis: S1[i + 1]
proof
set Y = [.((PI / 2) + H1(i - 1)),(((3 / 2) * PI) + H1(i - 1)).];
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_[.((PI_/_2)_+_H1(i_-_1)),(((3_/_2)_*_PI)_+_H1(i_-_1)).]_/\_(dom_sin)_&_r2_in_[.((PI_/_2)_+_H1(i_-_1)),(((3_/_2)_*_PI)_+_H1(i_-_1)).]_/\_(dom_sin)_&_r1_<_r2_holds_
sin_._r1_>_sin_._r2
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in [.((PI / 2) + H1(i - 1)),(((3 / 2) * PI) + H1(i - 1)).] /\ (dom sin) & r2 in [.((PI / 2) + H1(i - 1)),(((3 / 2) * PI) + H1(i - 1)).] /\ (dom sin) & r1 < r2 implies sin . r1 > sin . r2 )
assume  ( r1 in [.((PI / 2) + H1(i - 1)),(((3 / 2) * PI) + H1(i - 1)).] /\ (dom sin) & r2 in [.((PI / 2) + H1(i - 1)),(((3 / 2) * PI) + H1(i - 1)).] /\ (dom sin) ) ; ::_thesis: ( r1 < r2 implies sin . r1 > sin . r2 )
then A3: ( r1 + (2 * PI) in [.((PI / 2) + H1((i - 1) + 1)),(((3 / 2) * PI) + H1((i - 1) + 1)).] /\ (dom sin) & r2 + (2 * PI) in [.((PI / 2) + H1((i - 1) + 1)),(((3 / 2) * PI) + H1((i - 1) + 1)).] /\ (dom sin) ) by Lm12, SIN_COS:24;
assume  r1 < r2 ; ::_thesis: sin . r1 > sin . r2
then  r1 + (2 * PI) < r2 + (2 * PI) by XREAL_1:6;
then  sin . (r1 + (2 * PI)) > sin . (r2 + ((2 * PI) * 1)) by A2, A3, RFUNCT_2:21;
then  sin . (r1 + ((2 * PI) * 1)) > sin . r2 by Th8;
hence  sin . r1 > sin . r2 by Th8; ::_thesis: verum
end;
hence  S1[i - 1] by RFUNCT_2:21; ::_thesis: verum
end;
set Y = [.((PI / 2) + H1(i + 1)),(((3 / 2) * PI) + H1(i + 1)).];
A4: [.((PI / 2) + H1((i - 1) + 1)),(((3 / 2) * PI) + H1((i - 1) + 1)).] = [.((PI / 2) + H1((i + 1) - 1)),(((3 / 2) * PI) + H1((i + 1) - 1)).] ;
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_[.((PI_/_2)_+_H1(i_+_1)),(((3_/_2)_*_PI)_+_H1(i_+_1)).]_/\_(dom_sin)_&_r2_in_[.((PI_/_2)_+_H1(i_+_1)),(((3_/_2)_*_PI)_+_H1(i_+_1)).]_/\_(dom_sin)_&_r1_<_r2_holds_
sin_._r1_>_sin_._r2
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in [.((PI / 2) + H1(i + 1)),(((3 / 2) * PI) + H1(i + 1)).] /\ (dom sin) & r2 in [.((PI / 2) + H1(i + 1)),(((3 / 2) * PI) + H1(i + 1)).] /\ (dom sin) & r1 < r2 implies sin . r1 > sin . r2 )
assume  ( r1 in [.((PI / 2) + H1(i + 1)),(((3 / 2) * PI) + H1(i + 1)).] /\ (dom sin) & r2 in [.((PI / 2) + H1(i + 1)),(((3 / 2) * PI) + H1(i + 1)).] /\ (dom sin) ) ; ::_thesis: ( r1 < r2 implies sin . r1 > sin . r2 )
then A5: ( r1 - (2 * PI) in [.((PI / 2) + H1((i - 1) + 1)),(((3 / 2) * PI) + H1((i - 1) + 1)).] /\ (dom sin) & r2 - (2 * PI) in [.((PI / 2) + H1((i - 1) + 1)),(((3 / 2) * PI) + H1((i - 1) + 1)).] /\ (dom sin) ) by A4, Lm14, SIN_COS:24;
assume  r1 < r2 ; ::_thesis: sin . r1 > sin . r2
then  r1 - (2 * PI) < r2 - (2 * PI) by XREAL_1:9;
then  sin . (r1 - (2 * PI)) > sin . (r2 + ((2 * PI) * (- 1))) by A2, A5, RFUNCT_2:21;
then  sin . (r1 + ((2 * PI) * (- 1))) > sin . r2 by Th8;
hence  sin . r1 > sin . r2 by Th8; ::_thesis: verum
end;
hence  S1[i + 1] by RFUNCT_2:21; ::_thesis: verum
end;
A6: S1[ 0 ] by COMPTRIG:24;
 for i being integer number holds S1[i] from INT_1:sch_4(A6, A1);
hence  sin | [.((PI / 2) + ((2 * PI) * i)),(((3 / 2) * PI) + ((2 * PI) * i)).] is decreasing ; ::_thesis: verum
end;

theorem Th55: :: SIN_COS6:55
for i being integer number holds cos | [.((2 * PI) * i),(PI + ((2 * PI) * i)).] is decreasing
proof
let i be integer number ; ::_thesis: cos | [.((2 * PI) * i),(PI + ((2 * PI) * i)).] is decreasing
defpred S1[ Integer] means cos | [.H1($1),(PI + H1($1)).] is decreasing ;
A1: for i being integer number st S1[i] holds
( S1[i - 1] & S1[i + 1] )
proof
let i be integer number ; ::_thesis: ( S1[i] implies ( S1[i - 1] & S1[i + 1] ) )
assume A2: S1[i] ; ::_thesis: ( S1[i - 1] & S1[i + 1] )
set Z = [.(0 + H1((i - 1) + 1)),(PI + H1((i - 1) + 1)).];
thus  S1[i - 1] ::_thesis: S1[i + 1]
proof
set Y = [.H1(i - 1),(PI + H1(i - 1)).];
A3: [.H1(i - 1),(PI + H1(i - 1)).] = [.(0 + H1(i - 1)),(PI + H1(i - 1)).] ;
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_[.H1(i_-_1),(PI_+_H1(i_-_1)).]_/\_(dom_cos)_&_r2_in_[.H1(i_-_1),(PI_+_H1(i_-_1)).]_/\_(dom_cos)_&_r1_<_r2_holds_
cos_._r1_>_cos_._r2
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in [.H1(i - 1),(PI + H1(i - 1)).] /\ (dom cos) & r2 in [.H1(i - 1),(PI + H1(i - 1)).] /\ (dom cos) & r1 < r2 implies cos . r1 > cos . r2 )
assume  ( r1 in [.H1(i - 1),(PI + H1(i - 1)).] /\ (dom cos) & r2 in [.H1(i - 1),(PI + H1(i - 1)).] /\ (dom cos) ) ; ::_thesis: ( r1 < r2 implies cos . r1 > cos . r2 )
then A4: ( r1 + (2 * PI) in [.(0 + H1((i - 1) + 1)),(PI + H1((i - 1) + 1)).] /\ (dom cos) & r2 + (2 * PI) in [.(0 + H1((i - 1) + 1)),(PI + H1((i - 1) + 1)).] /\ (dom cos) ) by A3, Lm12, SIN_COS:24;
assume  r1 < r2 ; ::_thesis: cos . r1 > cos . r2
then  r1 + (2 * PI) < r2 + (2 * PI) by XREAL_1:6;
then  cos . (r1 + (2 * PI)) > cos . (r2 + ((2 * PI) * 1)) by A2, A4, RFUNCT_2:21;
then  cos . (r1 + ((2 * PI) * 1)) > cos . r2 by Th10;
hence  cos . r1 > cos . r2 by Th10; ::_thesis: verum
end;
hence  S1[i - 1] by RFUNCT_2:21; ::_thesis: verum
end;
set Y = [.H1(i + 1),(PI + H1(i + 1)).];
A5: ( [.H1(i + 1),(PI + H1(i + 1)).] = [.(0 + H1(i + 1)),(PI + H1(i + 1)).] & [.(0 + H1((i - 1) + 1)),(PI + H1((i - 1) + 1)).] = [.H1((i + 1) - 1),(PI + H1((i + 1) - 1)).] ) ;
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_[.H1(i_+_1),(PI_+_H1(i_+_1)).]_/\_(dom_cos)_&_r2_in_[.H1(i_+_1),(PI_+_H1(i_+_1)).]_/\_(dom_cos)_&_r1_<_r2_holds_
cos_._r1_>_cos_._r2
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in [.H1(i + 1),(PI + H1(i + 1)).] /\ (dom cos) & r2 in [.H1(i + 1),(PI + H1(i + 1)).] /\ (dom cos) & r1 < r2 implies cos . r1 > cos . r2 )
assume  ( r1 in [.H1(i + 1),(PI + H1(i + 1)).] /\ (dom cos) & r2 in [.H1(i + 1),(PI + H1(i + 1)).] /\ (dom cos) ) ; ::_thesis: ( r1 < r2 implies cos . r1 > cos . r2 )
then A6: ( r1 - (2 * PI) in [.(0 + H1((i - 1) + 1)),(PI + H1((i - 1) + 1)).] /\ (dom cos) & r2 - (2 * PI) in [.(0 + H1((i - 1) + 1)),(PI + H1((i - 1) + 1)).] /\ (dom cos) ) by A5, Lm14, SIN_COS:24;
assume  r1 < r2 ; ::_thesis: cos . r1 > cos . r2
then  r1 - (2 * PI) < r2 - (2 * PI) by XREAL_1:9;
then  cos . (r1 - (2 * PI)) > cos . (r2 + ((2 * PI) * (- 1))) by A2, A6, RFUNCT_2:21;
then  cos . (r1 + ((2 * PI) * (- 1))) > cos . r2 by Th10;
hence  cos . r1 > cos . r2 by Th10; ::_thesis: verum
end;
hence  S1[i + 1] by RFUNCT_2:21; ::_thesis: verum
end;
A7: S1[ 0 ] by COMPTRIG:25;
 for i being integer number holds S1[i] from INT_1:sch_4(A7, A1);
hence  cos | [.((2 * PI) * i),(PI + ((2 * PI) * i)).] is decreasing ; ::_thesis: verum
end;

theorem Th56: :: SIN_COS6:56
for i being integer number holds cos | [.(PI + ((2 * PI) * i)),((2 * PI) + ((2 * PI) * i)).] is increasing
proof
let i be integer number ; ::_thesis: cos | [.(PI + ((2 * PI) * i)),((2 * PI) + ((2 * PI) * i)).] is increasing
defpred S1[ Integer] means cos | [.(PI + H1($1)),((2 * PI) + H1($1)).] is increasing ;
A1: for i being integer number st S1[i] holds
( S1[i - 1] & S1[i + 1] )
proof
let i be integer number ; ::_thesis: ( S1[i] implies ( S1[i - 1] & S1[i + 1] ) )
assume A2: S1[i] ; ::_thesis: ( S1[i - 1] & S1[i + 1] )
set Z = [.(PI + H1((i - 1) + 1)),((2 * PI) + H1((i - 1) + 1)).];
thus  S1[i - 1] ::_thesis: S1[i + 1]
proof
set Y = [.(PI + H1(i - 1)),((2 * PI) + H1(i - 1)).];
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_[.(PI_+_H1(i_-_1)),((2_*_PI)_+_H1(i_-_1)).]_/\_(dom_cos)_&_r2_in_[.(PI_+_H1(i_-_1)),((2_*_PI)_+_H1(i_-_1)).]_/\_(dom_cos)_&_r1_<_r2_holds_
cos_._r1_<_cos_._r2
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in [.(PI + H1(i - 1)),((2 * PI) + H1(i - 1)).] /\ (dom cos) & r2 in [.(PI + H1(i - 1)),((2 * PI) + H1(i - 1)).] /\ (dom cos) & r1 < r2 implies cos . r1 < cos . r2 )
assume  ( r1 in [.(PI + H1(i - 1)),((2 * PI) + H1(i - 1)).] /\ (dom cos) & r2 in [.(PI + H1(i - 1)),((2 * PI) + H1(i - 1)).] /\ (dom cos) ) ; ::_thesis: ( r1 < r2 implies cos . r1 < cos . r2 )
then A3: ( r1 + (2 * PI) in [.(PI + H1((i - 1) + 1)),((2 * PI) + H1((i - 1) + 1)).] /\ (dom cos) & r2 + (2 * PI) in [.(PI + H1((i - 1) + 1)),((2 * PI) + H1((i - 1) + 1)).] /\ (dom cos) ) by Lm12, SIN_COS:24;
assume  r1 < r2 ; ::_thesis: cos . r1 < cos . r2
then  r1 + (2 * PI) < r2 + (2 * PI) by XREAL_1:6;
then  cos . (r1 + (2 * PI)) < cos . (r2 + ((2 * PI) * 1)) by A2, A3, RFUNCT_2:20;
then  cos . (r1 + ((2 * PI) * 1)) < cos . r2 by Th10;
hence  cos . r1 < cos . r2 by Th10; ::_thesis: verum
end;
hence  S1[i - 1] by RFUNCT_2:20; ::_thesis: verum
end;
set Y = [.(PI + H1(i + 1)),((2 * PI) + H1(i + 1)).];
A4: [.(PI + H1((i - 1) + 1)),((2 * PI) + H1((i - 1) + 1)).] = [.(PI + H1((i + 1) - 1)),((2 * PI) + H1((i + 1) - 1)).] ;
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_[.(PI_+_H1(i_+_1)),((2_*_PI)_+_H1(i_+_1)).]_/\_(dom_cos)_&_r2_in_[.(PI_+_H1(i_+_1)),((2_*_PI)_+_H1(i_+_1)).]_/\_(dom_cos)_&_r1_<_r2_holds_
cos_._r1_<_cos_._r2
let r1, r2 be Element of REAL ; ::_thesis: ( r1 in [.(PI + H1(i + 1)),((2 * PI) + H1(i + 1)).] /\ (dom cos) & r2 in [.(PI + H1(i + 1)),((2 * PI) + H1(i + 1)).] /\ (dom cos) & r1 < r2 implies cos . r1 < cos . r2 )
assume  ( r1 in [.(PI + H1(i + 1)),((2 * PI) + H1(i + 1)).] /\ (dom cos) & r2 in [.(PI + H1(i + 1)),((2 * PI) + H1(i + 1)).] /\ (dom cos) ) ; ::_thesis: ( r1 < r2 implies cos . r1 < cos . r2 )
then A5: ( r1 - (2 * PI) in [.(PI + H1((i - 1) + 1)),((2 * PI) + H1((i - 1) + 1)).] /\ (dom cos) & r2 - (2 * PI) in [.(PI + H1((i - 1) + 1)),((2 * PI) + H1((i - 1) + 1)).] /\ (dom cos) ) by A4, Lm14, SIN_COS:24;
assume  r1 < r2 ; ::_thesis: cos . r1 < cos . r2
then  r1 - (2 * PI) < r2 - (2 * PI) by XREAL_1:9;
then  cos . (r1 - (2 * PI)) < cos . (r2 + ((2 * PI) * (- 1))) by A2, A5, RFUNCT_2:20;
then  cos . (r1 + ((2 * PI) * (- 1))) < cos . r2 by Th10;
hence  cos . r1 < cos . r2 by Th10; ::_thesis: verum
end;
hence  S1[i + 1] by RFUNCT_2:20; ::_thesis: verum
end;
A6: S1[ 0 ] by COMPTRIG:26;
 for i being integer number holds S1[i] from INT_1:sch_4(A6, A1);
hence  cos | [.(PI + ((2 * PI) * i)),((2 * PI) + ((2 * PI) * i)).] is increasing ; ::_thesis: verum
end;

theorem Th57: :: SIN_COS6:57
for i being integer number holds sin | [.((- (PI / 2)) + ((2 * PI) * i)),((PI / 2) + ((2 * PI) * i)).] is one-to-one
proof
let i be integer number ; ::_thesis: sin | [.((- (PI / 2)) + ((2 * PI) * i)),((PI / 2) + ((2 * PI) * i)).] is one-to-one
set Q = [.((- (PI / 2)) + ((2 * PI) * i)),((PI / 2) + ((2 * PI) * i)).];
 sin | [.((- (PI / 2)) + ((2 * PI) * i)),((PI / 2) + ((2 * PI) * i)).] is increasing by Th53;
hence  sin | [.((- (PI / 2)) + ((2 * PI) * i)),((PI / 2) + ((2 * PI) * i)).] is one-to-one by FCONT_3:8; ::_thesis: verum
end;

theorem Th58: :: SIN_COS6:58
for i being integer number holds sin | [.((PI / 2) + ((2 * PI) * i)),(((3 / 2) * PI) + ((2 * PI) * i)).] is one-to-one
proof
let i be integer number ; ::_thesis: sin | [.((PI / 2) + ((2 * PI) * i)),(((3 / 2) * PI) + ((2 * PI) * i)).] is one-to-one
set Q = [.((PI / 2) + ((2 * PI) * i)),(((3 / 2) * PI) + ((2 * PI) * i)).];
 sin | [.((PI / 2) + ((2 * PI) * i)),(((3 / 2) * PI) + ((2 * PI) * i)).] is decreasing by Th54;
hence  sin | [.((PI / 2) + ((2 * PI) * i)),(((3 / 2) * PI) + ((2 * PI) * i)).] is one-to-one by FCONT_3:8; ::_thesis: verum
end;

registration
clustersin | [.(- (PI / 2)),(PI / 2).] ->  one-to-one ;
coherence
 sin | [.(- (PI / 2)),(PI / 2).] is one-to-one by Lm1, Th57;
clustersin | [.(PI / 2),((3 / 2) * PI).] ->  one-to-one ;
coherence
 sin | [.(PI / 2),((3 / 2) * PI).] is one-to-one by Lm2, Th58;
end;

registration
clustersin | [.(- (PI / 2)),0.] ->  one-to-one ;
coherence
 sin | [.(- (PI / 2)),0.] is one-to-one
proof
 sin | [.(- (PI / 2)),(PI / 2).] is one-to-one ;
hence  sin | [.(- (PI / 2)),0.] is one-to-one by Th2, XXREAL_1:34; ::_thesis: verum
end;
clustersin | [.0,(PI / 2).] ->  one-to-one ;
coherence
 sin | [.0,(PI / 2).] is one-to-one
proof
 sin | [.(- (PI / 2)),(PI / 2).] is one-to-one ;
hence  sin | [.0,(PI / 2).] is one-to-one by Th2, XXREAL_1:34; ::_thesis: verum
end;
clustersin | [.(PI / 2),PI.] ->  one-to-one ;
coherence
 sin | [.(PI / 2),PI.] is one-to-one
proof
 sin | [.(PI / 2),((3 / 2) * PI).] is one-to-one ;
hence  sin | [.(PI / 2),PI.] is one-to-one by Lm7, Th2, XXREAL_1:34; ::_thesis: verum
end;
clustersin | [.PI,((3 / 2) * PI).] ->  one-to-one ;
coherence
 sin | [.PI,((3 / 2) * PI).] is one-to-one
proof
 sin | [.(PI / 2),((3 / 2) * PI).] is one-to-one ;
hence  sin | [.PI,((3 / 2) * PI).] is one-to-one by Lm6, Th2, XXREAL_1:34; ::_thesis: verum
end;
clustersin | [.((3 / 2) * PI),(2 * PI).] ->  one-to-one ;
coherence
 sin | [.((3 / 2) * PI),(2 * PI).] is one-to-one
proof
 sin | [.((- (PI / 2)) + H1(1)),((PI / 2) + H1(1)).] is one-to-one by Th57;
hence  sin | [.((3 / 2) * PI),(2 * PI).] is one-to-one by Lm8, Th2, XXREAL_1:34; ::_thesis: verum
end;
end;

registration
clustersin | ].(- (PI / 2)),(PI / 2).[ ->  one-to-one ;
coherence
 sin | ].(- (PI / 2)),(PI / 2).[ is one-to-one
proof
 sin | [.(- (PI / 2)),(PI / 2).] is one-to-one ;
hence  sin | ].(- (PI / 2)),(PI / 2).[ is one-to-one by Th2, XXREAL_1:25; ::_thesis: verum
end;
clustersin | ].(PI / 2),((3 / 2) * PI).[ ->  one-to-one ;
coherence
 sin | ].(PI / 2),((3 / 2) * PI).[ is one-to-one
proof
 sin | [.(PI / 2),((3 / 2) * PI).] is one-to-one ;
hence  sin | ].(PI / 2),((3 / 2) * PI).[ is one-to-one by Th2, XXREAL_1:25; ::_thesis: verum
end;
clustersin | ].(- (PI / 2)),0.[ ->  one-to-one ;
coherence
 sin | ].(- (PI / 2)),0.[ is one-to-one
proof
 sin | [.(- (PI / 2)),0.] is one-to-one ;
hence  sin | ].(- (PI / 2)),0.[ is one-to-one by Th2, XXREAL_1:25; ::_thesis: verum
end;
clustersin | ].0,(PI / 2).[ ->  one-to-one ;
coherence
 sin | ].0,(PI / 2).[ is one-to-one
proof
 sin | [.0,(PI / 2).] is one-to-one ;
hence  sin | ].0,(PI / 2).[ is one-to-one by Th2, XXREAL_1:25; ::_thesis: verum
end;
clustersin | ].(PI / 2),PI.[ ->  one-to-one ;
coherence
 sin | ].(PI / 2),PI.[ is one-to-one
proof
 sin | [.(PI / 2),PI.] is one-to-one ;
hence  sin | ].(PI / 2),PI.[ is one-to-one by Th2, XXREAL_1:25; ::_thesis: verum
end;
clustersin | ].PI,((3 / 2) * PI).[ ->  one-to-one ;
coherence
 sin | ].PI,((3 / 2) * PI).[ is one-to-one
proof
 sin | [.PI,((3 / 2) * PI).] is one-to-one ;
hence  sin | ].PI,((3 / 2) * PI).[ is one-to-one by Th2, XXREAL_1:25; ::_thesis: verum
end;
clustersin | ].((3 / 2) * PI),(2 * PI).[ ->  one-to-one ;
coherence
 sin | ].((3 / 2) * PI),(2 * PI).[ is one-to-one
proof
 sin | [.((3 / 2) * PI),(2 * PI).] is one-to-one ;
hence  sin | ].((3 / 2) * PI),(2 * PI).[ is one-to-one by Th2, XXREAL_1:25; ::_thesis: verum
end;
end;

theorem Th59: :: SIN_COS6:59
for i being integer number holds cos | [.((2 * PI) * i),(PI + ((2 * PI) * i)).] is one-to-one
proof
let i be integer number ; ::_thesis: cos | [.((2 * PI) * i),(PI + ((2 * PI) * i)).] is one-to-one
set Q1 = [.((2 * PI) * i),(PI + ((2 * PI) * i)).];
 cos | [.((2 * PI) * i),(PI + ((2 * PI) * i)).] is decreasing by Th55;
hence  cos | [.((2 * PI) * i),(PI + ((2 * PI) * i)).] is one-to-one by FCONT_3:8; ::_thesis: verum
end;

theorem Th60: :: SIN_COS6:60
for i being integer number holds cos | [.(PI + ((2 * PI) * i)),((2 * PI) + ((2 * PI) * i)).] is one-to-one
proof
let i be integer number ; ::_thesis: cos | [.(PI + ((2 * PI) * i)),((2 * PI) + ((2 * PI) * i)).] is one-to-one
set Q1 = [.(PI + ((2 * PI) * i)),((2 * PI) + ((2 * PI) * i)).];
 cos | [.(PI + ((2 * PI) * i)),((2 * PI) + ((2 * PI) * i)).] is increasing by Th56;
hence  cos | [.(PI + ((2 * PI) * i)),((2 * PI) + ((2 * PI) * i)).] is one-to-one by FCONT_3:8; ::_thesis: verum
end;

registration
clustercos | [.0,PI.] ->  one-to-one ;
coherence
 cos | [.0,PI.] is one-to-one by Lm3, Th59;
clustercos | [.PI,(2 * PI).] ->  one-to-one ;
coherence
 cos | [.PI,(2 * PI).] is one-to-one by Lm4, Th60;
end;

registration
clustercos | [.0,(PI / 2).] ->  one-to-one ;
coherence
 cos | [.0,(PI / 2).] is one-to-one
proof
 cos | [.0,PI.] is one-to-one ;
hence  cos | [.0,(PI / 2).] is one-to-one by Lm6, Th2, XXREAL_1:34; ::_thesis: verum
end;
clustercos | [.(PI / 2),PI.] ->  one-to-one ;
coherence
 cos | [.(PI / 2),PI.] is one-to-one
proof
 cos | [.0,PI.] is one-to-one ;
hence  cos | [.(PI / 2),PI.] is one-to-one by Th2, XXREAL_1:34; ::_thesis: verum
end;
clustercos | [.PI,((3 / 2) * PI).] ->  one-to-one ;
coherence
 cos | [.PI,((3 / 2) * PI).] is one-to-one
proof
 cos | [.PI,(2 * PI).] is one-to-one ;
hence  cos | [.PI,((3 / 2) * PI).] is one-to-one by Lm9, Th2, XXREAL_1:34; ::_thesis: verum
end;
clustercos | [.((3 / 2) * PI),(2 * PI).] ->  one-to-one ;
coherence
 cos | [.((3 / 2) * PI),(2 * PI).] is one-to-one
proof
 cos | [.PI,(2 * PI).] is one-to-one ;
hence  cos | [.((3 / 2) * PI),(2 * PI).] is one-to-one by Lm7, Th2, XXREAL_1:34; ::_thesis: verum
end;
end;

registration
clustercos | ].0,PI.[ ->  one-to-one ;
coherence
 cos | ].0,PI.[ is one-to-one
proof
 cos | [.0,PI.] is one-to-one ;
hence  cos | ].0,PI.[ is one-to-one by Th2, XXREAL_1:25; ::_thesis: verum
end;
clustercos | ].PI,(2 * PI).[ ->  one-to-one ;
coherence
 cos | ].PI,(2 * PI).[ is one-to-one
proof
 cos | [.PI,(2 * PI).] is one-to-one ;
hence  cos | ].PI,(2 * PI).[ is one-to-one by Th2, XXREAL_1:25; ::_thesis: verum
end;
clustercos | ].0,(PI / 2).[ ->  one-to-one ;
coherence
 cos | ].0,(PI / 2).[ is one-to-one
proof
 cos | [.0,(PI / 2).] is one-to-one ;
hence  cos | ].0,(PI / 2).[ is one-to-one by Th2, XXREAL_1:25; ::_thesis: verum
end;
clustercos | ].(PI / 2),PI.[ ->  one-to-one ;
coherence
 cos | ].(PI / 2),PI.[ is one-to-one
proof
 cos | [.(PI / 2),PI.] is one-to-one ;
hence  cos | ].(PI / 2),PI.[ is one-to-one by Th2, XXREAL_1:25; ::_thesis: verum
end;
clustercos | ].PI,((3 / 2) * PI).[ ->  one-to-one ;
coherence
 cos | ].PI,((3 / 2) * PI).[ is one-to-one
proof
 cos | [.PI,((3 / 2) * PI).] is one-to-one ;
hence  cos | ].PI,((3 / 2) * PI).[ is one-to-one by Th2, XXREAL_1:25; ::_thesis: verum
end;
clustercos | ].((3 / 2) * PI),(2 * PI).[ ->  one-to-one ;
coherence
 cos | ].((3 / 2) * PI),(2 * PI).[ is one-to-one
proof
 cos | [.((3 / 2) * PI),(2 * PI).] is one-to-one ;
hence  cos | ].((3 / 2) * PI),(2 * PI).[ is one-to-one by Th2, XXREAL_1:25; ::_thesis: verum
end;
end;

theorem :: SIN_COS6:61
for r, s being real number
for i being integer number st (2 * PI) * i <= r & r < (2 * PI) + ((2 * PI) * i) & (2 * PI) * i <= s & s < (2 * PI) + ((2 * PI) * i) & sin r = sin s & cos r = cos s holds
r = s
proof
let r, s be real number ; ::_thesis: for i being integer number st (2 * PI) * i <= r & r < (2 * PI) + ((2 * PI) * i) & (2 * PI) * i <= s & s < (2 * PI) + ((2 * PI) * i) & sin r = sin s & cos r = cos s holds
r = s
let i be integer number ; ::_thesis: ( (2 * PI) * i <= r & r < (2 * PI) + ((2 * PI) * i) & (2 * PI) * i <= s & s < (2 * PI) + ((2 * PI) * i) & sin r = sin s & cos r = cos s implies r = s )
assume that
A1: (2 * PI) * i <= r and
A2: ( r < (2 * PI) + ((2 * PI) * i) & (2 * PI) * i <= s ) and
A3: s < (2 * PI) + ((2 * PI) * i) and
A4: ( sin r = sin s & cos r = cos s ) ; ::_thesis: r = s
A5: cos (r - s) = ((cos r) * (cos s)) + ((sin r) * (sin s)) by COMPLEX2:3
.= 1 by A4, SIN_COS:29 ;
A6: sin (r - s) = ((sin r) * (cos s)) - ((cos r) * (sin s)) by COMPLEX2:3
.= 0 by A4 ;
A7: cos (s - r) = ((cos r) * (cos s)) + ((sin r) * (sin s)) by COMPLEX2:3
.= 1 by A4, SIN_COS:29 ;
A8: sin (s - r) = ((sin s) * (cos r)) - ((cos s) * (sin r)) by COMPLEX2:3
.= 0 by A4 ;
percases ( r > s or r < s or r = s ) by XXREAL_0:1;
supposeA9: r > s ; ::_thesis: r = s
 r + ((2 * PI) * i) < ((2 * PI) + ((2 * PI) * i)) + s by A2, XREAL_1:8;
then  (r + ((2 * PI) * i)) - ((2 * PI) * i) < (((2 * PI) + ((2 * PI) * i)) + s) - ((2 * PI) * i) by XREAL_1:9;
then  r < (2 * PI) + s ;
then A10: r - s < 2 * PI by XREAL_1:19;
 r > s + 0 by A9;
then  0 <= r - s by XREAL_1:20;
then  ( r - s = 0 or r - s = PI ) by A6, A10, COMPTRIG:17;
hence  r = s by A5, SIN_COS:77; ::_thesis: verum
end;
supposeA11: r < s ; ::_thesis: r = s
 s + ((2 * PI) * i) < ((2 * PI) + ((2 * PI) * i)) + r by A1, A3, XREAL_1:8;
then  (s + ((2 * PI) * i)) - ((2 * PI) * i) < (((2 * PI) + ((2 * PI) * i)) + r) - ((2 * PI) * i) by XREAL_1:9;
then  s < (2 * PI) + r ;
then A12: s - r < 2 * PI by XREAL_1:19;
 s > r + 0 by A11;
then  0 <= s - r by XREAL_1:20;
then  ( s - r = 0 or s - r = PI ) by A8, A12, COMPTRIG:17;
hence  r = s by A7, SIN_COS:77; ::_thesis: verum
end;
suppose r = s ; ::_thesis: r = s
hence  r = s ; ::_thesis: verum
end;
end;
end;

begin

definition
func arcsin  ->  PartFunc of REAL,REAL equals :: SIN_COS6:def 1
(sin | [.(- (PI / 2)),(PI / 2).]) " ;
coherence
 (sin | [.(- (PI / 2)),(PI / 2).]) " is PartFunc of REAL,REAL ;
end;

:: deftheorem  defines arcsin SIN_COS6:def_1_:_
 arcsin = (sin | [.(- (PI / 2)),(PI / 2).]) " ;

definition
let r be set ;
func arcsin r ->  set  equals :: SIN_COS6:def 2
arcsin . r;
coherence
 arcsin . r is set ;
end;

:: deftheorem  defines arcsin SIN_COS6:def_2_:_
 for r being set holds arcsin r = arcsin . r;

definition
let r be set ;
:: original: arcsin
redefine func arcsin r ->  Real;
coherence
 arcsin r is Real ;
end;

Lm15:  arcsin " = sin | [.(- (PI / 2)),(PI / 2).]
by FUNCT_1:43;

theorem Th62: :: SIN_COS6:62
rng arcsin = [.(- (PI / 2)),(PI / 2).]
proof
 dom (sin | [.(- (PI / 2)),(PI / 2).]) = [.(- (PI / 2)),(PI / 2).] by RELAT_1:62, SIN_COS:24;
hence  rng arcsin = [.(- (PI / 2)),(PI / 2).] by FUNCT_1:33; ::_thesis: verum
end;

registration
cluster arcsin  ->  one-to-one ;
coherence
 arcsin is one-to-one ;
end;

theorem Th63: :: SIN_COS6:63
dom arcsin = [.(- 1),1.] by COMPTRIG:30, FUNCT_1:33;

theorem Th64: :: SIN_COS6:64
(sin | [.(- (PI / 2)),(PI / 2).]) * arcsin = id [.(- 1),1.] by COMPTRIG:30, FUNCT_1:39;

theorem :: SIN_COS6:65
arcsin * (sin | [.(- (PI / 2)),(PI / 2).]) = id [.(- 1),1.] by COMPTRIG:30, FUNCT_1:39;

theorem Th66: :: SIN_COS6:66
(sin | [.(- (PI / 2)),(PI / 2).]) * arcsin = id [.(- (PI / 2)),(PI / 2).] by Lm15, Th62, FUNCT_1:39;

theorem :: SIN_COS6:67
arcsin * (sin | [.(- (PI / 2)),(PI / 2).]) = id [.(- (PI / 2)),(PI / 2).] by Lm15, Th62, FUNCT_1:39;

theorem Th68: :: SIN_COS6:68
for r being real number st - 1 <= r & r <= 1 holds
sin (arcsin r) = r
proof
let r be real number ; ::_thesis: ( - 1 <= r & r <= 1 implies sin (arcsin r) = r )
assume  ( - 1 <= r & r <= 1 ) ; ::_thesis: sin (arcsin r) = r
then A1: r in [.(- 1),1.] by XXREAL_1:1;
then A2: arcsin . r in [.(- (PI / 2)),(PI / 2).] by Th62, Th63, FUNCT_1:def_3;
thus  sin (arcsin r) = sin . (arcsin . r) by SIN_COS:def_17
.= (sin | [.(- (PI / 2)),(PI / 2).]) . (arcsin . r) by A2, FUNCT_1:49
.= (id [.(- 1),1.]) . r by A1, Th63, Th64, FUNCT_1:13
.= r by A1, FUNCT_1:18 ; ::_thesis: verum
end;

theorem Th69: :: SIN_COS6:69
for r being real number st - (PI / 2) <= r & r <= PI / 2 holds
arcsin (sin r) = r
proof
let r be real number ; ::_thesis: ( - (PI / 2) <= r & r <= PI / 2 implies arcsin (sin r) = r )
A1: dom (sin | [.(- (PI / 2)),(PI / 2).]) = [.(- (PI / 2)),(PI / 2).] by RELAT_1:62, SIN_COS:24;
assume  ( - (PI / 2) <= r & r <= PI / 2 ) ; ::_thesis: arcsin (sin r) = r
then A2: r in [.(- (PI / 2)),(PI / 2).] by XXREAL_1:1;
thus  arcsin (sin r) = arcsin . (sin . r) by SIN_COS:def_17
.= arcsin . ((sin | [.(- (PI / 2)),(PI / 2).]) . r) by A2, FUNCT_1:49
.= (id [.(- (PI / 2)),(PI / 2).]) . r by A2, A1, Th66, FUNCT_1:13
.= r by A2, FUNCT_1:18 ; ::_thesis: verum
end;

theorem :: SIN_COS6:70
arcsin (- 1) = - (PI / 2) by Th7, Th69;

theorem :: SIN_COS6:71
arcsin 0 = 0 by Th69, SIN_COS:31;

theorem :: SIN_COS6:72
arcsin 1 = PI / 2 by Th69, SIN_COS:77;

theorem :: SIN_COS6:73
for r being real number st - 1 <= r & r <= 1 & arcsin r = - (PI / 2) holds
r = - 1 by Th7, Th68;

theorem :: SIN_COS6:74
for r being real number st - 1 <= r & r <= 1 & arcsin r = 0 holds
r = 0 by Th68, SIN_COS:31;

theorem :: SIN_COS6:75
for r being real number st - 1 <= r & r <= 1 & arcsin r = PI / 2 holds
r = 1 by Th68, SIN_COS:77;

theorem Th76: :: SIN_COS6:76
for r being real number st - 1 <= r & r <= 1 holds
( - (PI / 2) <= arcsin r & arcsin r <= PI / 2 )
proof
let r be real number ; ::_thesis: ( - 1 <= r & r <= 1 implies ( - (PI / 2) <= arcsin r & arcsin r <= PI / 2 ) )
assume  ( - 1 <= r & r <= 1 ) ; ::_thesis: ( - (PI / 2) <= arcsin r & arcsin r <= PI / 2 )
then  r in [.(- 1),1.] by XXREAL_1:1;
then  arcsin . r in rng arcsin by Th63, FUNCT_1:def_3;
hence  ( - (PI / 2) <= arcsin r & arcsin r <= PI / 2 ) by Th62, XXREAL_1:1; ::_thesis: verum
end;

theorem Th77: :: SIN_COS6:77
for r being real number st - 1 < r & r < 1 holds
( - (PI / 2) < arcsin r & arcsin r < PI / 2 )
proof
let r be real number ; ::_thesis: ( - 1 < r & r < 1 implies ( - (PI / 2) < arcsin r & arcsin r < PI / 2 ) )
assume A1: ( - 1 < r & r < 1 ) ; ::_thesis: ( - (PI / 2) < arcsin r & arcsin r < PI / 2 )
then  ( - (PI / 2) <= arcsin r & arcsin r <= PI / 2 ) by Th76;
then  ( ( - (PI / 2) < arcsin r & arcsin r < PI / 2 ) or - (PI / 2) = arcsin r or arcsin r = PI / 2 ) by XXREAL_0:1;
hence  ( - (PI / 2) < arcsin r & arcsin r < PI / 2 ) by A1, Th7, Th68, SIN_COS:77; ::_thesis: verum
end;

theorem Th78: :: SIN_COS6:78
for r being real number st - 1 <= r & r <= 1 holds
arcsin r = - (arcsin (- r))
proof
let r be real number ; ::_thesis: ( - 1 <= r & r <= 1 implies arcsin r = - (arcsin (- r)) )
assume  ( - 1 <= r & r <= 1 ) ; ::_thesis: arcsin r = - (arcsin (- r))
then A1: ( - (- 1) >= - r & - r >= - 1 ) by XREAL_1:24;
then  arcsin (- r) <= PI / 2 by Th76;
then A2: - (PI / 2) <= - (arcsin (- r)) by XREAL_1:24;
 - (PI / 2) <= arcsin (- r) by A1, Th76;
then A3: - (arcsin (- r)) <= - (- (PI / 2)) by XREAL_1:24;
r = 0 - (1 * (- r))
.= ((sin 0) * (cos (arcsin (- r)))) - ((cos 0) * (sin (arcsin (- r)))) by A1, Th68, SIN_COS:31
.= sin (0 - (arcsin (- r))) by COMPLEX2:3 ;
hence  arcsin r = - (arcsin (- r)) by A2, A3, Th69; ::_thesis: verum
end;

theorem Th79: :: SIN_COS6:79
for s, r being real number st 0 <= s & (r ^2) + (s ^2) = 1 holds
cos (arcsin r) = s
proof
let s, r be real number ; ::_thesis: ( 0 <= s & (r ^2) + (s ^2) = 1 implies cos (arcsin r) = s )
set x = arcsin r;
assume that
A1: 0 <= s and
A2: (r ^2) + (s ^2) = 1 ; ::_thesis: cos (arcsin r) = s
A3: ( - 1 <= r & r <= 1 ) by A2, Lm5;
then  ( - (PI / 2) <= arcsin r & arcsin r <= PI / 2 ) by Th76;
then A4: arcsin r in [.(- (PI / 2)),(PI / 2).] by XXREAL_1:1;
 ((sin . (arcsin r)) ^2) + ((cos . (arcsin r)) ^2) = 1 by SIN_COS:28;
then (cos . (arcsin r)) ^2 = 1 - ((sin . (arcsin r)) ^2)
.= 1 - ((sin (arcsin r)) ^2) by SIN_COS:def_17
.= 1 - (r ^2) by A3, Th68 ;
then A5: ( cos . (arcsin r) = s or cos . (arcsin r) = - s ) by A2, SQUARE_1:40;
 ( - (- (- s)) < 0 or s = 0 ) by A1;
hence  cos (arcsin r) = s by A5, A4, COMPTRIG:12, SIN_COS:def_19; ::_thesis: verum
end;

theorem :: SIN_COS6:80
for s, r being real number st s <= 0 & (r ^2) + (s ^2) = 1 holds
cos (arcsin r) = - s
proof
let s, r be real number ; ::_thesis: ( s <= 0 & (r ^2) + (s ^2) = 1 implies cos (arcsin r) = - s )
set x = arcsin r;
assume that
A1: s <= 0 and
A2: (r ^2) + (s ^2) = 1 ; ::_thesis: cos (arcsin r) = - s
A3: ( - 1 <= r & r <= 1 ) by A2, Lm5;
then  ( - (PI / 2) <= arcsin r & arcsin r <= PI / 2 ) by Th76;
then A4: arcsin r in [.(- (PI / 2)),(PI / 2).] by XXREAL_1:1;
 ((sin . (arcsin r)) ^2) + ((cos . (arcsin r)) ^2) = 1 by SIN_COS:28;
then (cos . (arcsin r)) ^2 = 1 - ((sin . (arcsin r)) ^2)
.= 1 - ((sin (arcsin r)) ^2) by SIN_COS:def_17
.= 1 - (r ^2) by A3, Th68 ;
then A5: ( cos . (arcsin r) = s or cos . (arcsin r) = - s ) by A2, SQUARE_1:40;
 ( 0 > s or s = 0 ) by A1;
hence  cos (arcsin r) = - s by A5, A4, COMPTRIG:12, SIN_COS:def_19; ::_thesis: verum
end;

theorem Th81: :: SIN_COS6:81
for r being real number st - 1 <= r & r <= 1 holds
cos (arcsin r) = sqrt (1 - (r ^2))
proof
let r be real number ; ::_thesis: ( - 1 <= r & r <= 1 implies cos (arcsin r) = sqrt (1 - (r ^2)) )
set s = sqrt (1 - (r ^2));
assume  ( - 1 <= r & r <= 1 ) ; ::_thesis: cos (arcsin r) = sqrt (1 - (r ^2))
then  (r ^2) + 0 <= 1 ^2 by SQUARE_1:49;
then  0 <= 1 - (r ^2) by XREAL_1:19;
then  ( 0 <= sqrt (1 - (r ^2)) & (r ^2) + ((sqrt (1 - (r ^2))) ^2) = (r ^2) + (1 - (r ^2)) ) by SQUARE_1:def_2;
hence  cos (arcsin r) = sqrt (1 - (r ^2)) by Th79; ::_thesis: verum
end;

theorem :: SIN_COS6:82
arcsin | [.(- 1),1.] is increasing
proof
set f = sin | [.(- (PI / 2)),(PI / 2).];
 ( (sin | [.(- (PI / 2)),(PI / 2).]) .: [.(- (PI / 2)),(PI / 2).] = [.(- 1),1.] & (((sin | [.(- (PI / 2)),(PI / 2).]) | [.(- (PI / 2)),(PI / 2).]) ") | ((sin | [.(- (PI / 2)),(PI / 2).]) .: [.(- (PI / 2)),(PI / 2).]) is increasing ) by Th45, COMPTRIG:23, FCONT_3:9, RELAT_1:129;
hence  arcsin | [.(- 1),1.] is increasing by RELAT_1:72; ::_thesis: verum
end;

theorem :: SIN_COS6:83
for r being real number holds
( arcsin is_differentiable_on ].(- 1),1.[ & ( - 1 < r & r < 1 implies diff (arcsin,r) = 1 / (sqrt (1 - (r ^2))) ) )
proof
let r be real number ; ::_thesis: ( arcsin is_differentiable_on ].(- 1),1.[ & ( - 1 < r & r < 1 implies diff (arcsin,r) = 1 / (sqrt (1 - (r ^2))) ) )
set g = arcsin | ].(- 1),1.[;
set h = sin | [.(- (PI / 2)),(PI / 2).];
set f = sin | ].(- (PI / 2)),(PI / 2).[;
A1: dom (sin | ].(- (PI / 2)),(PI / 2).[) = ].(- (PI / 2)),(PI / 2).[ /\ REAL by RELAT_1:61, SIN_COS:24
.= ].(- (PI / 2)),(PI / 2).[ by XBOOLE_1:28 ;
set x = arcsin . r;
set s = sqrt (1 - (r ^2));
A2: ].(- 1),1.[ c= dom arcsin by Th63, XXREAL_1:25;
A3: sin is_differentiable_on ].(- (PI / 2)),(PI / 2).[ by FDIFF_1:26, SIN_COS:68;
then A4: sin | ].(- (PI / 2)),(PI / 2).[ is_differentiable_on ].(- (PI / 2)),(PI / 2).[ by FDIFF_2:16;
A5: now__::_thesis:_for_x0_being_Real_st_x0_in_].(-_(PI_/_2)),(PI_/_2).[_holds_
0_<_diff_((sin_|_].(-_(PI_/_2)),(PI_/_2).[),x0)
let x0 be Real; ::_thesis: ( x0 in ].(- (PI / 2)),(PI / 2).[ implies 0 < diff ((sin | ].(- (PI / 2)),(PI / 2).[),x0) )
assume A6: x0 in ].(- (PI / 2)),(PI / 2).[ ; ::_thesis: 0 < diff ((sin | ].(- (PI / 2)),(PI / 2).[),x0)
diff ((sin | ].(- (PI / 2)),(PI / 2).[),x0) = ((sin | ].(- (PI / 2)),(PI / 2).[) `| ].(- (PI / 2)),(PI / 2).[) . x0 by A4, A6, FDIFF_1:def_7
.= (sin `| ].(- (PI / 2)),(PI / 2).[) . x0 by A3, FDIFF_2:16
.= diff (sin,x0) by A3, A6, FDIFF_1:def_7
.= cos . x0 by SIN_COS:68 ;
hence  0 < diff ((sin | ].(- (PI / 2)),(PI / 2).[),x0) by A6, COMPTRIG:11; ::_thesis: verum
end;
A7: (sin | ].(- (PI / 2)),(PI / 2).[) " = ((sin | [.(- (PI / 2)),(PI / 2).]) | ].(- (PI / 2)),(PI / 2).[) " by RELAT_1:74, XXREAL_1:25
.= ((sin | [.(- (PI / 2)),(PI / 2).]) ") | ((sin | [.(- (PI / 2)),(PI / 2).]) .: ].(- (PI / 2)),(PI / 2).[) by RFUNCT_2:17
.= arcsin | ].(- 1),1.[ by Th46, RELAT_1:129, XXREAL_1:25 ;
then A8: ( (sin | ].(- (PI / 2)),(PI / 2).[) | ].(- (PI / 2)),(PI / 2).[ = sin | ].(- (PI / 2)),(PI / 2).[ & dom ((sin | ].(- (PI / 2)),(PI / 2).[) ") = ].(- 1),1.[ ) by Th63, RELAT_1:62, RELAT_1:72, XXREAL_1:25;
then A9: arcsin | ].(- 1),1.[ is_differentiable_on ].(- 1),1.[ by A7, A4, A1, A5, FDIFF_2:48;
then  for x being Real st x in ].(- 1),1.[ holds
arcsin | ].(- 1),1.[ is_differentiable_in x by FDIFF_1:9;
hence A10: arcsin is_differentiable_on ].(- 1),1.[ by A2, FDIFF_1:def_6; ::_thesis: ( - 1 < r & r < 1 implies diff (arcsin,r) = 1 / (sqrt (1 - (r ^2))) )
assume A11: ( - 1 < r & r < 1 ) ; ::_thesis: diff (arcsin,r) = 1 / (sqrt (1 - (r ^2)))
then A12: r in ].(- 1),1.[ by XXREAL_1:4;
then A13: (arcsin | ].(- 1),1.[) . r = arcsin . r by FUNCT_1:49;
 arcsin . r = arcsin r ;
then  ( - (PI / 2) < arcsin . r & arcsin . r < PI / 2 ) by A11, Th77;
then A14: arcsin . r in ].(- (PI / 2)),(PI / 2).[ by XXREAL_1:4;
then A15: diff ((sin | ].(- (PI / 2)),(PI / 2).[),(arcsin . r)) = ((sin | ].(- (PI / 2)),(PI / 2).[) `| ].(- (PI / 2)),(PI / 2).[) . (arcsin . r) by A4, FDIFF_1:def_7
.= (sin `| ].(- (PI / 2)),(PI / 2).[) . (arcsin . r) by A3, FDIFF_2:16
.= diff (sin,(arcsin . r)) by A3, A14, FDIFF_1:def_7
.= cos . (arcsin . r) by SIN_COS:68
.= cos (arcsin r) by SIN_COS:def_19
.= sqrt (1 - (r ^2)) by A11, Th81 ;
thus  diff (arcsin,r) = (arcsin `| ].(- 1),1.[) . r by A10, A12, FDIFF_1:def_7
.= ((arcsin | ].(- 1),1.[) `| ].(- 1),1.[) . r by A10, FDIFF_2:16
.= diff ((arcsin | ].(- 1),1.[),r) by A9, A12, FDIFF_1:def_7
.= 1 / (sqrt (1 - (r ^2))) by A7, A8, A4, A1, A5, A12, A13, A15, FDIFF_2:48 ; ::_thesis: verum
end;

theorem :: SIN_COS6:84
arcsin | [.(- 1),1.] is continuous
proof
set f = sin | [.(- (PI / 2)),(PI / 2).];
 dom (sin | [.(- (PI / 2)),(PI / 2).]) = [.(- (PI / 2)),(PI / 2).] by RELAT_1:62, SIN_COS:24;
then  ( (sin | [.(- (PI / 2)),(PI / 2).]) | [.(- (PI / 2)),(PI / 2).] = sin | [.(- (PI / 2)),(PI / 2).] & (((sin | [.(- (PI / 2)),(PI / 2).]) | [.(- (PI / 2)),(PI / 2).]) ") | ((sin | [.(- (PI / 2)),(PI / 2).]) .: [.(- (PI / 2)),(PI / 2).]) is continuous ) by COMPTRIG:23, FCONT_1:47, RELAT_1:73;
hence  arcsin | [.(- 1),1.] is continuous by COMPTRIG:30, RELAT_1:115; ::_thesis: verum
end;

begin

definition
func arccos  ->  PartFunc of REAL,REAL equals :: SIN_COS6:def 3
(cos | [.0,PI.]) " ;
coherence
 (cos | [.0,PI.]) " is PartFunc of REAL,REAL ;
end;

:: deftheorem  defines arccos SIN_COS6:def_3_:_
 arccos = (cos | [.0,PI.]) " ;

definition
let r be set ;
func arccos r ->  set  equals :: SIN_COS6:def 4
arccos . r;
coherence
 arccos . r is set ;
end;

:: deftheorem  defines arccos SIN_COS6:def_4_:_
 for r being set holds arccos r = arccos . r;

definition
let r be set ;
:: original: arccos
redefine func arccos r ->  Real;
coherence
 arccos r is Real ;
end;

Lm16:  arccos " = cos | [.0,PI.]
by FUNCT_1:43;

theorem Th85: :: SIN_COS6:85
rng arccos = [.0,PI.]
proof
 dom (cos | [.0,PI.]) = [.0,PI.] by RELAT_1:62, SIN_COS:24;
hence  rng arccos = [.0,PI.] by FUNCT_1:33; ::_thesis: verum
end;

registration
cluster arccos  ->  one-to-one ;
coherence
 arccos is one-to-one ;
end;

theorem Th86: :: SIN_COS6:86
dom arccos = [.(- 1),1.] by COMPTRIG:32, FUNCT_1:33;

theorem Th87: :: SIN_COS6:87
(cos | [.0,PI.]) * arccos = id [.(- 1),1.] by COMPTRIG:32, FUNCT_1:39;

theorem :: SIN_COS6:88
arccos * (cos | [.0,PI.]) = id [.(- 1),1.] by COMPTRIG:32, FUNCT_1:39;

theorem Th89: :: SIN_COS6:89
(cos | [.0,PI.]) * arccos = id [.0,PI.] by Lm16, Th85, FUNCT_1:39;

theorem :: SIN_COS6:90
arccos * (cos | [.0,PI.]) = id [.0,PI.] by Lm16, Th85, FUNCT_1:39;

theorem Th91: :: SIN_COS6:91
for r being real number st - 1 <= r & r <= 1 holds
cos (arccos r) = r
proof
let r be real number ; ::_thesis: ( - 1 <= r & r <= 1 implies cos (arccos r) = r )
assume  ( - 1 <= r & r <= 1 ) ; ::_thesis: cos (arccos r) = r
then A1: r in [.(- 1),1.] by XXREAL_1:1;
then A2: arccos . r in [.0,PI.] by Th85, Th86, FUNCT_1:def_3;
thus  cos (arccos r) = cos . (arccos . r) by SIN_COS:def_19
.= (cos | [.0,PI.]) . (arccos . r) by A2, FUNCT_1:49
.= (id [.(- 1),1.]) . r by A1, Th86, Th87, FUNCT_1:13
.= r by A1, FUNCT_1:18 ; ::_thesis: verum
end;

theorem Th92: :: SIN_COS6:92
for r being real number st 0 <= r & r <= PI holds
arccos (cos r) = r
proof
let r be real number ; ::_thesis: ( 0 <= r & r <= PI implies arccos (cos r) = r )
A1: dom (cos | [.0,PI.]) = [.0,PI.] by RELAT_1:62, SIN_COS:24;
assume  ( 0 <= r & r <= PI ) ; ::_thesis: arccos (cos r) = r
then A2: r in [.0,PI.] by XXREAL_1:1;
thus  arccos (cos r) = arccos . (cos . r) by SIN_COS:def_19
.= arccos . ((cos | [.0,PI.]) . r) by A2, FUNCT_1:49
.= (id [.0,PI.]) . r by A2, A1, Th89, FUNCT_1:13
.= r by A2, FUNCT_1:18 ; ::_thesis: verum
end;

theorem :: SIN_COS6:93
arccos (- 1) = PI by Th92, SIN_COS:77;

theorem :: SIN_COS6:94
arccos 0 = PI / 2 by Lm6, Th92, SIN_COS:77;

theorem :: SIN_COS6:95
arccos 1 = 0 by Th92, SIN_COS:31;

theorem :: SIN_COS6:96
for r being real number st - 1 <= r & r <= 1 & arccos r = 0 holds
r = 1 by Th91, SIN_COS:31;

theorem :: SIN_COS6:97
for r being real number st - 1 <= r & r <= 1 & arccos r = PI / 2 holds
r = 0 by Th91, SIN_COS:77;

theorem :: SIN_COS6:98
for r being real number st - 1 <= r & r <= 1 & arccos r = PI holds
r = - 1 by Th91, SIN_COS:77;

theorem Th99: :: SIN_COS6:99
for r being real number st - 1 <= r & r <= 1 holds
( 0 <= arccos r & arccos r <= PI )
proof
let r be real number ; ::_thesis: ( - 1 <= r & r <= 1 implies ( 0 <= arccos r & arccos r <= PI ) )
assume  ( - 1 <= r & r <= 1 ) ; ::_thesis: ( 0 <= arccos r & arccos r <= PI )
then  r in [.(- 1),1.] by XXREAL_1:1;
then  arccos . r in rng arccos by Th86, FUNCT_1:def_3;
hence  ( 0 <= arccos r & arccos r <= PI ) by Th85, XXREAL_1:1; ::_thesis: verum
end;

theorem Th100: :: SIN_COS6:100
for r being real number st - 1 < r & r < 1 holds
( 0 < arccos r & arccos r < PI )
proof
let r be real number ; ::_thesis: ( - 1 < r & r < 1 implies ( 0 < arccos r & arccos r < PI ) )
assume A1: ( - 1 < r & r < 1 ) ; ::_thesis: ( 0 < arccos r & arccos r < PI )
then  arccos r <= PI by Th99;
then  ( ( 0 < arccos r & arccos r < PI ) or 0 = arccos r or arccos r = PI ) by A1, Th99, XXREAL_0:1;
hence  ( 0 < arccos r & arccos r < PI ) by A1, Th91, SIN_COS:31, SIN_COS:77; ::_thesis: verum
end;

theorem Th101: :: SIN_COS6:101
for r being real number st - 1 <= r & r <= 1 holds
arccos r = PI - (arccos (- r))
proof
let r be real number ; ::_thesis: ( - 1 <= r & r <= 1 implies arccos r = PI - (arccos (- r)) )
assume  ( - 1 <= r & r <= 1 ) ; ::_thesis: arccos r = PI - (arccos (- r))
then A1: ( - (- 1) >= - r & - r >= - 1 ) by XREAL_1:24;
then  0 + (arccos (- r)) <= PI by Th99;
then A2: 0 <= PI - (arccos (- r)) by XREAL_1:19;
 0 <= arccos (- r) by A1, Th99;
then  PI + 0 <= PI + (arccos (- r)) by XREAL_1:6;
then A3: PI - (arccos (- r)) <= PI by XREAL_1:20;
r = (- 1) * (- r)
.= ((cos PI) * (cos (arccos (- r)))) + ((sin PI) * (sin (arccos (- r)))) by A1, Th91, SIN_COS:77
.= cos (PI - (arccos (- r))) by COMPLEX2:3 ;
hence  arccos r = PI - (arccos (- r)) by A2, A3, Th92; ::_thesis: verum
end;

theorem Th102: :: SIN_COS6:102
for s, r being real number st 0 <= s & (r ^2) + (s ^2) = 1 holds
sin (arccos r) = s
proof
let s, r be real number ; ::_thesis: ( 0 <= s & (r ^2) + (s ^2) = 1 implies sin (arccos r) = s )
set x = arccos r;
assume that
A1: 0 <= s and
A2: (r ^2) + (s ^2) = 1 ; ::_thesis: sin (arccos r) = s
A3: ( - 1 <= r & r <= 1 ) by A2, Lm5;
then  ( 0 <= arccos r & arccos r <= PI ) by Th99;
then A4: arccos r in [.0,PI.] by XXREAL_1:1;
 ((sin . (arccos r)) ^2) + ((cos . (arccos r)) ^2) = 1 by SIN_COS:28;
then (sin . (arccos r)) ^2 = 1 - ((cos . (arccos r)) ^2)
.= 1 - ((cos (arccos r)) ^2) by SIN_COS:def_19
.= 1 - (r ^2) by A3, Th91 ;
then A5: ( sin . (arccos r) = s or sin . (arccos r) = - s ) by A2, SQUARE_1:40;
 ( - (- (- s)) < 0 or s = 0 ) by A1;
hence  sin (arccos r) = s by A5, A4, COMPTRIG:8, SIN_COS:def_17; ::_thesis: verum
end;

theorem :: SIN_COS6:103
for s, r being real number st s <= 0 & (r ^2) + (s ^2) = 1 holds
sin (arccos r) = - s
proof
let s, r be real number ; ::_thesis: ( s <= 0 & (r ^2) + (s ^2) = 1 implies sin (arccos r) = - s )
set x = arccos r;
assume that
A1: s <= 0 and
A2: (r ^2) + (s ^2) = 1 ; ::_thesis: sin (arccos r) = - s
A3: ( - 1 <= r & r <= 1 ) by A2, Lm5;
then  ( 0 <= arccos r & arccos r <= PI ) by Th99;
then A4: arccos r in [.0,PI.] by XXREAL_1:1;
 ((sin . (arccos r)) ^2) + ((cos . (arccos r)) ^2) = 1 by SIN_COS:28;
then (sin . (arccos r)) ^2 = 1 - ((cos . (arccos r)) ^2)
.= 1 - ((cos (arccos r)) ^2) by SIN_COS:def_19
.= 1 - (r ^2) by A3, Th91 ;
then A5: ( sin . (arccos r) = s or sin . (arccos r) = - s ) by A2, SQUARE_1:40;
 ( 0 > s or s = 0 ) by A1;
hence  sin (arccos r) = - s by A5, A4, COMPTRIG:8, SIN_COS:def_17; ::_thesis: verum
end;

theorem Th104: :: SIN_COS6:104
for r being real number st - 1 <= r & r <= 1 holds
sin (arccos r) = sqrt (1 - (r ^2))
proof
let r be real number ; ::_thesis: ( - 1 <= r & r <= 1 implies sin (arccos r) = sqrt (1 - (r ^2)) )
set s = sqrt (1 - (r ^2));
assume  ( - 1 <= r & r <= 1 ) ; ::_thesis: sin (arccos r) = sqrt (1 - (r ^2))
then  (r ^2) + 0 <= 1 ^2 by SQUARE_1:49;
then  0 <= 1 - (r ^2) by XREAL_1:19;
then  ( 0 <= sqrt (1 - (r ^2)) & (r ^2) + ((sqrt (1 - (r ^2))) ^2) = (r ^2) + (1 - (r ^2)) ) by SQUARE_1:def_2;
hence  sin (arccos r) = sqrt (1 - (r ^2)) by Th102; ::_thesis: verum
end;

theorem :: SIN_COS6:105
arccos | [.(- 1),1.] is decreasing
proof
set f = cos | [.0,PI.];
 ( (cos | [.0,PI.]) .: [.0,PI.] = [.(- 1),1.] & (((cos | [.0,PI.]) | [.0,PI.]) ") | ((cos | [.0,PI.]) .: [.0,PI.]) is decreasing ) by Th49, COMPTRIG:25, FCONT_3:10, RELAT_1:129;
hence  arccos | [.(- 1),1.] is decreasing by RELAT_1:72; ::_thesis: verum
end;

theorem :: SIN_COS6:106
for r being real number holds
( arccos is_differentiable_on ].(- 1),1.[ & ( - 1 < r & r < 1 implies diff (arccos,r) = - (1 / (sqrt (1 - (r ^2)))) ) )
proof
let r be real number ; ::_thesis: ( arccos is_differentiable_on ].(- 1),1.[ & ( - 1 < r & r < 1 implies diff (arccos,r) = - (1 / (sqrt (1 - (r ^2)))) ) )
set g = arccos | ].(- 1),1.[;
set h = cos | [.0,PI.];
set f = cos | ].0,PI.[;
A1: dom (cos | ].0,PI.[) = ].0,PI.[ /\ REAL by RELAT_1:61, SIN_COS:24
.= ].0,PI.[ by XBOOLE_1:28 ;
set x = arccos . r;
set s = sqrt (1 - (r ^2));
A2: ].(- 1),1.[ c= dom arccos by Th86, XXREAL_1:25;
A3: cos is_differentiable_on ].0,PI.[ by FDIFF_1:26, SIN_COS:67;
then A4: cos | ].0,PI.[ is_differentiable_on ].0,PI.[ by FDIFF_2:16;
A5: now__::_thesis:_for_x0_being_Real_st_x0_in_].0,PI.[_holds_
0_>_diff_((cos_|_].0,PI.[),x0)
let x0 be Real; ::_thesis: ( x0 in ].0,PI.[ implies 0 > diff ((cos | ].0,PI.[),x0) )
assume A6: x0 in ].0,PI.[ ; ::_thesis: 0 > diff ((cos | ].0,PI.[),x0)
A7: - (- (sin . x0)) > 0 by A6, COMPTRIG:7;
diff ((cos | ].0,PI.[),x0) = ((cos | ].0,PI.[) `| ].0,PI.[) . x0 by A4, A6, FDIFF_1:def_7
.= (cos `| ].0,PI.[) . x0 by A3, FDIFF_2:16
.= diff (cos,x0) by A3, A6, FDIFF_1:def_7
.= - (sin . x0) by SIN_COS:67 ;
hence  0 > diff ((cos | ].0,PI.[),x0) by A7; ::_thesis: verum
end;
A8: (cos | ].0,PI.[) " = ((cos | [.0,PI.]) | ].0,PI.[) " by RELAT_1:74, XXREAL_1:25
.= ((cos | [.0,PI.]) ") | ((cos | [.0,PI.]) .: ].0,PI.[) by RFUNCT_2:17
.= arccos | ].(- 1),1.[ by Th50, RELAT_1:129, XXREAL_1:25 ;
then A9: ( (cos | ].0,PI.[) | ].0,PI.[ = cos | ].0,PI.[ & dom ((cos | ].0,PI.[) ") = ].(- 1),1.[ ) by Th86, RELAT_1:62, RELAT_1:72, XXREAL_1:25;
then A10: arccos | ].(- 1),1.[ is_differentiable_on ].(- 1),1.[ by A8, A4, A1, A5, FDIFF_2:48;
then  for x being Real st x in ].(- 1),1.[ holds
arccos | ].(- 1),1.[ is_differentiable_in x by FDIFF_1:9;
hence A11: arccos is_differentiable_on ].(- 1),1.[ by A2, FDIFF_1:def_6; ::_thesis: ( - 1 < r & r < 1 implies diff (arccos,r) = - (1 / (sqrt (1 - (r ^2)))) )
assume A12: ( - 1 < r & r < 1 ) ; ::_thesis: diff (arccos,r) = - (1 / (sqrt (1 - (r ^2))))
then A13: r in ].(- 1),1.[ by XXREAL_1:4;
then A14: (arccos | ].(- 1),1.[) . r = arccos . r by FUNCT_1:49;
 arccos . r = arccos r ;
then  ( 0 < arccos . r & arccos . r < PI ) by A12, Th100;
then A15: arccos . r in ].0,PI.[ by XXREAL_1:4;
then A16: diff ((cos | ].0,PI.[),(arccos . r)) = ((cos | ].0,PI.[) `| ].0,PI.[) . (arccos . r) by A4, FDIFF_1:def_7
.= (cos `| ].0,PI.[) . (arccos . r) by A3, FDIFF_2:16
.= diff (cos,(arccos . r)) by A3, A15, FDIFF_1:def_7
.= - (sin . (arccos . r)) by SIN_COS:67
.= - (sin (arccos r)) by SIN_COS:def_17
.= - (sqrt (1 - (r ^2))) by A12, Th104 ;
thus  diff (arccos,r) = (arccos `| ].(- 1),1.[) . r by A11, A13, FDIFF_1:def_7
.= ((arccos | ].(- 1),1.[) `| ].(- 1),1.[) . r by A11, FDIFF_2:16
.= diff ((arccos | ].(- 1),1.[),r) by A10, A13, FDIFF_1:def_7
.= 1 / (- (sqrt (1 - (r ^2)))) by A8, A9, A4, A1, A5, A13, A14, A16, FDIFF_2:48
.= (- 1) / (sqrt (1 - (r ^2))) by XCMPLX_1:192
.= - (1 / (sqrt (1 - (r ^2)))) by XCMPLX_1:187 ; ::_thesis: verum
end;

theorem :: SIN_COS6:107
arccos | [.(- 1),1.] is continuous
proof
set f = cos | [.0,PI.];
 dom (cos | [.0,PI.]) = [.0,PI.] by RELAT_1:62, SIN_COS:24;
then  ( (cos | [.0,PI.]) | [.0,PI.] = cos | [.0,PI.] & (((cos | [.0,PI.]) | [.0,PI.]) ") | ((cos | [.0,PI.]) .: [.0,PI.]) is continuous ) by COMPTRIG:25, FCONT_1:47, RELAT_1:73;
hence  arccos | [.(- 1),1.] is continuous by COMPTRIG:32, RELAT_1:115; ::_thesis: verum
end;

theorem Th108: :: SIN_COS6:108
for r being real number st - 1 <= r & r <= 1 holds
(arcsin r) + (arccos r) = PI / 2
proof
let r be real number ; ::_thesis: ( - 1 <= r & r <= 1 implies (arcsin r) + (arccos r) = PI / 2 )
assume A1: ( - 1 <= r & r <= 1 ) ; ::_thesis: (arcsin r) + (arccos r) = PI / 2
then  (- (PI / 2)) + (PI / 2) <= arccos r by Th99;
then  - (PI / 2) <= (arccos r) - (PI / 2) by XREAL_1:19;
then A2: - (- (PI / 2)) >= - ((arccos r) - (PI / 2)) by XREAL_1:24;
 arccos r <= (PI / 2) + (PI / 2) by A1, Th99;
then  (arccos r) - (PI / 2) <= PI / 2 by XREAL_1:20;
then A3: - ((arccos r) - (PI / 2)) >= - (PI / 2) by XREAL_1:24;
r = ((sin (PI / 2)) * (cos (arccos r))) - ((cos (PI / 2)) * (sin (arccos r))) by A1, Th91, SIN_COS:77
.= sin ((PI / 2) - (arccos r)) by COMPLEX2:3 ;
then  arcsin r = (PI / 2) - (arccos r) by A2, A3, Th69;
hence  (arcsin r) + (arccos r) = PI / 2 ; ::_thesis: verum
end;

theorem :: SIN_COS6:109
for r being real number st - 1 <= r & r <= 1 holds
(arccos (- r)) - (arcsin r) = PI / 2
proof
let r be real number ; ::_thesis: ( - 1 <= r & r <= 1 implies (arccos (- r)) - (arcsin r) = PI / 2 )
assume A1: ( - 1 <= r & r <= 1 ) ; ::_thesis: (arccos (- r)) - (arcsin r) = PI / 2
then A2: (arcsin r) + (arccos r) = (PI / 2) + 0 by Th108;
 ( - (- 1) >= - r & - r >= - 1 ) by A1, XREAL_1:24;
then  arccos (- r) = PI - (arccos (- (- r))) by Th101
.= (arcsin r) + (PI / 2) by A2 ;
hence  (arccos (- r)) - (arcsin r) = PI / 2 ; ::_thesis: verum
end;

theorem :: SIN_COS6:110
for r being real number st - 1 <= r & r <= 1 holds
(arccos r) - (arcsin (- r)) = PI / 2
proof
let r be real number ; ::_thesis: ( - 1 <= r & r <= 1 implies (arccos r) - (arcsin (- r)) = PI / 2 )
assume A1: ( - 1 <= r & r <= 1 ) ; ::_thesis: (arccos r) - (arcsin (- r)) = PI / 2
then A2: (arcsin r) + (arccos r) = (PI / 2) + 0 by Th108;
 ( - (- 1) >= - r & - r >= - 1 ) by A1, XREAL_1:24;
then  arcsin (- r) = - (arcsin (- (- r))) by Th78
.= (arccos r) - (PI / 2) by A2 ;
hence  (arccos r) - (arcsin (- r)) = PI / 2 ; ::_thesis: verum
end;