:: SIN_COS4 semantic presentation

begin


definition
let th be real number ;
func tan th ->  Real equals :: SIN_COS4:def 1
(sin th) / (cos th);
correctness
coherence
(sin th) / (cos th) is Real;
by XREAL_0:def_1;
end;

:: deftheorem  defines tan SIN_COS4:def_1_:_
 for th being real number holds tan th = (sin th) / (cos th);

definition
let th be real number ;
func cot th ->  Real equals :: SIN_COS4:def 2
(cos th) / (sin th);
correctness
coherence
(cos th) / (sin th) is Real;
by XREAL_0:def_1;
end;

:: deftheorem  defines cot SIN_COS4:def_2_:_
 for th being real number holds cot th = (cos th) / (sin th);

definition
let th be real number ;
func cosec th ->  Real equals :: SIN_COS4:def 3
1 / (sin th);
correctness
coherence
1 / (sin th) is Real;
by XREAL_0:def_1;
end;

:: deftheorem  defines cosec SIN_COS4:def_3_:_
 for th being real number holds cosec th = 1 / (sin th);

definition
let th be real number ;
func sec th ->  Real equals :: SIN_COS4:def 4
1 / (cos th);
correctness
coherence
1 / (cos th) is Real;
by XREAL_0:def_1;
end;

:: deftheorem  defines sec SIN_COS4:def_4_:_
 for th being real number holds sec th = 1 / (cos th);

theorem :: SIN_COS4:1
for th being real number holds tan (- th) = - (tan th)
proof
let th be real number ; ::_thesis: tan (- th) = - (tan th)
tan (- th) = (sin (- th)) / (cos th) by SIN_COS:31
.= (- (sin th)) / (cos th) by SIN_COS:31
.= - (tan th) by XCMPLX_1:187 ;
hence  tan (- th) = - (tan th) ; ::_thesis: verum
end;

theorem :: SIN_COS4:2
for th being real number holds cosec (- th) = - (1 / (sin th))
proof
let th be real number ; ::_thesis: cosec (- th) = - (1 / (sin th))
cosec (- th) = 1 / (- (sin th)) by SIN_COS:31
.= - (1 / (sin th)) by XCMPLX_1:188 ;
hence  cosec (- th) = - (1 / (sin th)) ; ::_thesis: verum
end;

theorem :: SIN_COS4:3
for th being real number holds cot (- th) = - (cot th)
proof
let th be real number ; ::_thesis: cot (- th) = - (cot th)
cot (- th) = (cos th) / (sin (- th)) by SIN_COS:31
.= (cos th) / (- (sin th)) by SIN_COS:31
.= - (cot th) by XCMPLX_1:188 ;
hence  cot (- th) = - (cot th) ; ::_thesis: verum
end;

theorem Th4: :: SIN_COS4:4
for th being real number holds (sin th) * (sin th) = 1 - ((cos th) * (cos th))
proof
let th be real number ; ::_thesis: (sin th) * (sin th) = 1 - ((cos th) * (cos th))
(sin th) * (sin th) = ((sin th) * (sin th)) + (1 - 1)
.= ((sin th) * (sin th)) + (1 - (- (- (((sin th) * (sin th)) + ((cos th) * (cos th)))))) by SIN_COS:29
.= 1 - ((cos th) * (cos th)) ;
hence  (sin th) * (sin th) = 1 - ((cos th) * (cos th)) ; ::_thesis: verum
end;

theorem Th5: :: SIN_COS4:5
for th being real number holds (cos th) * (cos th) = 1 - ((sin th) * (sin th))
proof
let th be real number ; ::_thesis: (cos th) * (cos th) = 1 - ((sin th) * (sin th))
(cos th) * (cos th) = ((cos th) * (cos th)) + (1 - 1)
.= ((cos th) * (cos th)) + (1 - (- (- (((sin th) * (sin th)) + ((cos th) * (cos th)))))) by SIN_COS:29
.= 1 - ((sin th) * (sin th)) ;
hence  (cos th) * (cos th) = 1 - ((sin th) * (sin th)) ; ::_thesis: verum
end;

theorem Th6: :: SIN_COS4:6
for th being real number st cos th <> 0 holds
sin th = (cos th) * (tan th)
proof
let th be real number ; ::_thesis: ( cos th <> 0 implies sin th = (cos th) * (tan th) )
assume  cos th <> 0 ; ::_thesis: sin th = (cos th) * (tan th)
then  sin th = ((cos th) / (cos th)) * (sin th) by XCMPLX_1:88
.= (cos th) * (tan th) by XCMPLX_1:75 ;
hence  sin th = (cos th) * (tan th) ; ::_thesis: verum
end;

theorem :: SIN_COS4:7
for th1, th2 being real number st cos th1 <> 0 & cos th2 <> 0 holds
tan (th1 + th2) = ((tan th1) + (tan th2)) / (1 - ((tan th1) * (tan th2)))
proof
let th1, th2 be real number ; ::_thesis: ( cos th1 <> 0 & cos th2 <> 0 implies tan (th1 + th2) = ((tan th1) + (tan th2)) / (1 - ((tan th1) * (tan th2))) )
assume that
A1: cos th1 <> 0 and
A2: cos th2 <> 0 ; ::_thesis: tan (th1 + th2) = ((tan th1) + (tan th2)) / (1 - ((tan th1) * (tan th2)))
tan (th1 + th2) = ((sin (th1 + th2)) / ((cos th1) * (cos th2))) / ((cos (th1 + th2)) / ((cos th1) * (cos th2))) by A1, A2, XCMPLX_1:6, XCMPLX_1:55
.= ((((sin th1) * (cos th2)) + ((cos th1) * (sin th2))) / ((cos th1) * (cos th2))) / ((cos (th1 + th2)) / ((cos th1) * (cos th2))) by SIN_COS:75
.= ((((sin th1) * (cos th2)) + ((cos th1) * (sin th2))) / ((cos th1) * (cos th2))) / ((((cos th1) * (cos th2)) - ((sin th1) * (sin th2))) / ((cos th1) * (cos th2))) by SIN_COS:75
.= ((((sin th1) * (cos th2)) / ((cos th1) * (cos th2))) + (((cos th1) * (sin th2)) / ((cos th1) * (cos th2)))) / ((((cos th1) * (cos th2)) - ((sin th1) * (sin th2))) / ((cos th1) * (cos th2))) by XCMPLX_1:62
.= ((((sin th1) * (cos th2)) / ((cos th1) * (cos th2))) + (((cos th1) * (sin th2)) / ((cos th1) * (cos th2)))) / ((((cos th1) * (cos th2)) / ((cos th1) * (cos th2))) - (((sin th1) * (sin th2)) / ((cos th1) * (cos th2)))) by XCMPLX_1:120
.= ((((sin th1) / (cos th1)) * ((cos th2) / (cos th2))) + (((cos th1) * (sin th2)) / ((cos th1) * (cos th2)))) / ((((cos th1) * (cos th2)) / ((cos th1) * (cos th2))) - (((sin th1) * (sin th2)) / ((cos th1) * (cos th2)))) by XCMPLX_1:76
.= ((((sin th1) / (cos th1)) * ((cos th2) / (cos th2))) + (((sin th2) / (cos th2)) * ((cos th1) / (cos th1)))) / ((((cos th1) * (cos th2)) / ((cos th1) * (cos th2))) - (((sin th1) * (sin th2)) / ((cos th1) * (cos th2)))) by XCMPLX_1:76
.= ((((sin th1) / (cos th1)) * ((cos th2) / (cos th2))) + (((sin th2) / (cos th2)) * ((cos th1) / (cos th1)))) / ((((cos th1) / (cos th1)) * ((cos th2) / (cos th2))) - (((sin th1) * (sin th2)) / ((cos th1) * (cos th2)))) by XCMPLX_1:76
.= ((((sin th1) / (cos th1)) * ((cos th2) / (cos th2))) + (((sin th2) / (cos th2)) * ((cos th1) / (cos th1)))) / ((((cos th1) / (cos th1)) * ((cos th2) / (cos th2))) - (((sin th1) / (cos th1)) * ((sin th2) / (cos th2)))) by XCMPLX_1:76
.= (((sin th1) / (cos th1)) + (((sin th2) / (cos th2)) * ((cos th1) / (cos th1)))) / ((((cos th1) / (cos th1)) * ((cos th2) / (cos th2))) - (((sin th1) / (cos th1)) * ((sin th2) / (cos th2)))) by A2, XCMPLX_1:88
.= (((sin th1) / (cos th1)) + ((sin th2) / (cos th2))) / ((((cos th1) / (cos th1)) * ((cos th2) / (cos th2))) - (((sin th1) / (cos th1)) * ((sin th2) / (cos th2)))) by A1, XCMPLX_1:88
.= (((sin th1) / (cos th1)) + ((sin th2) / (cos th2))) / (((cos th1) / (cos th1)) - (((sin th1) / (cos th1)) * ((sin th2) / (cos th2)))) by A2, XCMPLX_1:88
.= ((tan th1) + (tan th2)) / (1 - ((tan th1) * (tan th2))) by A1, XCMPLX_1:60 ;
hence  tan (th1 + th2) = ((tan th1) + (tan th2)) / (1 - ((tan th1) * (tan th2))) ; ::_thesis: verum
end;

theorem :: SIN_COS4:8
for th1, th2 being real number st cos th1 <> 0 & cos th2 <> 0 holds
tan (th1 - th2) = ((tan th1) - (tan th2)) / (1 + ((tan th1) * (tan th2)))
proof
let th1, th2 be real number ; ::_thesis: ( cos th1 <> 0 & cos th2 <> 0 implies tan (th1 - th2) = ((tan th1) - (tan th2)) / (1 + ((tan th1) * (tan th2))) )
assume that
A1: cos th1 <> 0 and
A2: cos th2 <> 0 ; ::_thesis: tan (th1 - th2) = ((tan th1) - (tan th2)) / (1 + ((tan th1) * (tan th2)))
tan (th1 - th2) = ((sin (th1 + (- th2))) / ((cos th1) * (cos th2))) / ((cos (th1 + (- th2))) / ((cos th1) * (cos th2))) by A1, A2, XCMPLX_1:6, XCMPLX_1:55
.= ((((sin th1) * (cos (- th2))) + ((cos th1) * (sin (- th2)))) / ((cos th1) * (cos th2))) / ((cos (th1 + (- th2))) / ((cos th1) * (cos th2))) by SIN_COS:75
.= ((((sin th1) * (cos th2)) + ((cos th1) * (sin (- th2)))) / ((cos th1) * (cos th2))) / ((cos (th1 + (- th2))) / ((cos th1) * (cos th2))) by SIN_COS:31
.= ((((sin th1) * (cos th2)) + ((cos th1) * (- (sin th2)))) / ((cos th1) * (cos th2))) / ((cos (th1 + (- th2))) / ((cos th1) * (cos th2))) by SIN_COS:31
.= ((((sin th1) * (cos th2)) - ((cos th1) * (sin th2))) / ((cos th1) * (cos th2))) / ((((cos th1) * (cos (- th2))) - ((sin th1) * (sin (- th2)))) / ((cos th1) * (cos th2))) by SIN_COS:75
.= ((((sin th1) * (cos th2)) - ((cos th1) * (sin th2))) / ((cos th1) * (cos th2))) / ((((cos th1) * (cos th2)) - ((sin th1) * (sin (- th2)))) / ((cos th1) * (cos th2))) by SIN_COS:31
.= ((((sin th1) * (cos th2)) - ((cos th1) * (sin th2))) / ((cos th1) * (cos th2))) / ((((cos th1) * (cos th2)) - ((sin th1) * (- (sin th2)))) / ((cos th1) * (cos th2))) by SIN_COS:31
.= ((((sin th1) * (cos th2)) / ((cos th1) * (cos th2))) - (((cos th1) * (sin th2)) / ((cos th1) * (cos th2)))) / ((((cos th1) * (cos th2)) + ((sin th1) * (sin th2))) / ((cos th1) * (cos th2))) by XCMPLX_1:120
.= ((((sin th1) * (cos th2)) / ((cos th1) * (cos th2))) - (((cos th1) * (sin th2)) / ((cos th1) * (cos th2)))) / ((((cos th1) * (cos th2)) / ((cos th1) * (cos th2))) + (((sin th1) * (sin th2)) / ((cos th1) * (cos th2)))) by XCMPLX_1:62
.= ((((sin th1) / (cos th1)) * ((cos th2) / (cos th2))) - (((cos th1) * (sin th2)) / ((cos th1) * (cos th2)))) / ((((cos th1) * (cos th2)) / ((cos th1) * (cos th2))) + (((sin th1) * (sin th2)) / ((cos th1) * (cos th2)))) by XCMPLX_1:76
.= ((((sin th1) / (cos th1)) * ((cos th2) / (cos th2))) - (((sin th2) / (cos th2)) * ((cos th1) / (cos th1)))) / ((((cos th1) * (cos th2)) / ((cos th1) * (cos th2))) + (((sin th1) * (sin th2)) / ((cos th1) * (cos th2)))) by XCMPLX_1:76
.= ((((sin th1) / (cos th1)) * ((cos th2) / (cos th2))) - (((sin th2) / (cos th2)) * ((cos th1) / (cos th1)))) / ((((cos th1) / (cos th1)) * ((cos th2) / (cos th2))) + (((sin th1) * (sin th2)) / ((cos th1) * (cos th2)))) by XCMPLX_1:76
.= ((((sin th1) / (cos th1)) * ((cos th2) / (cos th2))) - (((sin th2) / (cos th2)) * ((cos th1) / (cos th1)))) / ((((cos th1) / (cos th1)) * ((cos th2) / (cos th2))) + (((sin th1) / (cos th1)) * ((sin th2) / (cos th2)))) by XCMPLX_1:76
.= (((sin th1) / (cos th1)) - (((sin th2) / (cos th2)) * ((cos th1) / (cos th1)))) / ((((cos th1) / (cos th1)) * ((cos th2) / (cos th2))) + (((sin th1) / (cos th1)) * ((sin th2) / (cos th2)))) by A2, XCMPLX_1:88
.= (((sin th1) / (cos th1)) - ((sin th2) / (cos th2))) / ((((cos th1) / (cos th1)) * ((cos th2) / (cos th2))) + (((sin th1) / (cos th1)) * ((sin th2) / (cos th2)))) by A1, XCMPLX_1:88
.= (((sin th1) / (cos th1)) - ((sin th2) / (cos th2))) / (((cos th1) / (cos th1)) + (((sin th1) / (cos th1)) * ((sin th2) / (cos th2)))) by A2, XCMPLX_1:88
.= ((tan th1) - (tan th2)) / (1 + ((tan th1) * (tan th2))) by A1, XCMPLX_1:60 ;
hence  tan (th1 - th2) = ((tan th1) - (tan th2)) / (1 + ((tan th1) * (tan th2))) ; ::_thesis: verum
end;

