:: SIN_COS7 semantic presentation

Lemma1: 1 / 1 = 1
;

Lemma2: ( number_e > 0 & number_e <> 1 )
by TAYLOR_1:11;

Lemma3: for b₁, b₂ being real number st b₁ ^2 < 1 & b₂ < 1 holds
(b₁ ^2 ) * b₂ < 1

proof end;

theorem Th1: :: SIN_COS7:1

for b₁ being real number st b₁ > 0 holds
1 / b₁ = b₁ to_power (- 1)

proof end;

Lemma5: for b₁ being real number st b₁ > 1 holds
b₁ ^2 > 1
by SQUARE_1:59, SQUARE_1:78;

theorem Th2: :: SIN_COS7:2

for b₁ being real number st b₁ > 1 holds
((sqrt ((b₁ ^2 ) - 1)) / b₁) ^2 < 1

proof end;

theorem Th3: :: SIN_COS7:3

for b₁ being real number holds (b₁ / (sqrt ((b₁ ^2 ) + 1))) ^2 < 1

proof end;

theorem Th4: :: SIN_COS7:4

for b₁ being real number holds sqrt ((b₁ ^2 ) + 1) > 0

proof end;

theorem Th5: :: SIN_COS7:5

for b₁ being real number holds (sqrt ((b₁ ^2 ) + 1)) + b₁ > 0

proof end;

Lemma10: for b₁ being real number st 1 <= b₁ holds
(b₁ ^2 ) - 1 >= 0

proof end;

theorem Th6: :: SIN_COS7:6

for b₁, b₂ being real number st b₁ >= 0 & b₂ >= 1 holds
(b₂ + 1) / b₁ >= 0

proof end;

theorem Th7: :: SIN_COS7:7

for b₁, b₂ being real number st b₁ >= 0 & b₂ >= 1 holds
(b₂ - 1) / b₁ >= 0

proof end;

theorem Th8: :: SIN_COS7:8

for b₁ being real number st b₁ >= 1 holds
sqrt ((b₁ + 1) / 2) >= 1

proof end;

theorem Th9: :: SIN_COS7:9

for b₁, b₂ being real number st b₁ >= 0 & b₂ >= 1 holds
((b₂ ^2 ) - 1) / b₁ >= 0

proof end;

theorem Th10: :: SIN_COS7:10

for b₁ being real number st b₁ >= 1 holds
(sqrt ((b₁ + 1) / 2)) + (sqrt ((b₁ - 1) / 2)) > 0

proof end;

theorem Th11: :: SIN_COS7:11

for b₁ being real number st b₁ ^2 < 1 holds
( b₁ + 1 > 0 & 1 - b₁ > 0 )

proof end;

Lemma17: for b₁ being real number st b₁ ^2 < 1 holds
(b₁ + 1) / (1 - b₁) > 0

proof end;

theorem Th12: :: SIN_COS7:12

for b₁ being real number st b₁ <> 1 holds
(1 - b₁) ^2 > 0

proof end;

theorem Th13: :: SIN_COS7:13

for b₁ being real number st b₁ ^2 < 1 holds
((b₁ ^2 ) + 1) / (1 - (b₁ ^2 )) >= 0

proof end;

theorem Th14: :: SIN_COS7:14

for b₁ being real number st b₁ ^2 < 1 holds
((2 * b₁) / (1 + (b₁ ^2 ))) ^2 < 1

proof end;

Lemma21: for b₁ being real number st 0 <= b₁ holds
1 + b₁ > 0

proof end;

theorem Th15: :: SIN_COS7:15

for b₁ being real number st 0 < b₁ & b₁ < 1 holds
(1 + b₁) / (1 - b₁) > 0

proof end;

theorem Th16: :: SIN_COS7:16

for b₁ being real number st 0 < b₁ & b₁ < 1 holds
b₁ ^2 < 1

proof end;

Lemma24: for b₁ being real number st 0 < b₁ & b₁ < 1 holds
0 < 1 - (b₁ ^2 )

proof end;

theorem Th17: :: SIN_COS7:17

