:: Properties of Trigonometric Function
:: by Takashi Mitsuishi and Yuguang Yang
::
:: Received March 13, 1999
:: Copyright (c) 1999 Association of Mizar Users
Lm1:
( 0 < PI / 2 & PI / 2 < PI & PI < (3 / 2) * PI & (3 / 2) * PI < 2 * PI )
theorem Th1: :: SIN_COS2:1
theorem :: SIN_COS2:2
Lm2:
for th being real number st th in ].0 ,(PI / 2).[ holds
0 < sin . th
theorem :: SIN_COS2:3
theorem :: SIN_COS2:4
theorem :: SIN_COS2:5
theorem :: SIN_COS2:6
theorem :: SIN_COS2:7
theorem :: SIN_COS2:8
theorem :: SIN_COS2:9
theorem :: SIN_COS2:10
theorem :: SIN_COS2:11
:: deftheorem Def1 defines sinh SIN_COS2:def 1 :
:: deftheorem defines sinh SIN_COS2:def 2 :
:: deftheorem Def3 defines cosh SIN_COS2:def 3 :
:: deftheorem defines cosh SIN_COS2:def 4 :
:: deftheorem Def5 defines tanh SIN_COS2:def 5 :
:: deftheorem defines tanh SIN_COS2:def 6 :
theorem Th12: :: SIN_COS2:12
theorem Th13: :: SIN_COS2:13
theorem Th14: :: SIN_COS2:14
Lm3:
for p, r being real number holds cosh . (p + r) = ((cosh . p) * (cosh . r)) + ((sinh . p) * (sinh . r))
Lm4:
for p, r being real number holds sinh . (p + r) = ((sinh . p) * (cosh . r)) + ((cosh . p) * (sinh . r))
theorem Th15: :: SIN_COS2:15
theorem Th16: :: SIN_COS2:16
theorem Th17: :: SIN_COS2:17
Lm5:
for r, q, p, a1 being real number st r <> 0 & q <> 0 & (r * q) + (p * a1) <> 0 holds
((p * q) + (r * a1)) / ((r * q) + (p * a1)) = ((p / r) + (a1 / q)) / (1 + ((p / r) * (a1 / q)))
Lm6:
for p, r being real number holds tanh . (p + r) = ((tanh . p) + (tanh . r)) / (1 + ((tanh . p) * (tanh . r)))
theorem Th18: :: SIN_COS2:18
Lm7:
for p being real number holds
( sinh . (2 * p) = (2 * (sinh . p)) * (cosh . p) & cosh . (2 * p) = (2 * ((cosh . p) ^2 )) - 1 )
theorem Th19: :: SIN_COS2:19
Lm8:
for p, r being real number holds cosh . (p - r) = ((cosh . p) * (cosh . r)) - ((sinh . p) * (sinh . r))
theorem :: SIN_COS2:20
Lm9:
for p, r being real number holds sinh . (p - r) = ((sinh . p) * (cosh . r)) - ((cosh . p) * (sinh . r))
theorem :: SIN_COS2:21
Lm10:
for p, r being real number holds tanh . (p - r) = ((tanh . p) - (tanh . r)) / (1 - ((tanh . p) * (tanh . r)))
theorem :: SIN_COS2:22
theorem :: SIN_COS2:23
theorem Th24: :: SIN_COS2:24
theorem Th25: :: SIN_COS2:25
theorem :: SIN_COS2:26
theorem :: SIN_COS2:27
theorem :: SIN_COS2:28
theorem :: SIN_COS2:29
theorem Th30: :: SIN_COS2:30
Lm11:
for d being real number holds compreal . d = (- 1) * d
Lm12:
( dom compreal = REAL & rng compreal c= REAL )
by FUNCT_2:def 1;
Lm13:
for f being PartFunc of REAL ,REAL st f = compreal holds
for p being real number holds
( f is_differentiable_in p & diff f,p = - 1 )
Lm14:
for p being real number
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)) )
Lm15:
for p being real number
for f being PartFunc of REAL ,REAL st f = compreal holds
exp_R . ((- 1) * p) = (exp_R * f) . p
Lm16:
for p being real number
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)) )
Lm17:
for p being real number
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) )
Lm18:
for p being real number
for ff being PartFunc of REAL ,REAL st ff = compreal holds
sinh . p = ((1 / 2) (#) (exp_R - (exp_R * ff))) . p
Lm19:
for ff being PartFunc of REAL ,REAL st ff = compreal holds
sinh = (1 / 2) (#) (exp_R - (exp_R * ff))
theorem Th31: :: SIN_COS2:31
Lm20:
for p being real number
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) )
Lm21:
for p being real number
for ff being PartFunc of REAL ,REAL st ff = compreal holds
cosh . p = ((1 / 2) (#) (exp_R + (exp_R * ff))) . p
Lm22:
for ff being PartFunc of REAL ,REAL st ff = compreal holds
cosh = (1 / 2) (#) (exp_R + (exp_R * ff))
theorem Th32: :: SIN_COS2:32
Lm23:
for p being real number holds
( sinh / cosh is_differentiable_in p & diff (sinh / cosh ),p = 1 / ((cosh . p) ^2 ) )
Lm24:
tanh = sinh / cosh
theorem :: SIN_COS2:33
theorem Th34: :: SIN_COS2:34
theorem Th35: :: SIN_COS2:35
theorem Th36: :: SIN_COS2:36
Lm25:
for p being real number holds (exp_R . p) + (exp_R . (- p)) >= 2
theorem :: SIN_COS2:37
theorem :: SIN_COS2:38
theorem :: SIN_COS2:39
theorem :: SIN_COS2:40
theorem :: SIN_COS2:41
theorem :: SIN_COS2:42
theorem :: SIN_COS2:43
theorem :: SIN_COS2:44