:: Formulas And Identities of Trigonometric Functions
::  by Yuzhong Ding and Xiquan Liang
::
:: Received March 18, 2004
:: Copyright (c) 2004-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SIN_COS, CARD_1, SIN_COS4, ARYTM_3, RELAT_1, ARYTM_1,
      SQUARE_1, NEWTON, COMPLEX1, XXREAL_0, REAL_1, SIN_COS2, FUNCT_1,
      SIN_COS5;
 notations FUNCT_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1,
      SQUARE_1, SIN_COS4, SIN_COS, NEWTON, NAT_1, SIN_COS2, XXREAL_0;
 constructors REAL_1, SQUARE_1, NAT_1, BINOP_2, SIN_COS, SIN_COS2, SIN_COS4,
      VALUED_1, NEWTON;
 registrations XREAL_0, SQUARE_1, MEMBERED, NEWTON, SIN_COS, VALUED_0,
      RELSET_1, SIN_COS2;
 requirements REAL, NUMERALS, SUBSET, ARITHM;


begin

reserve x,x1,x2,x3 for Real;

theorem :: SIN_COS5:1
  cos(x)<>0 implies cosec(x)=sec(x)/tan(x);

theorem :: SIN_COS5:2
  sin(x)<>0 implies cos(x) = sin(x)*cot(x);

theorem :: SIN_COS5:3
  sin(x1)<>0 & sin(x2)<>0 & sin(x3)<>0 implies sin(x1+x2+x3)=sin(x1)*sin
  (x2)*sin(x3)*(cot(x2)*cot(x3)+ cot(x1)*cot(x3)+cot(x1)*cot(x2)-1);

theorem :: SIN_COS5:4
  sin(x1)<>0 & sin(x2)<>0 & sin(x3)<>0 implies cos(x1+x2+x3)=-sin(x1)*
  sin(x2)*sin(x3)*(cot(x1)+cot(x2)+cot(x3)- cot(x1)*cot(x2)*cot(x3));

theorem :: SIN_COS5:5
  sin(2*x) = 2*sin(x)*cos(x);

theorem :: SIN_COS5:6
  cos(x)<>0 implies sin(2*x)=(2*tan(x))/(1+(tan(x))^2);

theorem :: SIN_COS5:7
  cos(2*x)=(cos(x))^2-(sin(x))^2 & cos(2*x)=2*(cos(x))^2-1 & cos(2*
  x)=1-2*(sin(x))^2;

theorem :: SIN_COS5:8
  cos(x)<>0 implies cos(2*x)=(1-(tan(x))^2)/(1+(tan(x))^2);

theorem :: SIN_COS5:9
  cos(x)<>0 implies tan(2*x)=(2*tan(x))/(1-(tan(x))^2);

theorem :: SIN_COS5:10
  sin(x)<>0 implies cot(2*x)=((cot(x))^2-1)/(2*cot(x));

theorem :: SIN_COS5:11
  cos(x)<>0 implies (sec x)^2 = 1 + (tan x)^2;

theorem :: SIN_COS5:12
  cot(x) = 1/tan(x);

theorem :: SIN_COS5:13
  cos(x)<>0 & sin(x)<>0 implies sec(2*x) = (sec(x))^2/(1-(tan(x))
  ^2) & sec(2*x)=(cot(x)+tan(x))/(cot(x)-tan(x));

theorem :: SIN_COS5:14
  sin(x)<>0 implies (cosec(x))^2 = 1 +(cot(x))^2;

theorem :: SIN_COS5:15
  cos(x)<>0 & sin(x)<>0 implies cosec(2*x)=sec(x)*cosec(x)/2 & cosec(2*x
  )=(tan(x)+cot(x))/2;

theorem :: SIN_COS5:16
  sin(3*x)=-4*(sin(x))|^3+3*sin(x);

theorem :: SIN_COS5:17
  cos(3*x)=4*(cos(x))|^3-3*cos(x);

theorem :: SIN_COS5:18
  cos(x)<>0 implies tan(3*x)=(3*tan(x)-(tan(x))|^3)/(1-3*(tan(x))^2);

theorem :: SIN_COS5:19
  sin(x)<>0 implies cot(3*x)=((cot(x))|^3-3*cot(x))/(3*(cot(x))^2-1);

theorem :: SIN_COS5:20
  (sin(x))^2=(1-cos(2*x))/2;

theorem :: SIN_COS5:21
  (cos(x))^2=(1+cos(2*x))/2;

theorem :: SIN_COS5:22
  (sin(x))|^3=(3*sin(x)-sin(3*x))/4;

theorem :: SIN_COS5:23
  (cos(x))|^3=(3*cos(x)+cos(3*x))/4;

theorem :: SIN_COS5:24
  (sin(x))|^4=(3-4*cos(2*x)+cos(4*x))/8;

theorem :: SIN_COS5:25
  (cos(x))|^4 = (3+4*cos(2*x)+cos(4*x))/8;