for b₁ being real number st 0 < b₁ & b₁ < 1 holds
1 / (sqrt (1 - (b₁ ^2 ))) > 1

proof end;

theorem Th18: :: SIN_COS7:18

for b₁ being real number st 0 < b₁ & b₁ < 1 holds
(2 * b₁) / (1 - (b₁ ^2 )) > 0

proof end;

theorem Th19: :: SIN_COS7:19

for b₁ being real number st 0 < b₁ & b₁ < 1 holds
0 < (1 - (b₁ ^2 )) ^2

proof end;

theorem Th20: :: SIN_COS7:20

for b₁ being real number st 0 < b₁ & b₁ < 1 holds
(1 + (b₁ ^2 )) / (1 - (b₁ ^2 )) > 1

proof end;

theorem Th21: :: SIN_COS7:21

for b₁ being real number st 1 < b₁ ^2 holds
(1 / b₁) ^2 < 1

proof end;

Lemma30: for b₁ being real number st b₁ > 0 & b₁ <= 1 holds
1 / b₁ >= 1
by Lemma1, REAL_2:152;

theorem Th22: :: SIN_COS7:22

for b₁ being real number st 0 < b₁ & b₁ <= 1 holds
1 - (b₁ ^2 ) >= 0

proof end;

theorem Th23: :: SIN_COS7:23

for b₁ being real number st 1 <= b₁ holds
0 < b₁ + (sqrt ((b₁ ^2 ) - 1))

proof end;

theorem Th24: :: SIN_COS7:24

for b₁, b₂ being real number st 1 <= b₁ & 1 <= b₂ holds
0 <= (b₁ * (sqrt ((b₂ ^2 ) - 1))) + (b₂ * (sqrt ((b₁ ^2 ) - 1)))

proof end;

theorem Th25: :: SIN_COS7:25

for b₁, b₂ being real number st 1 <= b₁ & 1 <= b₂ & abs b₂ <= abs b₁ holds
0 < b₂ - (sqrt ((b₂ ^2 ) - 1))

proof end;

theorem Th26: :: SIN_COS7:26

for b₁, b₂ being real number st 1 <= b₁ & 1 <= b₂ & abs b₂ <= abs b₁ holds
0 <= (b₂ * (sqrt ((b₁ ^2 ) - 1))) - (b₁ * (sqrt ((b₂ ^2 ) - 1)))

proof end;

theorem Th27: :: SIN_COS7:27

for b₁, b₂ being real number st b₁ ^2 < 1 & b₂ ^2 < 1 holds
b₁ * b₂ <> - 1

proof end;

Lemma37: for b₁, b₂ being real number st b₁ ^2 < 1 & b₂ ^2 < 1 holds
(b₁ * b₂) + 1 <> 0
by Th27;

theorem Th28: :: SIN_COS7:28

for b₁, b₂ being real number st b₁ ^2 < 1 & b₂ ^2 < 1 holds
b₁ * b₂ <> 1

proof end;

Lemma39: for b₁, b₂ being real number st b₁ ^2 < 1 & b₂ ^2 < 1 holds
1 - (b₁ * b₂) <> 0
by Th28;

theorem Th29: :: SIN_COS7:29

for b₁ being real number st b₁ <> 0 holds
exp b₁ <> 1

proof end;

theorem Th30: :: SIN_COS7:30

for b₁ being real number st 0 <> b₁ holds
((exp b₁) ^2 ) - 1 <> 0

proof end;

Lemma42: for b₁ being real number holds (b₁ ^2 ) + 1 > 0

proof end;

theorem Th31: :: SIN_COS7:31

for b₁ being real number st 0 < b₁ holds
((b₁ ^2 ) - 1) / ((b₁ ^2 ) + 1) < 1

proof end;

theorem Th32: :: SIN_COS7:32

for b₁ being real number st - 1 < b₁ & b₁ < 1 holds
0 < (b₁ + 1) / (1 - b₁)

proof end;

Lemma45: for b₁ being real number st ( 1 < b₁ or b₁ < - 1 ) holds
0 < (b₁ + 1) / (b₁ - 1)

proof end;

