:: Formulas And Identities of Trigonometric Functions
:: by Pacharapokin Chanapat, Kanchun and Hiroshi Yamazaki
::
:: Received February 3, 2004
:: Copyright (c) 2004-2021 Association of Mizar Users

definition

let th be Real;

func tan th -> Real equals :: SIN_COS4:def 1
(sin th) / (cos th);

correctness
coherence
(sin th) / (cos th) is Real;
;

end;

:: deftheorem defines tan SIN_COS4:def 1 :
for th being Real holds tan th = (sin th) / (cos th);

definition

let th be Real;

func cot th -> Real equals :: SIN_COS4:def 2
(cos th) / (sin th);

correctness
coherence
(cos th) / (sin th) is Real;
;

end;

:: deftheorem defines cot SIN_COS4:def 2 :
for th being Real holds cot th = (cos th) / (sin th);

definition

let th be Real;

func cosec th -> Real equals :: SIN_COS4:def 3
1 / (sin th);

correctness
coherence
1 / (sin th) is Real;
;

end;

:: deftheorem defines cosec SIN_COS4:def 3 :
for th being Real holds cosec th = 1 / (sin th);

definition

let th be Real;

func sec th -> Real equals :: SIN_COS4:def 4
1 / (cos th);

correctness
coherence
1 / (cos th) is Real;
;

end;

:: deftheorem defines sec SIN_COS4:def 4 :
for th being Real holds sec th = 1 / (cos th);

theorem :: SIN_COS4:1

for th being Real holds tan (- th) = - (tan th)

proof end;

theorem :: SIN_COS4:2

for th being Real holds cosec (- th) = - (1 / (sin th))

proof end;

theorem :: SIN_COS4:3

for th being Real holds cot (- th) = - (cot th)

proof end;

theorem Th4: :: SIN_COS4:4

for th being Real holds (sin th) * (sin th) = 1 - ((cos th) * (cos th))

proof end;

theorem Th5: :: SIN_COS4:5

for th being Real holds (cos th) * (cos th) = 1 - ((sin th) * (sin th))

proof end;

theorem Th6: :: SIN_COS4:6

for th being Real st cos th <> 0 holds
sin th = (cos th) * (tan th)

proof end;

theorem :: SIN_COS4:7

for th1, th2 being Real 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 holds (sin (th1 + th2)) + (sin (th1 - th2)) = 2 * ((sin th1) * (cos th2))

proof end;

theorem :: SIN_COS4:26

for th1, th2 being Real holds (sin (th1 + th2)) - (sin (th1 - th2)) = 2 * ((cos th1) * (sin th2))

proof end;

theorem :: SIN_COS4:27

for th1, th2 being Real holds (cos (th1 + th2)) + (cos (th1 - th2)) = 2 * ((cos th1) * (cos th2))

proof end;

theorem :: SIN_COS4:28

for th1, th2 being Real holds (cos (th1 + th2)) - (cos (th1 - th2)) = - (2 * ((sin th1) * (sin th2)))

proof end;

theorem Th29: :: SIN_COS4:29

for th1, th2 being Real 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 holds ((cos th1) + (cos th2)) / ((cos th1) - (cos th2)) = (cot ((th1 + th2) / 2)) * (cot ((th2 - th1) / 2))

proof end;