theorem :: SIN_COS4:9
for th1, th2 being real number st sin th1 <> 0 & sin th2 <> 0 holds
cot (th1 + th2) = (((cot th1) * (cot th2)) - 1) / ((cot th2) + (cot th1))
proof
let th1, th2 be real number ; ::_thesis: ( sin th1 <> 0 & sin th2 <> 0 implies cot (th1 + th2) = (((cot th1) * (cot th2)) - 1) / ((cot th2) + (cot th1)) )
assume that
A1: sin th1 <> 0 and
A2: sin th2 <> 0 ; ::_thesis: cot (th1 + th2) = (((cot th1) * (cot th2)) - 1) / ((cot th2) + (cot th1))
cot (th1 + th2) = ((cos (th1 + th2)) / ((sin th1) * (sin th2))) / ((sin (th1 + th2)) / ((sin th1) * (sin th2))) by A1, A2, XCMPLX_1:6, XCMPLX_1:55
.= ((((cos th1) * (cos th2)) - ((sin th1) * (sin th2))) / ((sin th1) * (sin th2))) / ((sin (th1 + th2)) / ((sin th1) * (sin th2))) by SIN_COS:75
.= ((((cos th1) * (cos th2)) - ((sin th1) * (sin th2))) / ((sin th1) * (sin th2))) / ((((sin th1) * (cos th2)) + ((cos th1) * (sin th2))) / ((sin th1) * (sin th2))) by SIN_COS:75
.= ((((cos th1) * (cos th2)) / ((sin th1) * (sin th2))) - (((sin th1) * (sin th2)) / ((sin th1) * (sin th2)))) / ((((sin th1) * (cos th2)) + ((cos th1) * (sin th2))) / ((sin th1) * (sin th2))) by XCMPLX_1:120
.= ((((cos th1) * (cos th2)) / ((sin th1) * (sin th2))) - (((sin th1) * (sin th2)) / ((sin th1) * (sin th2)))) / ((((sin th1) * (cos th2)) / ((sin th1) * (sin th2))) + (((cos th1) * (sin th2)) / ((sin th1) * (sin th2)))) by XCMPLX_1:62
.= ((((cos th1) / (sin th1)) * ((cos th2) / (sin th2))) - (((sin th1) * (sin th2)) / ((sin th1) * (sin th2)))) / ((((sin th1) * (cos th2)) / ((sin th1) * (sin th2))) + (((cos th1) * (sin th2)) / ((sin th1) * (sin th2)))) by XCMPLX_1:76
.= ((((cos th1) / (sin th1)) * ((cos th2) / (sin th2))) - (((sin th1) / (sin th1)) * ((sin th2) / (sin th2)))) / ((((sin th1) * (cos th2)) / ((sin th1) * (sin th2))) + (((cos th1) * (sin th2)) / ((sin th1) * (sin th2)))) by XCMPLX_1:76
.= ((((cos th1) / (sin th1)) * ((cos th2) / (sin th2))) - (((sin th1) / (sin th1)) * ((sin th2) / (sin th2)))) / ((((sin th1) / (sin th1)) * ((cos th2) / (sin th2))) + (((cos th1) * (sin th2)) / ((sin th1) * (sin th2)))) by XCMPLX_1:76
.= ((((cos th1) / (sin th1)) * ((cos th2) / (sin th2))) - (((sin th1) / (sin th1)) * ((sin th2) / (sin th2)))) / ((((sin th1) / (sin th1)) * ((cos th2) / (sin th2))) + (((cos th1) / (sin th1)) * ((sin th2) / (sin th2)))) by XCMPLX_1:76
.= ((((cos th1) / (sin th1)) * ((cos th2) / (sin th2))) - ((sin th1) / (sin th1))) / ((((sin th1) / (sin th1)) * ((cos th2) / (sin th2))) + (((cos th1) / (sin th1)) * ((sin th2) / (sin th2)))) by A2, XCMPLX_1:88
.= ((((cos th1) / (sin th1)) * ((cos th2) / (sin th2))) - 1) / ((((sin th1) / (sin th1)) * ((cos th2) / (sin th2))) + (((cos th1) / (sin th1)) * ((sin th2) / (sin th2)))) by A1, XCMPLX_1:60
.= ((((cos th1) / (sin th1)) * ((cos th2) / (sin th2))) - 1) / (((cos th2) / (sin th2)) + (((cos th1) / (sin th1)) * ((sin th2) / (sin th2)))) by A1, XCMPLX_1:88
.= (((cot th1) * (cot th2)) - 1) / ((cot th2) + (cot th1)) by A2, XCMPLX_1:88 ;
hence  cot (th1 + th2) = (((cot th1) * (cot th2)) - 1) / ((cot th2) + (cot th1)) ; ::_thesis: verum
end;

theorem :: SIN_COS4:10
for th1, th2 being real number st sin th1 <> 0 & sin th2 <> 0 holds
cot (th1 - th2) = (((cot th1) * (cot th2)) + 1) / ((cot th2) - (cot th1))
proof
let th1, th2 be real number ; ::_thesis: ( sin th1 <> 0 & sin th2 <> 0 implies cot (th1 - th2) = (((cot th1) * (cot th2)) + 1) / ((cot th2) - (cot th1)) )
assume that
A1: sin th1 <> 0 and
A2: sin th2 <> 0 ; ::_thesis: cot (th1 - th2) = (((cot th1) * (cot th2)) + 1) / ((cot th2) - (cot th1))
cot (th1 - th2) = ((cos (th1 - th2)) / ((sin th1) * (sin th2))) / ((sin (th1 - th2)) / ((sin th1) * (sin th2))) by A1, A2, XCMPLX_1:6, XCMPLX_1:55
.= ((((cos th1) * (cos th2)) + ((sin th1) * (sin th2))) / ((sin th1) * (sin th2))) / ((sin (th1 - th2)) / ((sin th1) * (sin th2))) by SIN_COS:83
.= ((((cos th1) * (cos th2)) + ((sin th1) * (sin th2))) / ((sin th1) * (sin th2))) / ((((sin th1) * (cos th2)) - ((cos th1) * (sin th2))) / ((sin th1) * (sin th2))) by SIN_COS:82
.= ((((cos th1) * (cos th2)) / ((sin th1) * (sin th2))) + (((sin th1) * (sin th2)) / ((sin th1) * (sin th2)))) / ((((sin th1) * (cos th2)) - ((cos th1) * (sin th2))) / ((sin th1) * (sin th2))) by XCMPLX_1:62
.= ((((cos th1) * (cos th2)) / ((sin th1) * (sin th2))) + (((sin th1) * (sin th2)) / ((sin th1) * (sin th2)))) / ((((sin th1) * (cos th2)) / ((sin th1) * (sin th2))) - (((cos th1) * (sin th2)) / ((sin th1) * (sin th2)))) by XCMPLX_1:120
.= ((((cos th1) / (sin th1)) * ((cos th2) / (sin th2))) + (((sin th1) * (sin th2)) / ((sin th1) * (sin th2)))) / ((((sin th1) * (cos th2)) / ((sin th1) * (sin th2))) - (((cos th1) * (sin th2)) / ((sin th1) * (sin th2)))) by XCMPLX_1:76
.= ((((cos th1) / (sin th1)) * ((cos th2) / (sin th2))) + (((sin th1) / (sin th1)) * ((sin th2) / (sin th2)))) / ((((sin th1) * (cos th2)) / ((sin th1) * (sin th2))) - (((cos th1) * (sin th2)) / ((sin th1) * (sin th2)))) by XCMPLX_1:76
.= ((((cos th1) / (sin th1)) * ((cos th2) / (sin th2))) + (((sin th1) / (sin th1)) * ((sin th2) / (sin th2)))) / ((((sin th1) / (sin th1)) * ((cos th2) / (sin th2))) - (((cos th1) * (sin th2)) / ((sin th1) * (sin th2)))) by XCMPLX_1:76
.= ((((cos th1) / (sin th1)) * ((cos th2) / (sin th2))) + (((sin th1) / (sin th1)) * ((sin th2) / (sin th2)))) / ((((sin th1) / (sin th1)) * ((cos th2) / (sin th2))) - (((cos th1) / (sin th1)) * ((sin th2) / (sin th2)))) by XCMPLX_1:76
.= ((((cos th1) / (sin th1)) * ((cos th2) / (sin th2))) + ((sin th1) / (sin th1))) / ((((sin th1) / (sin th1)) * ((cos th2) / (sin th2))) - (((cos th1) / (sin th1)) * ((sin th2) / (sin th2)))) by A2, XCMPLX_1:88
.= ((((cos th1) / (sin th1)) * ((cos th2) / (sin th2))) + 1) / ((((sin th1) / (sin th1)) * ((cos th2) / (sin th2))) - (((cos th1) / (sin th1)) * ((sin th2) / (sin th2)))) by A1, XCMPLX_1:60
.= ((((cos th1) / (sin th1)) * ((cos th2) / (sin th2))) + 1) / (((cos th2) / (sin th2)) - (((cos th1) / (sin th1)) * ((sin th2) / (sin th2)))) by A1, XCMPLX_1:88
.= (((cot th1) * (cot th2)) + 1) / ((cot th2) - (cot th1)) by A2, XCMPLX_1:88 ;
hence  cot (th1 - th2) = (((cot th1) * (cot th2)) + 1) / ((cot th2) - (cot th1)) ; ::_thesis: verum
end;

theorem Th11: :: SIN_COS4:11
for th1, th2, th3 being real number st cos th1 <> 0 & cos th2 <> 0 & cos th3 <> 0 holds
sin ((th1 + th2) + th3) = (((cos th1) * (cos th2)) * (cos th3)) * ((((tan th1) + (tan th2)) + (tan th3)) - (((tan th1) * (tan th2)) * (tan th3)))
proof
let th1, th2, th3 be real number ; ::_thesis: ( cos th1 <> 0 & cos th2 <> 0 & cos th3 <> 0 implies sin ((th1 + th2) + th3) = (((cos th1) * (cos th2)) * (cos th3)) * ((((tan th1) + (tan th2)) + (tan th3)) - (((tan th1) * (tan th2)) * (tan th3))) )
assume that
A1: cos th1 <> 0 and
A2: cos th2 <> 0 and
A3: cos th3 <> 0 ; ::_thesis: sin ((th1 + th2) + th3) = (((cos th1) * (cos th2)) * (cos th3)) * ((((tan th1) + (tan th2)) + (tan th3)) - (((tan th1) * (tan th2)) * (tan th3)))
sin ((th1 + th2) + th3) = sin (th1 + (th2 + th3))
.= ((sin th1) * (cos (th2 + th3))) + ((cos th1) * (sin (th2 + th3))) by SIN_COS:75
.= ((sin th1) * (((cos th2) * (cos th3)) - ((sin th2) * (sin th3)))) + ((cos th1) * (sin (th2 + th3))) by SIN_COS:75
.= (((sin th1) * ((cos th2) * (cos th3))) - ((sin th1) * ((sin th2) * (sin th3)))) + ((cos th1) * (((sin th2) * (cos th3)) + ((cos th2) * (sin th3)))) by SIN_COS:75
.= ((((cos th1) * (tan th1)) * ((cos th2) * (cos th3))) - ((sin th1) * ((sin th2) * (sin th3)))) + (((cos th1) * ((sin th2) * (cos th3))) + ((cos th1) * ((cos th2) * (sin th3)))) by A1, Th6
.= ((((cos th1) * (tan th1)) * ((cos th2) * (cos th3))) - (((cos th1) * (tan th1)) * ((sin th2) * (sin th3)))) + (((cos th1) * ((sin th2) * (cos th3))) + ((cos th1) * ((cos th2) * (sin th3)))) by A1, Th6
.= ((((cos th1) * (tan th1)) * ((cos th2) * (cos th3))) - (((cos th1) * (tan th1)) * (((cos th2) * (tan th2)) * (sin th3)))) + (((cos th1) * ((sin th2) * (cos th3))) + ((cos th1) * ((cos th2) * (sin th3)))) by A2, Th6
.= ((((cos th1) * (tan th1)) * ((cos th2) * (cos th3))) - (((cos th1) * (tan th1)) * (((cos th2) * (tan th2)) * ((cos th3) * (tan th3))))) + (((cos th1) * ((sin th2) * (cos th3))) + ((cos th1) * ((cos th2) * (sin th3)))) by A3, Th6
.= ((((cos th1) * (tan th1)) * ((cos th2) * (cos th3))) - (((cos th1) * (tan th1)) * (((cos th2) * (tan th2)) * ((cos th3) * (tan th3))))) + (((cos th1) * (((cos th2) * (tan th2)) * (cos th3))) + ((cos th1) * ((cos th2) * (sin th3)))) by A2, Th6
.= ((((cos th1) * (cos th2)) * ((cos th3) * (tan th1))) - ((((cos th1) * (cos th2)) * ((tan th1) * (tan th2))) * ((cos th3) * (tan th3)))) + (((cos th1) * (((cos th2) * (tan th2)) * (cos th3))) + ((cos th1) * ((cos th2) * ((cos th3) * (tan th3))))) by A3, Th6
.= (((cos th1) * (cos th2)) * (cos th3)) * ((((tan th1) + (tan th2)) + (tan th3)) - (((tan th1) * (tan th2)) * (tan th3))) ;
hence  sin ((th1 + th2) + th3) = (((cos th1) * (cos th2)) * (cos th3)) * ((((tan th1) + (tan th2)) + (tan th3)) - (((tan th1) * (tan th2)) * (tan th3))) ; ::_thesis: verum
end;

