SIN_COS2: Properties of Trigonometric Function

:: Properties of Trigonometric Function
:: by Takashi Mitsuishi and Yuguang Yang
::
:: Received March 13, 1999
:: Copyright (c) 1999-2021 Association of Mizar Users

theorem Th1: :: SIN_COS2:1

for p, r being Real st p >= 0 & r >= 0 holds
p + r >= 2 * (sqrt (p * r))

proof end;

theorem :: SIN_COS2:2

sin | ].0,(PI / 2).[ is increasing

proof end;

Lm1: for th being Real st th in ].0,(PI / 2).[ holds
0 < sin . th

proof end;

theorem :: SIN_COS2:3

sin | ].(PI / 2),PI.[ is decreasing

proof end;

theorem :: SIN_COS2:4

cos | ].0,(PI / 2).[ is decreasing

proof end;

theorem :: SIN_COS2:5

cos | ].(PI / 2),PI.[ is decreasing

proof end;

theorem :: SIN_COS2:6

sin | ].PI,((3 / 2) * PI).[ is decreasing

proof end;

theorem :: SIN_COS2:7

sin | ].((3 / 2) * PI),(2 * PI).[ is increasing

proof end;

theorem :: SIN_COS2:8

cos | ].PI,((3 / 2) * PI).[ is increasing

proof end;

theorem :: SIN_COS2:9

cos | ].((3 / 2) * PI),(2 * PI).[ is increasing

proof end;

theorem :: SIN_COS2:10

for th being Real
for n being Nat holds sin . th = sin . (((2 * PI) * n) + th)

proof end;

theorem :: SIN_COS2:11

for th being Real
for n being Nat holds cos . th = cos . (((2 * PI) * n) + th)

proof end;

definition

func sinh -> Function of REAL,REAL means :Def1: :: SIN_COS2:def 1
for d being Real holds it . d = ((exp_R . d) - (exp_R . (- d))) / 2;

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines sinh SIN_COS2:def 1 :

definition

let d be object ;

func sinh d -> number equals :: SIN_COS2:def 2
sinh . d;

coherence ;

end;

:: deftheorem defines sinh SIN_COS2:def 2 :

registration

let d be object ;

cluster sinh d -> real ;

coherence ;

end;

definition

func cosh -> Function of REAL,REAL means :Def3: :: SIN_COS2:def 3
for d being Real holds it . d = ((exp_R . d) + (exp_R . (- d))) / 2;

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines cosh SIN_COS2:def 3 :

definition

let d be object ;

func cosh d -> number equals :: SIN_COS2:def 4
cosh . d;

coherence ;

end;

:: deftheorem defines cosh SIN_COS2:def 4 :

registration

let d be object ;

cluster cosh d -> real ;

coherence ;

end;

definition

func tanh -> Function of REAL,REAL means :Def5: :: SIN_COS2:def 5
for d being Real holds it . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- d)));

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines tanh SIN_COS2:def 5 :

definition

let d be object ;

func tanh d -> number equals :: SIN_COS2:def 6
tanh . d;

coherence ;

end;

:: deftheorem defines tanh SIN_COS2:def 6 :

registration

let d be object ;

cluster tanh d -> real ;

coherence ;

end;

theorem Th12: :: SIN_COS2:12

for p, q being Real holds exp_R . (p + q) = (exp_R . p) * (exp_R . q)

proof end;

theorem Th13: :: SIN_COS2:13

exp_R . 0 = 1 by SIN_COS:51, SIN_COS:def 23;

theorem Th14: :: SIN_COS2:14

for p being Real holds
( ((cosh . p) ^2) - ((sinh . p) ^2) = 1 & ((cosh . p) * (cosh . p)) - ((sinh . p) * (sinh . p)) = 1 )

proof end;

Lm2: for p, r being Real holds cosh . (p + r) = ((cosh . p) * (cosh . r)) + ((sinh . p) * (sinh . r))

proof end;

Lm3: for p, r being Real holds sinh . (p + r) = ((sinh . p) * (cosh . r)) + ((cosh . p) * (sinh . r))

proof end;

theorem Th15: :: SIN_COS2:15

for p being Real holds
( cosh . p <> 0 & cosh . p > 0 & cosh . 0 = 1 )

proof end;

theorem Th16: :: SIN_COS2:16

sinh . 0 = 0

proof end;

theorem Th17: :: SIN_COS2:17

