:: Inverse Trigonometric Functions Arcsin and Arccos
:: by Artur Korni{\l}owicz and Yasunari Shidama
::
:: Received September 25, 2004
:: Copyright (c) 2004-2021 Association of Mizar Users


theorem Th1: :: SIN_COS6:1
for r, s being Real st 0 <= r & r < s holds
[\(r / s)/] = 0
proof 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 end;

theorem Th3: :: SIN_COS6:3
for r being Real holds - 1 <= sin r
proof end;

theorem Th4: :: SIN_COS6:4
for r being Real holds sin r <= 1
proof end;

theorem Th5: :: SIN_COS6:5
for r being Real holds - 1 <= cos r
proof end;

theorem Th6: :: SIN_COS6:6
for r being Real holds cos r <= 1
proof end;

deffunc H1( Integer) -> set = (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 st (r ^2) + (s ^2) = 1 holds
( - 1 <= r & r <= 1 )
proof end;

registration
cluster PI -> positive ;
coherence
PI is positive
proof 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 end;

theorem Th8: :: SIN_COS6:8
for r being Real
for i being Integer holds sin . r = sin . (r + ((2 * PI) * i))
proof end;

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

theorem Th10: :: SIN_COS6:10
for r being Real
for i being Integer holds cos . r = cos . (r + ((2 * PI) * i))
proof end;

theorem Th11: :: SIN_COS6:11
for r being Real
for i being Integer st (2 * PI) * i < r & r < PI + ((2 * PI) * i) holds
sin r > 0
proof end;

theorem Th12: :: SIN_COS6:12
for r being Real
for i being Integer st PI + ((2 * PI) * i) < r & r < (2 * PI) + ((2 * PI) * i) holds
sin r < 0
proof end;

theorem Th13: :: SIN_COS6:13
for r being Real
for i being Integer st (- (PI / 2)) + ((2 * PI) * i) < r & r < (PI / 2) + ((2 * PI) * i) holds
cos r > 0
proof end;

theorem Th14: :: SIN_COS6:14
for r being Real
for i being Integer st (PI / 2) + ((2 * PI) * i) < r & r < ((3 / 2) * PI) + ((2 * PI) * i) holds
cos r < 0
proof end;

theorem Th15: :: SIN_COS6:15
for r being Real
for i being Integer st ((3 / 2) * PI) + ((2 * PI) * i) < r & r < (2 * PI) + ((2 * PI) * i) holds
cos r > 0
proof end;

theorem :: SIN_COS6:16
for r being Real
for i being Integer st (2 * PI) * i <= r & r <= PI + ((2 * PI) * i) holds
sin r >= 0
proof end;

theorem :: SIN_COS6:17
for r being Real
for i being Integer st PI + ((2 * PI) * i) <= r & r <= (2 * PI) + ((2 * PI) * i) holds
sin r <= 0
proof end;

theorem :: SIN_COS6:18
for r being Real
for i being Integer st (- (PI / 2)) + ((2 * PI) * i) <= r & r <= (PI / 2) + ((2 * PI) * i) holds
cos r >= 0
proof end;

theorem :: SIN_COS6:19
for r being Real
for i being Integer st (PI / 2) + ((2 * PI) * i) <= r & r <= ((3 / 2) * PI) + ((2 * PI) * i) holds
cos r <= 0
proof end;

theorem :: SIN_COS6:20
for r being Real
for i being Integer st ((3 / 2) * PI) + ((2 * PI) * i) <= r & r <= (2 * PI) + ((2 * PI) * i) holds
cos r >= 0
proof end;

theorem Th21: :: SIN_COS6:21
for r being Real
for i being Integer 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 end;

theorem Th22: :: SIN_COS6:22
for r being Real
for i being Integer 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 end;

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

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

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

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

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

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

:: case cos(r) = 1 has been proved as UNIROOTS:17, COMPTRIG:79
theorem Th29: :: SIN_COS6:29
for r being Real st 0 <= r & r <= 2 * PI & cos r = - 1 holds
r = PI
proof end;

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

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

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

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

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

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

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

theorem :: SIN_COS6:37
for r being Real
for i being Integer st (2 * PI) * i <= r & r < (PI / 2) + ((2 * PI) * i) holds
sin r < 1
proof end;

theorem :: SIN_COS6:38
for r being Real
for i being Integer st (2 * PI) * i <= r & r < ((3 / 2) * PI) + ((2 * PI) * i) holds
sin r > - 1
proof end;

theorem :: SIN_COS6:39
for r being Real
for i being Integer st ((3 / 2) * PI) + ((2 * PI) * i) < r & r <= (2 * PI) + ((2 * PI) * i) holds
sin r > - 1
proof end;

theorem :: SIN_COS6:40
for r being Real
for i being Integer st (PI / 2) + ((2 * PI) * i) < r & r <= (2 * PI) + ((2 * PI) * i) holds
sin r < 1
proof end;

theorem :: SIN_COS6:41
for r being Real
for i being Integer st (2 * PI) * i < r & r < (2 * PI) + ((2 * PI) * i) holds
cos r < 1
proof end;

theorem :: SIN_COS6:42
for r being Real
for i being Integer st (2 * PI) * i <= r & r < PI + ((2 * PI) * i) holds
cos r > - 1
proof end;

theorem :: SIN_COS6:43
for r being Real
for i being Integer st PI + ((2 * PI) * i) < r & r <= (2 * PI) + ((2 * PI) * i) holds
cos r > - 1
proof end;

theorem :: SIN_COS6:44
for r being Real st cos ((2 * PI) * r) = 1 holds
r in INT
proof 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 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 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 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 end;

Lm11: now :: thesis: for i being Integer
for r, p1, p2 being Real 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; :: thesis: for r, p1, p2 being Real 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; :: thesis: for p1, p2 being Real 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; :: 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
for r, p1, p2 being Real 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; :: thesis: for r, p1, p2 being Real 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; :: thesis: for p1, p2 being Real 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; :: 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
for r, p1, p2 being Real 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; :: thesis: for r, p1, p2 being Real 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; :: thesis: for p1, p2 being Real 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; :: 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
for r, p1, p2 being Real 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; :: thesis: for r, p1, p2 being Real 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; :: thesis: for p1, p2 being Real 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; :: 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 holds sin | [.((- (PI / 2)) + ((2 * PI) * i)),((PI / 2) + ((2 * PI) * i)).] is increasing
proof end;

theorem Th54: :: SIN_COS6:54
for i being Integer holds sin | [.((PI / 2) + ((2 * PI) * i)),(((3 / 2) * PI) + ((2 * PI) * i)).] is decreasing
proof end;

theorem Th55: :: SIN_COS6:55
for i being Integer holds cos | [.((2 * PI) * i),(PI + ((2 * PI) * i)).] is decreasing
proof end;

theorem Th56: :: SIN_COS6:56
for i being Integer holds cos | [.(PI + ((2 * PI) * i)),((2 * PI) + ((2 * PI) * i)).] is increasing
proof end;

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

theorem Th58: :: SIN_COS6:58
for i being Integer holds sin | [.((PI / 2) + ((2 * PI) * i)),(((3 / 2) * PI) + ((2 * PI) * i)).] 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 Lm1, Th57;
cluster sin | [.(PI / 2),((3 / 2) * PI).] -> one-to-one ;
coherence
sin | [.(PI / 2),((3 / 2) * PI).] is one-to-one by Lm2, 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 i being Integer holds cos | [.((2 * PI) * i),(PI + ((2 * PI) * i)).] is one-to-one
proof end;

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

registration
cluster cos | [.0,PI.] -> one-to-one ;
coherence
cos | [.0,PI.] is one-to-one by Lm3, Th59;
cluster cos | [.PI,(2 * PI).] -> one-to-one ;
coherence
cos | [.PI,(2 * PI).] is one-to-one by Lm4, 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 :: SIN_COS6:61
for r, s being Real
for i being Integer 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 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 defines arcsin SIN_COS6:def 1 :
arcsin = (sin | [.(- (PI / 2)),(PI / 2).]) " ;

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

:: deftheorem defines arcsin SIN_COS6:def 2 :
for r being object holds arcsin r = arcsin . r;

registration
let r be object ;
cluster 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 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 st - 1 <= r & r <= 1 holds
sin (arcsin r) = r
proof end;

theorem Th69: :: SIN_COS6:69
for r being Real st - (PI / 2) <= r & r <= PI / 2 holds
arcsin (sin r) = r
proof 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 st - 1 <= r & r <= 1 & arcsin r = - (PI / 2) holds
r = - 1 by Th7, Th68;

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

theorem :: SIN_COS6:75
for r being Real 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 st - 1 <= r & r <= 1 holds
( - (PI / 2) <= arcsin r & arcsin r <= PI / 2 )
proof end;

theorem Th77: :: SIN_COS6:77
for r being Real st - 1 < r & r < 1 holds
( - (PI / 2) < arcsin r & arcsin r < PI / 2 )
proof end;

theorem Th78: :: SIN_COS6:78
for r being Real st - 1 <= r & r <= 1 holds
arcsin r = - (arcsin (- r))
proof end;

theorem Th79: :: SIN_COS6:79
for r, s being Real st 0 <= s & (r ^2) + (s ^2) = 1 holds
cos (arcsin r) = s
proof end;

theorem :: SIN_COS6:80
for r, s being Real st s <= 0 & (r ^2) + (s ^2) = 1 holds
cos (arcsin r) = - s
proof end;

theorem Th81: :: SIN_COS6:81
for r being Real st - 1 <= r & r <= 1 holds
cos (arcsin r) = sqrt (1 - (r ^2))
proof end;

theorem :: SIN_COS6:82
arcsin | [.(- 1),1.] is increasing
proof end;

theorem :: SIN_COS6:83
for r being Real holds
( arcsin is_differentiable_on ].(- 1),1.[ & ( - 1 < r & r < 1 implies diff (arcsin,r) = 1 / (sqrt (1 - (r ^2))) ) )
proof end;

theorem :: SIN_COS6:84
arcsin | [.(- 1),1.] is continuous
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 defines arccos SIN_COS6:def 3 :
arccos = (cos | [.0,PI.]) " ;

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

:: deftheorem defines arccos SIN_COS6:def 4 :
for r being object holds arccos r = arccos . r;

registration
let r be object ;
cluster 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 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 st - 1 <= r & r <= 1 holds
cos (arccos r) = r
proof end;

theorem Th92: :: SIN_COS6:92
for r being Real st 0 <= r & r <= PI holds
arccos (cos r) = r
proof 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 st - 1 <= r & r <= 1 & arccos r = 0 holds
r = 1 by Th91, SIN_COS:31;

theorem :: SIN_COS6:97
for r being Real 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 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 st - 1 <= r & r <= 1 holds
( 0 <= arccos r & arccos r <= PI )
proof end;

theorem Th100: :: SIN_COS6:100
for r being Real st - 1 < r & r < 1 holds
( 0 < arccos r & arccos r < PI )
proof end;

theorem Th101: :: SIN_COS6:101
for r being Real st - 1 <= r & r <= 1 holds
arccos r = PI - (arccos (- r))
proof end;

theorem Th102: :: SIN_COS6:102
for r, s being Real st 0 <= s & (r ^2) + (s ^2) = 1 holds
sin (arccos r) = s
proof end;

theorem :: SIN_COS6:103
for r, s being Real st s <= 0 & (r ^2) + (s ^2) = 1 holds
sin (arccos r) = - s
proof end;

theorem Th104: :: SIN_COS6:104
for r being Real st - 1 <= r & r <= 1 holds
sin (arccos r) = sqrt (1 - (r ^2))
proof end;

theorem :: SIN_COS6:105
arccos | [.(- 1),1.] is decreasing
proof end;

theorem :: SIN_COS6:106
for r being Real holds
( arccos is_differentiable_on ].(- 1),1.[ & ( - 1 < r & r < 1 implies diff (arccos,r) = - (1 / (sqrt (1 - (r ^2)))) ) )
proof end;

theorem :: SIN_COS6:107
arccos | [.(- 1),1.] is continuous
proof end;

:: Correspondence between arcsin and arccos
theorem Th108: :: SIN_COS6:108
for r being Real st - 1 <= r & r <= 1 holds
(arcsin r) + (arccos r) = PI / 2
proof end;

theorem :: SIN_COS6:109
for r being Real st - 1 <= r & r <= 1 holds
(arccos (- r)) - (arcsin r) = PI / 2
proof end;

theorem :: SIN_COS6:110
for r being Real st - 1 <= r & r <= 1 holds
(arccos r) - (arcsin (- r)) = PI / 2
proof end;