theorem Th12: :: SIN_COS4:12
for th1, th2, th3 being real number st cos th1 <> 0 & cos th2 <> 0 & cos th3 <> 0 holds
cos ((th1 + th2) + th3) = (((cos th1) * (cos th2)) * (cos th3)) * (((1 - ((tan th2) * (tan th3))) - ((tan th3) * (tan th1))) - ((tan th1) * (tan th2)))
proof
let th1, th2, th3 be real number ; ::_thesis: ( cos th1 <> 0 & cos th2 <> 0 & cos th3 <> 0 implies cos ((th1 + th2) + th3) = (((cos th1) * (cos th2)) * (cos th3)) * (((1 - ((tan th2) * (tan th3))) - ((tan th3) * (tan th1))) - ((tan th1) * (tan th2))) )
assume that
A1: cos th1 <> 0 and
A2: cos th2 <> 0 and
A3: cos th3 <> 0 ; ::_thesis: cos ((th1 + th2) + th3) = (((cos th1) * (cos th2)) * (cos th3)) * (((1 - ((tan th2) * (tan th3))) - ((tan th3) * (tan th1))) - ((tan th1) * (tan th2)))
cos ((th1 + th2) + th3) = cos (th1 + (th2 + th3))
.= ((cos th1) * (cos (th2 + th3))) - ((sin th1) * (sin (th2 + th3))) by SIN_COS:75
.= ((cos th1) * (((cos th2) * (cos th3)) - ((sin th2) * (sin th3)))) - ((sin th1) * (sin (th2 + th3))) by SIN_COS:75
.= (((cos th1) * ((cos th2) * (cos th3))) - ((cos th1) * ((sin th2) * (sin th3)))) - ((sin th1) * (((sin th2) * (cos th3)) + ((cos th2) * (sin th3)))) by SIN_COS:75
.= (((cos th1) * ((cos th2) * (cos th3))) - ((cos th1) * (((cos th2) * (tan th2)) * (sin th3)))) - ((sin th1) * (((sin th2) * (cos th3)) + ((cos th2) * (sin th3)))) by A2, Th6
.= (((cos th1) * ((cos th2) * (cos th3))) - ((cos th1) * (((cos th2) * (tan th2)) * ((cos th3) * (tan th3))))) - ((sin th1) * (((sin th2) * (cos th3)) + ((cos th2) * (sin th3)))) by A3, Th6
.= (((cos th1) * ((cos th2) * (cos th3))) - ((cos th1) * (((cos th2) * (tan th2)) * ((cos th3) * (tan th3))))) - (((cos th1) * (tan th1)) * (((sin th2) * (cos th3)) + ((cos th2) * (sin th3)))) by A1, Th6
.= (((cos th1) * ((cos th2) * (cos th3))) - ((cos th1) * (((cos th2) * (tan th2)) * ((cos th3) * (tan th3))))) - (((cos th1) * (tan th1)) * ((((cos th2) * (tan th2)) * (cos th3)) + ((cos th2) * (sin th3)))) by A2, Th6
.= ((((cos th1) * (cos th2)) * (cos th3)) - ((((cos th1) * (cos th2)) * (cos th3)) * ((tan th2) * (tan th3)))) - (((cos th1) * (tan th1)) * ((((cos th2) * (cos th3)) * (tan th2)) + ((cos th2) * ((cos th3) * (tan th3))))) by A3, Th6
.= (((cos th1) * (cos th2)) * (cos th3)) * (((1 - ((tan th2) * (tan th3))) - ((tan th3) * (tan th1))) - ((tan th1) * (tan th2))) ;
hence  cos ((th1 + th2) + th3) = (((cos th1) * (cos th2)) * (cos th3)) * (((1 - ((tan th2) * (tan th3))) - ((tan th3) * (tan th1))) - ((tan th1) * (tan th2))) ; ::_thesis: verum
end;

theorem :: SIN_COS4:13
for th1, th2, th3 being real number st cos th1 <> 0 & cos th2 <> 0 & cos th3 <> 0 holds
tan ((th1 + th2) + th3) = ((((tan th1) + (tan th2)) + (tan th3)) - (((tan th1) * (tan th2)) * (tan th3))) / (((1 - ((tan th2) * (tan th3))) - ((tan th3) * (tan th1))) - ((tan th1) * (tan th2)))
proof
let th1, th2, th3 be real number ; ::_thesis: ( cos th1 <> 0 & cos th2 <> 0 & cos th3 <> 0 implies tan ((th1 + th2) + th3) = ((((tan th1) + (tan th2)) + (tan th3)) - (((tan th1) * (tan th2)) * (tan th3))) / (((1 - ((tan th2) * (tan th3))) - ((tan th3) * (tan th1))) - ((tan th1) * (tan th2))) )
assume that
A1: ( cos th1 <> 0 & cos th2 <> 0 ) and
A2: cos th3 <> 0 ; ::_thesis: tan ((th1 + th2) + th3) = ((((tan th1) + (tan th2)) + (tan th3)) - (((tan th1) * (tan th2)) * (tan th3))) / (((1 - ((tan th2) * (tan th3))) - ((tan th3) * (tan th1))) - ((tan th1) * (tan th2)))
A3: (cos th1) * (cos th2) <> 0 by A1, XCMPLX_1:6;
tan ((th1 + th2) + th3) = ((((cos th1) * (cos th2)) * (cos th3)) * ((((tan th1) + (tan th2)) + (tan th3)) - (((tan th1) * (tan th2)) * (tan th3)))) / (cos ((th1 + th2) + th3)) by A1, A2, Th11
.= ((((cos th1) * (cos th2)) * (cos th3)) * ((((tan th1) + (tan th2)) + (tan th3)) - (((tan th1) * (tan th2)) * (tan th3)))) / ((((cos th1) * (cos th2)) * (cos th3)) * (((1 - ((tan th2) * (tan th3))) - ((tan th3) * (tan th1))) - ((tan th1) * (tan th2)))) by A1, A2, Th12
.= ((((cos th1) * (cos th2)) * (cos th3)) / (((cos th1) * (cos th2)) * (cos th3))) / ((((1 - ((tan th2) * (tan th3))) - ((tan th3) * (tan th1))) - ((tan th1) * (tan th2))) / ((((tan th1) + (tan th2)) + (tan th3)) - (((tan th1) * (tan th2)) * (tan th3)))) by XCMPLX_1:84
.= 1 / ((((1 - ((tan th2) * (tan th3))) - ((tan th3) * (tan th1))) - ((tan th1) * (tan th2))) / ((((tan th1) + (tan th2)) + (tan th3)) - (((tan th1) * (tan th2)) * (tan th3)))) by A2, A3, XCMPLX_1:6, XCMPLX_1:60
.= ((((tan th1) + (tan th2)) + (tan th3)) - (((tan th1) * (tan th2)) * (tan th3))) / (((1 - ((tan th2) * (tan th3))) - ((tan th3) * (tan th1))) - ((tan th1) * (tan th2))) by XCMPLX_1:57 ;
hence  tan ((th1 + th2) + th3) = ((((tan th1) + (tan th2)) + (tan th3)) - (((tan th1) * (tan th2)) * (tan th3))) / (((1 - ((tan th2) * (tan th3))) - ((tan th3) * (tan th1))) - ((tan th1) * (tan th2))) ; ::_thesis: verum
end;

theorem :: SIN_COS4:14
for th1, th2, th3 being real number st sin th1 <> 0 & sin th2 <> 0 & sin th3 <> 0 holds
cot ((th1 + th2) + th3) = ((((((cot th1) * (cot th2)) * (cot th3)) - (cot th1)) - (cot th2)) - (cot th3)) / (((((cot th2) * (cot th3)) + ((cot th3) * (cot th1))) + ((cot th1) * (cot th2))) - 1)
proof
let th1, th2, th3 be real number ; ::_thesis: ( sin th1 <> 0 & sin th2 <> 0 & sin th3 <> 0 implies cot ((th1 + th2) + th3) = ((((((cot th1) * (cot th2)) * (cot th3)) - (cot th1)) - (cot th2)) - (cot th3)) / (((((cot th2) * (cot th3)) + ((cot th3) * (cot th1))) + ((cot th1) * (cot th2))) - 1) )
assume that
A1: sin th1 <> 0 and
A2: sin th2 <> 0 and
A3: sin th3 <> 0 ; ::_thesis: cot ((th1 + th2) + th3) = ((((((cot th1) * (cot th2)) * (cot th3)) - (cot th1)) - (cot th2)) - (cot th3)) / (((((cot th2) * (cot th3)) + ((cot th3) * (cot th1))) + ((cot th1) * (cot th2))) - 1)
A4: (sin th1) * (sin th2) <> 0 by A1, A2, XCMPLX_1:6;
cot ((th1 + th2) + th3) = (((cos (th1 + th2)) * (cos th3)) - ((sin (th1 + th2)) * (sin th3))) / (sin ((th1 + th2) + th3)) by SIN_COS:75
.= (((((cos th1) * (cos th2)) - ((sin th1) * (sin th2))) * (cos th3)) - ((sin (th1 + th2)) * (sin th3))) / (sin ((th1 + th2) + th3)) by SIN_COS:75
.= (((cos th3) * (((cos th1) * (cos th2)) - ((sin th1) * (sin th2)))) - ((sin th3) * (((sin th1) * (cos th2)) + ((cos th1) * (sin th2))))) / (sin ((th1 + th2) + th3)) by SIN_COS:75
.= ((((cos th3) * (((cos th1) * (cos th2)) - ((sin th1) * (sin th2)))) - ((sin th3) * (((sin th1) * (cos th2)) + ((cos th1) * (sin th2))))) / (((sin th1) * (sin th2)) * (sin th3))) / ((sin ((th1 + th2) + th3)) / (((sin th1) * (sin th2)) * (sin th3))) by A3, A4, XCMPLX_1:6, XCMPLX_1:55
.= ((((cos th3) * (((cos th1) * (cos th2)) - ((sin th1) * (sin th2)))) / ((sin th3) * ((sin th1) * (sin th2)))) - (((sin th3) * (((sin th1) * (cos th2)) + ((cos th1) * (sin th2)))) / ((sin th3) * ((sin th1) * (sin th2))))) / ((sin ((th1 + th2) + th3)) / (((sin th1) * (sin th2)) * (sin th3))) by XCMPLX_1:120
.= (((cot th3) * ((((cos th1) * (cos th2)) - ((sin th1) * (sin th2))) / ((sin th1) * (sin th2)))) - (((sin th3) * (((sin th1) * (cos th2)) + ((cos th1) * (sin th2)))) / ((sin th3) * ((sin th1) * (sin th2))))) / ((sin ((th1 + th2) + th3)) / (((sin th1) * (sin th2)) * (sin th3))) by XCMPLX_1:76
.= (((cot th3) * ((((cos th1) * (cos th2)) / ((sin th1) * (sin th2))) - (((sin th1) * (sin th2)) / ((sin th1) * (sin th2))))) - (((sin th3) * (((sin th1) * (cos th2)) + ((cos th1) * (sin th2)))) / ((sin th3) * ((sin th1) * (sin th2))))) / ((sin ((th1 + th2) + th3)) / (((sin th1) * (sin th2)) * (sin th3))) by XCMPLX_1:120
.= (((cot th3) * (((cot th1) * ((cos th2) / (sin th2))) - (((sin th1) * (sin th2)) / ((sin th1) * (sin th2))))) - (((sin th3) * (((sin th1) * (cos th2)) + ((cos th1) * (sin th2)))) / ((sin th3) * ((sin th1) * (sin th2))))) / ((sin ((th1 + th2) + th3)) / (((sin th1) * (sin th2)) * (sin th3))) by XCMPLX_1:76
.= (((cot th3) * (((cot th1) * (cot th2)) - 1)) - (((((sin th1) * (cos th2)) + ((cos th1) * (sin th2))) * (sin th3)) / (((sin th1) * (sin th2)) * (sin th3)))) / ((sin ((th1 + th2) + th3)) / (((sin th1) * (sin th2)) * (sin th3))) by A1, A2, XCMPLX_1:6, XCMPLX_1:60
.= (((cot th3) * (((cot th1) * (cot th2)) - 1)) - ((((sin th1) * (cos th2)) + ((cos th1) * (sin th2))) / ((sin th1) * (sin th2)))) / ((sin ((th1 + th2) + th3)) / (((sin th1) * (sin th2)) * (sin th3))) by A3, XCMPLX_1:91
.= (((cot th3) * (((cot th1) * (cot th2)) - 1)) - ((((sin th1) * (cos th2)) / ((sin th1) * (sin th2))) + (((cos th1) * (sin th2)) / ((sin th1) * (sin th2))))) / ((sin ((th1 + th2) + th3)) / (((sin th1) * (sin th2)) * (sin th3))) by XCMPLX_1:62
.= (((cot th3) * (((cot th1) * (cot th2)) - 1)) - (((cos th2) / (sin th2)) + (((cos th1) * (sin th2)) / ((sin th1) * (sin th2))))) / ((sin ((th1 + th2) + th3)) / (((sin th1) * (sin th2)) * (sin th3))) by A1, XCMPLX_1:91
.= (((cot th3) * (((cot th1) * (cot th2)) - 1)) - ((cot th2) + ((cos th1) / (sin th1)))) / ((sin ((th1 + th2) + th3)) / (((sin th1) * (sin th2)) * (sin th3))) by A2, XCMPLX_1:91
.= ((((((cot th1) * (cot th2)) * (cot th3)) - (cot th1)) - (cot th2)) - (cot th3)) / ((((sin (th1 + th2)) * (cos th3)) + ((cos (th1 + th2)) * (sin th3))) / (((sin th1) * (sin th2)) * (sin th3))) by SIN_COS:75
.= ((((((cot th1) * (cot th2)) * (cot th3)) - (cot th1)) - (cot th2)) - (cot th3)) / ((((sin (th1 + th2)) * (cos th3)) / (((sin th1) * (sin th2)) * (sin th3))) + (((cos (th1 + th2)) * (sin th3)) / (((sin th1) * (sin th2)) * (sin th3)))) by XCMPLX_1:62
.= ((((((cot th1) * (cot th2)) * (cot th3)) - (cot th1)) - (cot th2)) - (cot th3)) / ((((sin (th1 + th2)) * (cos th3)) / (((sin th1) * (sin th2)) * (sin th3))) + ((cos (th1 + th2)) / ((sin th1) * (sin th2)))) by A3, XCMPLX_1:91
.= ((((((cot th1) * (cot th2)) * (cot th3)) - (cot th1)) - (cot th2)) - (cot th3)) / (((cot th3) * ((sin (th1 + th2)) / ((sin th1) * (sin th2)))) + ((cos (th1 + th2)) / ((sin th1) * (sin th2)))) by XCMPLX_1:76
.= ((((((cot th1) * (cot th2)) * (cot th3)) - (cot th1)) - (cot th2)) - (cot th3)) / (((cot th3) * ((((sin th1) * (cos th2)) + ((cos th1) * (sin th2))) / ((sin th1) * (sin th2)))) + ((cos (th1 + th2)) / ((sin th1) * (sin th2)))) by SIN_COS:75
.= ((((((cot th1) * (cot th2)) * (cot th3)) - (cot th1)) - (cot th2)) - (cot th3)) / (((cot th3) * ((((sin th1) * (cos th2)) / ((sin th1) * (sin th2))) + (((cos th1) * (sin th2)) / ((sin th1) * (sin th2))))) + ((cos (th1 + th2)) / ((sin th1) * (sin th2)))) by XCMPLX_1:62
.= ((((((cot th1) * (cot th2)) * (cot th3)) - (cot th1)) - (cot th2)) - (cot th3)) / (((cot th3) * (((cos th2) / (sin th2)) + (((cos th1) * (sin th2)) / ((sin th1) * (sin th2))))) + ((cos (th1 + th2)) / ((sin th1) * (sin th2)))) by A1, XCMPLX_1:91
.= ((((((cot th1) * (cot th2)) * (cot th3)) - (cot th1)) - (cot th2)) - (cot th3)) / (((cot th3) * ((cot th2) + ((cos th1) / (sin th1)))) + ((cos (th1 + th2)) / ((sin th1) * (sin th2)))) by A2, XCMPLX_1:91
.= ((((((cot th1) * (cot th2)) * (cot th3)) - (cot th1)) - (cot th2)) - (cot th3)) / (((cot th3) * ((cot th2) + (cot th1))) + ((((cos th1) * (cos th2)) - ((sin th1) * (sin th2))) / ((sin th1) * (sin th2)))) by SIN_COS:75
.= ((((((cot th1) * (cot th2)) * (cot th3)) - (cot th1)) - (cot th2)) - (cot th3)) / (((cot th3) * ((cot th2) + (cot th1))) + ((((cos th1) * (cos th2)) / ((sin th1) * (sin th2))) - (((sin th1) * (sin th2)) / ((sin th1) * (sin th2))))) by XCMPLX_1:120
.= ((((((cot th1) * (cot th2)) * (cot th3)) - (cot th1)) - (cot th2)) - (cot th3)) / (((cot th3) * ((cot th2) + (cot th1))) + ((((cos th1) * (cos th2)) / ((sin th1) * (sin th2))) - 1)) by A1, A2, XCMPLX_1:6, XCMPLX_1:60
.= ((((((cot th1) * (cot th2)) * (cot th3)) - (cot th1)) - (cot th2)) - (cot th3)) / (((cot th3) * ((cot th2) + (cot th1))) + (((cot th1) * ((cos th2) / (sin th2))) - 1)) by XCMPLX_1:76
.= ((((((cot th1) * (cot th2)) * (cot th3)) - (cot th1)) - (cot th2)) - (cot th3)) / (((((cot th2) * (cot th3)) + ((cot th3) * (cot th1))) + ((cot th1) * (cot th2))) - 1) ;
hence  cot ((th1 + th2) + th3) = ((((((cot th1) * (cot th2)) * (cot th3)) - (cot th1)) - (cot th2)) - (cot th3)) / (((((cot th2) * (cot th3)) + ((cot th3) * (cot th1))) + ((cot th1) * (cot th2))) - 1) ; ::_thesis: verum
end;

