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

begin

theorem Th1: :: SIN_COS6:1

for r, s being real number 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;

begin

theorem Th3: :: SIN_COS6:3

for r being real number holds - 1 <= sin r

proof end;

theorem Th4: :: SIN_COS6:4

for r being real number holds sin r <= 1

proof end;

theorem Th5: :: SIN_COS6:5

for r being real number holds - 1 <= cos r

proof end;

theorem Th6: :: SIN_COS6:6

for r being real number holds cos r <= 1

proof end;

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

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

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

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

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

Lm5: for r, s being real number 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:78;

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

Lm8: 0 + H₁(1) < (PI / 2) + H₁(1)
by XREAL_1:8;

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

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

theorem Th7: :: SIN_COS6:7

( sin (- (PI / 2)) = - 1 & sin . (- (PI / 2)) = - 1 )

proof 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 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 number
for i being integer number holds cos . r = cos . (r + ((2 * PI) * i))

proof 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 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 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 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 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 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 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 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 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 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 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 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 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 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 end;

theorem Th25: :: SIN_COS6:25

for r being real number st cos r = - 1 holds
r = PI + ((2 * PI) * [\(r / (2 * PI))/])

proof end;

theorem Th26: :: SIN_COS6:26

for r being real number st cos r = 1 holds
r = (2 * PI) * [\(r / (2 * PI))/]

proof 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 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 end;

theorem Th29: :: SIN_COS6:29

for r being real number st 0 <= r & r <= 2 * PI & cos r = - 1 holds
r = PI

proof end;

theorem Th30: :: SIN_COS6:30

for r being real number st 0 <= r & r < PI / 2 holds
sin r < 1

proof end;

theorem Th31: :: SIN_COS6:31

for r being real number st 0 <= r & r < (3 / 2) * PI holds
sin r > - 1

proof end;

theorem Th32: :: SIN_COS6:32

for r being real number st (3 / 2) * PI < r & r <= 2 * PI holds
sin r > - 1

proof end;

theorem Th33: :: SIN_COS6:33

for r being real number st PI / 2 < r & r <= 2 * PI holds
sin r < 1

proof end;

theorem Th34: :: SIN_COS6:34

for r being real number st 0 < r & r < 2 * PI holds
cos r < 1

proof end;

theorem Th35: :: SIN_COS6:35

for r being real number st 0 <= r & r < PI holds
cos r > - 1

proof end;

theorem Th36: :: SIN_COS6:36

for r being real number st PI < r & r <= 2 * PI holds
cos r > - 1

proof 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 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 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 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 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 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 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 end;

theorem :: SIN_COS6:44

for r being real number 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:48, RELAT_1:148;

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:49, RELAT_1:148;

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:50, RELAT_1:148;

theorem Th50: :: SIN_COS6:50