Lemma46: for b₁ being real number holds sqrt ((b₁ ^2 ) + 1) > b₁

proof end;

Lemma47: for b₁, b₂ being real number holds ((sqrt ((b₁ ^2 ) + 1)) * (sqrt ((b₂ ^2 ) + 1))) - (b₁ * b₂) > 0

proof end;

Lemma48: for b₁ being real number st 1 <= b₁ holds
b₁ + (sqrt ((b₁ ^2 ) - 1)) > 0

proof end;

Lemma49: for b₁ being real number st 0 < b₁ holds
- 1 < ((b₁ ^2 ) - 1) / ((b₁ ^2 ) + 1)

proof end;

Lemma50: for b₁ being real number st 0 < b₁ & b₁ <> 1 & not 1 < ((b₁ ^2 ) + 1) / ((b₁ ^2 ) - 1) holds
((b₁ ^2 ) + 1) / ((b₁ ^2 ) - 1) < - 1

proof end;

Lemma51: for b₁ being real number st 0 < b₁ holds
0 < (2 * b₁) / (1 + (b₁ ^2 ))

proof end;

Lemma52: for b₁ being real number st 0 < b₁ holds
(2 * b₁) / (1 + (b₁ ^2 )) <= 1

proof end;

Lemma53: for b₁ being real number st 0 < b₁ holds
0 < (1 + (sqrt (1 + (b₁ ^2 )))) / b₁

proof end;

Lemma54: for b₁ being real number st 0 < b₁ holds
(1 - (sqrt (1 + (b₁ ^2 )))) / b₁ < 0

proof end;

Lemma55: for b₁ being real number st 0 < b₁ & b₁ <= 1 holds
0 <= 1 - (b₁ ^2 )

proof end;

Lemma56: for b₁ being real number st 0 < b₁ & b₁ <= 1 holds
0 <= 4 - (4 * (b₁ ^2 ))

proof end;

Lemma57: for b₁ being real number st 0 < b₁ & b₁ <= 1 holds
0 < 1 + (sqrt (1 - (b₁ ^2 )))

proof end;

Lemma58: for b₁ being real number st 0 < b₁ & b₁ <= 1 holds
0 < (1 + (sqrt (1 - (b₁ ^2 )))) / b₁

proof end;

Lemma59: for b₁ being real number st 0 < b₁ & b₁ <> 1 holds
(2 * b₁) / ((b₁ ^2 ) - 1) <> 0

proof end;

Lemma60: for b₁ being real number st b₁ < 0 holds
(1 + (sqrt (1 + (b₁ ^2 )))) / b₁ < 0

proof end;

Lemma61: for b₁ being real number st b₁ < 0 holds
0 < (1 - (sqrt (1 + (b₁ ^2 )))) / b₁

proof end;

definition

let c₁ be real number ;
func sinh" c₁ -> real number equals :: SIN_COS7:def 1
log number_e ,(a₁ + (sqrt ((a₁ ^2 ) + 1)));
coherence ;

end;

:: deftheorem Def1 defines sinh" SIN_COS7:def 1 :

definition

let c₁ be real number ;
func cosh1" c₁ -> real number equals :: SIN_COS7:def 2
log number_e ,(a₁ + (sqrt ((a₁ ^2 ) - 1)));
coherence ;

end;

:: deftheorem Def2 defines cosh1" SIN_COS7:def 2 :

definition

let c₁ be real number ;
func cosh2" c₁ -> real number equals :: SIN_COS7:def 3
- (log number_e ,(a₁ + (sqrt ((a₁ ^2 ) - 1))));
coherence ;

end;

:: deftheorem Def3 defines cosh2" SIN_COS7:def 3 :

definition

let c₁ be real number ;
func tanh" c₁ -> real number equals :: SIN_COS7:def 4
(1 / 2) * (log number_e ,((1 + a₁) / (1 - a₁)));
coherence ;

end;

:: deftheorem Def4 defines tanh" SIN_COS7:def 4 :

definition

let c₁ be real number ;
func coth" c₁ -> real number equals :: SIN_COS7:def 5
(1 / 2) * (log number_e ,((a₁ + 1) / (a₁ - 1)));
coherence ;