:: Half Angle

theorem :: SIN_COS5:26
  sin(x/2)=sqrt((1-cos(x))/2) or sin(x/2)=-sqrt((1-cos(x))/2);

theorem :: SIN_COS5:27
  cos(x/2)=sqrt((1+cos(x))/2) or cos(x/2)=-sqrt((1+cos(x))/2);

theorem :: SIN_COS5:28
  sin(x/2)<>0 implies tan(x/2)=(1-cos(x))/sin(x);

theorem :: SIN_COS5:29
  cos(x/2)<>0 implies tan(x/2)=sin(x)/(1+cos(x));

theorem :: SIN_COS5:30
  tan(x/2)=sqrt((1-cos(x))/(1+cos(x))) or tan(x/2)=-sqrt((1-cos(x))/(1+
  cos(x)));

theorem :: SIN_COS5:31
  cos(x/2)<>0 implies cot(x/2)=(1+cos(x))/sin(x);

theorem :: SIN_COS5:32
  sin(x/2)<>0 implies cot(x/2)=sin(x)/(1-cos(x));

theorem :: SIN_COS5:33
  cot(x/2) = sqrt((1+cos(x))/(1-cos(x))) or cot(x/2) =-sqrt((1+cos(x))/(
  1-cos(x)));

theorem :: SIN_COS5:34
  sin(x/2)<>0 & cos(x/2)<>0 & 1-(tan(x/2))^2<>0 implies sec(x/2)= sqrt((
  2*sec(x))/(sec(x)+1)) or sec(x/2)=-sqrt((2*sec(x))/(sec(x)+1));

theorem :: SIN_COS5:35
  sin(x/2)<>0 & cos(x/2)<>0 & 1-(tan(x/2))^2<>0 implies cosec(x/2)= sqrt
  ((2*sec(x))/(sec(x)-1)) or cosec(x/2)=-sqrt((2*sec(x))/(sec(x)-1));

definition
  let x be Real;
  func coth(x) -> Real equals
:: SIN_COS5:def 1
  cosh(x)/sinh(x);
  func sech(x) -> Real equals
:: SIN_COS5:def 2
  1/cosh(x);
  func cosech(x) -> Real equals
:: SIN_COS5:def 3
  1/sinh(x);
end;

theorem :: SIN_COS5:36
  coth(x)=(exp_R(x)+exp_R(-x))/(exp_R(x)-exp_R(-x)) & sech(x)=2/(
  exp_R(x)+exp_R(-x)) & cosech(x)=2/(exp_R(x)-exp_R(-x));

theorem :: SIN_COS5:37
  exp_R(x)-exp_R(-x)<>0 implies tanh(x)*coth(x)=1;

theorem :: SIN_COS5:38
  (sech(x))^2+(tanh(x))^2=1;

theorem :: SIN_COS5:39
  sinh x <> 0 implies (coth x)^2-(cosech x)^2=1;

theorem :: SIN_COS5:40
  sinh(x1)<>0 & sinh(x2)<>0 implies coth(x1+x2)=(1+coth(x1)*coth(
  x2))/(coth(x1)+coth(x2));

theorem :: SIN_COS5:41
  sinh(x1)<>0 & sinh(x2)<>0 implies coth(x1-x2)=(1-coth(x1)*coth(x2))/(
  coth(x1)-coth(x2));

theorem :: SIN_COS5:42
  sinh(x1)<>0 & sinh(x2)<>0 implies coth(x1)+coth(x2)=sinh(x1+x2)/(sinh(
  x1)*sinh(x2)) & coth(x1)-coth(x2)=-(sinh(x1-x2))/(sinh(x1)*sinh(x2));

theorem :: SIN_COS5:43
  sinh(3*x)=3*sinh(x)+4*(sinh(x))|^3;

theorem :: SIN_COS5:44
  cosh(3*x)=4*(cosh(x))|^3-3*cosh(x);

theorem :: SIN_COS5:45
  sinh(x)<>0 implies coth(2*x)=(1+(coth(x))^2)/(2*coth(x));

theorem :: SIN_COS5:46
  x >= 0 implies sinh x >= 0;

theorem :: SIN_COS5:47
  x<=0 implies sinh x<=0;

theorem :: SIN_COS5:48
  cosh(x/2)=sqrt((cosh(x)+1)/2);

theorem :: SIN_COS5:49
  sinh(x/2)<>0 implies tanh(x/2)=(cosh(x)-1)/(sinh(x));

theorem :: SIN_COS5:50
  cosh(x/2)<>0 implies tanh(x/2)=(sinh(x))/(cosh(x)+1);

theorem :: SIN_COS5:51
  sinh(x/2)<>0 implies coth(x/2)=(sinh(x))/(cosh(x)-1);

theorem :: SIN_COS5:52
  cosh(x/2)<>0 implies coth(x/2)=(cosh(x)+1)/(sinh(x));