:: by Pacharapokin Chanapat, Kanchun and Hiroshi Yamazaki

::

:: Received February 3, 2004

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

begin

definition
end;

:: deftheorem defines tan SIN_COS4:def 1 :

for th being real number holds tan th = (sin th) / (cos th);

for th being real number holds tan th = (sin th) / (cos th);

definition
end;

:: deftheorem defines cot SIN_COS4:def 2 :

for th being real number holds cot th = (cos th) / (sin th);

for th being real number holds cot th = (cos th) / (sin th);

definition
end;

:: deftheorem defines cosec SIN_COS4:def 3 :

for th being real number holds cosec th = 1 / (sin th);

for th being real number holds cosec th = 1 / (sin th);

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

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

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

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

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

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

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

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)

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

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

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

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

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

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

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

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

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

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

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

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

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