:: Trigonometric Functions on Complex Space
:: by Takashi Mitsuishi , Noboru Endou and Keiji Ohkubo
::
:: Received October 10, 2002
:: Copyright (c) 2002 Association of Mizar Users
:: deftheorem Def1 defines sin_C SIN_COS3:def 1 :
:: deftheorem Def2 defines cos_C SIN_COS3:def 2 :
:: deftheorem Def3 defines sinh_C SIN_COS3:def 3 :
:: deftheorem Def4 defines cosh_C SIN_COS3:def 4 :
Lm2:
for z being complex number holds sinh_C /. z = ((exp z) - (exp (- z))) / 2
Lm3:
for z being complex number holds cosh_C /. z = ((exp z) + (exp (- z))) / 2
Lm5:
for z being Element of COMPLEX holds (exp z) * (exp (- z)) = 1
theorem :: SIN_COS3:1
theorem Th2: :: SIN_COS3:2
theorem Th3: :: SIN_COS3:3
theorem Th4: :: SIN_COS3:4
theorem :: SIN_COS3:5
theorem Th6: :: SIN_COS3:6
theorem :: SIN_COS3:7
theorem Th8: :: SIN_COS3:8
theorem Th9: :: SIN_COS3:9
theorem Th10: :: SIN_COS3:10
theorem Th11: :: SIN_COS3:11
theorem Th12: :: SIN_COS3:12
theorem Th13: :: SIN_COS3:13
theorem Th14: :: SIN_COS3:14
theorem Th15: :: SIN_COS3:15
theorem Th16: :: SIN_COS3:16
theorem Th17: :: SIN_COS3:17
theorem Th18: :: SIN_COS3:18
Lm6:
for x, y being Element of REAL holds exp (x + (y * <i> )) = (exp_R x) * ((cos y) + ((sin y) * <i> ))
theorem Th19: :: SIN_COS3:19
theorem :: SIN_COS3:20
theorem Th21: :: SIN_COS3:21
theorem :: SIN_COS3:22
theorem Th23: :: SIN_COS3:23
theorem :: SIN_COS3:24
theorem :: SIN_COS3:25
theorem :: SIN_COS3:26
theorem :: SIN_COS3:27
theorem Th28: :: SIN_COS3:28
theorem Th29: :: SIN_COS3:29
theorem :: SIN_COS3:30
theorem :: SIN_COS3:31
theorem :: SIN_COS3:32
theorem :: SIN_COS3:33
theorem :: SIN_COS3:34
theorem :: SIN_COS3:35
theorem Th36: :: SIN_COS3:36
theorem Th37: :: SIN_COS3:37
theorem Th38: :: SIN_COS3:38
theorem Th39: :: SIN_COS3:39
theorem Th40: :: SIN_COS3:40
theorem Th41: :: SIN_COS3:41
theorem :: SIN_COS3:42
canceled;
theorem Th43: :: SIN_COS3:43
theorem Th44: :: SIN_COS3:44
theorem Th45: :: SIN_COS3:45
theorem Th46: :: SIN_COS3:46
theorem Th47: :: SIN_COS3:47
theorem Th48: :: SIN_COS3:48
theorem Th49: :: SIN_COS3:49
theorem Th50: :: SIN_COS3:50
theorem Th51: :: SIN_COS3:51
theorem Th52: :: SIN_COS3:52
theorem :: SIN_COS3:53
theorem :: SIN_COS3:54
theorem :: SIN_COS3:55
theorem :: SIN_COS3:56
theorem :: SIN_COS3:57
theorem Th58: :: SIN_COS3:58
theorem Th59: :: SIN_COS3:59
theorem Th60: :: SIN_COS3:60
theorem Th61: :: SIN_COS3:61
theorem :: SIN_COS3:62
Lm10:
for z1 being Element of COMPLEX holds (sinh_C /. z1) * (sinh_C /. z1) = ((cosh_C /. z1) * (cosh_C /. z1)) - 1
theorem :: SIN_COS3:63