theorem Th15: :: SIN_COS4:15
for th1, th2 being real number holds (sin th1) + (sin th2) = 2 * ((cos ((th1 - th2) / 2)) * (sin ((th1 + th2) / 2)))
proof
let th1, th2 be real number ; ::_thesis: (sin th1) + (sin th2) = 2 * ((cos ((th1 - th2) / 2)) * (sin ((th1 + th2) / 2)))
(sin th1) + (sin th2) = (sin ((th1 / 2) + (th1 / 2))) + (sin ((th2 / 2) + (th2 / 2)))
.= (((sin (th1 / 2)) * (cos (th1 / 2))) + ((cos (th1 / 2)) * (sin (th1 / 2)))) + (sin ((th2 / 2) + (th2 / 2))) by SIN_COS:75
.= (2 * ((sin (th1 / 2)) * (cos (th1 / 2)))) + (((sin (th2 / 2)) * (cos (th2 / 2))) + ((sin (th2 / 2)) * (cos (th2 / 2)))) by SIN_COS:75
.= 2 * ((((sin (th1 / 2)) * (cos (th1 / 2))) * 1) + ((sin (th2 / 2)) * (cos (th2 / 2))))
.= 2 * ((((sin (th1 / 2)) * (cos (th1 / 2))) * (((cos (th2 / 2)) * (cos (th2 / 2))) + ((sin (th2 / 2)) * (sin (th2 / 2))))) + (((sin (th2 / 2)) * (cos (th2 / 2))) * 1)) by SIN_COS:29
.= 2 * (((((sin (th1 / 2)) * (cos (th1 / 2))) * ((cos (th2 / 2)) * (cos (th2 / 2)))) + (((sin (th1 / 2)) * (cos (th1 / 2))) * ((sin (th2 / 2)) * (sin (th2 / 2))))) + (((sin (th2 / 2)) * (cos (th2 / 2))) * (((cos (th1 / 2)) * (cos (th1 / 2))) + ((sin (th1 / 2)) * (sin (th1 / 2)))))) by SIN_COS:29
.= 2 * ((((sin (th1 / 2)) * (cos (th2 / 2))) + ((cos (th1 / 2)) * (sin (th2 / 2)))) * (((cos (th1 / 2)) * (cos (th2 / 2))) + ((sin (th1 / 2)) * (sin (th2 / 2)))))
.= 2 * ((sin ((th1 / 2) + (th2 / 2))) * (((cos (th1 / 2)) * (cos (th2 / 2))) + ((sin (th1 / 2)) * (sin (th2 / 2))))) by SIN_COS:75
.= 2 * ((cos ((th1 / 2) - (th2 / 2))) * (sin ((th1 + th2) / 2))) by SIN_COS:83
.= 2 * ((cos ((th1 - th2) / 2)) * (sin ((th1 + th2) / 2))) ;
hence  (sin th1) + (sin th2) = 2 * ((cos ((th1 - th2) / 2)) * (sin ((th1 + th2) / 2))) ; ::_thesis: verum
end;

theorem Th16: :: SIN_COS4:16
for th1, th2 being real number holds (sin th1) - (sin th2) = 2 * ((cos ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2)))
proof
let th1, th2 be real number ; ::_thesis: (sin th1) - (sin th2) = 2 * ((cos ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2)))
(sin th1) - (sin th2) = (sin ((th1 / 2) + (th1 / 2))) - (sin ((th2 / 2) + (th2 / 2)))
.= (((sin (th1 / 2)) * (cos (th1 / 2))) + ((cos (th1 / 2)) * (sin (th1 / 2)))) - (sin ((th2 / 2) + (th2 / 2))) by SIN_COS:75
.= (2 * ((sin (th1 / 2)) * (cos (th1 / 2)))) - (((sin (th2 / 2)) * (cos (th2 / 2))) + ((sin (th2 / 2)) * (cos (th2 / 2)))) by SIN_COS:75
.= 2 * ((((sin (th1 / 2)) * (cos (th1 / 2))) * 1) - ((sin (th2 / 2)) * (cos (th2 / 2))))
.= 2 * ((((sin (th1 / 2)) * (cos (th1 / 2))) * (((cos (th2 / 2)) * (cos (th2 / 2))) + ((sin (th2 / 2)) * (sin (th2 / 2))))) - (((sin (th2 / 2)) * (cos (th2 / 2))) * 1)) by SIN_COS:29
.= 2 * (((((sin (th1 / 2)) * (cos (th1 / 2))) * ((cos (th2 / 2)) * (cos (th2 / 2)))) + (((sin (th1 / 2)) * (cos (th1 / 2))) * ((sin (th2 / 2)) * (sin (th2 / 2))))) - (((sin (th2 / 2)) * (cos (th2 / 2))) * (((cos (th1 / 2)) * (cos (th1 / 2))) + ((sin (th1 / 2)) * (sin (th1 / 2)))))) by SIN_COS:29
.= 2 * ((((sin (th1 / 2)) * (cos (th2 / 2))) - ((cos (th1 / 2)) * (sin (th2 / 2)))) * (((cos (th1 / 2)) * (cos (th2 / 2))) + (- ((sin (th1 / 2)) * (sin (th2 / 2))))))
.= 2 * ((sin ((th1 / 2) - (th2 / 2))) * (((cos (th1 / 2)) * (cos (th2 / 2))) - ((sin (th1 / 2)) * (sin (th2 / 2))))) by SIN_COS:82
.= 2 * ((sin ((th1 - th2) / 2)) * (cos ((th1 / 2) + (th2 / 2)))) by SIN_COS:75
.= 2 * ((cos ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2))) ;
hence  (sin th1) - (sin th2) = 2 * ((cos ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2))) ; ::_thesis: verum
end;

theorem Th17: :: SIN_COS4:17
for th1, th2 being real number holds (cos th1) + (cos th2) = 2 * ((cos ((th1 + th2) / 2)) * (cos ((th1 - th2) / 2)))
proof
let th1, th2 be real number ; ::_thesis: (cos th1) + (cos th2) = 2 * ((cos ((th1 + th2) / 2)) * (cos ((th1 - th2) / 2)))
(cos th1) + (cos th2) = (cos ((th1 / 2) + (th1 / 2))) + (cos ((th2 / 2) + (th2 / 2)))
.= (((cos (th1 / 2)) * (cos (th1 / 2))) - ((sin (th1 / 2)) * (sin (th1 / 2)))) + (cos ((th2 / 2) + (th2 / 2))) by SIN_COS:75
.= ((((cos (th1 / 2)) * (cos (th1 / 2))) + (- ((sin (th1 / 2)) * (sin (th1 / 2))))) + (1 + (- 1))) + (((cos (th2 / 2)) * (cos (th2 / 2))) - ((sin (th2 / 2)) * (sin (th2 / 2)))) by SIN_COS:75
.= ((((cos (th1 / 2)) * (cos (th1 / 2))) + (- ((sin (th1 / 2)) * (sin (th1 / 2))))) + 1) + ((- 1) + (((cos (th2 / 2)) * (cos (th2 / 2))) - ((sin (th2 / 2)) * (sin (th2 / 2)))))
.= ((((cos (th1 / 2)) * (cos (th1 / 2))) + (- ((sin (th1 / 2)) * (sin (th1 / 2))))) + (((sin (th1 / 2)) * (sin (th1 / 2))) + ((cos (th1 / 2)) * (cos (th1 / 2))))) + ((- 1) + (((cos (th2 / 2)) * (cos (th2 / 2))) - ((sin (th2 / 2)) * (sin (th2 / 2))))) by SIN_COS:29
.= (((cos (th1 / 2)) * (cos (th1 / 2))) + ((((sin (th1 / 2)) * (sin (th1 / 2))) - (- (- ((sin (th1 / 2)) * (sin (th1 / 2)))))) + ((cos (th1 / 2)) * (cos (th1 / 2))))) + ((- (((sin (th2 / 2)) * (sin (th2 / 2))) + ((cos (th2 / 2)) * (cos (th2 / 2))))) + (((cos (th2 / 2)) * (cos (th2 / 2))) - ((sin (th2 / 2)) * (sin (th2 / 2))))) by SIN_COS:29
.= 2 * (((cos (th1 / 2)) * (cos (th1 / 2))) - (((sin (th2 / 2)) * (sin (th2 / 2))) * 1))
.= 2 * (((cos (th1 / 2)) * (cos (th1 / 2))) - (((sin (th2 / 2)) * (sin (th2 / 2))) * (((cos (th1 / 2)) * (cos (th1 / 2))) + ((sin (th1 / 2)) * (sin (th1 / 2)))))) by SIN_COS:29
.= 2 * ((((cos (th1 / 2)) * (cos (th1 / 2))) * (1 - (- (- ((sin (th2 / 2)) * (sin (th2 / 2))))))) + (- (((sin (th2 / 2)) * (sin (th2 / 2))) * ((sin (th1 / 2)) * (sin (th1 / 2))))))
.= 2 * ((((cos (th1 / 2)) * (cos (th1 / 2))) * ((((cos (th2 / 2)) * (cos (th2 / 2))) + ((sin (th2 / 2)) * (sin (th2 / 2)))) - (- (- ((sin (th2 / 2)) * (sin (th2 / 2))))))) + (- (((sin (th2 / 2)) * (sin (th2 / 2))) * ((sin (th1 / 2)) * (sin (th1 / 2)))))) by SIN_COS:29
.= 2 * ((((cos (th1 / 2)) * (cos (th2 / 2))) + ((sin (th1 / 2)) * (sin (th2 / 2)))) * (((cos (th1 / 2)) * (cos (th2 / 2))) + (- ((sin (th1 / 2)) * (sin (th2 / 2))))))
.= 2 * ((cos ((th1 / 2) - (th2 / 2))) * (((cos (th1 / 2)) * (cos (th2 / 2))) - ((sin (th1 / 2)) * (sin (th2 / 2))))) by SIN_COS:83
.= 2 * ((cos ((th1 - th2) / 2)) * (cos ((th1 / 2) + (th2 / 2)))) by SIN_COS:75
.= 2 * ((cos ((th1 + th2) / 2)) * (cos ((th1 - th2) / 2))) ;
hence  (cos th1) + (cos th2) = 2 * ((cos ((th1 + th2) / 2)) * (cos ((th1 - th2) / 2))) ; ::_thesis: verum
end;

