:: 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)
proofend;

theorem :: SIN_COS4:2
for th being real number holds cosec (- th) = - (1 / (sin th))
proofend;

theorem :: SIN_COS4:3
for th being real number holds cot (- th) = - (cot th)
proofend;

theorem Th4: :: SIN_COS4:4
for th being real number holds (sin th) * (sin th) = 1 - ((cos th) * (cos th))
proofend;

theorem Th5: :: SIN_COS4:5
for th being real number holds (cos th) * (cos th) = 1 - ((sin th) * (sin th))
proofend;

theorem Th6: :: SIN_COS4:6
for th being real number st cos th <> 0 holds
sin th = (cos th) * (tan th)
proofend;

theorem :: SIN_COS4:7
for th1, th2 being real number st cos th1 <> 0 &amp; cos th2 <> 0 holds
tan (th1 + th2) = ((tan th1) + (tan th2)) / (1 - ((tan th1) * (tan th2)))
proofend;

theorem :: SIN_COS4:8
for th1, th2 being real number st cos th1 <> 0 &amp; cos th2 <> 0 holds
tan (th1 - th2) = ((tan th1) - (tan th2)) / (1 + ((tan th1) * (tan th2)))
proofend;

theorem :: SIN_COS4:9
for th1, th2 being real number st sin th1 <> 0 &amp; sin th2 <> 0 holds
cot (th1 + th2) = (((cot th1) * (cot th2)) - 1) / ((cot th2) + (cot th1))
proofend;

theorem :: SIN_COS4:10
for th1, th2 being real number st sin th1 <> 0 &amp; sin th2 <> 0 holds
cot (th1 - th2) = (((cot th1) * (cot th2)) + 1) / ((cot th2) - (cot th1))
proofend;

theorem Th11: :: SIN_COS4:11
for th1, th2, th3 being real number st cos th1 <> 0 &amp; cos th2 <> 0 &amp; 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)))
proofend;

theorem Th12: :: SIN_COS4:12
for th1, th2, th3 being real number st cos th1 <> 0 &amp; cos th2 <> 0 &amp; 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)))
proofend;

theorem :: SIN_COS4:13
for th1, th2, th3 being real number st cos th1 <> 0 &amp; cos th2 <> 0 &amp; 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)))
proofend;

theorem :: SIN_COS4:14
for th1, th2, th3 being real number st sin th1 <> 0 &amp; sin th2 <> 0 &amp; 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)
proofend;

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

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

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

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

theorem :: SIN_COS4:19
for th1, th2 being real number st cos th1 <> 0 &amp; cos th2 <> 0 holds
(tan th1) + (tan th2) = (sin (th1 + th2)) / ((cos th1) * (cos th2))
proofend;

theorem :: SIN_COS4:20
for th1, th2 being real number st cos th1 <> 0 &amp; cos th2 <> 0 holds
(tan th1) - (tan th2) = (sin (th1 - th2)) / ((cos th1) * (cos th2))
proofend;

theorem :: SIN_COS4:21
for th1, th2 being real number st cos th1 <> 0 &amp; sin th2 <> 0 holds
(tan th1) + (cot th2) = (cos (th1 - th2)) / ((cos th1) * (sin th2))
proofend;

theorem :: SIN_COS4:22
for th1, th2 being real number st cos th1 <> 0 &amp; sin th2 <> 0 holds
(tan th1) - (cot th2) = - ((cos (th1 + th2)) / ((cos th1) * (sin th2)))
proofend;

theorem :: SIN_COS4:23
for th1, th2 being real number st sin th1 <> 0 &amp; sin th2 <> 0 holds
(cot th1) + (cot th2) = (sin (th1 + th2)) / ((sin th1) * (sin th2))
proofend;

theorem :: SIN_COS4:24
for th1, th2 being real number st sin th1 <> 0 &amp; sin th2 <> 0 holds
(cot th1) - (cot th2) = - ((sin (th1 - th2)) / ((sin th1) * (sin th2)))
proofend;

theorem :: SIN_COS4:25
for th1, th2 being real number holds (sin (th1 + th2)) + (sin (th1 - th2)) = 2 * ((sin th1) * (cos th2))
proofend;

theorem :: SIN_COS4:26
for th1, th2 being real number holds (sin (th1 + th2)) - (sin (th1 - th2)) = 2 * ((cos th1) * (sin th2))
proofend;

theorem :: SIN_COS4:27
for th1, th2 being real number holds (cos (th1 + th2)) + (cos (th1 - th2)) = 2 * ((cos th1) * (cos th2))
proofend;

theorem :: SIN_COS4:28
for th1, th2 being real number holds (cos (th1 + th2)) - (cos (th1 - th2)) = - (2 * ((sin th1) * (sin th2)))
proofend;

theorem Th29: :: SIN_COS4:29
for th1, th2 being real number holds (sin th1) * (sin th2) = - ((1 / 2) * ((cos (th1 + th2)) - (cos (th1 - th2))))
proofend;

theorem Th30: :: SIN_COS4:30
for th1, th2 being real number holds (sin th1) * (cos th2) = (1 / 2) * ((sin (th1 + th2)) + (sin (th1 - th2)))
proofend;

theorem Th31: :: SIN_COS4:31
for th1, th2 being real number holds (cos th1) * (sin th2) = (1 / 2) * ((sin (th1 + th2)) - (sin (th1 - th2)))
proofend;

theorem Th32: :: SIN_COS4:32
for th1, th2 being real number holds (cos th1) * (cos th2) = (1 / 2) * ((cos (th1 + th2)) + (cos (th1 - th2)))
proofend;

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

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

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

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

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

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

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

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

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

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

theorem :: SIN_COS4:43
for th1, th2 being real number st cos th1 <> 0 &amp; cos th2 <> 0 holds
(sin (th1 + th2)) / (sin (th1 - th2)) = ((tan th1) + (tan th2)) / ((tan th1) - (tan th2))
proofend;

theorem :: SIN_COS4:44
for th1, th2 being real number st cos th1 <> 0 &amp; cos th2 <> 0 holds
(cos (th1 + th2)) / (cos (th1 - th2)) = (1 - ((tan th1) * (tan th2))) / (1 + ((tan th1) * (tan th2)))
proofend;

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

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

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

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

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

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