:: SIN_COS4 semantic presentation

definition

let c₁ be real number ;
func tan c₁ -> Real equals :: SIN_COS4:def 1
(sin a₁) / (cos a₁);
correctness by XREAL_0:def 1;

end;

:: deftheorem Def1 defines tan SIN_COS4:def 1 :

definition

let c₁ be real number ;
func cot c₁ -> Real equals :: SIN_COS4:def 2
(cos a₁) / (sin a₁);
correctness by XREAL_0:def 1;

end;

:: deftheorem Def2 defines cot SIN_COS4:def 2 :

definition

let c₁ be real number ;
func cosec c₁ -> Real equals :: SIN_COS4:def 3
1 / (sin a₁);
correctness by XREAL_0:def 1;

end;

:: deftheorem Def3 defines cosec SIN_COS4:def 3 :

definition

let c₁ be real number ;
func sec c₁ -> Real equals :: SIN_COS4:def 4
1 / (cos a₁);
correctness by XREAL_0:def 1;

end;

:: deftheorem Def4 defines sec SIN_COS4:def 4 :

theorem Th1: :: SIN_COS4:1

for b₁ being real number holds tan b₁ = 1 / (cot b₁) by XCMPLX_1:57;

theorem Th2: :: SIN_COS4:2

for b₁ being real number holds tan (- b₁) = - (tan b₁)

proof end;

theorem Th3: :: SIN_COS4:3

for b₁ being real number holds cosec (- b₁) = - (1 / (sin b₁))

proof end;

theorem Th4: :: SIN_COS4:4

for b₁ being real number holds cot (- b₁) = - (cot b₁)

proof end;

theorem Th5: :: SIN_COS4:5

for b₁ being real number st cos b₁ <> 0 holds
(cos b₁) * (sec b₁) = 1 by XCMPLX_1:107;

theorem Th6: :: SIN_COS4:6

for b₁ being real number holds (sin b₁) * (sin b₁) = 1 - ((cos b₁) * (cos b₁))

proof end;

theorem Th7: :: SIN_COS4:7

for b₁ being real number holds (cos b₁) * (cos b₁) = 1 - ((sin b₁) * (sin b₁))

proof end;

theorem Th8: :: SIN_COS4:8

for b₁ being real number st cos b₁ <> 0 holds
sin b₁ = (cos b₁) * (tan b₁)

proof end;

Lemma4: for b₁, b₂ being real number holds sin (b₁ - b₂) = ((sin b₁) * (cos b₂)) - ((cos b₁) * (sin b₂))
by COMPLEX2:4;

Lemma5: for b₁, b₂ being real number holds cos (b₁ - b₂) = ((cos b₁) * (cos b₂)) + ((sin b₁) * (sin b₂))
by COMPLEX2:4;

theorem Th9: :: SIN_COS4:9

canceled;

theorem Th10: :: SIN_COS4:10

canceled;

theorem Th11: :: SIN_COS4:11

for b₁, b₂ being real number st cos b₁ <> 0 & cos b₂ <> 0 holds
tan (b₁ + b₂) = ((tan b₁) + (tan b₂)) / (1 - ((tan b₁) * (tan b₂)))

proof end;

theorem Th12: :: SIN_COS4:12

for b₁, b₂ being real number st cos b₁ <> 0 & cos b₂ <> 0 holds
tan (b₁ - b₂) = ((tan b₁) - (tan b₂)) / (1 + ((tan b₁) * (tan b₂)))

proof end;

theorem Th13: :: SIN_COS4:13

for b₁, b₂ being real number st sin b₁ <> 0 & sin b₂ <> 0 holds
cot (b₁ + b₂) = (((cot b₁) * (cot b₂)) - 1) / ((cot b₂) + (cot b₁))

proof end;

theorem Th14: :: SIN_COS4:14

for b₁, b₂ being real number st sin b₁ <> 0 & sin b₂ <> 0 holds
cot (b₁ - b₂) = (((cot b₁) * (cot b₂)) + 1) / ((cot b₂) - (cot b₁))