end;

:: deftheorem Def5 defines coth" SIN_COS7:def 5 :

definition

let c₁ be real number ;
func sech1" c₁ -> real number equals :: SIN_COS7:def 6
log number_e ,((1 + (sqrt (1 - (a₁ ^2 )))) / a₁);
coherence ;

end;

:: deftheorem Def6 defines sech1" SIN_COS7:def 6 :

definition

let c₁ be real number ;
func sech2" c₁ -> real number equals :: SIN_COS7:def 7
- (log number_e ,((1 + (sqrt (1 - (a₁ ^2 )))) / a₁));
coherence ;

end;

:: deftheorem Def7 defines sech2" SIN_COS7:def 7 :

definition

let c₁ be real number ;
func csch" c₁ -> real number equals :Def8: :: SIN_COS7:def 8
log number_e ,((1 + (sqrt (1 + (a₁ ^2 )))) / a₁) if 0 < a₁
log number_e ,((1 - (sqrt (1 + (a₁ ^2 )))) / a₁) if a₁ < 0
;
correctness ;

end;

:: deftheorem Def8 defines csch" SIN_COS7:def 8 :

theorem Th33: :: SIN_COS7:33

for b₁ being real number st 0 <= b₁ holds
sinh" b₁ = cosh1" (sqrt ((b₁ ^2 ) + 1))

proof end;

theorem Th34: :: SIN_COS7:34

for b₁ being real number st b₁ < 0 holds
sinh" b₁ = cosh2" (sqrt ((b₁ ^2 ) + 1))

proof end;

theorem Th35: :: SIN_COS7:35

for b₁ being real number holds sinh" b₁ = tanh" (b₁ / (sqrt ((b₁ ^2 ) + 1)))

proof end;

theorem Th36: :: SIN_COS7:36

for b₁ being real number st b₁ >= 1 holds
cosh1" b₁ = sinh" (sqrt ((b₁ ^2 ) - 1))

proof end;

theorem Th37: :: SIN_COS7:37

for b₁ being real number st b₁ > 1 holds
cosh1" b₁ = tanh" ((sqrt ((b₁ ^2 ) - 1)) / b₁)

proof end;

theorem Th38: :: SIN_COS7:38

for b₁ being real number st b₁ >= 1 holds
cosh1" b₁ = 2 * (cosh1" (sqrt ((b₁ + 1) / 2)))

proof end;

theorem Th39: :: SIN_COS7:39

for b₁ being real number st b₁ >= 1 holds
cosh2" b₁ = 2 * (cosh2" (sqrt ((b₁ + 1) / 2)))

proof end;

theorem Th40: :: SIN_COS7:40

for b₁ being real number st b₁ >= 1 holds
cosh1" b₁ = 2 * (sinh" (sqrt ((b₁ - 1) / 2)))

proof end;

theorem Th41: :: SIN_COS7:41

for b₁ being real number st b₁ ^2 < 1 holds
tanh" b₁ = sinh" (b₁ / (sqrt (1 - (b₁ ^2 ))))

proof end;

theorem Th42: :: SIN_COS7:42

for b₁ being real number st 0 < b₁ & b₁ < 1 holds
tanh" b₁ = cosh1" (1 / (sqrt (1 - (b₁ ^2 ))))

proof end;

theorem Th43: :: SIN_COS7:43

for b₁ being real number st b₁ ^2 < 1 holds
tanh" b₁ = (1 / 2) * (sinh" ((2 * b₁) / (1 - (b₁ ^2 ))))

proof end;

theorem Th44: :: SIN_COS7:44

for b₁ being real number st b₁ > 0 & b₁ < 1 holds
tanh" b₁ = (1 / 2) * (cosh1" ((1 + (b₁ ^2 )) / (1 - (b₁ ^2 ))))

proof end;

theorem Th45: :: SIN_COS7:45

for b₁ being real number st b₁ ^2 < 1 holds
tanh" b₁ = (1 / 2) * (tanh" ((2 * b₁) / (1 + (b₁ ^2 ))))

proof end;