theorem Th18: :: SIN_COS4:18
for th1, th2 being real number holds (cos th1) - (cos th2) = - (2 * ((sin ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2))))
proof
let th1, th2 be real number ; ::_thesis: (cos th1) - (cos th2) = - (2 * ((sin ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2))))
(cos th1) - (cos th2) = (cos ((th1 / 2) + (th1 / 2))) - (cos ((th2 / 2) + (th2 / 2)))
.= (((cos (th1 / 2)) * (cos (th1 / 2))) - ((sin (th1 / 2)) * (sin (th1 / 2)))) - (cos ((th2 / 2) + (th2 / 2))) by SIN_COS:75
.= ((((cos (th1 / 2)) * (cos (th1 / 2))) + (- ((sin (th1 / 2)) * (sin (th1 / 2))))) + (1 + (- 1))) - (((cos (th2 / 2)) * (cos (th2 / 2))) - ((sin (th2 / 2)) * (sin (th2 / 2)))) by SIN_COS:75
.= ((((cos (th1 / 2)) * (cos (th1 / 2))) + (- ((sin (th1 / 2)) * (sin (th1 / 2))))) + 1) + ((- 1) + ((- ((cos (th2 / 2)) * (cos (th2 / 2)))) + ((sin (th2 / 2)) * (sin (th2 / 2)))))
.= ((((cos (th1 / 2)) * (cos (th1 / 2))) + (- ((sin (th1 / 2)) * (sin (th1 / 2))))) + (((sin (th1 / 2)) * (sin (th1 / 2))) + ((cos (th1 / 2)) * (cos (th1 / 2))))) + ((- 1) + ((- ((cos (th2 / 2)) * (cos (th2 / 2)))) + ((sin (th2 / 2)) * (sin (th2 / 2))))) by SIN_COS:29
.= (((cos (th1 / 2)) * (cos (th1 / 2))) + ((((sin (th1 / 2)) * (sin (th1 / 2))) - (- (- ((sin (th1 / 2)) * (sin (th1 / 2)))))) + ((cos (th1 / 2)) * (cos (th1 / 2))))) + ((- (((sin (th2 / 2)) * (sin (th2 / 2))) + ((cos (th2 / 2)) * (cos (th2 / 2))))) + ((- ((cos (th2 / 2)) * (cos (th2 / 2)))) + ((sin (th2 / 2)) * (sin (th2 / 2))))) by SIN_COS:29
.= 2 * ((((cos (th1 / 2)) * (cos (th1 / 2))) * 1) - ((cos (th2 / 2)) * (cos (th2 / 2))))
.= 2 * ((((cos (th1 / 2)) * (cos (th1 / 2))) * (((sin (th2 / 2)) * (sin (th2 / 2))) + ((cos (th2 / 2)) * (cos (th2 / 2))))) - ((cos (th2 / 2)) * (cos (th2 / 2)))) by SIN_COS:29
.= 2 * ((((cos (th1 / 2)) * (cos (th1 / 2))) * ((sin (th2 / 2)) * (sin (th2 / 2)))) + (((cos (th2 / 2)) * (cos (th2 / 2))) * (((cos (th1 / 2)) * (cos (th1 / 2))) - (- (- 1)))))
.= 2 * ((((cos (th1 / 2)) * (cos (th1 / 2))) * ((sin (th2 / 2)) * (sin (th2 / 2)))) + (((cos (th2 / 2)) * (cos (th2 / 2))) * (((cos (th1 / 2)) * (cos (th1 / 2))) - (- (- (((cos (th1 / 2)) * (cos (th1 / 2))) + ((sin (th1 / 2)) * (sin (th1 / 2))))))))) by SIN_COS:29
.= - (2 * ((((sin (th1 / 2)) * (cos (th2 / 2))) - (- (- ((cos (th1 / 2)) * (sin (th2 / 2)))))) * (((sin (th1 / 2)) * (cos (th2 / 2))) + ((cos (th1 / 2)) * (sin (th2 / 2))))))
.= - (2 * ((sin ((th1 / 2) + (th2 / 2))) * (((sin (th1 / 2)) * (cos (th2 / 2))) - ((cos (th1 / 2)) * (sin (th2 / 2)))))) by SIN_COS:75
.= - (2 * ((sin ((th1 + th2) / 2)) * (sin ((th1 / 2) - (th2 / 2))))) by SIN_COS:82
.= - (2 * ((sin ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2)))) ;
hence  (cos th1) - (cos th2) = - (2 * ((sin ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2)))) ; ::_thesis: verum
end;

theorem :: SIN_COS4:19
for th1, th2 being real number st cos th1 <> 0 & cos th2 <> 0 holds
(tan th1) + (tan th2) = (sin (th1 + th2)) / ((cos th1) * (cos th2))
proof
let th1, th2 be real number ; ::_thesis: ( cos th1 <> 0 & cos th2 <> 0 implies (tan th1) + (tan th2) = (sin (th1 + th2)) / ((cos th1) * (cos th2)) )
assume  ( cos th1 <> 0 & cos th2 <> 0 ) ; ::_thesis: (tan th1) + (tan th2) = (sin (th1 + th2)) / ((cos th1) * (cos th2))
then (tan th1) + (tan th2) = (((sin th1) * (cos th2)) + ((sin th2) * (cos th1))) / ((cos th1) * (cos th2)) by XCMPLX_1:116
.= (sin (th1 + th2)) / ((cos th1) * (cos th2)) by SIN_COS:75 ;
hence  (tan th1) + (tan th2) = (sin (th1 + th2)) / ((cos th1) * (cos th2)) ; ::_thesis: verum
end;

theorem :: SIN_COS4:20
for th1, th2 being real number st cos th1 <> 0 & cos th2 <> 0 holds
(tan th1) - (tan th2) = (sin (th1 - th2)) / ((cos th1) * (cos th2))
proof
let th1, th2 be real number ; ::_thesis: ( cos th1 <> 0 & cos th2 <> 0 implies (tan th1) - (tan th2) = (sin (th1 - th2)) / ((cos th1) * (cos th2)) )
assume  ( cos th1 <> 0 & cos th2 <> 0 ) ; ::_thesis: (tan th1) - (tan th2) = (sin (th1 - th2)) / ((cos th1) * (cos th2))
then (tan th1) - (tan th2) = (((sin th1) * (cos th2)) - ((sin th2) * (cos th1))) / ((cos th1) * (cos th2)) by XCMPLX_1:130
.= (sin (th1 - th2)) / ((cos th1) * (cos th2)) by SIN_COS:82 ;
hence  (tan th1) - (tan th2) = (sin (th1 - th2)) / ((cos th1) * (cos th2)) ; ::_thesis: verum
end;

theorem :: SIN_COS4:21
for th1, th2 being real number st cos th1 <> 0 & sin th2 <> 0 holds
(tan th1) + (cot th2) = (cos (th1 - th2)) / ((cos th1) * (sin th2))
proof
let th1, th2 be real number ; ::_thesis: ( cos th1 <> 0 & sin th2 <> 0 implies (tan th1) + (cot th2) = (cos (th1 - th2)) / ((cos th1) * (sin th2)) )
assume  ( cos th1 <> 0 & sin th2 <> 0 ) ; ::_thesis: (tan th1) + (cot th2) = (cos (th1 - th2)) / ((cos th1) * (sin th2))
then (tan th1) + (cot th2) = (((cos th1) * (cos th2)) + ((sin th1) * (sin th2))) / ((cos th1) * (sin th2)) by XCMPLX_1:116
.= (cos (th1 - th2)) / ((cos th1) * (sin th2)) by SIN_COS:83 ;
hence  (tan th1) + (cot th2) = (cos (th1 - th2)) / ((cos th1) * (sin th2)) ; ::_thesis: verum
end;

theorem :: SIN_COS4:22
for th1, th2 being real number st cos th1 <> 0 & sin th2 <> 0 holds
(tan th1) - (cot th2) = - ((cos (th1 + th2)) / ((cos th1) * (sin th2)))
proof
let th1, th2 be real number ; ::_thesis: ( cos th1 <> 0 & sin th2 <> 0 implies (tan th1) - (cot th2) = - ((cos (th1 + th2)) / ((cos th1) * (sin th2))) )
assume  ( cos th1 <> 0 & sin th2 <> 0 ) ; ::_thesis: (tan th1) - (cot th2) = - ((cos (th1 + th2)) / ((cos th1) * (sin th2)))
then (tan th1) - (cot th2) = (((sin th1) * (sin th2)) - (- (- ((cos th1) * (cos th2))))) / ((cos th1) * (sin th2)) by XCMPLX_1:130
.= (- (((cos th1) * (cos th2)) - ((sin th1) * (sin th2)))) / ((cos th1) * (sin th2))
.= - ((((cos th1) * (cos th2)) - ((sin th1) * (sin th2))) / ((cos th1) * (sin th2))) by XCMPLX_1:187
.= - ((cos (th1 + th2)) / ((cos th1) * (sin th2))) by SIN_COS:75 ;
hence  (tan th1) - (cot th2) = - ((cos (th1 + th2)) / ((cos th1) * (sin th2))) ; ::_thesis: verum
end;

theorem :: SIN_COS4:23
for th1, th2 being real number st sin th1 <> 0 & sin th2 <> 0 holds
(cot th1) + (cot th2) = (sin (th1 + th2)) / ((sin th1) * (sin th2))
proof
let th1, th2 be real number ; ::_thesis: ( sin th1 <> 0 & sin th2 <> 0 implies (cot th1) + (cot th2) = (sin (th1 + th2)) / ((sin th1) * (sin th2)) )
assume  ( sin th1 <> 0 & sin th2 <> 0 ) ; ::_thesis: (cot th1) + (cot th2) = (sin (th1 + th2)) / ((sin th1) * (sin th2))
then (cot th1) + (cot th2) = (((cos th1) * (sin th2)) + ((cos th2) * (sin th1))) / ((sin th1) * (sin th2)) by XCMPLX_1:116
.= (sin (th1 + th2)) / ((sin th1) * (sin th2)) by SIN_COS:75 ;
hence  (cot th1) + (cot th2) = (sin (th1 + th2)) / ((sin th1) * (sin th2)) ; ::_thesis: verum
end;

theorem :: SIN_COS4:24
for th1, th2 being real number st sin th1 <> 0 & sin th2 <> 0 holds
(cot th1) - (cot th2) = - ((sin (th1 - th2)) / ((sin th1) * (sin th2)))
proof
let th1, th2 be real number ; ::_thesis: ( sin th1 <> 0 & sin th2 <> 0 implies (cot th1) - (cot th2) = - ((sin (th1 - th2)) / ((sin th1) * (sin th2))) )
assume  ( sin th1 <> 0 & sin th2 <> 0 ) ; ::_thesis: (cot th1) - (cot th2) = - ((sin (th1 - th2)) / ((sin th1) * (sin th2)))
then (cot th1) - (cot th2) = (((cos th1) * (sin th2)) - (- (- ((cos th2) * (sin th1))))) / ((sin th1) * (sin th2)) by XCMPLX_1:130
.= (- (((sin th1) * (cos th2)) - ((cos th1) * (sin th2)))) / ((sin th1) * (sin th2))
.= (- (sin (th1 - th2))) / ((sin th1) * (sin th2)) by SIN_COS:82
.= - ((sin (th1 - th2)) / ((sin th1) * (sin th2))) by XCMPLX_1:187 ;
hence  (cot th1) - (cot th2) = - ((sin (th1 - th2)) / ((sin th1) * (sin th2))) ; ::_thesis: verum
end;

theorem :: SIN_COS4:25
for th1, th2 being real number holds (sin (th1 + th2)) + (sin (th1 - th2)) = 2 * ((sin th1) * (cos th2))
proof
let th1, th2 be real number ; ::_thesis: (sin (th1 + th2)) + (sin (th1 - th2)) = 2 * ((sin th1) * (cos th2))
(sin (th1 + th2)) + (sin (th1 - th2)) = (((sin th1) * (cos th2)) + ((cos th1) * (sin th2))) + (sin (th1 - th2)) by SIN_COS:75
.= (((sin th1) * (cos th2)) + ((cos th1) * (sin th2))) + (((sin th1) * (cos th2)) - (- (- ((cos th1) * (sin th2))))) by SIN_COS:82
.= 2 * ((sin th1) * (cos th2)) ;
hence  (sin (th1 + th2)) + (sin (th1 - th2)) = 2 * ((sin th1) * (cos th2)) ; ::_thesis: verum
end;

theorem :: SIN_COS4:26
for th1, th2 being real number holds (sin (th1 + th2)) - (sin (th1 - th2)) = 2 * ((cos th1) * (sin th2))
proof
let th1, th2 be real number ; ::_thesis: (sin (th1 + th2)) - (sin (th1 - th2)) = 2 * ((cos th1) * (sin th2))
(sin (th1 + th2)) - (sin (th1 - th2)) = (((sin th1) * (cos th2)) + ((cos th1) * (sin th2))) - (sin (th1 - th2)) by SIN_COS:75
.= (((sin th1) * (cos th2)) + ((cos th1) * (sin th2))) - (- (- (((sin th1) * (cos th2)) - ((cos th1) * (sin th2))))) by SIN_COS:82
.= 2 * ((cos th1) * (sin th2)) ;
hence  (sin (th1 + th2)) - (sin (th1 - th2)) = 2 * ((cos th1) * (sin th2)) ; ::_thesis: verum
end;

theorem :: SIN_COS4:27
for th1, th2 being real number holds (cos (th1 + th2)) + (cos (th1 - th2)) = 2 * ((cos th1) * (cos th2))
proof
let th1, th2 be real number ; ::_thesis: (cos (th1 + th2)) + (cos (th1 - th2)) = 2 * ((cos th1) * (cos th2))
(cos (th1 + th2)) + (cos (th1 - th2)) = (((cos th1) * (cos th2)) - ((sin th1) * (sin th2))) + (cos (th1 - th2)) by SIN_COS:75
.= (((cos th1) * (cos th2)) + (- ((sin th1) * (sin th2)))) + (((sin th1) * (sin th2)) + ((cos th1) * (cos th2))) by SIN_COS:83
.= 2 * ((cos th1) * (cos th2)) ;
hence  (cos (th1 + th2)) + (cos (th1 - th2)) = 2 * ((cos th1) * (cos th2)) ; ::_thesis: verum
end;

theorem :: SIN_COS4:28
for th1, th2 being real number holds (cos (th1 + th2)) - (cos (th1 - th2)) = - (2 * ((sin th1) * (sin th2)))
proof
let th1, th2 be real number ; ::_thesis: (cos (th1 + th2)) - (cos (th1 - th2)) = - (2 * ((sin th1) * (sin th2)))
(cos (th1 + th2)) - (cos (th1 - th2)) = (((cos th1) * (cos th2)) - ((sin th1) * (sin th2))) - (cos (th1 - th2)) by SIN_COS:75
.= (((cos th1) * (cos th2)) + (- ((sin th1) * (sin th2)))) - (((cos th1) * (cos th2)) + ((sin th1) * (sin th2))) by SIN_COS:83
.= - (2 * ((sin th1) * (sin th2))) ;
hence  (cos (th1 + th2)) - (cos (th1 - th2)) = - (2 * ((sin th1) * (sin th2))) ; ::_thesis: verum
end;