proof end;

theorem Th15: :: SIN_COS4:15

for b₁, b₂, b₃ being real number st cos b₁ <> 0 & cos b₂ <> 0 & cos b₃ <> 0 holds
sin ((b₁ + b₂) + b₃) = (((cos b₁) * (cos b₂)) * (cos b₃)) * ((((tan b₁) + (tan b₂)) + (tan b₃)) - (((tan b₁) * (tan b₂)) * (tan b₃)))

proof end;

theorem Th16: :: SIN_COS4:16

for b₁, b₂, b₃ being real number st cos b₁ <> 0 & cos b₂ <> 0 & cos b₃ <> 0 holds
cos ((b₁ + b₂) + b₃) = (((cos b₁) * (cos b₂)) * (cos b₃)) * (((1 - ((tan b₂) * (tan b₃))) - ((tan b₃) * (tan b₁))) - ((tan b₁) * (tan b₂)))

proof end;

theorem Th17: :: SIN_COS4:17

for b₁, b₂, b₃ being real number st cos b₁ <> 0 & cos b₂ <> 0 & cos b₃ <> 0 holds
tan ((b₁ + b₂) + b₃) = ((((tan b₁) + (tan b₂)) + (tan b₃)) - (((tan b₁) * (tan b₂)) * (tan b₃))) / (((1 - ((tan b₂) * (tan b₃))) - ((tan b₃) * (tan b₁))) - ((tan b₁) * (tan b₂)))

proof end;

theorem Th18: :: SIN_COS4:18

for b₁, b₂, b₃ being real number st sin b₁ <> 0 & sin b₂ <> 0 & sin b₃ <> 0 holds
cot ((b₁ + b₂) + b₃) = ((((((cot b₁) * (cot b₂)) * (cot b₃)) - (cot b₁)) - (cot b₂)) - (cot b₃)) / (((((cot b₂) * (cot b₃)) + ((cot b₃) * (cot b₁))) + ((cot b₁) * (cot b₂))) - 1)

proof end;

theorem Th19: :: SIN_COS4:19

for b₁, b₂ being real number holds (sin b₁) + (sin b₂) = 2 * ((cos ((b₁ - b₂) / 2)) * (sin ((b₁ + b₂) / 2)))

proof end;

theorem Th20: :: SIN_COS4:20

for b₁, b₂ being real number holds (sin b₁) - (sin b₂) = 2 * ((cos ((b₁ + b₂) / 2)) * (sin ((b₁ - b₂) / 2)))

proof end;

theorem Th21: :: SIN_COS4:21

for b₁, b₂ being real number holds (cos b₁) + (cos b₂) = 2 * ((cos ((b₁ + b₂) / 2)) * (cos ((b₁ - b₂) / 2)))

proof end;

theorem Th22: :: SIN_COS4:22

for b₁, b₂ being real number holds (cos b₁) - (cos b₂) = - (2 * ((sin ((b₁ + b₂) / 2)) * (sin ((b₁ - b₂) / 2))))

proof end;

theorem Th23: :: SIN_COS4:23

for b₁, b₂ being real number st cos b₁ <> 0 & cos b₂ <> 0 holds
(tan b₁) + (tan b₂) = (sin (b₁ + b₂)) / ((cos b₁) * (cos b₂))

proof end;

theorem Th24: :: SIN_COS4:24

for b₁, b₂ being real number st cos b₁ <> 0 & cos b₂ <> 0 holds
(tan b₁) - (tan b₂) = (sin (b₁ - b₂)) / ((cos b₁) * (cos b₂))

proof end;

theorem Th25: :: SIN_COS4:25

for b₁, b₂ being real number st cos b₁ <> 0 & sin b₂ <> 0 holds
(tan b₁) + (cot b₂) = (cos (b₁ - b₂)) / ((cos b₁) * (sin b₂))

proof end;

theorem Th26: :: SIN_COS4:26

for b₁, b₂ being real number st cos b₁ <> 0 & sin b₂ <> 0 holds
(tan b₁) - (cot b₂) = - ((cos (b₁ + b₂)) / ((cos b₁) * (sin b₂)))

