:: Formulas And Identities of Trigonometric Functions
:: by Pacharapokin Chanapat, Kanchun and Hiroshi Yamazaki
::
:: Received February 3, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users
begin
definition
let
th
be
real
number
;
func
tan
th
->
Real
equals
:: SIN_COS4:def 1
(
sin
th
)
/
(
cos
th
)
;
correctness
coherence
(
sin
th
)
/
(
cos
th
)
is
Real
;
by
XREAL_0:def 1
;
end;
::
deftheorem
defines
tan
SIN_COS4:def 1 :
for
th
being
real
number
holds
tan
th
=
(
sin
th
)
/
(
cos
th
)
;
definition
let
th
be
real
number
;
func
cot
th
->
Real
equals
:: SIN_COS4:def 2
(
cos
th
)
/
(
sin
th
)
;
correctness
coherence
(
cos
th
)
/
(
sin
th
)
is
Real
;
by
XREAL_0:def 1
;
end;
::
deftheorem
defines
cot
SIN_COS4:def 2 :
for
th
being
real
number
holds
cot
th
=
(
cos
th
)
/
(
sin
th
)
;
definition
let
th
be
real
number
;
func
cosec
th
->
Real
equals
:: SIN_COS4:def 3
1
/
(
sin
th
)
;
correctness
coherence
1
/
(
sin
th
)
is
Real
;
by
XREAL_0:def 1
;
end;
::
deftheorem
defines
cosec
SIN_COS4:def 3 :
for
th
being
real
number
holds
cosec
th
=
1
/
(
sin
th
)
;
definition
let
th
be
real
number
;
func
sec
th
->
Real
equals
:: SIN_COS4:def 4
1
/
(
cos
th
)
;
correctness
coherence
1
/
(
cos
th
)
is
Real
;
by
XREAL_0:def 1
;
end;
::
deftheorem
defines
sec
SIN_COS4:def 4 :
for
th
being
real
number
holds
sec
th
=
1
/
(
cos
th
)
;
theorem
:: SIN_COS4:1
for
th
being
real
number
holds
tan
(
-
th
)
=
-
(
tan
th
)
proof
end;
theorem
:: SIN_COS4:2
for
th
being
real
number
holds
cosec
(
-
th
)
=
-
(
1
/
(
sin
th
)
)
proof
end;
theorem
:: SIN_COS4:3
for
th
being
real
number
holds
cot
(
-
th
)
=
-
(
cot
th
)
proof
end;
theorem
Th4
:
:: SIN_COS4:4
for
th
being
real
number
holds
(
sin
th
)
*
(
sin
th
)
=
1
-
(
(
cos
th
)
*
(
cos
th
)
)
proof
end;
theorem
Th5
:
:: SIN_COS4:5
for
th
being
real
number
holds
(
cos
th
)
*
(
cos
th
)
=
1
-
(
(
sin
th
)
*
(
sin
th
)
)
proof
end;
theorem
Th6
:
:: SIN_COS4:6
for
th
being
real
number
st
cos
th
<>
0
holds
sin
th
=
(
cos
th
)
*
(
tan
th
)
proof
end;
theorem
:: SIN_COS4:7
for
th1
,
th2
being
real
number
st
cos
th1
<>
0
&
cos
th2
<>
0
holds
tan
(
th1
+
th2
)
=
(
(
tan
th1
)
+
(
tan
th2
)
)
/
(
1
-
(
(
tan
th1
)
*
(
tan
th2
)
)
)
proof
end;
theorem
:: SIN_COS4:8
for
th1
,
th2
being
real
number
st
cos
th1
<>
0
&
cos
th2
<>
0
holds
tan
(
th1
-
th2
)
=
(
(
tan
th1
)
-
(
tan
th2
)
)
/
(
1
+
(
(
tan
th1
)
*
(
tan
th2
)
)
)
proof
end;
theorem
:: SIN_COS4:9
for
th1
,
th2
being
real
number
st
sin
th1
<>
0
&
sin
th2
<>
0
holds
cot
(
th1
+
th2
)
=
(
(
(
cot
th1
)
*
(
cot
th2
)
)
-
1
)
/
(
(
cot
th2
)
+
(
cot
th1
)
)
proof
end;
theorem
:: SIN_COS4:10
for
th1
,
th2
being
real
number
st
sin
th1
<>
0
&
sin
th2
<>
0
holds
cot
(
th1
-
th2
)
=
(
(
(
cot
th1
)
*
(
cot
th2
)
)
+
1
)
/
(
(
cot
th2
)
-
(
cot
th1
)
)
proof
end;
theorem
Th11
:
:: SIN_COS4:11
for
th1
,
th2
,
th3
being
real
number
st
cos
th1
<>
0
&
cos
th2
<>
0
&
cos
th3
<>
0
holds
sin
(
(
th1
+
th2
)
+
th3
)
=
(
(
(
cos
th1
)
*
(
cos
th2
)
)
*
(
cos
th3
)
)
*
(
(
(
(
tan
th1
)
+
(
tan
th2
)
)
+
(
tan
th3
)
)
-
(
(
(
tan
th1
)
*
(
tan
th2
)
)
*
(
tan
th3
)
)
)
proof
end;
theorem
Th12
:
:: SIN_COS4:12
for
th1
,
th2
,
th3
being
real
number
st
cos
th1
<>
0
&
cos
th2
<>
0
&
cos
th3
<>
0
holds
cos
(
(
th1
+
th2
)
+
th3
)
=
(
(
(
cos
th1
)
*
(
cos
th2
)
)
*
(
cos
th3
)
)
*
(
(
(
1
-
(
(
tan
th2
)
*
(
tan
th3
)
)
)
-
(
(
tan
th3
)
*
(
tan
th1
)
)
)
-
(
(
tan
th1
)
*
(
tan
th2
)
)
)
proof
end;
theorem
:: SIN_COS4:13
for
th1
,
th2
,
th3
being
real
number
st
cos
th1
<>
0
&
cos
th2
<>
0
&
cos
th3
<>
0
holds
tan
(
(
th1
+
th2
)
+
th3
)
=
(
(
(
(
tan
th1
)
+
(
tan
th2
)
)
+
(
tan
th3
)
)
-
(
(
(
tan
th1
)
*
(
tan
th2
)
)
*
(
tan
th3
)
)
)
/
(
(
(
1
-
(
(
tan
th2
)
*
(
tan
th3
)
)
)
-
(
(
tan
th3
)
*
(
tan
th1
)
)
)
-
(
(
tan
th1
)
*
(
tan
th2
)
)
)
proof
end;
theorem
:: SIN_COS4:14
for
th1
,
th2
,
th3
being
real
number
st
sin
th1
<>
0
&
sin
th2
<>
0
&
sin
th3
<>
0
holds
cot
(
(
th1
+
th2
)
+
th3
)
=
(
(
(
(
(
(
cot
th1
)
*
(
cot
th2
)
)
*
(
cot
th3
)
)
-
(
cot
th1
)
)
-
(
cot
th2
)
)
-
(
cot
th3
)
)
/
(
(
(
(
(
cot
th2
)
*
(
cot
th3
)
)
+
(
(
cot
th3
)
*
(
cot
th1
)
)
)
+
(
(
cot
th1
)
*
(
cot
th2
)
)
)
-
1
)
proof
end;
theorem
Th15
:
:: SIN_COS4:15
for
th1
,
th2
being
real
number
holds
(
sin
th1
)
+
(
sin
th2
)
=
2
*
(
(
cos
(
(
th1
-
th2
)
/
2
)
)
*
(
sin
(
(
th1
+
th2
)
/
2
)
)
)
proof
end;
theorem
Th16
:
:: SIN_COS4:16
for
th1
,
th2
being
real
number
holds
(
sin
th1
)
-
(
sin
th2
)
=
2
*
(
(
cos
(
(
th1
+
th2
)
/
2
)
)
*
(
sin
(
(
th1
-
th2
)
/
2
)
)
)
proof
end;
theorem
Th17
:
:: SIN_COS4:17
for
th1
,
th2
being
real
number
holds
(
cos
th1
)
+
(
cos
th2
)
=
2
*
(
(
cos
(
(
th1
+
th2
)
/
2
)
)
*
(
cos
(
(
th1
-
th2
)
/
2
)
)
)
proof
end;
theorem
Th18
:
:: SIN_COS4:18
for
th1
,
th2
being
real
number
holds
(
cos
th1
)
-
(
cos
th2
)
=
-
(
2
*
(
(
sin
(
(
th1
+
th2
)
/
2
)
)
*
(
sin
(
(
th1
-
th2
)
/
2
)
)
)
)
proof
end;
theorem
:: SIN_COS4:19
for
th1
,
th2
being
real
number
st
cos
th1
<>
0
&
cos
th2
<>
0
holds
(
tan
th1
)
+
(
tan
th2
)
=
(
sin
(
th1
+
th2
)
)
/
(
(
cos
th1
)
*
(
cos
th2
)
)
proof
end;
theorem
:: SIN_COS4:20
for
th1
,
th2
being
real
number
st
cos
th1
<>
0
&
cos
th2
<>
0
holds
(
tan
th1
)
-
(
tan
th2
)
=
(
sin
(
th1
-
th2
)
)
/
(
(
cos
th1
)
*
(
cos
th2
)
)
proof
end;
theorem
:: SIN_COS4:21
for
th1
,
th2
being
real
number
st
cos
th1
<>
0
&
sin
th2
<>
0
holds
(
tan
th1
)
+
(
cot
th2
)
=
(
cos
(
th1
-
th2
)
)
/
(
(
cos
th1
)
*
(
sin
th2
)
)
proof
end;
theorem
:: SIN_COS4:22
for
th1
,
th2
being
real
number
st
cos
th1
<>
0
&
sin
th2
<>
0
holds
(
tan
th1
)
-
(
cot
th2
)
=
-
(
(
cos
(
th1
+
th2
)
)
/
(
(
cos
th1
)
*
(
sin
th2
)
)
)
proof
end;
theorem
:: SIN_COS4:23
for
th1
,
th2
being
real
number
st
sin
th1
<>
0
&
sin
th2
<>
0
holds
(
cot
th1
)
+
(
cot
th2
)
=
(
sin
(
th1
+
th2
)
)
/
(
(
sin
th1
)
*
(
sin
th2
)
)
proof
end;
theorem
:: SIN_COS4:24
for
th1
,
th2
being
real
number
st
sin
th1
<>
0
&
sin
th2
<>
0
holds
(
cot
th1
)
-
(
cot
th2
)
=
-
(
(
sin
(
th1
-
th2
)
)
/
(
(
sin
th1
)
*
(
sin
th2
)
)
)
proof
end;
theorem
:: SIN_COS4:25
for
th1
,
th2
being
real
number
holds
(
sin
(
th1
+
th2
)
)
+
(
sin
(
th1
-
th2
)
)
=
2
*
(
(
sin
th1
)
*
(
cos
th2
)
)
proof
end;
theorem
:: SIN_COS4:26
for
th1
,
th2
being
real
number
holds
(
sin
(
th1
+
th2
)
)
-
(
sin
(
th1
-
th2
)
)
=
2
*
(
(
cos
th1
)
*
(
sin
th2
)
)
proof
end;
theorem
:: SIN_COS4:27
for
th1
,
th2
being
real
number
holds
(
cos
(
th1
+
th2
)
)
+
(
cos
(
th1
-
th2
)
)
=
2
*
(
(
cos
th1
)
*
(
cos
th2
)
)
proof
end;
theorem
:: SIN_COS4:28
for
th1
,
th2
being
real
number
holds
(
cos
(
th1
+
th2
)
)
-
(
cos
(
th1
-
th2
)
)
=
-
(
2
*
(
(
sin
th1
)
*
(
sin
th2
)
)
)
proof
end;
theorem
Th29
:
:: SIN_COS4:29
for
th1
,
th2
being
real
number
holds
(
sin
th1
)
*
(
sin
th2
)
=
-
(
(
1
/
2
)
*
(
(
cos
(
th1
+
th2
)
)
-
(
cos
(
th1
-
th2
)
)
)
)
proof
end;
theorem
Th30
:
:: SIN_COS4:30
for
th1
,
th2
being
real
number
holds
(
sin
th1
)
*
(
cos
th2
)
=
(
1
/
2
)
*
(
(
sin
(
th1
+
th2
)
)
+
(
sin
(
th1
-
th2
)
)
)
proof
end;
theorem
Th31
:
:: SIN_COS4:31
for
th1
,
th2
being
real
number
holds
(
cos
th1
)
*
(
sin
th2
)
=
(
1
/
2
)
*
(
(
sin
(
th1
+
th2
)
)
-
(
sin
(
th1
-
th2
)
)
)
proof
end;
theorem
Th32
:
:: SIN_COS4:32
for
th1
,
th2
being
real
number
holds
(
cos
th1
)
*
(
cos
th2
)
=
(
1
/
2
)
*
(
(
cos
(
th1
+
th2
)
)
+
(
cos
(
th1
-
th2
)
)
)
proof
end;
theorem
:: SIN_COS4:33
for
th1
,
th2
,
th3
being
real
number
holds
(
(
sin
th1
)
*
(
sin
th2
)
)
*
(
sin
th3
)
=
(
1
/
4
)
*
(
(
(
(
sin
(
(
th1
+
th2
)
-
th3
)
)
+
(
sin
(
(
th2
+
th3
)
-
th1
)
)
)
+
(
sin
(
(
th3
+
th1
)
-
th2
)
)
)
-
(
sin
(
(
th1
+
th2
)
+
th3
)
)
)
proof
end;
theorem
:: SIN_COS4:34
for
th1
,
th2
,
th3
being
real
number
holds
(
(
sin
th1
)
*
(
sin
th2
)
)
*
(
cos
th3
)
=
(
1
/
4
)
*
(
(
(
(
-
(
cos
(
(
th1
+
th2
)
-
th3
)
)
)
+
(
cos
(
(
th2
+
th3
)
-
th1
)
)
)
+
(
cos
(
(
th3
+
th1
)
-
th2
)
)
)
-
(
cos
(
(
th1
+
th2
)
+
th3
)
)
)
proof
end;
theorem
:: SIN_COS4:35
for
th1
,
th2
,
th3
being
real
number
holds
(
(
sin
th1
)
*
(
cos
th2
)
)
*
(
cos
th3
)
=
(
1
/
4
)
*
(
(
(
(
sin
(
(
th1
+
th2
)
-
th3
)
)
-
(
sin
(
(
th2
+
th3
)
-
th1
)
)
)
+
(
sin
(
(
th3
+
th1
)
-
th2
)
)
)
+
(
sin
(
(
th1
+
th2
)
+
th3
)
)
)
proof
end;
theorem
:: SIN_COS4:36
for
th1
,
th2
,
th3
being
real
number
holds
(
(
cos
th1
)
*
(
cos
th2
)
)
*
(
cos
th3
)
=
(
1
/
4
)
*
(
(
(
(
cos
(
(
th1
+
th2
)
-
th3
)
)
+
(
cos
(
(
th2
+
th3
)
-
th1
)
)
)
+
(
cos
(
(
th3
+
th1
)
-
th2
)
)
)
+
(
cos
(
(
th1
+
th2
)
+
th3
)
)
)
proof
end;
theorem
Th37
:
:: SIN_COS4:37
for
th1
,
th2
being
real
number
holds
(
sin
(
th1
+
th2
)
)
*
(
sin
(
th1
-
th2
)
)
=
(
(
sin
th1
)
*
(
sin
th1
)
)
-
(
(
sin
th2
)
*
(
sin
th2
)
)
proof
end;
theorem
:: SIN_COS4:38
for
th1
,
th2
being
real
number
holds
(
sin
(
th1
+
th2
)
)
*
(
sin
(
th1
-
th2
)
)
=
(
(
cos
th2
)
*
(
cos
th2
)
)
-
(
(
cos
th1
)
*
(
cos
th1
)
)
proof
end;
theorem
Th39
:
:: SIN_COS4:39
for
th1
,
th2
being
real
number
holds
(
sin
(
th1
+
th2
)
)
*
(
cos
(
th1
-
th2
)
)
=
(
(
sin
th1
)
*
(
cos
th1
)
)
+
(
(
sin
th2
)
*
(
cos
th2
)
)
proof
end;
theorem
:: SIN_COS4:40
for
th1
,
th2
being
real
number
holds
(
cos
(
th1
+
th2
)
)
*
(
sin
(
th1
-
th2
)
)
=
(
(
sin
th1
)
*
(
cos
th1
)
)
-
(
(
sin
th2
)
*
(
cos
th2
)
)
proof
end;
theorem
Th41
:
:: SIN_COS4:41
for
th1
,
th2
being
real
number
holds
(
cos
(
th1
+
th2
)
)
*
(
cos
(
th1
-
th2
)
)
=
(
(
cos
th1
)
*
(
cos
th1
)
)
-
(
(
sin
th2
)
*
(
sin
th2
)
)
proof
end;
theorem
:: SIN_COS4:42
for
th1
,
th2
being
real
number
holds
(
cos
(
th1
+
th2
)
)
*
(
cos
(
th1
-
th2
)
)
=
(
(
cos
th2
)
*
(
cos
th2
)
)
-
(
(
sin
th1
)
*
(
sin
th1
)
)
proof
end;
theorem
:: SIN_COS4:43
for
th1
,
th2
being
real
number
st
cos
th1
<>
0
&
cos
th2
<>
0
holds
(
sin
(
th1
+
th2
)
)
/
(
sin
(
th1
-
th2
)
)
=
(
(
tan
th1
)
+
(
tan
th2
)
)
/
(
(
tan
th1
)
-
(
tan
th2
)
)
proof
end;
theorem
:: SIN_COS4:44
for
th1
,
th2
being
real
number
st
cos
th1
<>
0
&
cos
th2
<>
0
holds
(
cos
(
th1
+
th2
)
)
/
(
cos
(
th1
-
th2
)
)
=
(
1
-
(
(
tan
th1
)
*
(
tan
th2
)
)
)
/
(
1
+
(
(
tan
th1
)
*
(
tan
th2
)
)
)
proof
end;
theorem
:: SIN_COS4:45
for
th1
,
th2
being
real
number
holds
(
(
sin
th1
)
+
(
sin
th2
)
)
/
(
(
sin
th1
)
-
(
sin
th2
)
)
=
(
tan
(
(
th1
+
th2
)
/
2
)
)
*
(
cot
(
(
th1
-
th2
)
/
2
)
)
proof
end;
theorem
:: SIN_COS4:46
for
th1
,
th2
being
real
number
st
cos
(
(
th1
-
th2
)
/
2
)
<>
0
holds
(
(
sin
th1
)
+
(
sin
th2
)
)
/
(
(
cos
th1
)
+
(
cos
th2
)
)
=
tan
(
(
th1
+
th2
)
/
2
)
proof
end;
theorem
:: SIN_COS4:47
for
th1
,
th2
being
real
number
st
cos
(
(
th1
+
th2
)
/
2
)
<>
0
holds
(
(
sin
th1
)
-
(
sin
th2
)
)
/
(
(
cos
th1
)
+
(
cos
th2
)
)
=
tan
(
(
th1
-
th2
)
/
2
)
proof
end;
theorem
:: SIN_COS4:48
for
th1
,
th2
being
real
number
st
sin
(
(
th1
+
th2
)
/
2
)
<>
0
holds
(
(
sin
th1
)
+
(
sin
th2
)
)
/
(
(
cos
th2
)
-
(
cos
th1
)
)
=
cot
(
(
th1
-
th2
)
/
2
)
proof
end;
theorem
:: SIN_COS4:49
for
th1
,
th2
being
real
number
st
sin
(
(
th1
-
th2
)
/
2
)
<>
0
holds
(
(
sin
th1
)
-
(
sin
th2
)
)
/
(
(
cos
th2
)
-
(
cos
th1
)
)
=
cot
(
(
th1
+
th2
)
/
2
)
proof
end;
theorem
:: SIN_COS4:50
for
th1
,
th2
being
real
number
holds
(
(
cos
th1
)
+
(
cos
th2
)
)
/
(
(
cos
th1
)
-
(
cos
th2
)
)
=
(
cot
(
(
th1
+
th2
)
/
2
)
)
*
(
cot
(
(
th2
-
th1
)
/
2
)
)
proof
end;