theorem Th29: :: SIN_COS4:29
for th1, th2 being real number holds (sin th1) * (sin th2) = - ((1 / 2) * ((cos (th1 + th2)) - (cos (th1 - th2))))
proof
let th1, th2 be real number ; ::_thesis: (sin th1) * (sin th2) = - ((1 / 2) * ((cos (th1 + th2)) - (cos (th1 - th2))))
(sin th1) * (sin th2) = (((((cos th1) * (cos th2)) + ((sin th1) * (sin th2))) - ((cos th1) * (cos th2))) + ((sin th1) * (sin th2))) / 2
.= (((((cos th1) * (cos (- th2))) + ((sin th1) * (sin th2))) - ((cos th1) * (cos th2))) + ((sin th1) * (sin th2))) / 2 by SIN_COS:31
.= (((((cos th1) * (cos (- th2))) - ((sin th1) * (- (sin th2)))) - ((cos th1) * (cos th2))) + ((sin th1) * (sin th2))) / 2
.= (((((cos th1) * (cos (- th2))) - ((sin th1) * (sin (- th2)))) - ((cos th1) * (cos th2))) + ((sin th1) * (sin th2))) / 2 by SIN_COS:31
.= (((cos (th1 + (- th2))) - ((cos th1) * (cos th2))) + ((sin th1) * (sin th2))) / 2 by SIN_COS:75
.= ((cos (th1 - th2)) - (((cos th1) * (cos th2)) - ((sin th1) * (sin th2)))) / 2
.= ((cos (th1 - th2)) - (cos (th1 + th2))) / (2 / 1) by SIN_COS:75
.= - ((1 / 2) * ((cos (th1 + th2)) - (cos (th1 - th2)))) ;
hence  (sin th1) * (sin th2) = - ((1 / 2) * ((cos (th1 + th2)) - (cos (th1 - th2)))) ; ::_thesis: verum
end;

theorem Th30: :: SIN_COS4:30
for th1, th2 being real number holds (sin th1) * (cos th2) = (1 / 2) * ((sin (th1 + th2)) + (sin (th1 - th2)))
proof
let th1, th2 be real number ; ::_thesis: (sin th1) * (cos th2) = (1 / 2) * ((sin (th1 + th2)) + (sin (th1 - th2)))
(sin th1) * (cos th2) = (1 / 2) * ((((sin th1) * (cos th2)) + ((cos th1) * (sin th2))) + (((sin th1) * (cos th2)) - ((cos th1) * (sin th2))))
.= (1 / 2) * ((sin (th1 + th2)) + (((sin th1) * (cos th2)) + ((cos th1) * (- (sin th2))))) by SIN_COS:75
.= (1 / 2) * ((sin (th1 + th2)) + (((sin th1) * (cos th2)) + ((cos th1) * (sin (- th2))))) by SIN_COS:31
.= (1 / 2) * ((sin (th1 + th2)) + (((sin th1) * (cos (- th2))) + ((cos th1) * (sin (- th2))))) by SIN_COS:31
.= (1 / 2) * ((sin (th1 + th2)) + (sin (th1 + (- th2)))) by SIN_COS:75
.= (1 / 2) * ((sin (th1 + th2)) + (sin (th1 - th2))) ;
hence  (sin th1) * (cos th2) = (1 / 2) * ((sin (th1 + th2)) + (sin (th1 - th2))) ; ::_thesis: verum
end;

theorem Th31: :: SIN_COS4:31
for th1, th2 being real number holds (cos th1) * (sin th2) = (1 / 2) * ((sin (th1 + th2)) - (sin (th1 - th2)))
proof
let th1, th2 be real number ; ::_thesis: (cos th1) * (sin th2) = (1 / 2) * ((sin (th1 + th2)) - (sin (th1 - th2)))
(cos th1) * (sin th2) = (1 / 2) * ((((sin th1) * (cos th2)) + ((cos th1) * (sin th2))) - (((sin th1) * (cos th2)) - ((cos th1) * (sin th2))))
.= (1 / 2) * ((sin (th1 + th2)) - (((sin th1) * (cos th2)) + ((cos th1) * (- (sin th2))))) by SIN_COS:75
.= (1 / 2) * ((sin (th1 + th2)) - (((sin th1) * (cos th2)) + ((cos th1) * (sin (- th2))))) by SIN_COS:31
.= (1 / 2) * ((sin (th1 + th2)) - (((sin th1) * (cos (- th2))) + ((cos th1) * (sin (- th2))))) by SIN_COS:31
.= (1 / 2) * ((sin (th1 + th2)) - (sin (th1 + (- th2)))) by SIN_COS:75
.= (1 / 2) * ((sin (th1 + th2)) - (sin (th1 - th2))) ;
hence  (cos th1) * (sin th2) = (1 / 2) * ((sin (th1 + th2)) - (sin (th1 - th2))) ; ::_thesis: verum
end;

theorem Th32: :: SIN_COS4:32
for th1, th2 being real number holds (cos th1) * (cos th2) = (1 / 2) * ((cos (th1 + th2)) + (cos (th1 - th2)))
proof
let th1, th2 be real number ; ::_thesis: (cos th1) * (cos th2) = (1 / 2) * ((cos (th1 + th2)) + (cos (th1 - th2)))
(cos th1) * (cos th2) = (1 / 2) * ((((cos th1) * (cos th2)) - ((sin th1) * (sin th2))) + (((cos th1) * (cos th2)) - (- ((sin th1) * (sin th2)))))
.= (1 / 2) * ((cos (th1 + th2)) + (((cos th1) * (cos th2)) - ((sin th1) * (- (sin th2))))) by SIN_COS:75
.= (1 / 2) * ((cos (th1 + th2)) + (((cos th1) * (cos th2)) - ((sin th1) * (sin (- th2))))) by SIN_COS:31
.= (1 / 2) * ((cos (th1 + th2)) + (((cos th1) * (cos (- th2))) - ((sin th1) * (sin (- th2))))) by SIN_COS:31
.= (1 / 2) * ((cos (th1 + th2)) + (cos (th1 + (- th2)))) by SIN_COS:75
.= (1 / 2) * ((cos (th1 + th2)) + (cos (th1 - th2))) ;
hence  (cos th1) * (cos th2) = (1 / 2) * ((cos (th1 + th2)) + (cos (th1 - th2))) ; ::_thesis: verum
end;

theorem :: SIN_COS4:33
for th1, th2, th3 being real number holds ((sin th1) * (sin th2)) * (sin th3) = (1 / 4) * ((((sin ((th1 + th2) - th3)) + (sin ((th2 + th3) - th1))) + (sin ((th3 + th1) - th2))) - (sin ((th1 + th2) + th3)))
proof
let th1, th2, th3 be real number ; ::_thesis: ((sin th1) * (sin th2)) * (sin th3) = (1 / 4) * ((((sin ((th1 + th2) - th3)) + (sin ((th2 + th3) - th1))) + (sin ((th3 + th1) - th2))) - (sin ((th1 + th2) + th3)))
((sin th1) * (sin th2)) * (sin th3) = (- ((1 / 2) * ((cos (th1 + th2)) - (cos (th1 - th2))))) * (sin th3) by Th29
.= (1 / 2) * (((cos (th1 - th2)) * (sin th3)) - ((cos (th1 + th2)) * (sin th3)))
.= (1 / 2) * (((1 / 2) * ((sin ((th1 - th2) + th3)) - (sin ((th1 - th2) - th3)))) - ((cos (th1 + th2)) * (sin th3))) by Th31
.= (1 / 2) * (((1 / 2) * ((sin ((th1 - th2) + th3)) - (sin ((th1 - th2) - th3)))) - ((1 / 2) * ((sin ((th1 + th2) + th3)) - (sin ((th1 + th2) - th3))))) by Th31
.= (1 / (2 * 2)) * (((sin ((th1 - th2) + th3)) + (- (sin ((th1 - th2) - th3)))) + ((sin ((th1 + th2) - th3)) - (sin ((th1 + th2) + th3))))
.= (1 / (2 * 2)) * (((sin ((th1 - th2) + th3)) + (sin (- ((th1 - th2) - th3)))) + ((sin ((th1 + th2) - th3)) - (sin ((th1 + th2) + th3)))) by SIN_COS:31
.= (1 / (2 * 2)) * ((((sin ((th1 + th2) - th3)) + (sin ((th2 + th3) - th1))) + (sin ((th3 + th1) - th2))) - (sin ((th1 + th2) + th3))) ;
hence  ((sin th1) * (sin th2)) * (sin th3) = (1 / 4) * ((((sin ((th1 + th2) - th3)) + (sin ((th2 + th3) - th1))) + (sin ((th3 + th1) - th2))) - (sin ((th1 + th2) + th3))) ; ::_thesis: verum
end;

theorem :: SIN_COS4:34
for th1, th2, th3 being real number holds ((sin th1) * (sin th2)) * (cos th3) = (1 / 4) * ((((- (cos ((th1 + th2) - th3))) + (cos ((th2 + th3) - th1))) + (cos ((th3 + th1) - th2))) - (cos ((th1 + th2) + th3)))
proof
let th1, th2, th3 be real number ; ::_thesis: ((sin th1) * (sin th2)) * (cos th3) = (1 / 4) * ((((- (cos ((th1 + th2) - th3))) + (cos ((th2 + th3) - th1))) + (cos ((th3 + th1) - th2))) - (cos ((th1 + th2) + th3)))
((sin th1) * (sin th2)) * (cos th3) = (- ((1 / 2) * ((cos (th1 + th2)) - (cos (th1 - th2))))) * (cos th3) by Th29
.= (1 / 2) * (((cos (th1 - th2)) * (cos th3)) - ((cos (th1 + th2)) * (cos th3)))
.= (1 / 2) * (((1 / 2) * ((cos ((th1 - th2) + th3)) + (cos ((th1 - th2) - th3)))) - ((cos (th1 + th2)) * (cos th3))) by Th32
.= (1 / 2) * (((1 / 2) * ((cos ((th1 - th2) + th3)) + (cos ((th1 - th2) - th3)))) - ((1 / 2) * ((cos ((th1 + th2) + th3)) + (cos ((th1 + th2) - th3))))) by Th32
.= (1 / (2 * 2)) * (((- (cos ((th1 + th2) - th3))) + (cos (- ((th2 - th1) + th3)))) + ((cos ((th3 + th1) + (- th2))) + (- (cos ((th1 + th2) + th3)))))
.= (1 / (2 * 2)) * (((- (cos ((th1 + th2) - th3))) + (cos ((th2 - th1) + th3))) + ((cos ((th3 + th1) + (- th2))) + (- (cos ((th1 + th2) + th3))))) by SIN_COS:31
.= (1 / (2 * 2)) * ((((- (cos ((th1 + th2) - th3))) + (cos ((th2 + th3) - th1))) + (cos ((th3 + th1) - th2))) - (cos ((th1 + th2) + th3))) ;
hence  ((sin th1) * (sin th2)) * (cos th3) = (1 / 4) * ((((- (cos ((th1 + th2) - th3))) + (cos ((th2 + th3) - th1))) + (cos ((th3 + th1) - th2))) - (cos ((th1 + th2) + th3))) ; ::_thesis: verum
end;

theorem :: SIN_COS4:35
for th1, th2, th3 being real number holds ((sin th1) * (cos th2)) * (cos th3) = (1 / 4) * ((((sin ((th1 + th2) - th3)) - (sin ((th2 + th3) - th1))) + (sin ((th3 + th1) - th2))) + (sin ((th1 + th2) + th3)))
proof
let th1, th2, th3 be real number ; ::_thesis: ((sin th1) * (cos th2)) * (cos th3) = (1 / 4) * ((((sin ((th1 + th2) - th3)) - (sin ((th2 + th3) - th1))) + (sin ((th3 + th1) - th2))) + (sin ((th1 + th2) + th3)))
((sin th1) * (cos th2)) * (cos th3) = ((1 / 2) * ((sin (th1 + th2)) + (sin (th1 - th2)))) * (cos th3) by Th30
.= (1 / 2) * (((sin (th1 + th2)) * (cos th3)) + ((sin (th1 - th2)) * (cos th3)))
.= (1 / 2) * (((1 / 2) * ((sin ((th1 + th2) + th3)) + (sin ((th1 + th2) - th3)))) + ((sin (th1 - th2)) * (cos th3))) by Th30
.= (1 / 2) * (((1 / 2) * ((sin ((th1 + th2) + th3)) + (sin ((th1 + th2) - th3)))) + ((1 / 2) * ((sin ((th1 - th2) + th3)) + (sin ((th1 - th2) - th3))))) by Th30
.= (1 / (2 * 2)) * (((sin ((th1 + th2) + th3)) + (sin ((th1 + th2) - th3))) + ((sin ((th1 + (- th2)) + th3)) + (sin (- ((th2 - th1) + th3)))))
.= (1 / (2 * 2)) * (((sin ((th1 + th2) + th3)) + (sin ((th1 + th2) - th3))) + ((- (sin ((th2 - th1) + th3))) + (sin ((th3 + th1) + (- th2))))) by SIN_COS:31
.= (1 / (2 * 2)) * ((((sin ((th1 + th2) - th3)) - (sin ((th2 + th3) - th1))) + (sin ((th3 + th1) - th2))) + (sin ((th1 + th2) + th3))) ;
hence  ((sin th1) * (cos th2)) * (cos th3) = (1 / 4) * ((((sin ((th1 + th2) - th3)) - (sin ((th2 + th3) - th1))) + (sin ((th3 + th1) - th2))) + (sin ((th1 + th2) + th3))) ; ::_thesis: verum
end;