for p being Real holds tanh . p = (sinh . p) / (cosh . p)

proof end;

Lm4: for p, q, r, a1 being Real st r <> 0 & q <> 0 holds
((p * q) + (r * a1)) / ((r * q) + (p * a1)) = ((p / r) + (a1 / q)) / (1 + ((p / r) * (a1 / q)))

proof end;

Lm5: for p, r being Real holds tanh . (p + r) = ((tanh . p) + (tanh . r)) / (1 + ((tanh . p) * (tanh . r)))

proof end;

theorem Th18: :: SIN_COS2:18

for p being Real holds
( (sinh . p) ^2 = (1 / 2) * ((cosh . (2 * p)) - 1) & (cosh . p) ^2 = (1 / 2) * ((cosh . (2 * p)) + 1) )

proof end;

Lm6: for p being Real holds
( sinh . (2 * p) = (2 * (sinh . p)) * (cosh . p) & cosh . (2 * p) = (2 * ((cosh . p) ^2)) - 1 )

proof end;

theorem Th19: :: SIN_COS2:19

for p being Real holds
( cosh . (- p) = cosh . p & sinh . (- p) = - (sinh . p) & tanh . (- p) = - (tanh . p) )

proof end;

Lm7: for p, r being Real holds cosh . (p - r) = ((cosh . p) * (cosh . r)) - ((sinh . p) * (sinh . r))

proof end;

theorem :: SIN_COS2:20

for p, r being Real holds
( cosh . (p + r) = ((cosh . p) * (cosh . r)) + ((sinh . p) * (sinh . r)) & cosh . (p - r) = ((cosh . p) * (cosh . r)) - ((sinh . p) * (sinh . r)) ) by Lm2, Lm7;

Lm8: for p, r being Real holds sinh . (p - r) = ((sinh . p) * (cosh . r)) - ((cosh . p) * (sinh . r))

proof end;

theorem :: SIN_COS2:21

for p, r being Real holds
( sinh . (p + r) = ((sinh . p) * (cosh . r)) + ((cosh . p) * (sinh . r)) & sinh . (p - r) = ((sinh . p) * (cosh . r)) - ((cosh . p) * (sinh . r)) ) by Lm3, Lm8;

Lm9: for p, r being Real holds tanh . (p - r) = ((tanh . p) - (tanh . r)) / (1 - ((tanh . p) * (tanh . r)))

proof end;

theorem :: SIN_COS2:22

for p, r being Real holds
( tanh . (p + r) = ((tanh . p) + (tanh . r)) / (1 + ((tanh . p) * (tanh . r))) & tanh . (p - r) = ((tanh . p) - (tanh . r)) / (1 - ((tanh . p) * (tanh . r))) ) by Lm5, Lm9;

theorem :: SIN_COS2:23

for p being Real holds
( 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)) )

proof end;

theorem Th24: :: SIN_COS2:24

for p, q being Real holds
( ((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) )

proof end;

theorem Th25: :: SIN_COS2:25

for p, q being Real holds
( ((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) )

proof end;

theorem :: SIN_COS2:26

for p, r being Real holds
( (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))) )

proof end;

theorem :: SIN_COS2:27

for p, r being Real holds
( (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))) )

proof end;

theorem :: SIN_COS2:28

for p, r being Real holds
( (tanh . p) + (tanh . r) = (sinh . (p + r)) / ((cosh . p) * (cosh . r)) & (tanh . p) - (tanh . r) = (sinh . (p - r)) / ((cosh . p) * (cosh . r)) )

proof end;

theorem :: SIN_COS2:29

for p being Real
for n being Nat holds ((cosh . p) + (sinh . p)) |^ n = (cosh . (n * p)) + (sinh . (n * p))

proof end;

theorem Th30: :: SIN_COS2:30

( dom sinh = REAL & dom cosh = REAL & dom tanh = REAL ) by FUNCT_2:def 1;

Lm10: for d being Real holds compreal . d = (- 1) * d

proof end;

Lm11: dom compreal = REAL
by FUNCT_2:def 1;

Lm12: for f being PartFunc of REAL,REAL st f = compreal holds
for p being Real holds
( f is_differentiable_in p & diff (f,p) = - 1 )

proof end;

Lm13: for p being Real
for f being PartFunc of REAL,REAL st f = compreal holds
( exp_R * f is_differentiable_in p & diff ((exp_R * f),p) = (- 1) * (exp_R . (f . p)) )

