:: SIN_COS3 semantic presentation

Lemma1: [*2,0*] = 2 + (0 * <i> )
by COMPLEX1:27;

definition
func sin_C -> Function of COMPLEX , COMPLEX means :Def1: :: SIN_COS3:def 1
for b1 being Element of COMPLEX holds a1 . b1 = ((exp (<i> * b1)) - (exp (- (<i> * b1)))) / (2 * <i> );
existence
ex b1 being Function of COMPLEX , COMPLEX st
for b2 being Element of COMPLEX holds b1 . b2 = ((exp (<i> * b2)) - (exp (- (<i> * b2)))) / (2 * <i> )
proof end;
uniqueness
for b1, b2 being Function of COMPLEX , COMPLEX st ( for b3 being Element of COMPLEX holds b1 . b3 = ((exp (<i> * b3)) - (exp (- (<i> * b3)))) / (2 * <i> ) ) & ( for b3 being Element of COMPLEX holds b2 . b3 = ((exp (<i> * b3)) - (exp (- (<i> * b3)))) / (2 * <i> ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines sin_C SIN_COS3:def 1 :
for b1 being Function of COMPLEX , COMPLEX holds
( b1 = sin_C iff for b2 being Element of COMPLEX holds b1 . b2 = ((exp (<i> * b2)) - (exp (- (<i> * b2)))) / (2 * <i> ) );

definition
func cos_C -> Function of COMPLEX , COMPLEX means :Def2: :: SIN_COS3:def 2
for b1 being Element of COMPLEX holds a1 . b1 = ((exp (<i> * b1)) + (exp (- (<i> * b1)))) / 2;
existence
ex b1 being Function of COMPLEX , COMPLEX st
for b2 being Element of COMPLEX holds b1 . b2 = ((exp (<i> * b2)) + (exp (- (<i> * b2)))) / 2
proof end;
uniqueness
for b1, b2 being Function of COMPLEX , COMPLEX st ( for b3 being Element of COMPLEX holds b1 . b3 = ((exp (<i> * b3)) + (exp (- (<i> * b3)))) / 2 ) & ( for b3 being Element of COMPLEX holds b2 . b3 = ((exp (<i> * b3)) + (exp (- (<i> * b3)))) / 2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines cos_C SIN_COS3:def 2 :
for b1 being Function of COMPLEX , COMPLEX holds
( b1 = cos_C iff for b2 being Element of COMPLEX holds b1 . b2 = ((exp (<i> * b2)) + (exp (- (<i> * b2)))) / 2 );

definition
func sinh_C -> Function of COMPLEX , COMPLEX means :Def3: :: SIN_COS3:def 3
for b1 being Element of COMPLEX holds a1 . b1 = ((exp b1) - (exp (- b1))) / 2;
existence
ex b1 being Function of COMPLEX , COMPLEX st
for b2 being Element of COMPLEX holds b1 . b2 = ((exp b2) - (exp (- b2))) / 2
proof end;
uniqueness
for b1, b2 being Function of COMPLEX , COMPLEX st ( for b3 being Element of COMPLEX holds b1 . b3 = ((exp b3) - (exp (- b3))) / 2 ) & ( for b3 being Element of COMPLEX holds b2 . b3 = ((exp b3) - (exp (- b3))) / 2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines sinh_C SIN_COS3:def 3 :
for b1 being Function of COMPLEX , COMPLEX holds
( b1 = sinh_C iff for b2 being Element of COMPLEX holds b1 . b2 = ((exp b2) - (exp (- b2))) / 2 );

definition
func cosh_C -> Function of COMPLEX , COMPLEX means :Def4: :: SIN_COS3:def 4
for b1 being Element of COMPLEX holds a1 . b1 = ((exp b1) + (exp (- b1))) / 2;
existence
ex b1 being Function of COMPLEX , COMPLEX st
for b2 being Element of COMPLEX holds b1 . b2 = ((exp b2) + (exp (- b2))) / 2
proof end;
uniqueness
for b1, b2 being Function of COMPLEX , COMPLEX st ( for b3 being Element of COMPLEX holds b1 . b3 = ((exp b3) + (exp (- b3))) / 2 ) & ( for b3 being Element of COMPLEX holds b2 . b3 = ((exp b3) + (exp (- b3))) / 2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines cosh_C SIN_COS3:def 4 :
for b1 being Function of COMPLEX , COMPLEX holds
( b1 = cosh_C iff for b2 being Element of COMPLEX holds b1 . b2 = ((exp b2) + (exp (- b2))) / 2 );

Lemma6: for b1 being Element of COMPLEX holds sin_C /. b1 = ((exp (<i> * b1)) - (exp (- (<i> * b1)))) / (2 * <i> )
proof end;

Lemma7: for b1 being Element of COMPLEX holds cos_C /. b1 = ((exp (<i> * b1)) + (exp (- (<i> * b1)))) / 2
proof end;

Lemma8: for b1 being Element of COMPLEX holds sinh_C /. b1 = ((exp b1) - (exp (- b1))) / 2
proof end;

Lemma9: for b1 being Element of COMPLEX holds cosh_C /. b1 = ((exp b1) + (exp (- b1))) / 2
proof end;

Lemma10: 0c = [*0,0*]
by ARYTM_0:def 7;

Lemma11: 1r = [*1,0*]
by ARYTM_0:def 7, COMPLEX1:def 7;

Lemma12: for b1 being Element of COMPLEX holds (exp b1) * (exp (- b1)) = 1
proof end;

theorem Th1: :: SIN_COS3:1
for b1 being Element of COMPLEX holds ((sin_C /. b1) * (sin_C /. b1)) + ((cos_C /. b1) * (cos_C /. b1)) = 1
proof end;

theorem Th2: :: SIN_COS3:2
for b1 being Element of COMPLEX holds - (sin_C /. b1) = sin_C /. (- b1)
proof end;

theorem Th3: :: SIN_COS3:3
for b1 being Element of COMPLEX holds cos_C /. b1 = cos_C /. (- b1)
proof end;

theorem Th4: :: SIN_COS3:4
for b1, b2 being Element of COMPLEX holds sin_C /. (b1 + b2) = ((sin_C /. b1) * (cos_C /. b2)) + ((cos_C /. b1) * (sin_C /. b2))
proof end;

theorem Th5: :: SIN_COS3:5
for b1, b2 being Element of COMPLEX holds sin_C /. (b1 - b2) = ((sin_C /. b1) * (cos_C /. b2)) - ((cos_C /. b1) * (sin_C /. b2))
proof end;

theorem Th6: :: SIN_COS3:6
for b1, b2 being Element of COMPLEX holds cos_C /. (b1 + b2) = ((cos_C /. b1) * (cos_C /. b2)) - ((sin_C /. b1) * (sin_C /. b2))
proof end;

theorem Th7: :: SIN_COS3:7
for b1, b2 being Element of COMPLEX holds cos_C /. (b1 - b2) = ((cos_C /. b1) * (cos_C /. b2)) + ((sin_C /. b1) * (sin_C /. b2))
proof end;

theorem Th8: :: SIN_COS3:8
for b1 being Element of COMPLEX holds ((cosh_C /. b1) * (cosh_C /. b1)) - ((sinh_C /. b1) * (sinh_C /. b1)) = 1
proof end;

theorem Th9: :: SIN_COS3:9
for b1 being Element of COMPLEX holds - (sinh_C /. b1) = sinh_C /. (- b1)
proof end;

theorem Th10: :: SIN_COS3:10
for b1 being Element of COMPLEX holds cosh_C /. b1 = cosh_C /. (- b1)
proof end;

theorem Th11: :: SIN_COS3:11
for b1, b2 being Element of COMPLEX holds sinh_C /. (b1 + b2) = ((sinh_C /. b1) * (cosh_C /. b2)) + ((cosh_C /. b1) * (sinh_C /. b2))
proof end;

theorem Th12: :: SIN_COS3:12
for b1, b2 being Element of COMPLEX holds sinh_C /. (b1 - b2) = ((sinh_C /. b1) * (cosh_C /. b2)) - ((cosh_C /. b1) * (sinh_C /. b2))
proof end;

theorem Th13: :: SIN_COS3:13
for b1, b2 being Element of COMPLEX holds cosh_C /. (b1 - b2) = ((cosh_C /. b1) * (cosh_C /. b2)) - ((sinh_C /. b1) * (sinh_C /. b2))
proof end;

theorem Th14: :: SIN_COS3:14
for b1, b2 being Element of COMPLEX holds cosh_C /. (b1 + b2) = ((cosh_C /. b1) * (cosh_C /. b2)) + ((sinh_C /. b1) * (sinh_C /. b2))
proof end;

theorem Th15: :: SIN_COS3:15
for b1 being Element of COMPLEX holds sin_C /. (<i> * b1) = <i> * (sinh_C /. b1)
proof end;

theorem Th16: :: SIN_COS3:16
for b1 being Element of COMPLEX holds cos_C /. (<i> * b1) = cosh_C /. b1
proof end;

theorem Th17: :: SIN_COS3:17
for b1 being Element of COMPLEX holds sinh_C /. (<i> * b1) = <i> * (sin_C /. b1)
proof end;

theorem Th18: :: SIN_COS3:18
for b1 being Element of COMPLEX holds cosh_C /. (<i> * b1) = cos_C /. b1
proof end;

Lemma28: for b1, b2 being Element of REAL holds exp [*b1,b2*] = [*(exp b1),0*] * [*(cos b2),(sin b2)*]
proof end;

theorem Th19: :: SIN_COS3:19
for b1, b2 being Element of REAL holds exp [*b1,b2*] = [*((exp . b1) * (cos . b2)),((exp . b1) * (sin . b2))*]
proof end;

theorem Th20: :: SIN_COS3:20
exp 0c = 1
proof end;

theorem Th21: :: SIN_COS3:21
sin_C /. 0c = 0
proof end;

theorem Th22: :: SIN_COS3:22
sinh_C /. 0c = 0
proof end;

theorem Th23: :: SIN_COS3:23
cos_C /. 0c = 1
proof end;

theorem Th24: :: SIN_COS3:24
cosh_C /. 0c = 1
proof end;

theorem Th25: :: SIN_COS3:25
for b1 being Element of COMPLEX holds exp b1 = (cosh_C /. b1) + (sinh_C /. b1)
proof end;

theorem Th26: :: SIN_COS3:26
for b1 being Element of COMPLEX holds exp (- b1) = (cosh_C /. b1) - (sinh_C /. b1)
proof end;

Lemma33: for b1 being Element of REAL holds [*b1,0*] * <i> = [*0,b1*]
proof end;

theorem Th27: :: SIN_COS3:27
for b1 being Element of COMPLEX holds
( exp (b1 + ([*(2 * PI ),0*] * <i> )) = exp b1 & exp (b1 + [*0,(2 * PI )*]) = exp b1 )
proof end;

theorem Th28: :: SIN_COS3:28
for b1 being Nat holds
( exp [*0,((2 * PI ) * b1)*] = 1 & exp ([*((2 * PI ) * b1),0*] * <i> ) = 1 )
proof end;

theorem Th29: :: SIN_COS3:29
for b1 being Nat holds
( exp [*0,(- ((2 * PI ) * b1))*] = 1 & exp ([*(- ((2 * PI ) * b1)),0*] * <i> ) = 1 )
proof end;

theorem Th30: :: SIN_COS3:30
for b1 being Nat holds
( exp [*0,(((2 * b1) + 1) * PI )*] = [*(- 1),0*] & exp ([*(((2 * b1) + 1) * PI ),0*] * <i> ) = [*(- 1),0*] )
proof end;

theorem Th31: :: SIN_COS3:31
for b1 being Nat holds
( exp [*0,(- (((2 * b1) + 1) * PI ))*] = [*(- 1),0*] & exp ([*(- (((2 * b1) + 1) * PI )),0*] * <i> ) = [*(- 1),0*] )
proof end;

theorem Th32: :: SIN_COS3:32
for b1 being Nat holds
( exp [*0,(((2 * b1) + (1 / 2)) * PI )*] = [*0,1*] & exp ([*(((2 * b1) + (1 / 2)) * PI ),0*] * <i> ) = [*0,1*] )
proof end;

theorem Th33: :: SIN_COS3:33
for b1 being Nat holds
( exp [*0,(- (((2 * b1) + (1 / 2)) * PI ))*] = [*0,(- 1)*] & exp ([*(- (((2 * b1) + (1 / 2)) * PI )),0*] * <i> ) = [*0,(- 1)*] )
proof end;

Lemma36: for b1, b2 being Element of REAL holds - [*b1,b2*] = [*(- b1),(- b2)*]
proof end;

Lemma37: [*1,0*] = 1 + (0 * <i> )
by COMPLEX1:27;

theorem Th34: :: SIN_COS3:34
for b1 being Element of COMPLEX
for b2 being Nat holds sin_C /. (b1 + ((2 * b2) * PI )) = sin_C /. b1
proof end;

theorem Th35: :: SIN_COS3:35
for b1 being Element of COMPLEX
for b2 being Nat holds cos_C /. (b1 + ((2 * b2) * PI )) = cos_C /. b1
proof end;

theorem Th36: :: SIN_COS3:36
for b1 being Element of COMPLEX holds exp (<i> * b1) = (cos_C /. b1) + (<i> * (sin_C /. b1))
proof end;

theorem Th37: :: SIN_COS3:37
for b1 being Element of COMPLEX holds exp (- (<i> * b1)) = (cos_C /. b1) - (<i> * (sin_C /. b1))
proof end;

Lemma40: for b1, b2 being Element of REAL holds <i> * [*b1,b2*] = [*(- b2),b1*]
proof end;

theorem Th38: :: SIN_COS3:38
for b1 being Element of REAL holds sin_C /. [*b1,0*] = sin . b1
proof end;

theorem Th39: :: SIN_COS3:39
for b1 being Element of REAL holds cos_C /. [*b1,0*] = cos . b1
proof end;

theorem Th40: :: SIN_COS3:40
for b1 being Element of REAL holds sinh_C /. [*b1,0*] = sinh . b1
proof end;

theorem Th41: :: SIN_COS3:41
for b1 being Element of REAL holds cosh_C /. [*b1,0*] = cosh . b1
proof end;

theorem Th42: :: SIN_COS3:42
for b1, b2 being Element of REAL holds [*b1,0*] + (<i> * [*b2,0*]) = [*b1,b2*]
proof end;

theorem Th43: :: SIN_COS3:43
for b1, b2 being Element of REAL holds sin_C /. [*b1,b2*] = [*((sin . b1) * (cosh . b2)),((cos . b1) * (sinh . b2))*]
proof end;

theorem Th44: :: SIN_COS3:44
for b1, b2 being Element of REAL holds sin_C /. [*b1,(- b2)*] = [*((sin . b1) * (cosh . b2)),(- ((cos . b1) * (sinh . b2)))*]
proof end;

theorem Th45: :: SIN_COS3:45
for b1, b2 being Element of REAL holds cos_C /. [*b1,b2*] = [*((cos . b1) * (cosh . b2)),(- ((sin . b1) * (sinh . b2)))*]
proof end;

theorem Th46: :: SIN_COS3:46
for b1, b2 being Element of REAL holds cos_C /. [*b1,(- b2)*] = [*((cos . b1) * (cosh . b2)),((sin . b1) * (sinh . b2))*]
proof end;

theorem Th47: :: SIN_COS3:47
for b1, b2 being Element of REAL holds sinh_C /. [*b1,b2*] = [*((sinh . b1) * (cos . b2)),((cosh . b1) * (sin . b2))*]
proof end;

theorem Th48: :: SIN_COS3:48
for b1, b2 being Element of REAL holds sinh_C /. [*b1,(- b2)*] = [*((sinh . b1) * (cos . b2)),(- ((cosh . b1) * (sin . b2)))*]
proof end;

theorem Th49: :: SIN_COS3:49
for b1, b2 being Element of REAL holds cosh_C /. [*b1,b2*] = [*((cosh . b1) * (cos . b2)),((sinh . b1) * (sin . b2))*]
proof end;

theorem Th50: :: SIN_COS3:50
for b1, b2 being Element of REAL holds cosh_C /. [*b1,(- b2)*] = [*((cosh . b1) * (cos . b2)),(- ((sinh . b1) * (sin . b2)))*]
proof end;

theorem Th51: :: SIN_COS3:51
for b1 being Nat
for b2 being Element of COMPLEX holds ((cos_C /. b2) + (<i> * (sin_C /. b2))) #N b1 = (cos_C /. ([*b1,0*] * b2)) + (<i> * (sin_C /. ([*b1,0*] * b2)))
proof end;

theorem Th52: :: SIN_COS3:52
for b1 being Nat
for b2 being Element of COMPLEX holds ((cos_C /. b2) - (<i> * (sin_C /. b2))) #N b1 = (cos_C /. ([*b1,0*] * b2)) - (<i> * (sin_C /. ([*b1,0*] * b2)))
proof end;

theorem Th53: :: SIN_COS3:53
for b1 being Nat
for b2 being Element of COMPLEX holds exp ((<i> * [*b1,0*]) * b2) = ((cos_C /. b2) + (<i> * (sin_C /. b2))) #N b1
proof end;

theorem Th54: :: SIN_COS3:54
for b1 being Nat
for b2 being Element of COMPLEX holds exp (- ((<i> * [*b1,0*]) * b2)) = ((cos_C /. b2) - (<i> * (sin_C /. b2))) #N b1
proof end;

theorem Th55: :: SIN_COS3:55
for b1, b2 being Element of REAL holds (([*1,(- 1)*] / 2) * (sinh_C /. [*b1,b2*])) + (([*1,1*] / 2) * (sinh_C /. [*b1,(- b2)*])) = [*(((sinh . b1) * (cos . b2)) + ((cosh . b1) * (sin . b2))),0*]
proof end;

theorem Th56: :: SIN_COS3:56
for b1, b2 being Element of REAL holds (([*1,(- 1)*] / 2) * (cosh_C /. [*b1,b2*])) + (([*1,1*] / 2) * (cosh_C /. [*b1,(- b2)*])) = ((sinh . b1) * (sin . b2)) + ((cosh . b1) * (cos . b2))
proof end;

theorem Th57: :: SIN_COS3:57
for b1 being Element of COMPLEX holds (sinh_C /. b1) * (sinh_C /. b1) = ((cosh_C /. (2 * b1)) - 1) / 2
proof end;

theorem Th58: :: SIN_COS3:58
for b1 being Element of COMPLEX holds (cosh_C /. b1) * (cosh_C /. b1) = ((cosh_C /. (2 * b1)) + 1) / 2
proof end;

theorem Th59: :: SIN_COS3:59
for b1 being Element of COMPLEX holds
( sinh_C /. (2 * b1) = (2 * (sinh_C /. b1)) * (cosh_C /. b1) & cosh_C /. (2 * b1) = ((2 * (cosh_C /. b1)) * (cosh_C /. b1)) - 1 )
proof end;

theorem Th60: :: SIN_COS3:60
for b1, b2 being Element of COMPLEX holds
( ((sinh_C /. b1) * (sinh_C /. b1)) - ((sinh_C /. b2) * (sinh_C /. b2)) = (sinh_C /. (b1 + b2)) * (sinh_C /. (b1 - b2)) & ((cosh_C /. b1) * (cosh_C /. b1)) - ((cosh_C /. b2) * (cosh_C /. b2)) = (sinh_C /. (b1 + b2)) * (sinh_C /. (b1 - b2)) & ((sinh_C /. b1) * (sinh_C /. b1)) - ((sinh_C /. b2) * (sinh_C /. b2)) = ((cosh_C /. b1) * (cosh_C /. b1)) - ((cosh_C /. b2) * (cosh_C /. b2)) )
proof end;

theorem Th61: :: SIN_COS3:61
for b1, b2 being Element of COMPLEX holds
( (cosh_C /. (b1 + b2)) * (cosh_C /. (b1 - b2)) = ((sinh_C /. b1) * (sinh_C /. b1)) + ((cosh_C /. b2) * (cosh_C /. b2)) & (cosh_C /. (b1 + b2)) * (cosh_C /. (b1 - b2)) = ((cosh_C /. b1) * (cosh_C /. b1)) + ((sinh_C /. b2) * (sinh_C /. b2)) & ((sinh_C /. b1) * (sinh_C /. b1)) + ((cosh_C /. b2) * (cosh_C /. b2)) = ((cosh_C /. b1) * (cosh_C /. b1)) + ((sinh_C /. b2) * (sinh_C /. b2)) )
proof end;

theorem Th62: :: SIN_COS3:62
for b1, b2 being Element of COMPLEX holds
( (sinh_C /. (2 * b1)) + (sinh_C /. (2 * b2)) = (2 * (sinh_C /. (b1 + b2))) * (cosh_C /. (b1 - b2)) & (sinh_C /. (2 * b1)) - (sinh_C /. (2 * b2)) = (2 * (sinh_C /. (b1 - b2))) * (cosh_C /. (b1 + b2)) )
proof end;

Lemma59: for b1 being Element of COMPLEX holds (sinh_C /. b1) * (sinh_C /. b1) = ((cosh_C /. b1) * (cosh_C /. b1)) - 1
proof end;

theorem Th63: :: SIN_COS3:63
for b1, b2 being Element of COMPLEX holds
( (cosh_C /. (2 * b1)) + (cosh_C /. (2 * b2)) = (2 * (cosh_C /. (b1 + b2))) * (cosh_C /. (b1 - b2)) & (cosh_C /. (2 * b1)) - (cosh_C /. (2 * b2)) = (2 * (sinh_C /. (b1 + b2))) * (sinh_C /. (b1 - b2)) )
proof end;