:: 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;