Journal of Formalized Mathematics
Volume 11, 1999
University of Bialystok
Copyright (c) 1999 Association of Mizar Users

### Properties of the Trigonometric Function

by
Takashi Mitsuishi, and
Yuguang Yang

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