The abstract of the Mizar article:

Properties of the Trigonometric Function

by

Takashi Mitsuishi, and

Yuguang Yang

Received March 13, 1999

MML identifier: SIN_COS2

[ Mizar article, MML identifier index ]

environ

 vocabulary ARYTM, RCOMP_1, ARYTM_3, SIN_COS, ARYTM_1, SQUARE_1, RFUNCT_2,
      FDIFF_1, FUNCT_1, PARTFUN1, RELAT_1, ORDINAL2, VECTSP_1, SEQ_1, SEQ_2,
      SEQM_3, BOOLE, PRE_TOPC, FCONT_1, SIN_COS2, FINSEQ_4, GROUP_1;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      REAL_1, RELAT_1, FCONT_1, FDIFF_1, NAT_1, FINSEQ_4, SQUARE_1, PREPOWER,
      PARTFUN1, SEQ_2, SEQM_3, RCOMP_1, RFUNCT_1, RFUNCT_2, SIN_COS, SEQ_1,
      VECTSP_1;
 constructors NAT_1, COMSEQ_3, REAL_1, SEQ_2, RCOMP_1, FINSEQ_4, FCONT_1,
      RFUNCT_1, FDIFF_1, GOBOARD1, SQUARE_1, PREPOWER, PARTFUN1, RFUNCT_2,
      SIN_COS, MEMBERED;
 clusters XREAL_0, RELSET_1, FDIFF_1, RCOMP_1, SEQ_1, MEMBERED, NUMBERS,
      ORDINAL2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin :: Monotone increasing and monotone decreasing of sine and cosine.

reserve p,q,r,th for Real;
reserve n for Nat;

 theorem :: SIN_COS2:1
 p>=0 & r>=0 implies p+r>=2*sqrt(p*r);