theorem :: SIN_COS4:36
for th1, th2, th3 being real number holds ((cos th1) * (cos th2)) * (cos th3) = (1 / 4) * ((((cos ((th1 + th2) - th3)) + (cos ((th2 + th3) - th1))) + (cos ((th3 + th1) - th2))) + (cos ((th1 + th2) + th3)))
proof
let th1, th2, th3 be real number ; ::_thesis: ((cos th1) * (cos th2)) * (cos th3) = (1 / 4) * ((((cos ((th1 + th2) - th3)) + (cos ((th2 + th3) - th1))) + (cos ((th3 + th1) - th2))) + (cos ((th1 + th2) + th3)))
((cos th1) * (cos th2)) * (cos th3) = ((1 / 2) * ((cos (th1 + th2)) + (cos (th1 - th2)))) * (cos th3) by Th32
.= (1 / 2) * (((cos (th1 + th2)) * (cos th3)) + ((cos (th1 - th2)) * (cos th3)))
.= (1 / 2) * (((1 / 2) * ((cos ((th1 + th2) + th3)) + (cos ((th1 + th2) - th3)))) + ((cos (th1 - th2)) * (cos th3))) by Th32
.= (1 / 2) * (((1 / 2) * ((cos ((th1 + th2) + th3)) + (cos ((th1 + th2) - th3)))) + ((1 / 2) * ((cos ((th1 - th2) + th3)) + (cos ((th1 - th2) - th3))))) by Th32
.= (1 / (2 * 2)) * (((cos ((th1 + th2) + th3)) + (cos ((th1 + th2) - th3))) + ((cos ((th3 + th1) + (- th2))) + (cos (- ((th2 - th1) + th3)))))
.= (1 / (2 * 2)) * (((cos ((th1 + th2) + th3)) + (cos ((th1 + th2) - th3))) + ((cos ((th3 + th1) - th2)) + (cos ((th2 + th3) + (- th1))))) by SIN_COS:31
.= (1 / (2 * 2)) * ((((cos ((th1 + th2) - th3)) + (cos ((th2 + th3) - th1))) + (cos ((th3 + th1) - th2))) + (cos ((th1 + th2) + th3))) ;
hence  ((cos th1) * (cos th2)) * (cos th3) = (1 / 4) * ((((cos ((th1 + th2) - th3)) + (cos ((th2 + th3) - th1))) + (cos ((th3 + th1) - th2))) + (cos ((th1 + th2) + th3))) ; ::_thesis: verum
end;

theorem Th37: :: SIN_COS4:37
for th1, th2 being real number holds (sin (th1 + th2)) * (sin (th1 - th2)) = ((sin th1) * (sin th1)) - ((sin th2) * (sin th2))
proof
let th1, th2 be real number ; ::_thesis: (sin (th1 + th2)) * (sin (th1 - th2)) = ((sin th1) * (sin th1)) - ((sin th2) * (sin th2))
(sin (th1 + th2)) * (sin (th1 - th2)) = (((sin th1) * (cos th2)) + ((cos th1) * (sin th2))) * (sin (th1 - th2)) by SIN_COS:75
.= (((sin th1) * (cos th2)) + ((cos th1) * (sin th2))) * (((sin th1) * (cos th2)) - (- (- ((cos th1) * (sin th2))))) by SIN_COS:82
.= (((sin th1) * (sin th1)) * ((cos th2) * (cos th2))) - ((((cos th1) * (sin th2)) * (cos th1)) * (sin th2))
.= (((sin th1) * (sin th1)) * (1 - ((sin th2) * (sin th2)))) - ((((cos th1) * (cos th1)) * (sin th2)) * (sin th2)) by Th5
.= (((sin th1) * (sin th1)) * (1 + (- ((sin th2) * (sin th2))))) - (((1 - (- (- ((sin th1) * (sin th1))))) * (sin th2)) * (sin th2)) by Th5
.= ((sin th1) * (sin th1)) - ((sin th2) * (sin th2)) ;
hence  (sin (th1 + th2)) * (sin (th1 - th2)) = ((sin th1) * (sin th1)) - ((sin th2) * (sin th2)) ; ::_thesis: verum
end;

theorem :: SIN_COS4:38
for th1, th2 being real number holds (sin (th1 + th2)) * (sin (th1 - th2)) = ((cos th2) * (cos th2)) - ((cos th1) * (cos th1))
proof
let th1, th2 be real number ; ::_thesis: (sin (th1 + th2)) * (sin (th1 - th2)) = ((cos th2) * (cos th2)) - ((cos th1) * (cos th1))
(sin (th1 + th2)) * (sin (th1 - th2)) = ((sin th1) * (sin th1)) - ((sin th2) * (sin th2)) by Th37
.= (1 - ((cos th1) * (cos th1))) - ((sin th2) * (sin th2)) by Th4
.= (1 - (- (- ((cos th1) * (cos th1))))) - (- (- (1 - ((cos th2) * (cos th2))))) by Th4
.= ((cos th2) * (cos th2)) - ((cos th1) * (cos th1)) ;
hence  (sin (th1 + th2)) * (sin (th1 - th2)) = ((cos th2) * (cos th2)) - ((cos th1) * (cos th1)) ; ::_thesis: verum
end;

theorem Th39: :: SIN_COS4:39
for th1, th2 being real number holds (sin (th1 + th2)) * (cos (th1 - th2)) = ((sin th1) * (cos th1)) + ((sin th2) * (cos th2))
proof
let th1, th2 be real number ; ::_thesis: (sin (th1 + th2)) * (cos (th1 - th2)) = ((sin th1) * (cos th1)) + ((sin th2) * (cos th2))
(sin (th1 + th2)) * (cos (th1 - th2)) = (((sin th1) * (cos th2)) + ((cos th1) * (sin th2))) * (cos (th1 - th2)) by SIN_COS:75
.= (((sin th1) * (cos th2)) + ((cos th1) * (sin th2))) * (((cos th1) * (cos th2)) + ((sin th1) * (sin th2))) by SIN_COS:83
.= (((sin th1) * (cos th1)) * (((sin th2) * (sin th2)) + ((cos th2) * (cos th2)))) + ((((sin th2) * (cos th2)) * ((sin th1) * (sin th1))) + (((sin th2) * (cos th2)) * ((cos th1) * (cos th1))))
.= (((sin th1) * (cos th1)) * 1) + (((sin th2) * (cos th2)) * (((sin th1) * (sin th1)) + ((cos th1) * (cos th1)))) by SIN_COS:29
.= ((sin th1) * (cos th1)) + (((sin th2) * (cos th2)) * (1 / 1)) by SIN_COS:29
.= ((sin th1) * (cos th1)) + ((sin th2) * (cos th2)) ;
hence  (sin (th1 + th2)) * (cos (th1 - th2)) = ((sin th1) * (cos th1)) + ((sin th2) * (cos th2)) ; ::_thesis: verum
end;

theorem :: SIN_COS4:40
for th1, th2 being real number holds (cos (th1 + th2)) * (sin (th1 - th2)) = ((sin th1) * (cos th1)) - ((sin th2) * (cos th2))
proof
let th1, th2 be real number ; ::_thesis: (cos (th1 + th2)) * (sin (th1 - th2)) = ((sin th1) * (cos th1)) - ((sin th2) * (cos th2))
(cos (th1 + th2)) * (sin (th1 - th2)) = (sin (th1 + (- th2))) * (cos (th1 - (- th2)))
.= ((sin th1) * (cos th1)) + ((sin (- th2)) * (cos (- th2))) by Th39
.= ((sin th1) * (cos th1)) + ((sin (- th2)) * (cos th2)) by SIN_COS:31
.= ((sin th1) * (cos th1)) + ((- (sin th2)) * (cos th2)) by SIN_COS:31
.= ((sin th1) * (cos th1)) - ((sin th2) * (cos th2)) ;
hence  (cos (th1 + th2)) * (sin (th1 - th2)) = ((sin th1) * (cos th1)) - ((sin th2) * (cos th2)) ; ::_thesis: verum
end;

theorem Th41: :: SIN_COS4:41
for th1, th2 being real number holds (cos (th1 + th2)) * (cos (th1 - th2)) = ((cos th1) * (cos th1)) - ((sin th2) * (sin th2))
proof
let th1, th2 be real number ; ::_thesis: (cos (th1 + th2)) * (cos (th1 - th2)) = ((cos th1) * (cos th1)) - ((sin th2) * (sin th2))
(cos (th1 + th2)) * (cos (th1 - th2)) = (((cos th1) * (cos th2)) - ((sin th1) * (sin th2))) * (cos (th1 - th2)) by SIN_COS:75
.= (((cos th1) * (cos th2)) + (- ((sin th1) * (sin th2)))) * (((cos th1) * (cos th2)) + ((sin th1) * (sin th2))) by SIN_COS:83
.= (((((cos th1) * (cos th1)) * ((cos th2) * (cos th2))) + (((cos th1) * (cos th2)) * ((sin th1) * (sin th2)))) + (- (((sin th1) * (sin th2)) * ((cos th1) * (cos th2))))) + (- ((((sin th1) * (sin th1)) * (sin th2)) * (sin th2)))
.= (((cos th1) * (cos th1)) * (1 - (- (- ((sin th2) * (sin th2)))))) + (- (((sin th1) * (sin th1)) * ((sin th2) * (sin th2)))) by Th5
.= (((cos th1) * (cos th1)) * 1) + (((sin th2) * (sin th2)) * (- (((cos th1) * (cos th1)) + ((sin th1) * (sin th1)))))
.= (((cos th1) * (cos th1)) * 1) + (((sin th2) * (sin th2)) * (- 1)) by SIN_COS:29
.= ((cos th1) * (cos th1)) - ((sin th2) * (sin th2)) ;
hence  (cos (th1 + th2)) * (cos (th1 - th2)) = ((cos th1) * (cos th1)) - ((sin th2) * (sin th2)) ; ::_thesis: verum
end;

theorem :: SIN_COS4:42
for th1, th2 being real number holds (cos (th1 + th2)) * (cos (th1 - th2)) = ((cos th2) * (cos th2)) - ((sin th1) * (sin th1))
proof
let th1, th2 be real number ; ::_thesis: (cos (th1 + th2)) * (cos (th1 - th2)) = ((cos th2) * (cos th2)) - ((sin th1) * (sin th1))
(cos (th1 + th2)) * (cos (th1 - th2)) = ((cos th1) * (cos th1)) - ((sin th2) * (sin th2)) by Th41
.= (1 - ((sin th1) * (sin th1))) - ((sin th2) * (sin th2)) by Th5
.= (1 - ((sin th1) * (sin th1))) - (1 - ((cos th2) * (cos th2))) by Th4
.= ((cos th2) * (cos th2)) - ((sin th1) * (sin th1)) ;
hence  (cos (th1 + th2)) * (cos (th1 - th2)) = ((cos th2) * (cos th2)) - ((sin th1) * (sin th1)) ; ::_thesis: verum
end;

theorem :: SIN_COS4:43
for th1, th2 being real number st cos th1 <> 0 & cos th2 <> 0 holds
(sin (th1 + th2)) / (sin (th1 - th2)) = ((tan th1) + (tan th2)) / ((tan th1) - (tan th2))
proof
let th1, th2 be real number ; ::_thesis: ( cos th1 <> 0 & cos th2 <> 0 implies (sin (th1 + th2)) / (sin (th1 - th2)) = ((tan th1) + (tan th2)) / ((tan th1) - (tan th2)) )
assume that
A1: cos th1 <> 0 and
A2: cos th2 <> 0 ; ::_thesis: (sin (th1 + th2)) / (sin (th1 - th2)) = ((tan th1) + (tan th2)) / ((tan th1) - (tan th2))
(sin (th1 + th2)) / (sin (th1 - th2)) = (((sin th1) * (cos th2)) + ((cos th1) * (sin th2))) / (sin (th1 - th2)) by SIN_COS:75
.= (((sin th1) * (cos th2)) + ((cos th1) * (sin th2))) / (((sin th1) * (cos th2)) - ((cos th1) * (sin th2))) by SIN_COS:82
.= ((((sin th1) * (cos th2)) + ((cos th1) * (sin th2))) / ((cos th1) * (cos th2))) / ((((sin th1) * (cos th2)) - ((cos th1) * (sin th2))) / ((cos th1) * (cos th2))) by A1, A2, XCMPLX_1:6, XCMPLX_1:55
.= ((((sin th1) * (cos th2)) / ((cos th1) * (cos th2))) + (((cos th1) * (sin th2)) / ((cos th1) * (cos th2)))) / ((((sin th1) * (cos th2)) + (- ((cos th1) * (sin th2)))) / ((cos th1) * (cos th2))) by XCMPLX_1:62
.= ((((sin th1) * (cos th2)) / ((cos th1) * (cos th2))) + (((cos th1) * (sin th2)) / ((cos th1) * (cos th2)))) / ((((sin th1) * (cos th2)) / ((cos th1) * (cos th2))) + ((- ((cos th1) * (sin th2))) / ((cos th1) * (cos th2)))) by XCMPLX_1:62
.= ((((sin th1) / (cos th1)) * ((cos th2) / (cos th2))) + (((cos th1) * (sin th2)) / ((cos th1) * (cos th2)))) / ((((sin th1) * (cos th2)) / ((cos th1) * (cos th2))) + ((- ((cos th1) * (sin th2))) / ((cos th1) * (cos th2)))) by XCMPLX_1:76
.= ((((sin th1) / (cos th1)) * ((cos th2) / (cos th2))) + (((cos th1) / (cos th1)) * ((sin th2) / (cos th2)))) / ((((sin th1) * (cos th2)) / ((cos th1) * (cos th2))) + ((- ((cos th1) * (sin th2))) / ((cos th1) * (cos th2)))) by XCMPLX_1:76
.= ((((sin th1) / (cos th1)) * ((cos th2) / (cos th2))) + (((cos th1) / (cos th1)) * ((sin th2) / (cos th2)))) / ((((sin th1) / (cos th1)) * ((cos th2) / (cos th2))) + (((cos th1) * (- (sin th2))) / ((cos th1) * (cos th2)))) by XCMPLX_1:76
.= ((((sin th1) / (cos th1)) * ((cos th2) / (cos th2))) + (((cos th1) / (cos th1)) * ((sin th2) / (cos th2)))) / ((((sin th1) / (cos th1)) * ((cos th2) / (cos th2))) + (((cos th1) / (cos th1)) * ((- (sin th2)) / (cos th2)))) by XCMPLX_1:76
.= (((sin th1) / (cos th1)) + (((cos th1) / (cos th1)) * ((sin th2) / (cos th2)))) / ((((sin th1) / (cos th1)) * ((cos th2) / (cos th2))) + (((cos th1) / (cos th1)) * ((- (sin th2)) / (cos th2)))) by A2, XCMPLX_1:88
.= (((sin th1) / (cos th1)) + ((sin th2) / (cos th2))) / ((((sin th1) / (cos th1)) * ((cos th2) / (cos th2))) + (((cos th1) / (cos th1)) * ((- (sin th2)) / (cos th2)))) by A1, XCMPLX_1:88
.= (((sin th1) / (cos th1)) + ((sin th2) / (cos th2))) / (((sin th1) / (cos th1)) + (((cos th1) / (cos th1)) * ((- (sin th2)) / (cos th2)))) by A2, XCMPLX_1:88
.= (((sin th1) / (cos th1)) + ((sin th2) / (cos th2))) / (((sin th1) / (cos th1)) + ((- (sin th2)) / (cos th2))) by A1, XCMPLX_1:88
.= ((tan th1) + (tan th2)) / ((tan th1) + (- ((sin th2) / (cos th2)))) by XCMPLX_1:187
.= ((tan th1) + (tan th2)) / ((tan th1) - (tan th2)) ;
hence  (sin (th1 + th2)) / (sin (th1 - th2)) = ((tan th1) + (tan th2)) / ((tan th1) - (tan th2)) ; ::_thesis: verum
end;