proof end;

theorem Th27: :: SIN_COS4:27

for b₁, b₂ being real number st sin b₁ <> 0 & sin b₂ <> 0 holds
(cot b₁) + (cot b₂) = (sin (b₁ + b₂)) / ((sin b₁) * (sin b₂))

proof end;

theorem Th28: :: SIN_COS4:28

for b₁, b₂ being real number st sin b₁ <> 0 & sin b₂ <> 0 holds
(cot b₁) - (cot b₂) = - ((sin (b₁ - b₂)) / ((sin b₁) * (sin b₂)))

proof end;

theorem Th29: :: SIN_COS4:29

for b₁, b₂ being real number holds (sin (b₁ + b₂)) + (sin (b₁ - b₂)) = 2 * ((sin b₁) * (cos b₂))

proof end;

theorem Th30: :: SIN_COS4:30

for b₁, b₂ being real number holds (sin (b₁ + b₂)) - (sin (b₁ - b₂)) = 2 * ((cos b₁) * (sin b₂))

proof end;

theorem Th31: :: SIN_COS4:31

for b₁, b₂ being real number holds (cos (b₁ + b₂)) + (cos (b₁ - b₂)) = 2 * ((cos b₁) * (cos b₂))

proof end;

theorem Th32: :: SIN_COS4:32

for b₁, b₂ being real number holds (cos (b₁ + b₂)) - (cos (b₁ - b₂)) = - (2 * ((sin b₁) * (sin b₂)))

proof end;

theorem Th33: :: SIN_COS4:33

for b₁, b₂ being real number holds (sin b₁) * (sin b₂) = - ((1 / 2) * ((cos (b₁ + b₂)) - (cos (b₁ - b₂))))

proof end;

theorem Th34: :: SIN_COS4:34

for b₁, b₂ being real number holds (sin b₁) * (cos b₂) = (1 / 2) * ((sin (b₁ + b₂)) + (sin (b₁ - b₂)))

proof end;

theorem Th35: :: SIN_COS4:35

for b₁, b₂ being real number holds (cos b₁) * (sin b₂) = (1 / 2) * ((sin (b₁ + b₂)) - (sin (b₁ - b₂)))

proof end;

theorem Th36: :: SIN_COS4:36

for b₁, b₂ being real number holds (cos b₁) * (cos b₂) = (1 / 2) * ((cos (b₁ + b₂)) + (cos (b₁ - b₂)))

proof end;

theorem Th37: :: SIN_COS4:37

for b₁, b₂, b₃ being real number holds ((sin b₁) * (sin b₂)) * (sin b₃) = (1 / 4) * ((((sin ((b₁ + b₂) - b₃)) + (sin ((b₂ + b₃) - b₁))) + (sin ((b₃ + b₁) - b₂))) - (sin ((b₁ + b₂) + b₃)))

proof end;

theorem Th38: :: SIN_COS4:38

for b₁, b₂, b₃ being real number holds ((sin b₁) * (sin b₂)) * (cos b₃) = (1 / 4) * ((((- (cos ((b₁ + b₂) - b₃))) + (cos ((b₂ + b₃) - b₁))) + (cos ((b₃ + b₁) - b₂))) - (cos ((b₁ + b₂) + b₃)))

proof end;

theorem Th39: :: SIN_COS4:39

for b₁, b₂, b₃ being real number holds ((sin b₁) * (cos b₂)) * (cos b₃) = (1 / 4) * ((((sin ((b₁ + b₂) - b₃)) - (sin ((b₂ + b₃) - b₁))) + (sin ((b₃ + b₁) - b₂))) + (sin ((b₁ + b₂) + b₃)))

proof end;

theorem Th40: :: SIN_COS4:40

for b₁, b₂, b₃ being real number holds ((cos b₁) * (cos b₂)) * (cos b₃) = (1 / 4) * ((((cos ((b₁ + b₂) - b₃)) + (cos ((b₂ + b₃) - b₁))) + (cos ((b₃ + b₁) - b₂))) + (cos ((b₁ + b₂) + b₃)))