theorem :: SIN_COS2:2
  sin is_increasing_on ].0,PI/2.[;

theorem :: SIN_COS2:3
  sin is_decreasing_on ].PI/2,PI.[;

theorem :: SIN_COS2:4
  cos is_decreasing_on ].0,PI/2.[;

theorem :: SIN_COS2:5
  cos is_decreasing_on ].PI/2,PI.[;

theorem :: SIN_COS2:6
  sin is_decreasing_on ].PI,3/2*PI.[;

theorem :: SIN_COS2:7
  sin is_increasing_on ].3/2*PI,2*PI.[;

theorem :: SIN_COS2:8
  cos is_increasing_on ].PI,3/2*PI.[;

theorem :: SIN_COS2:9
  cos is_increasing_on ].3/2*PI,2*PI.[;

theorem :: SIN_COS2:10
  sin.th = sin.(2*PI*n + th);

theorem :: SIN_COS2:11
  cos.th = cos.(2*PI*n + th);

begin ::Hyperbolic sine, hyperbolic cosine and hyperbolic tangent.

definition
func sinh -> PartFunc of REAL, REAL means
:: SIN_COS2:def 1
 dom it= REAL & for d being real number holds it.d=(exp.(d) - exp.(-d))/2;
 end;

definition
let d be number;
 func sinh(d) equals
:: SIN_COS2:def 2
 sinh.d;
end;

definition
  let d be number;
 cluster sinh(d) -> real;
end;

definition
let d be number;
 redefine func sinh(d) -> Real;
end;

definition
func cosh -> PartFunc of REAL, REAL means
:: SIN_COS2:def 3
 dom it= REAL & for d being real number holds it.d=(exp.(d) + exp.(-d))/2;
 end;

definition let d be number;
  func cosh(d) equals
:: SIN_COS2:def 4
  cosh.d;
end;

definition let d be number;
 cluster cosh(d) -> real;
end;

definition let d be number;
 redefine func cosh(d) -> Real;
end;

 definition
 func tanh -> PartFunc of REAL, REAL means
:: SIN_COS2:def 5
  dom it= REAL &
  for d being real number holds it.d=(exp.(d) - exp.(-d))/(exp.(d) + exp.(-d));
 end;

 definition let d be number;
   func tanh(d) equals
:: SIN_COS2:def 6
   tanh.d;
 end;

 definition let d be number;
  cluster tanh(d) -> real;
 end;

 definition let d be number;
   redefine func tanh(d) -> Real;
 end;

 theorem :: SIN_COS2:12
 exp.(p+q) = exp.(p) * exp.(q);

 theorem :: SIN_COS2:13
 exp.0 = 1;

 theorem :: SIN_COS2:14
 (cosh.p)^2-(sinh.p)^2=1 &
 (cosh.p)*(cosh.p)-(sinh.p)*(sinh.p)=1;

theorem :: SIN_COS2:15
cosh.p <> 0 & cosh.p > 0 & cosh.0 = 1;

theorem :: SIN_COS2:16
sinh.0 = 0;

theorem :: SIN_COS2:17
tanh.p = (sinh.p)/(cosh.p);

theorem :: SIN_COS2:18
(sinh.p)^2 = 1/2*(cosh.(2*p) - 1) &
(cosh.p)^2 = 1/2*(cosh.(2*p) + 1);

theorem :: SIN_COS2:19
cosh.(-p) = cosh.p &
sinh.(-p) = -sinh.p &
tanh.(-p) = -tanh.p;

theorem :: SIN_COS2:20
  cosh.(p+r)=(cosh.p)*(cosh.r) + (sinh.p)*(sinh.r) &
cosh.(p-r)=(cosh.p)*(cosh.r) - (sinh.p)*(sinh.r);

theorem :: SIN_COS2:21
  sinh.(p+r)=(sinh.p)*(cosh.r) + (cosh.p)*(sinh.r) &
sinh.(p-r)=(sinh.p)*(cosh.r) - (cosh.p)*(sinh.r);

theorem :: SIN_COS2:22
  tanh.(p+r) = (tanh.p + tanh.r)/(1+ (tanh.p)*(tanh.r)) &
tanh.(p-r) = (tanh.p - tanh.r)/(1- (tanh.p)*(tanh.r));

theorem :: SIN_COS2:23
   sinh.(2*p) = 2*(sinh.p)*(cosh.p) &
 cosh.(2*p) = 2*(cosh.p)^2 - 1 &
 tanh.(2*p) = (2*tanh.p)/(1+(tanh.p)^2);

theorem :: SIN_COS2:24
(sinh.p)^2 - (sinh.q)^2 = (sinh.(p+q))*(sinh.(p-q)) &
(sinh.(p+q))*(sinh.(p-q)) = (cosh.p)^2 - (cosh.q)^2 &
(sinh.p)^2 - (sinh.q)^2 = (cosh.p)^2 - (cosh.q)^2;

theorem :: SIN_COS2:25
(sinh.p)^2 + (cosh.q)^2 = (cosh.(p+q))*(cosh.(p-q)) &
(cosh.(p+q))*(cosh.(p-q)) = (cosh.p)^2 + (sinh.q)^2 &
(sinh.p)^2 + (cosh.q)^2 = (cosh.p)^2 + (sinh.q)^2;

theorem :: SIN_COS2:26
   sinh.p + sinh.r = 2*(sinh.(p/2+r/2))*(cosh.(p/2-r/2)) &
 sinh.p - sinh.r = 2*(sinh.(p/2-r/2))*(cosh.(p/2+r/2));

 theorem :: SIN_COS2:27
   cosh.p + cosh.r = 2*(cosh.(p/2+r/2))*(cosh.(p/2-r/2)) &
 cosh.p - cosh.r = 2*(sinh.(p/2-r/2))*(sinh.(p/2+r/2));

 theorem :: SIN_COS2:28
   tanh.p + tanh.r = (sinh.(p+r))/((cosh.p)*(cosh.r)) &
 tanh.p - tanh.r = (sinh.(p-r))/((cosh.p)*(cosh.r));

theorem :: SIN_COS2:29
  (cosh.p + sinh.p) |^ n = cosh.(n*p) + sinh.(n*p);

definition
  cluster sinh -> total;

  cluster cosh -> total;

  cluster tanh -> total;
end;

theorem :: SIN_COS2:30
dom sinh=REAL & dom cosh=REAL & dom tanh=REAL;

 theorem :: SIN_COS2:31
 sinh is_differentiable_in p & diff(sinh,p)=cosh.p;

  theorem :: SIN_COS2:32
  cosh is_differentiable_in p & diff(cosh,p)=sinh.p;

 theorem :: SIN_COS2:33
  tanh is_differentiable_in p & diff(tanh,p)=1/(cosh.p)^2;

 theorem :: SIN_COS2:34
   sinh is_differentiable_on REAL &
   diff(sinh,p)=cosh.p;

 theorem :: SIN_COS2:35
  cosh is_differentiable_on REAL &
  diff(cosh,p)=sinh.p;

 theorem :: SIN_COS2:36
  tanh is_differentiable_on REAL &
  diff(tanh,p)=1/(cosh.p)^2;

 theorem :: SIN_COS2:37
   cosh.p >= 1;

 theorem :: SIN_COS2:38
   sinh is_continuous_in p;

 theorem :: SIN_COS2:39
   cosh is_continuous_in p;

 theorem :: SIN_COS2:40
   tanh is_continuous_in p;

 theorem :: SIN_COS2:41
   sinh is_continuous_on REAL;

 theorem :: SIN_COS2:42
   cosh is_continuous_on REAL;

 theorem :: SIN_COS2:43
   tanh is_continuous_on REAL;

 theorem :: SIN_COS2:44
   tanh.p<1 & tanh.p>-1;