:: by Artur Korni{\l}owicz and Yasunari Shidama

::

:: Received September 25, 2004

:: Copyright (c) 2004-2018 Association of Mizar Users

deffunc H

Lm1: [.((- (PI / 2)) + H

;

Lm2: [.((PI / 2) + H

;

Lm3: [.H

;

Lm4: [.(PI + H

;

Lm5: for r, s being Real st (r ^2) + (s ^2) = 1 holds

( - 1 <= r & r <= 1 )

proof end;

Lm6: PI / 2 < PI / 1

by XREAL_1:76;

Lm7: 1 * PI < (3 / 2) * PI

by XREAL_1:68;

Lm8: 0 + H

by XREAL_1:6;

Lm9: (3 / 2) * PI < 2 * PI

by XREAL_1:68;

Lm10: 1 * PI < 2 * PI

by XREAL_1:68;

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

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

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

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

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

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

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

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

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

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)

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)

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;

:: case cos(r) = 1 has been proved as UNIROOTS:17, COMPTRIG:79

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

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

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

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

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

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

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

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:47

Lm11: now :: thesis: for i being Integer

for r, p1, p2 being Real st r in [.(p1 + H_{1}(i)),(p2 + H_{1}(i)).] holds

r + (2 * PI) in [.(p1 + H_{1}(i + 1)),(p2 + H_{1}(i + 1)).]

for r, p1, p2 being Real st r in [.(p1 + H

r + (2 * PI) in [.(p1 + H

let i be Integer; :: thesis: for r, p1, p2 being Real st r in [.(p1 + H_{1}(i)),(p2 + H_{1}(i)).] holds

r + (2 * PI) in [.(p1 + H_{1}(i + 1)),(p2 + H_{1}(i + 1)).]

let r be Real; :: thesis: for p1, p2 being Real st r in [.(p1 + H_{1}(i)),(p2 + H_{1}(i)).] holds

r + (2 * PI) in [.(p1 + H_{1}(i + 1)),(p2 + H_{1}(i + 1)).]

let p1, p2 be Real; :: thesis: ( r in [.(p1 + H_{1}(i)),(p2 + H_{1}(i)).] implies r + (2 * PI) in [.(p1 + H_{1}(i + 1)),(p2 + H_{1}(i + 1)).] )

assume A1: r in [.(p1 + H_{1}(i)),(p2 + H_{1}(i)).]
; :: thesis: r + (2 * PI) in [.(p1 + H_{1}(i + 1)),(p2 + H_{1}(i + 1)).]

then r <= p2 + H_{1}(i)
by XXREAL_1:1;

then A2: r + (2 * PI) <= (p2 + H_{1}(i)) + (2 * PI)
by XREAL_1:6;

p1 + H_{1}(i) <= r
by A1, XXREAL_1:1;

then (p1 + H_{1}(i)) + (2 * PI) <= r + (2 * PI)
by XREAL_1:6;

hence r + (2 * PI) in [.(p1 + H_{1}(i + 1)),(p2 + H_{1}(i + 1)).]
by A2, XXREAL_1:1; :: thesis: verum

end;
r + (2 * PI) in [.(p1 + H

let r be Real; :: thesis: for p1, p2 being Real st r in [.(p1 + H

r + (2 * PI) in [.(p1 + H

let p1, p2 be Real; :: thesis: ( r in [.(p1 + H

assume A1: r in [.(p1 + H

then r <= p2 + H

then A2: r + (2 * PI) <= (p2 + H

p1 + H

then (p1 + H

hence r + (2 * PI) in [.(p1 + H

Lm12: now :: thesis: for i being Integer

for r, p1, p2 being Real st r in [.(p1 + H_{1}(i)),(p2 + H_{1}(i)).] /\ REAL holds

r + (2 * PI) in [.(p1 + H_{1}(i + 1)),(p2 + H_{1}(i + 1)).] /\ REAL

for r, p1, p2 being Real st r in [.(p1 + H

r + (2 * PI) in [.(p1 + H

let i be Integer; :: thesis: for r, p1, p2 being Real st r in [.(p1 + H_{1}(i)),(p2 + H_{1}(i)).] /\ REAL holds

r + (2 * PI) in [.(p1 + H_{1}(i + 1)),(p2 + H_{1}(i + 1)).] /\ REAL

let r be Real; :: thesis: for p1, p2 being Real st r in [.(p1 + H_{1}(i)),(p2 + H_{1}(i)).] /\ REAL holds

r + (2 * PI) in [.(p1 + H_{1}(i + 1)),(p2 + H_{1}(i + 1)).] /\ REAL

let p1, p2 be Real; :: thesis: ( r in [.(p1 + H_{1}(i)),(p2 + H_{1}(i)).] /\ REAL implies r + (2 * PI) in [.(p1 + H_{1}(i + 1)),(p2 + H_{1}(i + 1)).] /\ REAL )

assume r in [.(p1 + H_{1}(i)),(p2 + H_{1}(i)).] /\ REAL
; :: thesis: r + (2 * PI) in [.(p1 + H_{1}(i + 1)),(p2 + H_{1}(i + 1)).] /\ REAL

then r in [.(p1 + H_{1}(i)),(p2 + H_{1}(i)).]
by XBOOLE_0:def 4;

then r + (2 * PI) in [.(p1 + H_{1}(i + 1)),(p2 + H_{1}(i + 1)).]
by Lm11;

hence r + (2 * PI) in [.(p1 + H_{1}(i + 1)),(p2 + H_{1}(i + 1)).] /\ REAL
by XBOOLE_0:def 4; :: thesis: verum

end;
r + (2 * PI) in [.(p1 + H

let r be Real; :: thesis: for p1, p2 being Real st r in [.(p1 + H

r + (2 * PI) in [.(p1 + H

let p1, p2 be Real; :: thesis: ( r in [.(p1 + H

assume r in [.(p1 + H

then r in [.(p1 + H

then r + (2 * PI) in [.(p1 + H

hence r + (2 * PI) in [.(p1 + H

Lm13: now :: thesis: for i being Integer

for r, p1, p2 being Real st r in [.(p1 + H_{1}(i)),(p2 + H_{1}(i)).] holds

r - (2 * PI) in [.(p1 + H_{1}(i - 1)),(p2 + H_{1}(i - 1)).]

for r, p1, p2 being Real st r in [.(p1 + H

r - (2 * PI) in [.(p1 + H

let i be Integer; :: thesis: for r, p1, p2 being Real st r in [.(p1 + H_{1}(i)),(p2 + H_{1}(i)).] holds

r - (2 * PI) in [.(p1 + H_{1}(i - 1)),(p2 + H_{1}(i - 1)).]

let r be Real; :: thesis: for p1, p2 being Real st r in [.(p1 + H_{1}(i)),(p2 + H_{1}(i)).] holds

r - (2 * PI) in [.(p1 + H_{1}(i - 1)),(p2 + H_{1}(i - 1)).]

let p1, p2 be Real; :: thesis: ( r in [.(p1 + H_{1}(i)),(p2 + H_{1}(i)).] implies r - (2 * PI) in [.(p1 + H_{1}(i - 1)),(p2 + H_{1}(i - 1)).] )

assume A1: r in [.(p1 + H_{1}(i)),(p2 + H_{1}(i)).]
; :: thesis: r - (2 * PI) in [.(p1 + H_{1}(i - 1)),(p2 + H_{1}(i - 1)).]

then r <= p2 + H_{1}(i)
by XXREAL_1:1;

then A2: r - (2 * PI) <= (p2 + H_{1}(i)) - (2 * PI)
by XREAL_1:9;

p1 + H_{1}(i) <= r
by A1, XXREAL_1:1;

then (p1 + H_{1}(i)) - (2 * PI) <= r - (2 * PI)
by XREAL_1:9;

hence r - (2 * PI) in [.(p1 + H_{1}(i - 1)),(p2 + H_{1}(i - 1)).]
by A2, XXREAL_1:1; :: thesis: verum

end;
r - (2 * PI) in [.(p1 + H

let r be Real; :: thesis: for p1, p2 being Real st r in [.(p1 + H

r - (2 * PI) in [.(p1 + H

let p1, p2 be Real; :: thesis: ( r in [.(p1 + H

assume A1: r in [.(p1 + H

then r <= p2 + H

then A2: r - (2 * PI) <= (p2 + H

p1 + H

then (p1 + H

hence r - (2 * PI) in [.(p1 + H

Lm14: now :: thesis: for i being Integer

for r, p1, p2 being Real st r in [.(p1 + H_{1}(i)),(p2 + H_{1}(i)).] /\ REAL holds

r - (2 * PI) in [.(p1 + H_{1}(i - 1)),(p2 + H_{1}(i - 1)).] /\ REAL

for r, p1, p2 being Real st r in [.(p1 + H

r - (2 * PI) in [.(p1 + H

let i be Integer; :: thesis: for r, p1, p2 being Real st r in [.(p1 + H_{1}(i)),(p2 + H_{1}(i)).] /\ REAL holds

r - (2 * PI) in [.(p1 + H_{1}(i - 1)),(p2 + H_{1}(i - 1)).] /\ REAL

let r be Real; :: thesis: for p1, p2 being Real st r in [.(p1 + H_{1}(i)),(p2 + H_{1}(i)).] /\ REAL holds

r - (2 * PI) in [.(p1 + H_{1}(i - 1)),(p2 + H_{1}(i - 1)).] /\ REAL

let p1, p2 be Real; :: thesis: ( r in [.(p1 + H_{1}(i)),(p2 + H_{1}(i)).] /\ REAL implies r - (2 * PI) in [.(p1 + H_{1}(i - 1)),(p2 + H_{1}(i - 1)).] /\ REAL )

assume r in [.(p1 + H_{1}(i)),(p2 + H_{1}(i)).] /\ REAL
; :: thesis: r - (2 * PI) in [.(p1 + H_{1}(i - 1)),(p2 + H_{1}(i - 1)).] /\ REAL

then r in [.(p1 + H_{1}(i)),(p2 + H_{1}(i)).]
by XBOOLE_0:def 4;

then r - (2 * PI) in [.(p1 + H_{1}(i - 1)),(p2 + H_{1}(i - 1)).]
by Lm13;

hence r - (2 * PI) in [.(p1 + H_{1}(i - 1)),(p2 + H_{1}(i - 1)).] /\ REAL
by XBOOLE_0:def 4; :: thesis: verum

end;
r - (2 * PI) in [.(p1 + H

let r be Real; :: thesis: for p1, p2 being Real st r in [.(p1 + H

r - (2 * PI) in [.(p1 + H

let p1, p2 be Real; :: thesis: ( r in [.(p1 + H

assume r in [.(p1 + H

then r in [.(p1 + H

then r - (2 * PI) in [.(p1 + H

hence r - (2 * PI) in [.(p1 + H

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

coherence

sin | [.(- (PI / 2)),(PI / 2).] is one-to-one by Lm1, Th57;

coherence

sin | [.(PI / 2),((3 / 2) * PI).] is one-to-one by Lm2, Th58;

end;
sin | [.(- (PI / 2)),(PI / 2).] is one-to-one by Lm1, Th57;

coherence

sin | [.(PI / 2),((3 / 2) * PI).] is one-to-one by Lm2, Th58;

registration

coherence

sin | [.(- (PI / 2)),0.] is one-to-one

sin | [.0,(PI / 2).] is one-to-one

sin | [.(PI / 2),PI.] is one-to-one

sin | [.PI,((3 / 2) * PI).] is one-to-one

sin | [.((3 / 2) * PI),(2 * PI).] is one-to-one

end;
sin | [.(- (PI / 2)),0.] is one-to-one

proof end;

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

proof end;

coherence sin | [.(PI / 2),PI.] is one-to-one

proof end;

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

proof end;

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

proof end;

registration

coherence

sin | ].(- (PI / 2)),(PI / 2).[ is one-to-one

sin | ].(PI / 2),((3 / 2) * PI).[ is one-to-one

sin | ].(- (PI / 2)),0.[ is one-to-one

sin | ].0,(PI / 2).[ is one-to-one

sin | ].(PI / 2),PI.[ is one-to-one

sin | ].PI,((3 / 2) * PI).[ is one-to-one

sin | ].((3 / 2) * PI),(2 * PI).[ is one-to-one

end;
sin | ].(- (PI / 2)),(PI / 2).[ is one-to-one

proof end;

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

proof end;

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

proof end;

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

proof end;

coherence sin | ].(PI / 2),PI.[ is one-to-one

proof end;

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

proof end;

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

proof end;

registration

coherence

cos | [.0,PI.] is one-to-one by Lm3, Th59;

coherence

cos | [.PI,(2 * PI).] is one-to-one by Lm4, Th60;

end;
cos | [.0,PI.] is one-to-one by Lm3, Th59;

coherence

cos | [.PI,(2 * PI).] is one-to-one by Lm4, Th60;

registration

coherence

cos | [.0,(PI / 2).] is one-to-one

cos | [.(PI / 2),PI.] is one-to-one

cos | [.PI,((3 / 2) * PI).] is one-to-one

cos | [.((3 / 2) * PI),(2 * PI).] is one-to-one

end;
cos | [.0,(PI / 2).] is one-to-one

proof end;

coherence cos | [.(PI / 2),PI.] is one-to-one

proof end;

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

proof end;

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

proof end;

registration

coherence

cos | ].0,PI.[ is one-to-one

cos | ].PI,(2 * PI).[ is one-to-one

cos | ].0,(PI / 2).[ is one-to-one

cos | ].(PI / 2),PI.[ is one-to-one

cos | ].PI,((3 / 2) * PI).[ is one-to-one

cos | ].((3 / 2) * PI),(2 * PI).[ is one-to-one

end;
cos | ].0,PI.[ is one-to-one

proof end;

coherence cos | ].PI,(2 * PI).[ is one-to-one

proof end;

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

proof end;

coherence cos | ].(PI / 2),PI.[ is one-to-one

proof end;

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

proof end;

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

proof 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

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;

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

by FUNCT_1:43;

theorem :: SIN_COS6:65

theorem :: SIN_COS6:67

theorem :: SIN_COS6:73

theorem :: SIN_COS6:74

theorem :: SIN_COS6:75

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))) ) )

( arcsin is_differentiable_on ].(- 1),1.[ & ( - 1 < r & r < 1 implies diff (arcsin,r) = 1 / (sqrt (1 - (r ^2))) ) )

proof end;

Lm16: arccos " = cos | [.0,PI.]

by FUNCT_1:43;

theorem :: SIN_COS6:96

theorem :: SIN_COS6:97

theorem :: SIN_COS6:98

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)))) ) )

( arccos is_differentiable_on ].(- 1),1.[ & ( - 1 < r & r < 1 implies diff (arccos,r) = - (1 / (sqrt (1 - (r ^2)))) ) )

proof end;

:: Correspondence between arcsin and arccos