:: SIN_COS6 semantic presentation

theorem Th1: :: SIN_COS6:1
for b1, b2 being real number st 0 <= b1 & b1 < b2 holds
[\(b1 / b2)/] = 0
proof end;

theorem Th2: :: SIN_COS6:2
for b1 being Function
for b2, b3 being set st b1 | b2 is one-to-one & b3 c= b2 holds
b1 | b3 is one-to-one
proof end;

theorem Th3: :: SIN_COS6:3
for b1 being real number holds - 1 <= sin b1
proof end;

theorem Th4: :: SIN_COS6:4
for b1 being real number holds sin b1 <= 1
proof end;

theorem Th5: :: SIN_COS6:5
for b1 being real number holds - 1 <= cos b1
proof end;

theorem Th6: :: SIN_COS6:6
for b1 being real number holds cos b1 <= 1
proof end;

deffunc H1( Integer) -> set = (2 * PI ) * a1;

Lemma7: dom sin = REAL
by SIN_COS:def 20;

Lemma8: dom cos = REAL
by SIN_COS:def 22;

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

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

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

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

Lemma13: for b1, b2 being real number st (b1 ^2 ) + (b2 ^2 ) = 1 holds
( - 1 <= b1 & b1 <= 1 )
proof end;

registration
cluster PI -> positive ;
coherence
PI is positive
proof end;
end;

Lemma14: - (PI / 2) < - 0
by XREAL_1:26;

then Lemma15: - (PI / 2) < PI / 2
;

Lemma16: PI / 2 < PI / 1
by REAL_2:200;

Lemma17: 1 * PI < (3 / 2) * PI
by XREAL_1:70;

Lemma18: 0 + H1(1) < (PI / 2) + H1(1)
by XREAL_1:8;

Lemma19: (3 / 2) * PI < 2 * PI
by XREAL_1:70;

Lemma20: 1 * PI < 2 * PI
by XREAL_1:70;