theorem Th46: :: SIN_COS7:46

for b₁ being real number st b₁ ^2 > 1 holds
coth" b₁ = tanh" (1 / b₁)

proof end;

theorem Th47: :: SIN_COS7:47

for b₁ being real number st b₁ > 0 & b₁ <= 1 holds
sech1" b₁ = cosh1" (1 / b₁)

proof end;

theorem Th48: :: SIN_COS7:48

for b₁ being real number st b₁ > 0 & b₁ <= 1 holds
sech2" b₁ = cosh2" (1 / b₁)

proof end;

theorem Th49: :: SIN_COS7:49

for b₁ being real number st b₁ > 0 holds
csch" b₁ = sinh" (1 / b₁)

proof end;

theorem Th50: :: SIN_COS7:50

for b₁, b₂ being real number st (b₁ * b₂) + ((sqrt ((b₁ ^2 ) + 1)) * (sqrt ((b₂ ^2 ) + 1))) >= 0 holds
(sinh" b₁) + (sinh" b₂) = sinh" ((b₁ * (sqrt (1 + (b₂ ^2 )))) + (b₂ * (sqrt (1 + (b₁ ^2 )))))

proof end;

theorem Th51: :: SIN_COS7:51

for b₁, b₂ being real number holds (sinh" b₁) - (sinh" b₂) = sinh" ((b₁ * (sqrt (1 + (b₂ ^2 )))) - (b₂ * (sqrt (1 + (b₁ ^2 )))))

proof end;

theorem Th52: :: SIN_COS7:52

for b₁, b₂ being real number st 1 <= b₁ & 1 <= b₂ holds
(cosh1" b₁) + (cosh1" b₂) = cosh1" ((b₁ * b₂) + (sqrt (((b₁ ^2 ) - 1) * ((b₂ ^2 ) - 1))))

proof end;

theorem Th53: :: SIN_COS7:53

for b₁, b₂ being real number st 1 <= b₁ & 1 <= b₂ holds
(cosh2" b₁) + (cosh2" b₂) = cosh2" ((b₁ * b₂) + (sqrt (((b₁ ^2 ) - 1) * ((b₂ ^2 ) - 1))))

proof end;

theorem Th54: :: SIN_COS7:54

for b₁, b₂ being real number st 1 <= b₁ & 1 <= b₂ & abs b₂ <= abs b₁ holds
(cosh1" b₁) - (cosh1" b₂) = cosh1" ((b₁ * b₂) - (sqrt (((b₁ ^2 ) - 1) * ((b₂ ^2 ) - 1))))

proof end;

theorem Th55: :: SIN_COS7:55

for b₁, b₂ being real number st 1 <= b₁ & 1 <= b₂ & abs b₂ <= abs b₁ holds
(cosh2" b₁) - (cosh2" b₂) = cosh2" ((b₁ * b₂) - (sqrt (((b₁ ^2 ) - 1) * ((b₂ ^2 ) - 1))))

proof end;

theorem Th56: :: SIN_COS7:56

for b₁, b₂ being real number st b₁ ^2 < 1 & b₂ ^2 < 1 holds
(tanh" b₁) + (tanh" b₂) = tanh" ((b₁ + b₂) / (1 + (b₁ * b₂)))

proof end;

theorem Th57: :: SIN_COS7:57

for b₁, b₂ being real number st b₁ ^2 < 1 & b₂ ^2 < 1 holds
(tanh" b₁) - (tanh" b₂) = tanh" ((b₁ - b₂) / (1 - (b₁ * b₂)))

proof end;

theorem Th58: :: SIN_COS7:58