proof end;

theorem Th41: :: SIN_COS4:41

for b₁, b₂ being real number holds (sin (b₁ + b₂)) * (sin (b₁ - b₂)) = ((sin b₁) * (sin b₁)) - ((sin b₂) * (sin b₂))

proof end;

theorem Th42: :: SIN_COS4:42

for b₁, b₂ being real number holds (sin (b₁ + b₂)) * (sin (b₁ - b₂)) = ((cos b₂) * (cos b₂)) - ((cos b₁) * (cos b₁))

proof end;

theorem Th43: :: SIN_COS4:43

for b₁, b₂ being real number holds (sin (b₁ + b₂)) * (cos (b₁ - b₂)) = ((sin b₁) * (cos b₁)) + ((sin b₂) * (cos b₂))

proof end;

theorem Th44: :: SIN_COS4:44

for b₁, b₂ being real number holds (cos (b₁ + b₂)) * (sin (b₁ - b₂)) = ((sin b₁) * (cos b₁)) - ((sin b₂) * (cos b₂))

proof end;

theorem Th45: :: SIN_COS4:45

for b₁, b₂ being real number holds (cos (b₁ + b₂)) * (cos (b₁ - b₂)) = ((cos b₁) * (cos b₁)) - ((sin b₂) * (sin b₂))

proof end;

theorem Th46: :: SIN_COS4:46

for b₁, b₂ being real number holds (cos (b₁ + b₂)) * (cos (b₁ - b₂)) = ((cos b₂) * (cos b₂)) - ((sin b₁) * (sin b₁))

proof end;

theorem Th47: :: SIN_COS4:47

for b₁, b₂ being real number st cos b₁ <> 0 & cos b₂ <> 0 holds
(sin (b₁ + b₂)) / (sin (b₁ - b₂)) = ((tan b₁) + (tan b₂)) / ((tan b₁) - (tan b₂))

proof end;

theorem Th48: :: SIN_COS4:48

for b₁, b₂ being real number st cos b₁ <> 0 & cos b₂ <> 0 holds
(cos (b₁ + b₂)) / (cos (b₁ - b₂)) = (1 - ((tan b₁) * (tan b₂))) / (1 + ((tan b₁) * (tan b₂)))

proof end;

theorem Th49: :: SIN_COS4:49

for b₁, b₂ being real number holds ((sin b₁) + (sin b₂)) / ((sin b₁) - (sin b₂)) = (tan ((b₁ + b₂) / 2)) * (cot ((b₁ - b₂) / 2))

proof end;

theorem Th50: :: SIN_COS4:50

for b₁, b₂ being real number st cos ((b₁ - b₂) / 2) <> 0 holds
((sin b₁) + (sin b₂)) / ((cos b₁) + (cos b₂)) = tan ((b₁ + b₂) / 2)

proof end;

theorem Th51: :: SIN_COS4:51

for b₁, b₂ being real number st cos ((b₁ + b₂) / 2) <> 0 holds
((sin b₁) - (sin b₂)) / ((cos b₁) + (cos b₂)) = tan ((b₁ - b₂) / 2)

proof end;

theorem Th52: :: SIN_COS4:52

for b₁, b₂ being real number st sin ((b₁ + b₂) / 2) <> 0 holds
((sin b₁) + (sin b₂)) / ((cos b₂) - (cos b₁)) = cot ((b₁ - b₂) / 2)

proof end;

theorem Th53: :: SIN_COS4:53

for b₁, b₂ being real number st sin ((b₁ - b₂) / 2) <> 0 holds
((sin b₁) - (sin b₂)) / ((cos b₂) - (cos b₁)) = cot ((b₁ + b₂) / 2)

proof end;

theorem Th54: :: SIN_COS4:54

for b₁, b₂ being real number holds ((cos b₁) + (cos b₂)) / ((cos b₁) - (cos b₂)) = (cot ((b₁ + b₂) / 2)) * (cot ((b₂ - b₁) / 2))

proof end;