Lemma21: ].(- 1),1.[ c= [.(- 1),1.]
by RCOMP_1:15;

Lemma22: ].(- (PI / 2)),0.[ c= [.(- (PI / 2)),0.]
by RCOMP_1:15;

Lemma23: ].(- (PI / 2)),(PI / 2).[ c= [.(- (PI / 2)),(PI / 2).]
by RCOMP_1:15;

Lemma24: ].0,(PI / 2).[ c= [.0,(PI / 2).]
by RCOMP_1:15;

Lemma25: ].0,PI .[ c= [.0,PI .]
by RCOMP_1:15;

Lemma26: ].(PI / 2),PI .[ c= [.(PI / 2),PI .]
by RCOMP_1:15;

Lemma27: ].(PI / 2),((3 / 2) * PI ).[ c= [.(PI / 2),((3 / 2) * PI ).]
by RCOMP_1:15;

Lemma28: ].PI ,((3 / 2) * PI ).[ c= [.PI ,((3 / 2) * PI ).]
by RCOMP_1:15;

Lemma29: ].PI ,(2 * PI ).[ c= [.PI ,(2 * PI ).]
by RCOMP_1:15;

Lemma30: ].((3 / 2) * PI ),(2 * PI ).[ c= [.((3 / 2) * PI ),(2 * PI ).]
by RCOMP_1:15;

Lemma31: [.(- (PI / 2)),0.] c= [.(- (PI / 2)),(PI / 2).]
by TREAL_1:1;

Lemma32: [.0,(PI / 2).] c= [.(- (PI / 2)),(PI / 2).]
by Lemma14, TREAL_1:1;

Lemma33: [.0,(PI / 2).] c= [.0,PI .]
by Lemma16, TREAL_1:1;

Lemma34: [.(PI / 2),PI .] c= [.(PI / 2),((3 / 2) * PI ).]
by Lemma17, TREAL_1:1;

Lemma35: [.(PI / 2),PI .] c= [.0,PI .]
by TREAL_1:1;

Lemma36: [.PI ,((3 / 2) * PI ).] c= [.(PI / 2),((3 / 2) * PI ).]
by Lemma16, TREAL_1:1;

Lemma37: [.PI ,((3 / 2) * PI ).] c= [.PI ,(2 * PI ).]
by Lemma19, TREAL_1:1;

Lemma38: [.((3 / 2) * PI ),(2 * PI ).] c= [.((- (PI / 2)) + H1(1)),((PI / 2) + H1(1)).]
by Lemma18, TREAL_1:1;

Lemma39: [.((3 / 2) * PI ),(2 * PI ).] c= [.PI ,(2 * PI ).]
by Lemma17, TREAL_1:1;

theorem Th7: :: SIN_COS6:7
( sin (- (PI / 2)) = - 1 & sin . (- (PI / 2)) = - 1 )
proof end;

theorem Th8: :: SIN_COS6:8
for b1 being real number
for b2 being integer number holds sin . b1 = sin . (b1 + ((2 * PI ) * b2))
proof end;

theorem Th9: :: SIN_COS6:9
( cos (- (PI / 2)) = 0 & cos . (- (PI / 2)) = 0 )
proof end;

theorem Th10: :: SIN_COS6:10
for b1 being real number
for b2 being integer number holds cos . b1 = cos . (b1 + ((2 * PI ) * b2))
proof end;

theorem Th11: :: SIN_COS6:11
for b1 being real number
for b2 being integer number st (2 * PI ) * b2 < b1 & b1 < PI + ((2 * PI ) * b2) holds
sin b1 > 0
proof end;

theorem Th12: :: SIN_COS6:12
for b1 being real number
for b2 being integer number st PI + ((2 * PI ) * b2) < b1 & b1 < (2 * PI ) + ((2 * PI ) * b2) holds
sin b1 < 0
proof end;

theorem Th13: :: SIN_COS6:13
for b1 being real number
for b2 being integer number st (- (PI / 2)) + ((2 * PI ) * b2) < b1 & b1 < (PI / 2) + ((2 * PI ) * b2) holds
cos b1 > 0
proof end;

theorem Th14: :: SIN_COS6:14
for b1 being real number
for b2 being integer number st (PI / 2) + ((2 * PI ) * b2) < b1 & b1 < ((3 / 2) * PI ) + ((2 * PI ) * b2) holds
cos b1 < 0
proof end;

theorem Th15: :: SIN_COS6:15
for b1 being real number
for b2 being integer number st ((3 / 2) * PI ) + ((2 * PI ) * b2) < b1 & b1 < (2 * PI ) + ((2 * PI ) * b2) holds
cos b1 > 0
proof end;

theorem Th16: :: SIN_COS6:16
for b1 being real number
for b2 being integer number st (2 * PI ) * b2 <= b1 & b1 <= PI + ((2 * PI ) * b2) holds
sin b1 >= 0
proof end;

theorem Th17: :: SIN_COS6:17
for b1 being real number
for b2 being integer number st PI + ((2 * PI ) * b2) <= b1 & b1 <= (2 * PI ) + ((2 * PI ) * b2) holds
sin b1 <= 0
proof end;

theorem Th18: :: SIN_COS6:18
for b1 being real number
for b2 being integer number st (- (PI / 2)) + ((2 * PI ) * b2) <= b1 & b1 <= (PI / 2) + ((2 * PI ) * b2) holds
cos b1 >= 0
proof end;

theorem Th19: :: SIN_COS6:19
for b1 being real number
for b2 being integer number st (PI / 2) + ((2 * PI ) * b2) <= b1 & b1 <= ((3 / 2) * PI ) + ((2 * PI ) * b2) holds
cos b1 <= 0
proof end;

theorem Th20: :: SIN_COS6:20
for b1 being real number
for b2 being integer number st ((3 / 2) * PI ) + ((2 * PI ) * b2) <= b1 & b1 <= (2 * PI ) + ((2 * PI ) * b2) holds
cos b1 >= 0
proof end;

theorem Th21: :: SIN_COS6:21
for b1 being real number
for b2 being integer number st (2 * PI ) * b2 <= b1 & b1 < (2 * PI ) + ((2 * PI ) * b2) & sin b1 = 0 & not b1 = (2 * PI ) * b2 holds
b1 = PI + ((2 * PI ) * b2)
proof end;

theorem Th22: :: SIN_COS6:22
for b1 being real number
for b2 being integer number st (2 * PI ) * b2 <= b1 & b1 < (2 * PI ) + ((2 * PI ) * b2) & cos b1 = 0 & not b1 = (PI / 2) + ((2 * PI ) * b2) holds
b1 = ((3 / 2) * PI ) + ((2 * PI ) * b2)
proof end;

theorem Th23: :: SIN_COS6:23
for b1 being real number st sin b1 = - 1 holds
b1 = ((3 / 2) * PI ) + ((2 * PI ) * [\(b1 / (2 * PI ))/])
proof end;

theorem Th24: :: SIN_COS6:24
for b1 being real number st sin b1 = 1 holds
b1 = (PI / 2) + ((2 * PI ) * [\(b1 / (2 * PI ))/])
proof end;

theorem Th25: :: SIN_COS6:25
for b1 being real number st cos b1 = - 1 holds
b1 = PI + ((2 * PI ) * [\(b1 / (2 * PI ))/])
proof end;

theorem Th26: :: SIN_COS6:26
for b1 being real number st cos b1 = 1 holds
b1 = (2 * PI ) * [\(b1 / (2 * PI ))/]
proof end;

theorem Th27: :: SIN_COS6:27
for b1 being real number st 0 <= b1 & b1 <= 2 * PI & sin b1 = - 1 holds
b1 = (3 / 2) * PI
proof end;

theorem Th28: :: SIN_COS6:28
for b1 being real number st 0 <= b1 & b1 <= 2 * PI & sin b1 = 1 holds
b1 = PI / 2
proof end;

theorem Th29: :: SIN_COS6:29
for b1 being real number st 0 <= b1 & b1 <= 2 * PI & cos b1 = - 1 holds
b1 = PI
proof end;

theorem Th30: :: SIN_COS6:30
for b1 being real number st 0 <= b1 & b1 < PI / 2 holds
sin b1 < 1
proof end;

theorem Th31: :: SIN_COS6:31
for b1 being real number st 0 <= b1 & b1 < (3 / 2) * PI holds
sin b1 > - 1
proof end;

theorem Th32: :: SIN_COS6:32
for b1 being real number st (3 / 2) * PI < b1 & b1 <= 2 * PI holds
sin b1 > - 1
proof end;

theorem Th33: :: SIN_COS6:33
for b1 being real number st PI / 2 < b1 & b1 <= 2 * PI holds
sin b1 < 1
proof end;

theorem Th34: :: SIN_COS6:34
for b1 being real number st 0 < b1 & b1 < 2 * PI holds
cos b1 < 1
proof end;

theorem Th35: :: SIN_COS6:35
for b1 being real number st 0 <= b1 & b1 < PI holds
cos b1 > - 1
proof end;

theorem Th36: :: SIN_COS6:36
for b1 being real number st PI < b1 & b1 <= 2 * PI holds
cos b1 > - 1
proof end;

theorem Th37: :: SIN_COS6:37
for b1 being real number
for b2 being integer number st (2 * PI ) * b2 <= b1 & b1 < (PI / 2) + ((2 * PI ) * b2) holds
sin b1 < 1
proof end;

theorem Th38: :: SIN_COS6:38
for b1 being real number
for b2 being integer number st (2 * PI ) * b2 <= b1 & b1 < ((3 / 2) * PI ) + ((2 * PI ) * b2) holds
sin b1 > - 1
proof end;

theorem Th39: :: SIN_COS6:39
for b1 being real number
for b2 being integer number st ((3 / 2) * PI ) + ((2 * PI ) * b2) < b1 & b1 <= (2 * PI ) + ((2 * PI ) * b2) holds
sin b1 > - 1
proof end;

theorem Th40: :: SIN_COS6:40
for b1 being real number
for b2 being integer number st (PI / 2) + ((2 * PI ) * b2) < b1 & b1 <= (2 * PI ) + ((2 * PI ) * b2) holds
sin b1 < 1
proof end;

theorem Th41: :: SIN_COS6:41
for b1 being real number
for b2 being integer number st (2 * PI ) * b2 < b1 & b1 < (2 * PI ) + ((2 * PI ) * b2) holds
cos b1 < 1
proof end;

theorem Th42: :: SIN_COS6:42
for b1 being real number
for b2 being integer number st (2 * PI ) * b2 <= b1 & b1 < PI + ((2 * PI ) * b2) holds
cos b1 > - 1
proof end;

theorem Th43: :: SIN_COS6:43
for b1 being real number
for b2 being integer number st PI + ((2 * PI ) * b2) < b1 & b1 <= (2 * PI ) + ((2 * PI ) * b2) holds
cos b1 > - 1
proof end;

theorem Th44: :: SIN_COS6:44
for b1 being real number st cos ((2 * PI ) * b1) = 1 holds
b1 in INT
proof end;

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

theorem Th46: :: SIN_COS6:46
sin .: ].(- (PI / 2)),(PI / 2).[ = ].(- 1),1.[
proof end;

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

theorem Th48: :: SIN_COS6:48
sin .: ].(PI / 2),((3 / 2) * PI ).[ = ].(- 1),1.[
proof end;

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

theorem Th50: :: SIN_COS6:50
cos .: ].0,PI .[ = ].(- 1),1.[
proof end;

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

theorem Th52: :: SIN_COS6:52
cos .: ].PI ,(2 * PI ).[ = ].(- 1),1.[
proof end;

E69: now
let c1 be integer number ;
let c2 be real number ;
let c3, c4 be real number ;
assume c2 in [.(c3 + H1(c1)),(c4 + H1(c1)).] ;
then ( c3 + H1(c1) <= c2 & c2 <= c4 + H1(c1) ) by RCOMP_1:48;
then ( (c3 + H1(c1)) + (2 * PI ) <= c2 + (2 * PI ) & c2 + (2 * PI ) <= (c4 + H1(c1)) + (2 * PI ) ) by XREAL_1:8;
hence c2 + (2 * PI ) in [.(c3 + H1(c1 + 1)),(c4 + H1(c1 + 1)).] by RCOMP_1:48;
end;

E70: now
let c1 be integer number ;
let c2 be real number ;
let c3, c4 be real number ;
assume c2 in [.(c3 + H1(c1)),(c4 + H1(c1)).] /\ REAL ;
then ( c2 in [.(c3 + H1(c1)),(c4 + H1(c1)).] & c2 in REAL ) by XBOOLE_0:def 3;
then ( c2 + (2 * PI ) in [.(c3 + H1(c1 + 1)),(c4 + H1(c1 + 1)).] & c2 + (2 * PI ) in REAL ) by Lemma69, XREAL_0:def 1;
hence c2 + (2 * PI ) in [.(c3 + H1(c1 + 1)),(c4 + H1(c1 + 1)).] /\ REAL by XBOOLE_0:def 3;
end;

E71: now
let c1 be integer number ;
let c2 be real number ;
let c3, c4 be real number ;
assume c2 in [.(c3 + H1(c1)),(c4 + H1(c1)).] ;
then ( c3 + H1(c1) <= c2 & c2 <= c4 + H1(c1) ) by RCOMP_1:48;
then ( (c3 + H1(c1)) - (2 * PI ) <= c2 - (2 * PI ) & c2 - (2 * PI ) <= (c4 + H1(c1)) - (2 * PI ) ) by XREAL_1:11;
hence c2 - (2 * PI ) in [.(c3 + H1(c1 - 1)),(c4 + H1(c1 - 1)).] by RCOMP_1:48;
end;

E72: now
let c1 be integer number ;
let c2 be real number ;
let c3, c4 be real number ;
assume c2 in [.(c3 + H1(c1)),(c4 + H1(c1)).] /\ REAL ;
then ( c2 in [.(c3 + H1(c1)),(c4 + H1(c1)).] & c2 in REAL ) by XBOOLE_0:def 3;
then ( c2 - (2 * PI ) in [.(c3 + H1(c1 - 1)),(c4 + H1(c1 - 1)).] & c2 - (2 * PI ) in REAL ) by Lemma71, XREAL_0:def 1;
hence c2 - (2 * PI ) in [.(c3 + H1(c1 - 1)),(c4 + H1(c1 - 1)).] /\ REAL by XBOOLE_0:def 3;
end;

theorem Th53: :: SIN_COS6:53
for b1 being integer number holds sin is_increasing_on [.((- (PI / 2)) + ((2 * PI ) * b1)),((PI / 2) + ((2 * PI ) * b1)).]
proof end;

theorem Th54: :: SIN_COS6:54
for b1 being integer number holds sin is_decreasing_on [.((PI / 2) + ((2 * PI ) * b1)),(((3 / 2) * PI ) + ((2 * PI ) * b1)).]
proof end;

theorem Th55: :: SIN_COS6:55
for b1 being integer number holds cos is_decreasing_on [.((2 * PI ) * b1),(PI + ((2 * PI ) * b1)).]
proof end;

theorem Th56: :: SIN_COS6:56
for b1 being integer number holds cos is_increasing_on [.(PI + ((2 * PI ) * b1)),((2 * PI ) + ((2 * PI ) * b1)).]
proof end;

theorem Th57: :: SIN_COS6:57
for b1 being integer number holds sin | [.((- (PI / 2)) + ((2 * PI ) * b1)),((PI / 2) + ((2 * PI ) * b1)).] is one-to-one
proof end;

theorem Th58: :: SIN_COS6:58
for b1 being integer number holds sin | [.((PI / 2) + ((2 * PI ) * b1)),(((3 / 2) * PI ) + ((2 * PI ) * b1)).] is one-to-one
proof end;

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

registration
cluster sin | [.(- (PI / 2)),0.] -> one-to-one ;
coherence
sin | [.(- (PI / 2)),0.] is one-to-one
proof end;
cluster sin | [.0,(PI / 2).] -> one-to-one ;
coherence
sin | [.0,(PI / 2).] is one-to-one
proof end;
cluster sin | [.(PI / 2),PI .] -> one-to-one ;
coherence
sin | [.(PI / 2),PI .] is one-to-one
proof end;
cluster sin | [.PI ,((3 / 2) * PI ).] -> one-to-one ;
coherence
sin | [.PI ,((3 / 2) * PI ).] is one-to-one
proof end;
cluster sin | [.((3 / 2) * PI ),(2 * PI ).] -> one-to-one ;
coherence
sin | [.((3 / 2) * PI ),(2 * PI ).] is one-to-one
proof end;
end;

registration
cluster sin | ].(- (PI / 2)),(PI / 2).[ -> one-to-one ;
coherence
sin | ].(- (PI / 2)),(PI / 2).[ is one-to-one
proof end;
cluster sin | ].(PI / 2),((3 / 2) * PI ).[ -> one-to-one ;
coherence
sin | ].(PI / 2),((3 / 2) * PI ).[ is one-to-one
proof end;
cluster sin | ].(- (PI / 2)),0.[ -> one-to-one ;
coherence
sin | ].(- (PI / 2)),0.[ is one-to-one
proof end;
cluster sin | ].0,(PI / 2).[ -> one-to-one ;
coherence
sin | ].0,(PI / 2).[ is one-to-one
proof end;
cluster sin | ].(PI / 2),PI .[ -> one-to-one ;
coherence
sin | ].(PI / 2),PI .[ is one-to-one
proof end;
cluster sin | ].PI ,((3 / 2) * PI ).[ -> one-to-one ;
coherence
sin | ].PI ,((3 / 2) * PI ).[ is one-to-one
proof end;
cluster sin | ].((3 / 2) * PI ),(2 * PI ).[ -> one-to-one ;
coherence
sin | ].((3 / 2) * PI ),(2 * PI ).[ is one-to-one
proof end;
end;

theorem Th59: :: SIN_COS6:59
for b1 being integer number holds cos | [.((2 * PI ) * b1),(PI + ((2 * PI ) * b1)).] is one-to-one
proof end;

theorem Th60: :: SIN_COS6:60
for b1 being integer number holds cos | [.(PI + ((2 * PI ) * b1)),((2 * PI ) + ((2 * PI ) * b1)).] is one-to-one
proof end;

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

registration
cluster cos | [.0,(PI / 2).] -> one-to-one ;
coherence
cos | [.0,(PI / 2).] is one-to-one
proof end;
cluster cos | [.(PI / 2),PI .] -> one-to-one ;
coherence
cos | [.(PI / 2),PI .] is one-to-one
proof end;
cluster cos | [.PI ,((3 / 2) * PI ).] -> one-to-one ;
coherence
cos | [.PI ,((3 / 2) * PI ).] is one-to-one
proof end;
cluster cos | [.((3 / 2) * PI ),(2 * PI ).] -> one-to-one ;
coherence
cos | [.((3 / 2) * PI ),(2 * PI ).] is one-to-one
proof end;
end;

registration
cluster cos | ].0,PI .[ -> one-to-one ;
coherence
cos | ].0,PI .[ is one-to-one
proof end;
cluster cos | ].PI ,(2 * PI ).[ -> one-to-one ;
coherence
cos | ].PI ,(2 * PI ).[ is one-to-one
proof end;
cluster cos | ].0,(PI / 2).[ -> one-to-one ;
coherence
cos | ].0,(PI / 2).[ is one-to-one
proof end;
cluster cos | ].(PI / 2),PI .[ -> one-to-one ;
coherence
cos | ].(PI / 2),PI .[ is one-to-one
proof end;
cluster cos | ].PI ,((3 / 2) * PI ).[ -> one-to-one ;
coherence
cos | ].PI ,((3 / 2) * PI ).[ is one-to-one
proof end;
cluster cos | ].((3 / 2) * PI ),(2 * PI ).[ -> one-to-one ;
coherence
cos | ].((3 / 2) * PI ),(2 * PI ).[ is one-to-one
proof end;
end;

theorem Th61: :: SIN_COS6:61
for b1, b2 being real number
for b3 being integer number st (2 * PI ) * b3 <= b1 & b1 < (2 * PI ) + ((2 * PI ) * b3) & (2 * PI ) * b3 <= b2 & b2 < (2 * PI ) + ((2 * PI ) * b3) & sin b1 = sin b2 & cos b1 = cos b2 holds
b1 = b2
proof end;

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 Def1 defines arcsin SIN_COS6:def 1 :
arcsin = (sin | [.(- (PI / 2)),(PI / 2).]) " ;

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

:: deftheorem Def2 defines arcsin SIN_COS6:def 2 :
for b1 being set holds arcsin b1 = arcsin . b1;

definition
let c1 be set ;
redefine func arcsin as arcsin c1 -> Real;
coherence
arcsin c1 is Real ;
end;

theorem Th62: :: SIN_COS6:62
arcsin " = sin | [.(- (PI / 2)),(PI / 2).] by FUNCT_1:65;

theorem Th63: :: SIN_COS6:63
rng arcsin = [.(- (PI / 2)),(PI / 2).]
proof end;

registration
cluster arcsin -> one-to-one ;
coherence
arcsin is one-to-one by FUNCT_1:62;
end;

theorem Th64: :: SIN_COS6:64
dom arcsin = [.(- 1),1.] by COMPTRIG:48, FUNCT_1:55;

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

theorem Th66: :: SIN_COS6:66
arcsin * (sin | [.(- (PI / 2)),(PI / 2).]) = id [.(- 1),1.] by COMPTRIG:48, FUNCT_1:61;

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

theorem Th68: :: SIN_COS6:68
arcsin * (sin | [.(- (PI / 2)),(PI / 2).]) = id [.(- (PI / 2)),(PI / 2).] by Th62, Th63, FUNCT_1:61;

theorem Th69: :: SIN_COS6:69
for b1 being real number st - 1 <= b1 & b1 <= 1 holds
sin (arcsin b1) = b1
proof end;

theorem Th70: :: SIN_COS6:70
for b1 being real number st - (PI / 2) <= b1 & b1 <= PI / 2 holds
arcsin (sin b1) = b1
proof end;

theorem Th71: :: SIN_COS6:71
arcsin (- 1) = - (PI / 2) by Lemma15, Th7, Th70;

theorem Th72: :: SIN_COS6:72
arcsin 0 = 0 by Lemma14, Th70, SIN_COS:34;

theorem Th73: :: SIN_COS6:73
arcsin 1 = PI / 2 by Lemma15, Th70, SIN_COS:82;

theorem Th74: :: SIN_COS6:74
for b1 being real number st - 1 <= b1 & b1 <= 1 & arcsin b1 = - (PI / 2) holds
b1 = - 1 by Th7, Th69;

theorem Th75: :: SIN_COS6:75
for b1 being real number st - 1 <= b1 & b1 <= 1 & arcsin b1 = 0 holds
b1 = 0 by Th69, SIN_COS:34;

theorem Th76: :: SIN_COS6:76
for b1 being real number st - 1 <= b1 & b1 <= 1 & arcsin b1 = PI / 2 holds
b1 = 1 by Th69, SIN_COS:82;

theorem Th77: :: SIN_COS6:77
for b1 being real number st - 1 <= b1 & b1 <= 1 holds
( - (PI / 2) <= arcsin b1 & arcsin b1 <= PI / 2 )
proof end;

theorem Th78: :: SIN_COS6:78
for b1 being real number st - 1 < b1 & b1 < 1 holds
( - (PI / 2) < arcsin b1 & arcsin b1 < PI / 2 )
proof end;

theorem Th79: :: SIN_COS6:79
for b1 being real number st - 1 <= b1 & b1 <= 1 holds
arcsin b1 = - (arcsin (- b1))
proof end;

theorem Th80: :: SIN_COS6:80
for b1, b2 being real number st 0 <= b1 & (b2 ^2 ) + (b1 ^2 ) = 1 holds
cos (arcsin b2) = b1
proof end;

theorem Th81: :: SIN_COS6:81
for b1, b2 being real number st b1 <= 0 & (b2 ^2 ) + (b1 ^2 ) = 1 holds
cos (arcsin b2) = - b1
proof end;

theorem Th82: :: SIN_COS6:82
for b1 being real number st - 1 <= b1 & b1 <= 1 holds
cos (arcsin b1) = sqrt (1 - (b1 ^2 ))
proof end;

theorem Th83: :: SIN_COS6:83
arcsin is_increasing_on [.(- 1),1.]
proof end;

theorem Th84: :: SIN_COS6:84
for b1 being real number holds
( arcsin is_differentiable_on ].(- 1),1.[ & ( - 1 < b1 & b1 < 1 implies diff arcsin ,b1 = 1 / (sqrt (1 - (b1 ^2 ))) ) )
proof end;

theorem Th85: :: SIN_COS6:85
arcsin is_continuous_on [.(- 1),1.]
proof end;

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 Def3 defines arccos SIN_COS6:def 3 :
arccos = (cos | [.0,PI .]) " ;

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

:: deftheorem Def4 defines arccos SIN_COS6:def 4 :
for b1 being set holds arccos b1 = arccos . b1;

definition
let c1 be set ;
redefine func arccos as arccos c1 -> Real;
coherence
arccos c1 is Real ;
end;

theorem Th86: :: SIN_COS6:86
arccos " = cos | [.0,PI .] by FUNCT_1:65;

theorem Th87: :: SIN_COS6:87
rng arccos = [.0,PI .]
proof end;

registration
cluster arccos -> one-to-one ;
coherence
arccos is one-to-one by FUNCT_1:62;
end;

theorem Th88: :: SIN_COS6:88
dom arccos = [.(- 1),1.] by COMPTRIG:50, FUNCT_1:55;

theorem Th89: :: SIN_COS6:89
(cos | [.0,PI .]) * arccos = id [.(- 1),1.] by COMPTRIG:50, FUNCT_1:61;

theorem Th90: :: SIN_COS6:90
arccos * (cos | [.0,PI .]) = id [.(- 1),1.] by COMPTRIG:50, FUNCT_1:61;

theorem Th91: :: SIN_COS6:91
(cos | [.0,PI .]) * arccos = id [.0,PI .] by Th86, Th87, FUNCT_1:61;

theorem Th92: :: SIN_COS6:92
arccos * (cos | [.0,PI .]) = id [.0,PI .] by Th86, Th87, FUNCT_1:61;

theorem Th93: :: SIN_COS6:93
for b1 being real number st - 1 <= b1 & b1 <= 1 holds
cos (arccos b1) = b1
proof end;

theorem Th94: :: SIN_COS6:94
for b1 being real number st 0 <= b1 & b1 <= PI holds
arccos (cos b1) = b1
proof end;

theorem Th95: :: SIN_COS6:95
arccos (- 1) = PI by Th94, SIN_COS:82;

theorem Th96: :: SIN_COS6:96
arccos 0 = PI / 2 by Lemma16, Th94, SIN_COS:82;

theorem Th97: :: SIN_COS6:97
arccos 1 = 0 by Th94, SIN_COS:34;

theorem Th98: :: SIN_COS6:98
for b1 being real number st - 1 <= b1 & b1 <= 1 & arccos b1 = 0 holds
b1 = 1 by Th93, SIN_COS:34;

theorem Th99: :: SIN_COS6:99
for b1 being real number st - 1 <= b1 & b1 <= 1 & arccos b1 = PI / 2 holds
b1 = 0 by Th93, SIN_COS:82;

theorem Th100: :: SIN_COS6:100
for b1 being real number st - 1 <= b1 & b1 <= 1 & arccos b1 = PI holds
b1 = - 1 by Th93, SIN_COS:82;

theorem Th101: :: SIN_COS6:101
for b1 being real number st - 1 <= b1 & b1 <= 1 holds
( 0 <= arccos b1 & arccos b1 <= PI )
proof end;

theorem Th102: :: SIN_COS6:102
for b1 being real number st - 1 < b1 & b1 < 1 holds
( 0 < arccos b1 & arccos b1 < PI )
proof end;

theorem Th103: :: SIN_COS6:103
for b1 being real number st - 1 <= b1 & b1 <= 1 holds
arccos b1 = PI - (arccos (- b1))
proof end;

theorem Th104: :: SIN_COS6:104
for b1, b2 being real number st 0 <= b1 & (b2 ^2 ) + (b1 ^2 ) = 1 holds
sin (arccos b2) = b1
proof end;

theorem Th105: :: SIN_COS6:105
for b1, b2 being real number st b1 <= 0 & (b2 ^2 ) + (b1 ^2 ) = 1 holds
sin (arccos b2) = - b1
proof end;

theorem Th106: :: SIN_COS6:106
for b1 being real number st - 1 <= b1 & b1 <= 1 holds
sin (arccos b1) = sqrt (1 - (b1 ^2 ))
proof end;

theorem Th107: :: SIN_COS6:107
arccos is_decreasing_on [.(- 1),1.]
proof end;

theorem Th108: :: SIN_COS6:108
for b1 being real number holds
( arccos is_differentiable_on ].(- 1),1.[ & ( - 1 < b1 & b1 < 1 implies diff arccos ,b1 = - (1 / (sqrt (1 - (b1 ^2 )))) ) )
proof end;

theorem Th109: :: SIN_COS6:109
arccos is_continuous_on [.(- 1),1.]
proof end;

theorem Th110: :: SIN_COS6:110
for b1 being real number st - 1 <= b1 & b1 <= 1 holds
(arcsin b1) + (arccos b1) = PI / 2
proof end;

theorem Th111: :: SIN_COS6:111
for b1 being real number st - 1 <= b1 & b1 <= 1 holds
(arccos (- b1)) - (arcsin b1) = PI / 2
proof end;

theorem Th112: :: SIN_COS6:112
for b1 being real number st - 1 <= b1 & b1 <= 1 holds
(arccos b1) - (arcsin (- b1)) = PI / 2
proof end;