for b₁ being real number st 0 < b₁ & ((b₁ - 1) / (b₁ + 1)) ^2 < 1 holds
log number_e ,b₁ = 2 * (tanh" ((b₁ - 1) / (b₁ + 1)))

proof end;

theorem Th59: :: SIN_COS7:59

for b₁ being real number st 0 < b₁ & (((b₁ ^2 ) - 1) / ((b₁ ^2 ) + 1)) ^2 < 1 holds
log number_e ,b₁ = tanh" (((b₁ ^2 ) - 1) / ((b₁ ^2 ) + 1))

proof end;

theorem Th60: :: SIN_COS7:60

for b₁ being real number st 1 < b₁ & 1 <= ((b₁ ^2 ) + 1) / (2 * b₁) holds
log number_e ,b₁ = cosh1" (((b₁ ^2 ) + 1) / (2 * b₁))

proof end;

theorem Th61: :: SIN_COS7:61

for b₁ being real number st 0 < b₁ & b₁ < 1 & 1 <= ((b₁ ^2 ) + 1) / (2 * b₁) holds
log number_e ,b₁ = cosh2" (((b₁ ^2 ) + 1) / (2 * b₁))

proof end;

theorem Th62: :: SIN_COS7:62

for b₁ being real number st 0 < b₁ holds
log number_e ,b₁ = sinh" (((b₁ ^2 ) - 1) / (2 * b₁))

proof end;

theorem Th63: :: SIN_COS7:63

for b₁, b₂ being real number st b₁ = (1 / 2) * ((exp b₂) - (exp (- b₂))) holds
b₂ = log number_e ,(b₁ + (sqrt ((b₁ ^2 ) + 1)))

proof end;

theorem Th64: :: SIN_COS7:64

for b₁, b₂ being real number st b₁ = (1 / 2) * ((exp b₂) + (exp (- b₂))) & 1 <= b₁ & not b₂ = log number_e ,(b₁ + (sqrt ((b₁ ^2 ) - 1))) holds
b₂ = - (log number_e ,(b₁ + (sqrt ((b₁ ^2 ) - 1))))

proof end;

theorem Th65: :: SIN_COS7:65

for b₁, b₂ being real number st b₁ = ((exp b₂) - (exp (- b₂))) / ((exp b₂) + (exp (- b₂))) holds
b₂ = (1 / 2) * (log number_e ,((1 + b₁) / (1 - b₁)))

proof end;

theorem Th66: :: SIN_COS7:66

for b₁, b₂ being real number st b₁ = ((exp b₂) + (exp (- b₂))) / ((exp b₂) - (exp (- b₂))) & b₂ <> 0 holds
b₂ = (1 / 2) * (log number_e ,((b₁ + 1) / (b₁ - 1)))

proof end;

theorem Th67: :: SIN_COS7:67

for b₁, b₂ being real number holds
( not b₁ = 1 / (((exp b₂) + (exp (- b₂))) / 2) or b₂ = log number_e ,((1 + (sqrt (1 - (b₁ ^2 )))) / b₁) or b₂ = - (log number_e ,((1 + (sqrt (1 - (b₁ ^2 )))) / b₁)) )

proof end;

theorem Th68: :: SIN_COS7:68

for b₁, b₂ being real number st b₁ = 1 / (((exp b₂) - (exp (- b₂))) / 2) & b₂ <> 0 & not b₂ = log number_e ,((1 + (sqrt (1 + (b₁ ^2 )))) / b₁) holds
b₂ = log number_e ,((1 - (sqrt (1 + (b₁ ^2 )))) / b₁)

proof end;

theorem Th69: :: SIN_COS7:69

for b₁ being real number holds cosh . (2 * b₁) = 1 + (2 * ((sinh . b₁) ^2 ))

proof end;

theorem Th70: :: SIN_COS7:70

for b₁ being real number holds (cosh . b₁) ^2 = 1 + ((sinh . b₁) ^2 )

proof end;

theorem Th71: :: SIN_COS7:71

for b₁ being real number holds (sinh . b₁) ^2 = ((cosh . b₁) ^2 ) - 1

proof end;

theorem Th72: :: SIN_COS7:72

for b₁ being real number holds sinh (5 * b₁) = ((5 * (sinh b₁)) + (20 * ((sinh b₁) |^ 3))) + (16 * ((sinh b₁) |^ 5))

proof end;

theorem Th73: :: SIN_COS7:73

for b₁ being real number holds cosh (5 * b₁) = ((5 * (cosh b₁)) - (20 * ((cosh b₁) |^ 3))) + (16 * ((cosh b₁) |^ 5))

proof end;