theorem :: SIN_COS4:44
for th1, th2 being real number st cos th1 <> 0 & cos th2 <> 0 holds
(cos (th1 + th2)) / (cos (th1 - th2)) = (1 - ((tan th1) * (tan th2))) / (1 + ((tan th1) * (tan th2)))
proof
let th1, th2 be real number ; ::_thesis: ( cos th1 <> 0 & cos th2 <> 0 implies (cos (th1 + th2)) / (cos (th1 - th2)) = (1 - ((tan th1) * (tan th2))) / (1 + ((tan th1) * (tan th2))) )
assume A1: ( cos th1 <> 0 & cos th2 <> 0 ) ; ::_thesis: (cos (th1 + th2)) / (cos (th1 - th2)) = (1 - ((tan th1) * (tan th2))) / (1 + ((tan th1) * (tan th2)))
(cos (th1 + th2)) / (cos (th1 - th2)) = (((cos th1) * (cos th2)) - ((sin th1) * (sin th2))) / (cos (th1 - th2)) by SIN_COS:75
.= ((((cos th1) * (cos th2)) - ((sin th1) * (sin th2))) / ((cos th1) * (cos th2))) / ((cos (th1 - th2)) / ((cos th1) * (cos th2))) by A1, XCMPLX_1:6, XCMPLX_1:55
.= ((((cos th1) * (cos th2)) / ((cos th1) * (cos th2))) - (((sin th1) * (sin th2)) / ((cos th1) * (cos th2)))) / ((cos (th1 - th2)) / ((cos th1) * (cos th2))) by XCMPLX_1:120
.= (1 - (((sin th1) * (sin th2)) / ((cos th1) * (cos th2)))) / ((cos (th1 - th2)) / ((cos th1) * (cos th2))) by A1, XCMPLX_1:6, XCMPLX_1:60
.= (1 - ((tan th1) * ((sin th2) / (cos th2)))) / ((cos (th1 - th2)) / ((cos th1) * (cos th2))) by XCMPLX_1:76
.= (1 - ((tan th1) * (tan th2))) / ((((cos th1) * (cos th2)) + ((sin th1) * (sin th2))) / ((cos th1) * (cos th2))) by SIN_COS:83
.= (1 - ((tan th1) * (tan th2))) / ((((cos th1) * (cos th2)) / ((cos th1) * (cos th2))) + (((sin th1) * (sin th2)) / ((cos th1) * (cos th2)))) by XCMPLX_1:62
.= (1 - ((tan th1) * (tan th2))) / (1 + (((sin th1) * (sin th2)) / ((cos th1) * (cos th2)))) by A1, XCMPLX_1:6, XCMPLX_1:60
.= (1 - ((tan th1) * (tan th2))) / (1 + ((tan th1) * (tan th2))) by XCMPLX_1:76 ;
hence  (cos (th1 + th2)) / (cos (th1 - th2)) = (1 - ((tan th1) * (tan th2))) / (1 + ((tan th1) * (tan th2))) ; ::_thesis: verum
end;

theorem :: SIN_COS4:45
for th1, th2 being real number holds ((sin th1) + (sin th2)) / ((sin th1) - (sin th2)) = (tan ((th1 + th2) / 2)) * (cot ((th1 - th2) / 2))
proof
let th1, th2 be real number ; ::_thesis: ((sin th1) + (sin th2)) / ((sin th1) - (sin th2)) = (tan ((th1 + th2) / 2)) * (cot ((th1 - th2) / 2))
((sin th1) + (sin th2)) / ((sin th1) - (sin th2)) = (2 * ((cos ((th1 - th2) / 2)) * (sin ((th1 + th2) / 2)))) / ((sin th1) - (sin th2)) by Th15
.= (2 * ((cos ((th1 - th2) / 2)) * (sin ((th1 + th2) / 2)))) / (2 * ((cos ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2)))) by Th16
.= (2 / 2) * (((cos ((th1 - th2) / 2)) * (sin ((th1 + th2) / 2))) / ((cos ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2)))) by XCMPLX_1:76
.= (tan ((th1 + th2) / 2)) * (cot ((th1 - th2) / 2)) by XCMPLX_1:76 ;
hence  ((sin th1) + (sin th2)) / ((sin th1) - (sin th2)) = (tan ((th1 + th2) / 2)) * (cot ((th1 - th2) / 2)) ; ::_thesis: verum
end;

theorem :: SIN_COS4:46
for th1, th2 being real number st cos ((th1 - th2) / 2) <> 0 holds
((sin th1) + (sin th2)) / ((cos th1) + (cos th2)) = tan ((th1 + th2) / 2)
proof
let th1, th2 be real number ; ::_thesis: ( cos ((th1 - th2) / 2) <> 0 implies ((sin th1) + (sin th2)) / ((cos th1) + (cos th2)) = tan ((th1 + th2) / 2) )
assume A1: cos ((th1 - th2) / 2) <> 0 ; ::_thesis: ((sin th1) + (sin th2)) / ((cos th1) + (cos th2)) = tan ((th1 + th2) / 2)
((sin th1) + (sin th2)) / ((cos th1) + (cos th2)) = (2 * ((cos ((th1 - th2) / 2)) * (sin ((th1 + th2) / 2)))) / ((cos th1) + (cos th2)) by Th15
.= (2 * ((cos ((th1 - th2) / 2)) * (sin ((th1 + th2) / 2)))) / (2 * ((cos ((th1 + th2) / 2)) * (cos ((th1 - th2) / 2)))) by Th17
.= (2 / 2) * (((cos ((th1 - th2) / 2)) * (sin ((th1 + th2) / 2))) / ((cos ((th1 - th2) / 2)) * (cos ((th1 + th2) / 2)))) by XCMPLX_1:76
.= ((cos ((th1 - th2) / 2)) / (cos ((th1 - th2) / 2))) * ((sin ((th1 + th2) / 2)) / (cos ((th1 + th2) / 2))) by XCMPLX_1:76
.= tan ((th1 + th2) / 2) by A1, XCMPLX_1:88 ;
hence  ((sin th1) + (sin th2)) / ((cos th1) + (cos th2)) = tan ((th1 + th2) / 2) ; ::_thesis: verum
end;

theorem :: SIN_COS4:47
for th1, th2 being real number st cos ((th1 + th2) / 2) <> 0 holds
((sin th1) - (sin th2)) / ((cos th1) + (cos th2)) = tan ((th1 - th2) / 2)
proof
let th1, th2 be real number ; ::_thesis: ( cos ((th1 + th2) / 2) <> 0 implies ((sin th1) - (sin th2)) / ((cos th1) + (cos th2)) = tan ((th1 - th2) / 2) )
assume A1: cos ((th1 + th2) / 2) <> 0 ; ::_thesis: ((sin th1) - (sin th2)) / ((cos th1) + (cos th2)) = tan ((th1 - th2) / 2)
((sin th1) - (sin th2)) / ((cos th1) + (cos th2)) = (2 * ((cos ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2)))) / ((cos th1) + (cos th2)) by Th16
.= (2 * ((cos ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2)))) / (2 * ((cos ((th1 + th2) / 2)) * (cos ((th1 - th2) / 2)))) by Th17
.= (2 / 2) * (((cos ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2))) / ((cos ((th1 + th2) / 2)) * (cos ((th1 - th2) / 2)))) by XCMPLX_1:76
.= ((cos ((th1 + th2) / 2)) / (cos ((th1 + th2) / 2))) * ((sin ((th1 - th2) / 2)) / (cos ((th1 - th2) / 2))) by XCMPLX_1:76
.= tan ((th1 - th2) / 2) by A1, XCMPLX_1:88 ;
hence  ((sin th1) - (sin th2)) / ((cos th1) + (cos th2)) = tan ((th1 - th2) / 2) ; ::_thesis: verum
end;

theorem :: SIN_COS4:48
for th1, th2 being real number st sin ((th1 + th2) / 2) <> 0 holds
((sin th1) + (sin th2)) / ((cos th2) - (cos th1)) = cot ((th1 - th2) / 2)
proof
let th1, th2 be real number ; ::_thesis: ( sin ((th1 + th2) / 2) <> 0 implies ((sin th1) + (sin th2)) / ((cos th2) - (cos th1)) = cot ((th1 - th2) / 2) )
assume A1: sin ((th1 + th2) / 2) <> 0 ; ::_thesis: ((sin th1) + (sin th2)) / ((cos th2) - (cos th1)) = cot ((th1 - th2) / 2)
((sin th1) + (sin th2)) / ((cos th2) - (cos th1)) = (2 * ((cos ((th1 - th2) / 2)) * (sin ((th1 + th2) / 2)))) / ((cos th2) - (cos th1)) by Th15
.= (2 * ((cos ((th1 - th2) / 2)) * (sin ((th1 + th2) / 2)))) / (- (2 * ((sin ((th2 + th1) / 2)) * (sin ((th2 - th1) / 2))))) by Th18
.= (2 * ((cos ((th1 - th2) / 2)) * (sin ((th1 + th2) / 2)))) / (2 * ((sin ((th2 + th1) / 2)) * (- (sin ((th2 - th1) / 2)))))
.= (2 * ((cos ((th1 - th2) / 2)) * (sin ((th1 + th2) / 2)))) / (2 * ((sin ((th2 + th1) / 2)) * (sin (- ((th2 - th1) / 2))))) by SIN_COS:31
.= (2 / 2) * (((cos ((th1 - th2) / 2)) * (sin ((th1 + th2) / 2))) / ((sin ((th2 + th1) / 2)) * (sin ((th1 - th2) / 2)))) by XCMPLX_1:76
.= ((cos ((th1 - th2) / 2)) / (sin ((th1 - th2) / 2))) * ((sin ((th1 + th2) / 2)) / (sin ((th2 + th1) / 2))) by XCMPLX_1:76
.= cot ((th1 - th2) / 2) by A1, XCMPLX_1:88 ;
hence  ((sin th1) + (sin th2)) / ((cos th2) - (cos th1)) = cot ((th1 - th2) / 2) ; ::_thesis: verum
end;

theorem :: SIN_COS4:49
for th1, th2 being real number st sin ((th1 - th2) / 2) <> 0 holds
((sin th1) - (sin th2)) / ((cos th2) - (cos th1)) = cot ((th1 + th2) / 2)
proof
let th1, th2 be real number ; ::_thesis: ( sin ((th1 - th2) / 2) <> 0 implies ((sin th1) - (sin th2)) / ((cos th2) - (cos th1)) = cot ((th1 + th2) / 2) )
assume A1: sin ((th1 - th2) / 2) <> 0 ; ::_thesis: ((sin th1) - (sin th2)) / ((cos th2) - (cos th1)) = cot ((th1 + th2) / 2)
((sin th1) - (sin th2)) / ((cos th2) - (cos th1)) = (2 * ((cos ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2)))) / ((cos th2) - (cos th1)) by Th16
.= (2 * ((cos ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2)))) / (- (2 * ((sin ((th2 + th1) / 2)) * (sin ((th2 - th1) / 2))))) by Th18
.= (2 * ((cos ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2)))) / (2 * ((sin ((th2 + th1) / 2)) * (- (sin ((th2 - th1) / 2)))))
.= (2 * ((cos ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2)))) / (2 * ((sin ((th2 + th1) / 2)) * (sin (- ((th2 - th1) / 2))))) by SIN_COS:31
.= (2 / 2) * (((cos ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2))) / ((sin ((th2 + th1) / 2)) * (sin ((th1 - th2) / 2)))) by XCMPLX_1:76
.= ((cos ((th1 + th2) / 2)) / (sin ((th2 + th1) / 2))) * ((sin ((th1 - th2) / 2)) / (sin ((th1 - th2) / 2))) by XCMPLX_1:76
.= cot ((th1 + th2) / 2) by A1, XCMPLX_1:88 ;
hence  ((sin th1) - (sin th2)) / ((cos th2) - (cos th1)) = cot ((th1 + th2) / 2) ; ::_thesis: verum
end;

theorem :: SIN_COS4:50
for th1, th2 being real number holds ((cos th1) + (cos th2)) / ((cos th1) - (cos th2)) = (cot ((th1 + th2) / 2)) * (cot ((th2 - th1) / 2))
proof
let th1, th2 be real number ; ::_thesis: ((cos th1) + (cos th2)) / ((cos th1) - (cos th2)) = (cot ((th1 + th2) / 2)) * (cot ((th2 - th1) / 2))
((cos th1) + (cos th2)) / ((cos th1) - (cos th2)) = (2 * ((cos ((th1 + th2) / 2)) * (cos ((th1 - th2) / 2)))) / ((cos th1) - (cos th2)) by Th17
.= (2 * ((cos ((th1 + th2) / 2)) * (cos ((th1 - th2) / 2)))) / (- (2 * ((sin ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2))))) by Th18
.= (2 * ((cos ((th1 + th2) / 2)) * (cos ((th1 - th2) / 2)))) / (2 * ((sin ((th1 + th2) / 2)) * (- (sin ((th1 - th2) / 2)))))
.= (2 * ((cos ((th1 + th2) / 2)) * (cos ((th1 - th2) / 2)))) / (2 * ((sin ((th1 + th2) / 2)) * (sin (- ((th1 - th2) / 2))))) by SIN_COS:31
.= (2 / 2) * (((cos ((th1 + th2) / 2)) * (cos ((th1 - th2) / 2))) / ((sin ((th1 + th2) / 2)) * (sin ((th2 - th1) / 2)))) by XCMPLX_1:76
.= ((cos ((th1 + th2) / 2)) / (sin ((th1 + th2) / 2))) * ((cos (- ((th2 - th1) / 2))) / (sin ((th2 - th1) / 2))) by XCMPLX_1:76
.= (cot ((th1 + th2) / 2)) * (cot ((th2 - th1) / 2)) by SIN_COS:31 ;
hence  ((cos th1) + (cos th2)) / ((cos th1) - (cos th2)) = (cot ((th1 + th2) / 2)) * (cot ((th2 - th1) / 2)) ; ::_thesis: verum
end;