:: SIN_COS6 semantic presentation

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;

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) -> set = (2 * PI ) * $1;

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

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

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

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

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

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

Lm7: for r, s being real number st (r ^2 ) + (s ^2 ) = 1 holds
( - 1 <= r & r <= 1 )

proof end;

registration

cluster PI -> positive ;
coherence

proof end;

end;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Lm32: [.((3 / 2) * PI ),(2 * PI ).] c= [.((- (PI / 2)) + H₁(1)),((PI / 2) + H₁(1)).]
by Lm12, TREAL_1:1;

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

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;

Lm34: now

let i be integer number ; :: thesis:
let r be real number ; :: thesis:
let p1, p2 be real number ; :: thesis:
assume r in [.(p1 + H₁(i)),(p2 + H₁(i)).] ; :: thesis:
then ( p1 + H₁(i) <= r & r <= p2 + H₁(i) ) by RCOMP_1:48;
then ( (p1 + H₁(i)) + (2 * PI ) <= r + (2 * PI ) & r + (2 * PI ) <= (p2 + H₁(i)) + (2 * PI ) ) by XREAL_1:8;
hence r + (2 * PI ) in [.(p1 + H₁(i + 1)),(p2 + H₁(i + 1)).] by RCOMP_1:48; :: thesis:

end;

Lm35: now

let i be integer number ; :: thesis:
let r be real number ; :: thesis:
let p1, p2 be real number ; :: thesis:
assume r in [.(p1 + H₁(i)),(p2 + H₁(i)).] /\ REAL ; :: thesis:
then ( r in [.(p1 + H₁(i)),(p2 + H₁(i)).] & r in REAL ) by XBOOLE_0:def 3;
then ( r + (2 * PI ) in [.(p1 + H₁(i + 1)),(p2 + H₁(i + 1)).] & r + (2 * PI ) in REAL ) by Lm34, XREAL_0:def 1;
hence r + (2 * PI ) in [.(p1 + H₁(i + 1)),(p2 + H₁(i + 1)).] /\ REAL by XBOOLE_0:def 3; :: thesis:

end;

Lm36: now

let i be integer number ; :: thesis:
let r be real number ; :: thesis:
let p1, p2 be real number ; :: thesis:
assume r in [.(p1 + H₁(i)),(p2 + H₁(i)).] ; :: thesis:
then ( p1 + H₁(i) <= r & r <= p2 + H₁(i) ) by RCOMP_1:48;
then ( (p1 + H₁(i)) - (2 * PI ) <= r - (2 * PI ) & r - (2 * PI ) <= (p2 + H₁(i)) - (2 * PI ) ) by XREAL_1:11;
hence r - (2 * PI ) in [.(p1 + H₁(i - 1)),(p2 + H₁(i - 1)).] by RCOMP_1:48; :: thesis:

end;

Lm37: now

let i be integer number ; :: thesis:
let r be real number ; :: thesis:
let p1, p2 be real number ; :: thesis:
assume r in [.(p1 + H₁(i)),(p2 + H₁(i)).] /\ REAL ; :: thesis:
then ( r in [.(p1 + H₁(i)),(p2 + H₁(i)).] & r in REAL ) by XBOOLE_0:def 3;
then ( r - (2 * PI ) in [.(p1 + H₁(i - 1)),(p2 + H₁(i - 1)).] & r - (2 * PI ) in REAL ) by Lm36, XREAL_0:def 1;
hence r - (2 * PI ) in [.(p1 + H₁(i - 1)),(p2 + H₁(i - 1)).] /\ REAL by XBOOLE_0:def 3; :: thesis:

end;

theorem Th53: :: SIN_COS6:53

for i being integer number holds sin is_increasing_on [.((- (PI / 2)) + ((2 * PI ) * i)),((PI / 2) + ((2 * PI ) * i)).]

proof end;

theorem Th54: :: SIN_COS6:54

for i being integer number holds sin is_decreasing_on [.((PI / 2) + ((2 * PI ) * i)),(((3 / 2) * PI ) + ((2 * PI ) * i)).]

proof end;

theorem Th55: :: SIN_COS6:55

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

proof end;

theorem Th56: :: SIN_COS6:56

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

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 by Lm3, Th57;
cluster sin | [.(PI / 2),((3 / 2) * PI ).] -> one-to-one ;
coherence by Lm4, Th58;

end;

registration

cluster sin | [.(- (PI / 2)),0.] -> one-to-one ;
coherence

proof end;

cluster sin | [.0,(PI / 2).] -> one-to-one ;
coherence

proof end;

cluster sin | [.(PI / 2),PI .] -> one-to-one ;
coherence

proof end;

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

proof end;

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

proof end;

end;

registration

cluster sin | ].(- (PI / 2)),(PI / 2).[ -> one-to-one ;
coherence

proof end;

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

proof end;

cluster sin | ].(- (PI / 2)),0.[ -> one-to-one ;
coherence

proof end;

cluster sin | ].0,(PI / 2).[ -> one-to-one ;
coherence

proof end;

cluster sin | ].(PI / 2),PI .[ -> one-to-one ;
coherence

proof end;

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

proof end;

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

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 by Lm5, Th59;
cluster cos | [.PI ,(2 * PI ).] -> one-to-one ;
coherence by Lm6, Th60;

end;

registration

cluster cos | [.0,(PI / 2).] -> one-to-one ;
coherence

proof end;

cluster cos | [.(PI / 2),PI .] -> one-to-one ;
coherence

proof end;

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

proof end;

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

proof end;

end;

registration

cluster cos | ].0,PI .[ -> one-to-one ;
coherence

proof end;

cluster cos | ].PI ,(2 * PI ).[ -> one-to-one ;
coherence

proof end;

cluster cos | ].0,(PI / 2).[ -> one-to-one ;
coherence

proof end;

cluster cos | ].(PI / 2),PI .[ -> one-to-one ;
coherence

proof end;

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

proof end;

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

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;

definition

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

end;

:: deftheorem defines arcsin SIN_COS6:def 1 :

definition

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

end;

:: deftheorem defines arcsin SIN_COS6:def 2 :

definition

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

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 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 :: 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 :: 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 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 Lm9, Th7, Th70;

theorem :: SIN_COS6:72

arcsin 0 = 0 by Lm8, Th70, SIN_COS:34;

theorem :: SIN_COS6:73

arcsin 1 = PI / 2 by Lm9, 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 is_increasing_on [.(- 1),1.]

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 is_continuous_on [.(- 1),1.]

proof end;

definition

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

end;

:: deftheorem defines arccos SIN_COS6:def 3 :

definition

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

end;

:: deftheorem defines arccos SIN_COS6:def 4 :

definition

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

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 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 :: 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 :: SIN_COS6:92

arccos * (cos | [.0,PI .]) = id [.0,PI .] by Th86, 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 Lm10, 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 is_decreasing_on [.(- 1),1.]

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 is_continuous_on [.(- 1),1.]

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;