:: Formulas And Identities of Trigonometric Functions
:: by Yuzhong Ding and Xiquan Liang
::
:: Received March 18, 2004
:: Copyright (c) 2004 Association of Mizar Users
theorem Th1: :: SIN_COS5:1
theorem Th2: :: SIN_COS5:2
theorem :: SIN_COS5:3
theorem :: SIN_COS5:4
theorem Th5: :: SIN_COS5:5
theorem Th6: :: SIN_COS5:6
theorem Th7: :: SIN_COS5:7
theorem Th8: :: SIN_COS5:8
theorem :: SIN_COS5:9
theorem :: SIN_COS5:10
theorem Th11: :: SIN_COS5:11
theorem :: SIN_COS5:12
theorem Th13: :: SIN_COS5:13
theorem :: SIN_COS5:14
theorem :: SIN_COS5:15
theorem Th16: :: SIN_COS5:16
theorem Th17: :: SIN_COS5:17
theorem :: SIN_COS5:18
theorem :: SIN_COS5:19
theorem :: SIN_COS5:20
theorem :: SIN_COS5:21
theorem :: SIN_COS5:22
theorem :: SIN_COS5:23
theorem :: SIN_COS5:24
theorem :: SIN_COS5:25
theorem :: SIN_COS5:26
theorem :: SIN_COS5:27
theorem :: SIN_COS5:28
theorem :: SIN_COS5:29
theorem :: SIN_COS5:30
theorem :: SIN_COS5:31
theorem :: SIN_COS5:32
theorem :: SIN_COS5:33
theorem :: SIN_COS5:34
theorem :: SIN_COS5:35
:: deftheorem defines coth SIN_COS5:def 1 :
:: deftheorem defines sech SIN_COS5:def 2 :
:: deftheorem defines cosech SIN_COS5:def 3 :
theorem Th36: :: SIN_COS5:36
theorem :: SIN_COS5:37
theorem :: SIN_COS5:38
theorem :: SIN_COS5:39
Lm1:
for x being real number holds coth (- x) = - (coth x)
theorem Th40: :: SIN_COS5:40
theorem :: SIN_COS5:41
theorem :: SIN_COS5:42
Lm2:
for x being real number holds (cosh . x) ^2 = 1 + ((sinh . x) ^2 )
Lm3:
for x being real number holds ((cosh . x) ^2 ) - 1 = (sinh . x) ^2
theorem :: SIN_COS5:43
theorem :: SIN_COS5:44
theorem :: SIN_COS5:45
Lm4:
for x being real number st x > 0 holds
sinh x >= 0
theorem :: SIN_COS5:46
theorem :: SIN_COS5:47
theorem :: SIN_COS5:48
theorem :: SIN_COS5:49
theorem :: SIN_COS5:50
theorem :: SIN_COS5:51
theorem :: SIN_COS5:52