proof end;

Lm14: for p being Real
for f being PartFunc of REAL,REAL st f = compreal holds
exp_R . ((- 1) * p) = (exp_R * f) . p

proof end;

Lm15: for p being Real
for f being PartFunc of REAL,REAL st f = compreal holds
( exp_R - (exp_R * f) is_differentiable_in p & exp_R + (exp_R * f) is_differentiable_in p & diff ((exp_R - (exp_R * f)),p) = (exp_R . p) + (exp_R . (- p)) & diff ((exp_R + (exp_R * f)),p) = (exp_R . p) - (exp_R . (- p)) )

proof end;

Lm16: for p being Real
for f being PartFunc of REAL,REAL st f = compreal holds
( (1 / 2) (#) (exp_R - (exp_R * f)) is_differentiable_in p & diff (((1 / 2) (#) (exp_R - (exp_R * f))),p) = (1 / 2) * (diff ((exp_R - (exp_R * f)),p)) )

proof end;

Lm17: for p being Real
for ff being PartFunc of REAL,REAL st ff = compreal holds
sinh . p = ((1 / 2) (#) (exp_R - (exp_R * ff))) . p

proof end;

Lm18: for ff being PartFunc of REAL,REAL st ff = compreal holds
sinh = (1 / 2) (#) (exp_R - (exp_R * ff))

proof end;

theorem Th31: :: SIN_COS2:31

for p being Real holds
( sinh is_differentiable_in p & diff (sinh,p) = cosh . p )

proof end;

Lm19: for p being Real
for ff being PartFunc of REAL,REAL st ff = compreal holds
( (1 / 2) (#) (exp_R + (exp_R * ff)) is_differentiable_in p & diff (((1 / 2) (#) (exp_R + (exp_R * ff))),p) = (1 / 2) * (diff ((exp_R + (exp_R * ff)),p)) )

proof end;

Lm20: for p being Real
for ff being PartFunc of REAL,REAL st ff = compreal holds
cosh . p = ((1 / 2) (#) (exp_R + (exp_R * ff))) . p

proof end;

Lm21: for ff being PartFunc of REAL,REAL st ff = compreal holds
cosh = (1 / 2) (#) (exp_R + (exp_R * ff))

proof end;

theorem Th32: :: SIN_COS2:32

for p being Real holds
( cosh is_differentiable_in p & diff (cosh,p) = sinh . p )

proof end;

Lm22: for p being Real holds
( sinh / cosh is_differentiable_in p & diff ((sinh / cosh),p) = 1 / ((cosh . p) ^2) )

proof end;

Lm23: tanh = sinh / cosh

proof end;

theorem :: SIN_COS2:33

for p being Real holds
( tanh is_differentiable_in p & diff (tanh,p) = 1 / ((cosh . p) ^2) ) by Lm22, Lm23;

theorem Th34: :: SIN_COS2:34

for p being Real holds
( sinh is_differentiable_on REAL & diff (sinh,p) = cosh . p )

proof end;

theorem Th35: :: SIN_COS2:35

for p being Real holds
( cosh is_differentiable_on REAL & diff (cosh,p) = sinh . p )

proof end;

theorem Th36: :: SIN_COS2:36

for p being Real holds
( tanh is_differentiable_on REAL & diff (tanh,p) = 1 / ((cosh . p) ^2) )

proof end;

Lm24: for p being Real holds (exp_R . p) + (exp_R . (- p)) >= 2

proof end;

theorem :: SIN_COS2:37

for p being Real holds cosh . p >= 1

proof end;

theorem :: SIN_COS2:38

for p being Real holds sinh is_continuous_in p by Th31, FDIFF_1:24;

theorem :: SIN_COS2:39

for p being Real holds cosh is_continuous_in p by Th32, FDIFF_1:24;

theorem :: SIN_COS2:40

for p being Real holds tanh is_continuous_in p by Lm22, Lm23, FDIFF_1:24;

theorem :: SIN_COS2:41

sinh | REAL is continuous by Th34, FDIFF_1:25;

theorem :: SIN_COS2:42

cosh | REAL is continuous by Th35, FDIFF_1:25;

theorem :: SIN_COS2:43

tanh | REAL is continuous by Th36, FDIFF_1:25;

theorem :: SIN_COS2:44

for p being Real holds
( tanh . p < 1 & tanh . p > - 1 )

proof end;