cos .: ].0,PI.[ = ].(- 1),1.[

proof end;

theorem :: SIN_COS6:51

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

theorem :: SIN_COS6:52

cos .: ].PI,(2 * PI).[ = ].(- 1),1.[

proof end;

Lm11: now

let i be integer number ; :: thesis: for r, p1, p2 being real number st r in [.(p1 + H₁(i)),(p2 + H₁(i)).] holds
r + (2 * PI) in [.(p1 + H₁(i + 1)),(p2 + H₁(i + 1)).]
let r be real number ; :: thesis: for p1, p2 being real number st r in [.(p1 + H₁(i)),(p2 + H₁(i)).] holds
r + (2 * PI) in [.(p1 + H₁(i + 1)),(p2 + H₁(i + 1)).]
let p1, p2 be real number ; :: thesis: ( r in [.(p1 + H₁(i)),(p2 + H₁(i)).] implies r + (2 * PI) in [.(p1 + H₁(i + 1)),(p2 + H₁(i + 1)).] )
assume A1: r in [.(p1 + H₁(i)),(p2 + H₁(i)).] ; :: thesis: r + (2 * PI) in [.(p1 + H₁(i + 1)),(p2 + H₁(i + 1)).]
then r <= p2 + H₁(i) by XXREAL_1:1;
then A2: r + (2 * PI) <= (p2 + H₁(i)) + (2 * PI) by XREAL_1:8;
p1 + H₁(i) <= r by A1, XXREAL_1:1;
then (p1 + H₁(i)) + (2 * PI) <= r + (2 * PI) by XREAL_1:8;
hence r + (2 * PI) in [.(p1 + H₁(i + 1)),(p2 + H₁(i + 1)).] by A2, XXREAL_1:1; :: thesis: verum

end;

Lm12: now

let i be integer number ; :: thesis: for r, p1, p2 being real number st r in [.(p1 + H₁(i)),(p2 + H₁(i)).] /\ REAL holds
r + (2 * PI) in [.(p1 + H₁(i + 1)),(p2 + H₁(i + 1)).] /\ REAL
let r be real number ; :: thesis: for p1, p2 being real number st r in [.(p1 + H₁(i)),(p2 + H₁(i)).] /\ REAL holds
r + (2 * PI) in [.(p1 + H₁(i + 1)),(p2 + H₁(i + 1)).] /\ REAL
let p1, p2 be real number ; :: thesis: ( r in [.(p1 + H₁(i)),(p2 + H₁(i)).] /\ REAL implies r + (2 * PI) in [.(p1 + H₁(i + 1)),(p2 + H₁(i + 1)).] /\ REAL )
assume r in [.(p1 + H₁(i)),(p2 + H₁(i)).] /\ REAL ; :: thesis: r + (2 * PI) in [.(p1 + H₁(i + 1)),(p2 + H₁(i + 1)).] /\ REAL
then r in [.(p1 + H₁(i)),(p2 + H₁(i)).] by XBOOLE_0:def 4;
then r + (2 * PI) in [.(p1 + H₁(i + 1)),(p2 + H₁(i + 1)).] by Lm11;
hence r + (2 * PI) in [.(p1 + H₁(i + 1)),(p2 + H₁(i + 1)).] /\ REAL by XBOOLE_0:def 4; :: thesis: verum

end;

Lm13: now

let i be integer number ; :: thesis: for r, p1, p2 being real number st r in [.(p1 + H₁(i)),(p2 + H₁(i)).] holds
r - (2 * PI) in [.(p1 + H₁(i - 1)),(p2 + H₁(i - 1)).]
let r be real number ; :: thesis: for p1, p2 being real number st r in [.(p1 + H₁(i)),(p2 + H₁(i)).] holds
r - (2 * PI) in [.(p1 + H₁(i - 1)),(p2 + H₁(i - 1)).]
let p1, p2 be real number ; :: thesis: ( r in [.(p1 + H₁(i)),(p2 + H₁(i)).] implies r - (2 * PI) in [.(p1 + H₁(i - 1)),(p2 + H₁(i - 1)).] )
assume A1: r in [.(p1 + H₁(i)),(p2 + H₁(i)).] ; :: thesis: r - (2 * PI) in [.(p1 + H₁(i - 1)),(p2 + H₁(i - 1)).]
then r <= p2 + H₁(i) by XXREAL_1:1;
then A2: r - (2 * PI) <= (p2 + H₁(i)) - (2 * PI) by XREAL_1:11;
p1 + H₁(i) <= r by A1, XXREAL_1:1;
then (p1 + H₁(i)) - (2 * PI) <= r - (2 * PI) by XREAL_1:11;
hence r - (2 * PI) in [.(p1 + H₁(i - 1)),(p2 + H₁(i - 1)).] by A2, XXREAL_1:1; :: thesis: verum

end;

Lm14: now

let i be integer number ; :: thesis: for r, p1, p2 being real number st r in [.(p1 + H₁(i)),(p2 + H₁(i)).] /\ REAL holds
r - (2 * PI) in [.(p1 + H₁(i - 1)),(p2 + H₁(i - 1)).] /\ REAL
let r be real number ; :: thesis: for p1, p2 being real number st r in [.(p1 + H₁(i)),(p2 + H₁(i)).] /\ REAL holds
r - (2 * PI) in [.(p1 + H₁(i - 1)),(p2 + H₁(i - 1)).] /\ REAL
let p1, p2 be real number ; :: thesis: ( r in [.(p1 + H₁(i)),(p2 + H₁(i)).] /\ REAL implies r - (2 * PI) in [.(p1 + H₁(i - 1)),(p2 + H₁(i - 1)).] /\ REAL )
assume r in [.(p1 + H₁(i)),(p2 + H₁(i)).] /\ REAL ; :: thesis: r - (2 * PI) in [.(p1 + H₁(i - 1)),(p2 + H₁(i - 1)).] /\ REAL
then r in [.(p1 + H₁(i)),(p2 + H₁(i)).] by XBOOLE_0:def 4;
then r - (2 * PI) in [.(p1 + H₁(i - 1)),(p2 + H₁(i - 1)).] by Lm13;
hence r - (2 * PI) in [.(p1 + H₁(i - 1)),(p2 + H₁(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 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 end;

theorem Th55: :: SIN_COS6:55

for i being integer number holds cos | [.((2 * PI) * i),(PI + ((2 * PI) * i)).] is decreasing

proof 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 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 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 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 number holds cos | [.((2 * PI) * i),(PI + ((2 * PI) * i)).] is one-to-one

proof 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 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 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 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:65;

theorem :: SIN_COS6:62

canceled;

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 ;

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 :: 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 Lm15, Th63, FUNCT_1:61;

theorem :: SIN_COS6:68

arcsin * (sin | [.(- (PI / 2)),(PI / 2).]) = id [.(- (PI / 2)),(PI / 2).] by Lm15, Th63, FUNCT_1:61;

theorem Th69: :: SIN_COS6:69

for r being real number st - 1 <= r & r <= 1 holds
sin (arcsin r) = r

proof end;

theorem Th70: :: SIN_COS6:70

for r being real number st - (PI / 2) <= r & r <= PI / 2 holds
arcsin (sin r) = r

proof end;

theorem :: SIN_COS6:71

arcsin (- 1) = - (PI / 2) by Th7, Th70;

theorem :: SIN_COS6:72

arcsin 0 = 0 by Th70, SIN_COS:34;

theorem :: SIN_COS6:73

arcsin 1 = PI / 2 by Th70, SIN_COS:82;

theorem :: SIN_COS6:74

for r being real number st - 1 <= r & r <= 1 & arcsin r = - (PI / 2) holds
r = - 1 by Th7, Th69;

theorem :: SIN_COS6:75

for r being real number st - 1 <= r & r <= 1 & arcsin r = 0 holds
r = 0 by Th69, SIN_COS:34;

theorem :: SIN_COS6:76

for r being real number st - 1 <= r & r <= 1 & arcsin r = PI / 2 holds
r = 1 by Th69, SIN_COS:82;

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 end;

theorem Th78: :: SIN_COS6:78

for r being real number st - 1 < r & r < 1 holds
( - (PI / 2) < arcsin r & arcsin r < PI / 2 )

proof end;

theorem Th79: :: SIN_COS6:79

for r being real number st - 1 <= r & r <= 1 holds
arcsin r = - (arcsin (- r))

proof end;

theorem Th80: :: SIN_COS6:80

for s, r being real number st 0 <= s & (r ^2) + (s ^2) = 1 holds
cos (arcsin r) = s

proof end;

theorem :: SIN_COS6:81

for s, r being real number st s <= 0 & (r ^2) + (s ^2) = 1 holds
cos (arcsin r) = - s

proof end;

theorem Th82: :: SIN_COS6:82

for r being real number st - 1 <= r & r <= 1 holds
cos (arcsin r) = sqrt (1 - (r ^2))

proof end;

theorem :: SIN_COS6:83

arcsin | [.(- 1),1.] is increasing

proof end;

theorem :: SIN_COS6:84

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 end;

theorem :: SIN_COS6:85

arcsin | [.(- 1),1.] is continuous

proof 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:65;

theorem :: SIN_COS6:86

canceled;

theorem Th87: :: SIN_COS6:87

rng arccos = [.0,PI.]

proof end;

registration

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

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 :: 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 Lm16, Th87, FUNCT_1:61;

theorem :: SIN_COS6:92

arccos * (cos | [.0,PI.]) = id [.0,PI.] by Lm16, Th87, FUNCT_1:61;

theorem Th93: :: SIN_COS6:93

for r being real number st - 1 <= r & r <= 1 holds
cos (arccos r) = r

proof end;

theorem Th94: :: SIN_COS6:94

for r being real number st 0 <= r & r <= PI holds
arccos (cos r) = r

proof end;

theorem :: SIN_COS6:95

arccos (- 1) = PI by Th94, SIN_COS:82;

theorem :: SIN_COS6:96

arccos 0 = PI / 2 by Lm6, Th94, SIN_COS:82;

theorem :: SIN_COS6:97

arccos 1 = 0 by Th94, SIN_COS:34;

theorem :: SIN_COS6:98

for r being real number st - 1 <= r & r <= 1 & arccos r = 0 holds
r = 1 by Th93, SIN_COS:34;

theorem :: SIN_COS6:99

for r being real number st - 1 <= r & r <= 1 & arccos r = PI / 2 holds
r = 0 by Th93, SIN_COS:82;

theorem :: SIN_COS6:100

for r being real number st - 1 <= r & r <= 1 & arccos r = PI holds
r = - 1 by Th93, SIN_COS:82;

theorem Th101: :: SIN_COS6:101

for r being real number st - 1 <= r & r <= 1 holds
( 0 <= arccos r & arccos r <= PI )

proof end;

theorem Th102: :: SIN_COS6:102

for r being real number st - 1 < r & r < 1 holds
( 0 < arccos r & arccos r < PI )

proof end;

theorem Th103: :: SIN_COS6:103

for r being real number st - 1 <= r & r <= 1 holds
arccos r = PI - (arccos (- r))

proof end;

theorem Th104: :: SIN_COS6:104

for s, r being real number st 0 <= s & (r ^2) + (s ^2) = 1 holds
sin (arccos r) = s

proof end;

theorem :: SIN_COS6:105

for s, r being real number st s <= 0 & (r ^2) + (s ^2) = 1 holds
sin (arccos r) = - s

proof end;

theorem Th106: :: SIN_COS6:106

for r being real number st - 1 <= r & r <= 1 holds
sin (arccos r) = sqrt (1 - (r ^2))

proof end;

theorem :: SIN_COS6:107

arccos | [.(- 1),1.] is decreasing

proof end;

theorem :: SIN_COS6:108

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 end;

theorem :: SIN_COS6:109

arccos | [.(- 1),1.] is continuous

proof end;

theorem Th110: :: SIN_COS6:110

for r being real number st - 1 <= r & r <= 1 holds
(arcsin r) + (arccos r) = PI / 2

proof end;

theorem :: SIN_COS6:111

for r being real number st - 1 <= r & r <= 1 holds
(arccos (- r)) - (arcsin r) = PI / 2

proof end;

theorem :: SIN_COS6:112

for r being real number st - 1 <= r & r <= 1 holds
(arccos r) - (arcsin (- r)) = PI / 2

proof end;