:: SIN_COS3 semantic presentation begin definition func sin_C -> Function of COMPLEX,COMPLEX means :Def1: :: SIN_COS3:def 1 for z being Element of COMPLEX holds it . z = ((exp ( * z)) - (exp (- ( * z)))) / (2 * ); existence ex b1 being Function of COMPLEX,COMPLEX st for z being Element of COMPLEX holds b1 . z = ((exp ( * z)) - (exp (- ( * z)))) / (2 * ) proof deffunc H1( Element of COMPLEX ) -> Element of COMPLEX = ((exp ( * $1)) - (exp (- ( * $1)))) / (2 * ); ex f being Function of COMPLEX,COMPLEX st for z being Element of COMPLEX holds f . z = H1(z) from FUNCT_2:sch_4(); hence ex b1 being Function of COMPLEX,COMPLEX st for z being Element of COMPLEX holds b1 . z = ((exp ( * z)) - (exp (- ( * z)))) / (2 * ) ; ::_thesis: verum end; uniqueness for b1, b2 being Function of COMPLEX,COMPLEX st ( for z being Element of COMPLEX holds b1 . z = ((exp ( * z)) - (exp (- ( * z)))) / (2 * ) ) & ( for z being Element of COMPLEX holds b2 . z = ((exp ( * z)) - (exp (- ( * z)))) / (2 * ) ) holds b1 = b2 proof deffunc H1( Element of COMPLEX ) -> Element of COMPLEX = ((exp ( * $1)) - (exp (- ( * $1)))) / (2 * ); for f1, f2 being Function of COMPLEX,COMPLEX st ( for z being Element of COMPLEX holds f1 . z = H1(z) ) & ( for z being Element of COMPLEX holds f2 . z = H1(z) ) holds f1 = f2 from BINOP_2:sch_1(); hence for b1, b2 being Function of COMPLEX,COMPLEX st ( for z being Element of COMPLEX holds b1 . z = ((exp ( * z)) - (exp (- ( * z)))) / (2 * ) ) & ( for z being Element of COMPLEX holds b2 . z = ((exp ( * z)) - (exp (- ( * z)))) / (2 * ) ) holds b1 = b2 ; ::_thesis: verum end; end; :: deftheorem Def1 defines sin_C SIN_COS3:def_1_:_ for b1 being Function of COMPLEX,COMPLEX holds ( b1 = sin_C iff for z being Element of COMPLEX holds b1 . z = ((exp ( * z)) - (exp (- ( * z)))) / (2 * ) ); definition func cos_C -> Function of COMPLEX,COMPLEX means :Def2: :: SIN_COS3:def 2 for z being Element of COMPLEX holds it . z = ((exp ( * z)) + (exp (- ( * z)))) / 2; existence ex b1 being Function of COMPLEX,COMPLEX st for z being Element of COMPLEX holds b1 . z = ((exp ( * z)) + (exp (- ( * z)))) / 2 proof deffunc H1( Element of COMPLEX ) -> Element of COMPLEX = ((exp ( * $1)) + (exp (- ( * $1)))) / 2; ex f being Function of COMPLEX,COMPLEX st for z being Element of COMPLEX holds f . z = H1(z) from FUNCT_2:sch_4(); hence ex b1 being Function of COMPLEX,COMPLEX st for z being Element of COMPLEX holds b1 . z = ((exp ( * z)) + (exp (- ( * z)))) / 2 ; ::_thesis: verum end; uniqueness for b1, b2 being Function of COMPLEX,COMPLEX st ( for z being Element of COMPLEX holds b1 . z = ((exp ( * z)) + (exp (- ( * z)))) / 2 ) & ( for z being Element of COMPLEX holds b2 . z = ((exp ( * z)) + (exp (- ( * z)))) / 2 ) holds b1 = b2 proof deffunc H1( Element of COMPLEX ) -> Element of COMPLEX = ((exp ( * $1)) + (exp (- ( * $1)))) / 2; for f1, f2 being Function of COMPLEX,COMPLEX st ( for z being Element of COMPLEX holds f1 . z = H1(z) ) & ( for z being Element of COMPLEX holds f2 . z = H1(z) ) holds f1 = f2 from BINOP_2:sch_1(); hence for b1, b2 being Function of COMPLEX,COMPLEX st ( for z being Element of COMPLEX holds b1 . z = ((exp ( * z)) + (exp (- ( * z)))) / 2 ) & ( for z being Element of COMPLEX holds b2 . z = ((exp ( * z)) + (exp (- ( * z)))) / 2 ) holds b1 = b2 ; ::_thesis: verum end; end; :: deftheorem Def2 defines cos_C SIN_COS3:def_2_:_ for b1 being Function of COMPLEX,COMPLEX holds ( b1 = cos_C iff for z being Element of COMPLEX holds b1 . z = ((exp ( * z)) + (exp (- ( * z)))) / 2 ); definition func sinh_C -> Function of COMPLEX,COMPLEX means :Def3: :: SIN_COS3:def 3 for z being Element of COMPLEX holds it . z = ((exp z) - (exp (- z))) / 2; existence ex b1 being Function of COMPLEX,COMPLEX st for z being Element of COMPLEX holds b1 . z = ((exp z) - (exp (- z))) / 2 proof deffunc H1( Element of COMPLEX ) -> Element of COMPLEX = ((exp $1) - (exp (- $1))) / 2; ex f being Function of COMPLEX,COMPLEX st for z being Element of COMPLEX holds f . z = H1(z) from FUNCT_2:sch_4(); hence ex b1 being Function of COMPLEX,COMPLEX st for z being Element of COMPLEX holds b1 . z = ((exp z) - (exp (- z))) / 2 ; ::_thesis: verum end; uniqueness for b1, b2 being Function of COMPLEX,COMPLEX st ( for z being Element of COMPLEX holds b1 . z = ((exp z) - (exp (- z))) / 2 ) & ( for z being Element of COMPLEX holds b2 . z = ((exp z) - (exp (- z))) / 2 ) holds b1 = b2 proof deffunc H1( Element of COMPLEX ) -> Element of COMPLEX = ((exp $1) - (exp (- $1))) / 2; for f1, f2 being Function of COMPLEX,COMPLEX st ( for z being Element of COMPLEX holds f1 . z = H1(z) ) & ( for z being Element of COMPLEX holds f2 . z = H1(z) ) holds f1 = f2 from BINOP_2:sch_1(); hence for b1, b2 being Function of COMPLEX,COMPLEX st ( for z being Element of COMPLEX holds b1 . z = ((exp z) - (exp (- z))) / 2 ) & ( for z being Element of COMPLEX holds b2 . z = ((exp z) - (exp (- z))) / 2 ) holds b1 = b2 ; ::_thesis: verum end; end; :: deftheorem Def3 defines sinh_C SIN_COS3:def_3_:_ for b1 being Function of COMPLEX,COMPLEX holds ( b1 = sinh_C iff for z being Element of COMPLEX holds b1 . z = ((exp z) - (exp (- z))) / 2 ); definition func cosh_C -> Function of COMPLEX,COMPLEX means :Def4: :: SIN_COS3:def 4 for z being Element of COMPLEX holds it . z = ((exp z) + (exp (- z))) / 2; existence ex b1 being Function of COMPLEX,COMPLEX st for z being Element of COMPLEX holds b1 . z = ((exp z) + (exp (- z))) / 2 proof deffunc H1( Element of COMPLEX ) -> Element of COMPLEX = ((exp $1) + (exp (- $1))) / 2; ex f being Function of COMPLEX,COMPLEX st for z being Element of COMPLEX holds f . z = H1(z) from FUNCT_2:sch_4(); hence ex b1 being Function of COMPLEX,COMPLEX st for z being Element of COMPLEX holds b1 . z = ((exp z) + (exp (- z))) / 2 ; ::_thesis: verum end; uniqueness for b1, b2 being Function of COMPLEX,COMPLEX st ( for z being Element of COMPLEX holds b1 . z = ((exp z) + (exp (- z))) / 2 ) & ( for z being Element of COMPLEX holds b2 . z = ((exp z) + (exp (- z))) / 2 ) holds b1 = b2 proof deffunc H1( Element of COMPLEX ) -> Element of COMPLEX = ((exp $1) + (exp (- $1))) / 2; for f1, f2 being Function of COMPLEX,COMPLEX st ( for z being Element of COMPLEX holds f1 . z = H1(z) ) & ( for z being Element of COMPLEX holds f2 . z = H1(z) ) holds f1 = f2 from BINOP_2:sch_1(); hence for b1, b2 being Function of COMPLEX,COMPLEX st ( for z being Element of COMPLEX holds b1 . z = ((exp z) + (exp (- z))) / 2 ) & ( for z being Element of COMPLEX holds b2 . z = ((exp z) + (exp (- z))) / 2 ) holds b1 = b2 ; ::_thesis: verum end; end; :: deftheorem Def4 defines cosh_C SIN_COS3:def_4_:_ for b1 being Function of COMPLEX,COMPLEX holds ( b1 = cosh_C iff for z being Element of COMPLEX holds b1 . z = ((exp z) + (exp (- z))) / 2 ); Lm1: for z being complex number holds sinh_C /. z = ((exp z) - (exp (- z))) / 2 proof let z be complex number ; ::_thesis: sinh_C /. z = ((exp z) - (exp (- z))) / 2 reconsider z = z as Element of COMPLEX by XCMPLX_0:def_2; sinh_C /. z = ((exp z) - (exp (- z))) / 2 by Def3; hence sinh_C /. z = ((exp z) - (exp (- z))) / 2 ; ::_thesis: verum end; Lm2: for z being complex number holds cosh_C /. z = ((exp z) + (exp (- z))) / 2 proof let z be complex number ; ::_thesis: cosh_C /. z = ((exp z) + (exp (- z))) / 2 reconsider z = z as Element of COMPLEX by XCMPLX_0:def_2; cosh_C /. z = ((exp z) + (exp (- z))) / 2 by Def4; hence cosh_C /. z = ((exp z) + (exp (- z))) / 2 ; ::_thesis: verum end; Lm3: for z being Element of COMPLEX holds (exp z) * (exp (- z)) = 1 proof let z be Element of COMPLEX ; ::_thesis: (exp z) * (exp (- z)) = 1 thus (exp z) * (exp (- z)) = exp (z + (- z)) by SIN_COS:23 .= 1 by SIN_COS:49, SIN_COS:51 ; ::_thesis: verum end; begin theorem :: SIN_COS3:1 for z being Element of COMPLEX holds ((sin_C /. z) * (sin_C /. z)) + ((cos_C /. z) * (cos_C /. z)) = 1 proof let z be Element of COMPLEX ; ::_thesis: ((sin_C /. z) * (sin_C /. z)) + ((cos_C /. z) * (cos_C /. z)) = 1 set z1 = exp ( * z); set z2 = exp (- ( * z)); ((sin_C /. z) * (sin_C /. z)) + ((cos_C /. z) * (cos_C /. z)) = ((sin_C /. z) * (sin_C /. z)) + ((cos_C /. z) * (((exp ( * z)) + (exp (- ( * z)))) / 2)) by Def2 .= ((sin_C /. z) * (sin_C /. z)) + ((((exp ( * z)) + (exp (- ( * z)))) / 2) * (((exp ( * z)) + (exp (- ( * z)))) / 2)) by Def2 .= ((((exp ( * z)) - (exp (- ( * z)))) / (2 * )) * (sin_C /. z)) + ((((exp ( * z)) + (exp (- ( * z)))) / 2) * (((exp ( * z)) + (exp (- ( * z)))) / 2)) by Def1 .= ((((exp ( * z)) - (exp (- ( * z)))) / (2 * )) * (((exp ( * z)) - (exp (- ( * z)))) / (2 * ))) + ((((exp ( * z)) + (exp (- ( * z)))) / 2) * (((exp ( * z)) + (exp (- ( * z)))) / 2)) by Def1 .= ((((exp ( * z)) * (exp (- ( * z)))) + ((exp ( * z)) * (exp (- ( * z))))) + (((exp ( * z)) * (exp (- ( * z)))) + ((exp ( * z)) * (exp (- ( * z)))))) / 4 .= ((1 + ((exp ( * z)) * (exp (- ( * z))))) + (((exp ( * z)) * (exp (- ( * z)))) + ((exp ( * z)) * (exp (- ( * z)))))) / 4 by Lm3 .= ((1 + 1) + (((exp ( * z)) * (exp (- ( * z)))) + ((exp ( * z)) * (exp (- ( * z)))))) / 4 by Lm3 .= ((1 + 1) + (((exp ( * z)) * (exp (- ( * z)))) + 1)) / 4 by Lm3 .= (2 + 2) / 4 by Lm3 ; hence ((sin_C /. z) * (sin_C /. z)) + ((cos_C /. z) * (cos_C /. z)) = 1 ; ::_thesis: verum end; theorem Th2: :: SIN_COS3:2 for z being complex number holds - (sin_C /. z) = sin_C /. (- z) proof let z be complex number ; ::_thesis: - (sin_C /. z) = sin_C /. (- z) reconsider z = z as Element of COMPLEX by XCMPLX_0:def_2; sin_C /. (- z) = ((exp ( * (- z))) - (exp (- ( * (- z))))) / (2 * ) by Def1 .= - (((exp ( * z)) - (exp (- ( * z)))) / (2 * )) ; then - (sin_C /. z) = sin_C /. (- z) by Def1; hence - (sin_C /. z) = sin_C /. (- z) ; ::_thesis: verum end; theorem Th3: :: SIN_COS3:3 for z being complex number holds cos_C /. z = cos_C /. (- z) proof let z be complex number ; ::_thesis: cos_C /. z = cos_C /. (- z) reconsider z = z as Element of COMPLEX by XCMPLX_0:def_2; cos_C /. (- z) = ((exp ( * (- z))) + (exp (- ( * (- z))))) / 2 by Def2 .= ((exp (- ( * z))) + (exp ( * z))) / 2 ; then cos_C /. z = cos_C /. (- z) by Def2; hence cos_C /. z = cos_C /. (- z) ; ::_thesis: verum end; theorem Th4: :: SIN_COS3:4 for z1, z2 being complex number holds sin_C /. (z1 + z2) = ((sin_C /. z1) * (cos_C /. z2)) + ((cos_C /. z1) * (sin_C /. z2)) proof let z1, z2 be complex number ; ::_thesis: sin_C /. (z1 + z2) = ((sin_C /. z1) * (cos_C /. z2)) + ((cos_C /. z1) * (sin_C /. z2)) reconsider z1 = z1, z2 = z2 as Element of COMPLEX by XCMPLX_0:def_2; set e1 = exp ( * z1); set e2 = exp (- ( * z1)); set e3 = exp ( * z2); set e4 = exp (- ( * z2)); ((sin_C /. z1) * (cos_C /. z2)) + ((cos_C /. z1) * (sin_C /. z2)) = ((((exp ( * z1)) - (exp (- ( * z1)))) / (2 * )) * (cos_C /. z2)) + ((cos_C /. z1) * (sin_C /. z2)) by Def1 .= ((((exp ( * z1)) - (exp (- ( * z1)))) / (2 * )) * (cos_C /. z2)) + ((cos_C /. z1) * (((exp ( * z2)) - (exp (- ( * z2)))) / (2 * ))) by Def1 .= ((((exp ( * z1)) - (exp (- ( * z1)))) / (2 * )) * (((exp (- ( * z2))) + (exp ( * z2))) / 2)) + ((cos_C /. z1) * (((exp ( * z2)) - (exp (- ( * z2)))) / (2 * ))) by Def2 .= ((((exp ( * z1)) - (exp (- ( * z1)))) * ((exp (- ( * z2))) + (exp ( * z2)))) / ((2 * ) * 2)) + ((((exp (- ( * z1))) + (exp ( * z1))) / 2) * (((exp ( * z2)) - (exp (- ( * z2)))) / (2 * ))) by Def2 .= ((((exp ( * z1)) * (exp ( * z2))) + ((exp ( * z1)) * (exp ( * z2)))) - ((((exp ( * z1)) * (exp (- ( * z2)))) + ((exp (- ( * z1))) * (exp (- ( * z2))))) - (((exp ( * z1)) * (exp (- ( * z2)))) - ((exp (- ( * z1))) * (exp (- ( * z2))))))) / ((2 * ) * 2) .= ((((Re ((exp ( * z1)) * (exp ( * z2)))) + (Re ((exp ( * z1)) * (exp ( * z2))))) + (((Im ((exp ( * z1)) * (exp ( * z2)))) + (Im ((exp ( * z1)) * (exp ( * z2))))) * )) - (((exp (- ( * z1))) * (exp (- ( * z2)))) + ((exp (- ( * z1))) * (exp (- ( * z2)))))) / ((2 * ) * 2) by COMPLEX1:def_5 .= (((2 * (Re ((exp ( * z1)) * (exp ( * z2))))) + ((2 * (Im ((exp ( * z1)) * (exp ( * z2))))) * )) - (((exp (- ( * z1))) * (exp (- ( * z2)))) + ((exp (- ( * z1))) * (exp (- ( * z2)))))) / ((2 * ) * 2) .= (((Re (2 * ((exp ( * z1)) * (exp ( * z2))))) + ((2 * (Im ((exp ( * z1)) * (exp ( * z2))))) * )) - (((exp (- ( * z1))) * (exp (- ( * z2)))) + ((exp (- ( * z1))) * (exp (- ( * z2)))))) / ((2 * ) * 2) by COMSEQ_3:17 .= (((Re (2 * ((exp ( * z1)) * (exp ( * z2))))) + ((Im (2 * ((exp ( * z1)) * (exp ( * z2))))) * )) - (((exp (- ( * z1))) * (exp (- ( * z2)))) + ((exp (- ( * z1))) * (exp (- ( * z2)))))) / ((2 * ) * 2) by COMSEQ_3:17 .= ((2 * ((exp ( * z1)) * (exp ( * z2)))) - (((exp (- ( * z1))) * (exp (- ( * z2)))) + ((exp (- ( * z1))) * (exp (- ( * z2)))))) / ((2 * ) * 2) by COMPLEX1:13 .= ((2 * ((exp ( * z1)) * (exp ( * z2)))) - (((Re ((exp (- ( * z1))) * (exp (- ( * z2))))) + (Re ((exp (- ( * z1))) * (exp (- ( * z2)))))) + (((Im ((exp (- ( * z1))) * (exp (- ( * z2))))) + (Im ((exp (- ( * z1))) * (exp (- ( * z2)))))) * ))) / ((2 * ) * 2) by COMPLEX1:def_5 .= ((2 * ((exp ( * z1)) * (exp ( * z2)))) - ((2 * (Re ((exp (- ( * z1))) * (exp (- ( * z2)))))) + ((2 * (Im ((exp (- ( * z1))) * (exp (- ( * z2)))))) * ))) / ((2 * ) * 2) .= ((2 * ((exp ( * z1)) * (exp ( * z2)))) - ((Re (2 * ((exp (- ( * z1))) * (exp (- ( * z2)))))) + ((2 * (Im ((exp (- ( * z1))) * (exp (- ( * z2)))))) * ))) / ((2 * ) * 2) by COMSEQ_3:17 .= ((2 * ((exp ( * z1)) * (exp ( * z2)))) - ((Re (2 * ((exp (- ( * z1))) * (exp (- ( * z2)))))) + ((Im (2 * ((exp (- ( * z1))) * (exp (- ( * z2)))))) * ))) / ((2 * ) * 2) by COMSEQ_3:17 .= ((2 * ((exp ( * z1)) * (exp ( * z2)))) - (2 * ((exp (- ( * z1))) * (exp (- ( * z2)))))) / ((2 * ) * 2) by COMPLEX1:13 .= (((exp ( * z1)) * (exp ( * z2))) / (2 * )) - ((2 * ((exp (- ( * z1))) * (exp (- ( * z2))))) / ((2 * ) * 2)) .= ((exp (( * z1) + ( * z2))) / (2 * )) - (((exp (- ( * z1))) * (exp (- ( * z2)))) / (2 * )) by SIN_COS:23 .= ((exp ( * (z1 + z2))) / (2 * )) - ((exp ((- ( * z1)) + (- ( * z2)))) / (2 * )) by SIN_COS:23 .= ((exp ( * (z1 + z2))) - (exp (- ( * (z1 + z2))))) / (2 * ) ; then sin_C /. (z1 + z2) = ((sin_C /. z1) * (cos_C /. z2)) + ((cos_C /. z1) * (sin_C /. z2)) by Def1; hence sin_C /. (z1 + z2) = ((sin_C /. z1) * (cos_C /. z2)) + ((cos_C /. z1) * (sin_C /. z2)) ; ::_thesis: verum end; theorem :: SIN_COS3:5 for z1, z2 being Element of COMPLEX holds sin_C /. (z1 - z2) = ((sin_C /. z1) * (cos_C /. z2)) - ((cos_C /. z1) * (sin_C /. z2)) proof let z1, z2 be Element of COMPLEX ; ::_thesis: sin_C /. (z1 - z2) = ((sin_C /. z1) * (cos_C /. z2)) - ((cos_C /. z1) * (sin_C /. z2)) sin_C /. (z1 - z2) = sin_C /. (z1 + (- z2)) .= ((sin_C /. z1) * (cos_C /. (- z2))) + ((cos_C /. z1) * (sin_C /. (- z2))) by Th4 .= ((sin_C /. z1) * (cos_C /. z2)) + ((cos_C /. z1) * (sin_C /. (- z2))) by Th3 .= ((sin_C /. z1) * (cos_C /. z2)) + ((cos_C /. z1) * (- (sin_C /. z2))) by Th2 .= ((sin_C /. z1) * (cos_C /. z2)) + (- ((cos_C /. z1) * (sin_C /. z2))) ; hence sin_C /. (z1 - z2) = ((sin_C /. z1) * (cos_C /. z2)) - ((cos_C /. z1) * (sin_C /. z2)) ; ::_thesis: verum end; theorem Th6: :: SIN_COS3:6 for z1, z2 being complex number holds cos_C /. (z1 + z2) = ((cos_C /. z1) * (cos_C /. z2)) - ((sin_C /. z1) * (sin_C /. z2)) proof let z1, z2 be complex number ; ::_thesis: cos_C /. (z1 + z2) = ((cos_C /. z1) * (cos_C /. z2)) - ((sin_C /. z1) * (sin_C /. z2)) reconsider z1 = z1, z2 = z2 as Element of COMPLEX by XCMPLX_0:def_2; set e1 = exp ( * z1); set e2 = exp (- ( * z1)); set e3 = exp ( * z2); set e4 = exp (- ( * z2)); ((cos_C /. z1) * (cos_C /. z2)) - ((sin_C /. z1) * (sin_C /. z2)) = ((cos_C /. z1) * (cos_C /. z2)) - ((((exp ( * z1)) - (exp (- ( * z1)))) / (2 * )) * (sin_C /. z2)) by Def1 .= ((cos_C /. z1) * (cos_C /. z2)) - ((((exp ( * z1)) - (exp (- ( * z1)))) / (2 * )) * (((exp ( * z2)) - (exp (- ( * z2)))) / (2 * ))) by Def1 .= ((cos_C /. z1) * (((exp ( * z2)) + (exp (- ( * z2)))) / 2)) - ((((exp ( * z1)) - (exp (- ( * z1)))) / (2 * )) * (((exp ( * z2)) - (exp (- ( * z2)))) / (2 * ))) by Def2 .= ((((exp ( * z1)) + (exp (- ( * z1)))) / 2) * (((exp ( * z2)) + (exp (- ( * z2)))) / 2)) - ((((exp ( * z1)) - (exp (- ( * z1)))) / (2 * )) * (((exp ( * z2)) - (exp (- ( * z2)))) / (2 * ))) by Def2 .= ((((exp ( * z1)) * (exp ( * z2))) + ((exp ( * z1)) * (exp ( * z2)))) + (((exp (- ( * z1))) * (exp (- ( * z2)))) + ((exp (- ( * z1))) * (exp (- ( * z2)))))) / (2 * 2) .= ((((Re ((exp ( * z1)) * (exp ( * z2)))) + (Re ((exp ( * z1)) * (exp ( * z2))))) + (((Im ((exp ( * z1)) * (exp ( * z2)))) + (Im ((exp ( * z1)) * (exp ( * z2))))) * )) + (((exp (- ( * z1))) * (exp (- ( * z2)))) + ((exp (- ( * z1))) * (exp (- ( * z2)))))) / (2 * 2) by COMPLEX1:def_5 .= (((2 * (Re ((exp ( * z1)) * (exp ( * z2))))) + ((2 * (Im ((exp ( * z1)) * (exp ( * z2))))) * )) + (((exp (- ( * z1))) * (exp (- ( * z2)))) + ((exp (- ( * z1))) * (exp (- ( * z2)))))) / (2 * 2) .= (((Re (2 * ((exp ( * z1)) * (exp ( * z2))))) + ((2 * (Im ((exp ( * z1)) * (exp ( * z2))))) * )) + (((exp (- ( * z1))) * (exp (- ( * z2)))) + ((exp (- ( * z1))) * (exp (- ( * z2)))))) / (2 * 2) by COMSEQ_3:17 .= (((Re (2 * ((exp ( * z1)) * (exp ( * z2))))) + ((Im (2 * ((exp ( * z1)) * (exp ( * z2))))) * )) + (((exp (- ( * z1))) * (exp (- ( * z2)))) + ((exp (- ( * z1))) * (exp (- ( * z2)))))) / (2 * 2) by COMSEQ_3:17 .= ((2 * ((exp ( * z1)) * (exp ( * z2)))) + (((exp (- ( * z1))) * (exp (- ( * z2)))) + ((exp (- ( * z1))) * (exp (- ( * z2)))))) / (2 * 2) by COMPLEX1:13 .= ((2 * ((exp ( * z1)) * (exp ( * z2)))) + (((Re ((exp (- ( * z1))) * (exp (- ( * z2))))) + (Re ((exp (- ( * z1))) * (exp (- ( * z2)))))) + (((Im ((exp (- ( * z1))) * (exp (- ( * z2))))) + (Im ((exp (- ( * z1))) * (exp (- ( * z2)))))) * ))) / (2 * 2) by COMPLEX1:def_5 .= ((2 * ((exp ( * z1)) * (exp ( * z2)))) + ((2 * (Re ((exp (- ( * z1))) * (exp (- ( * z2)))))) + ((2 * (Im ((exp (- ( * z1))) * (exp (- ( * z2)))))) * ))) / (2 * 2) .= ((2 * ((exp ( * z1)) * (exp ( * z2)))) + ((Re (2 * ((exp (- ( * z1))) * (exp (- ( * z2)))))) + ((2 * (Im ((exp (- ( * z1))) * (exp (- ( * z2)))))) * ))) / (2 * 2) by COMSEQ_3:17 .= ((2 * ((exp ( * z1)) * (exp ( * z2)))) + ((Re (2 * ((exp (- ( * z1))) * (exp (- ( * z2)))))) + ((Im (2 * ((exp (- ( * z1))) * (exp (- ( * z2)))))) * ))) / (2 * 2) by COMSEQ_3:17 .= ((2 * ((exp ( * z1)) * (exp ( * z2)))) + (2 * ((exp (- ( * z1))) * (exp (- ( * z2)))))) / (2 * 2) by COMPLEX1:13 .= (((exp ( * z1)) * (exp ( * z2))) / 2) + ((2 * ((exp (- ( * z1))) * (exp (- ( * z2))))) / (2 * 2)) .= ((exp (( * z1) + ( * z2))) / 2) + (((exp (- ( * z1))) * (exp (- ( * z2)))) / 2) by SIN_COS:23 .= ((exp ( * (z1 + z2))) / 2) + ((exp ((- ( * z1)) + (- ( * z2)))) / 2) by SIN_COS:23 .= ((exp ( * (z1 + z2))) + (exp (- ( * (z1 + z2))))) / 2 ; then cos_C /. (z1 + z2) = ((cos_C /. z1) * (cos_C /. z2)) - ((sin_C /. z1) * (sin_C /. z2)) by Def2; hence cos_C /. (z1 + z2) = ((cos_C /. z1) * (cos_C /. z2)) - ((sin_C /. z1) * (sin_C /. z2)) ; ::_thesis: verum end; theorem :: SIN_COS3:7 for z1, z2 being Element of COMPLEX holds cos_C /. (z1 - z2) = ((cos_C /. z1) * (cos_C /. z2)) + ((sin_C /. z1) * (sin_C /. z2)) proof let z1, z2 be Element of COMPLEX ; ::_thesis: cos_C /. (z1 - z2) = ((cos_C /. z1) * (cos_C /. z2)) + ((sin_C /. z1) * (sin_C /. z2)) cos_C /. (z1 - z2) = cos_C /. (z1 + (- z2)) .= ((cos_C /. z1) * (cos_C /. (- z2))) - ((sin_C /. z1) * (sin_C /. (- z2))) by Th6 .= ((cos_C /. z1) * (cos_C /. z2)) - ((sin_C /. z1) * (sin_C /. (- z2))) by Th3 .= ((cos_C /. z1) * (cos_C /. z2)) - ((sin_C /. z1) * (- (sin_C /. z2))) by Th2 .= ((cos_C /. z1) * (cos_C /. z2)) - (- ((sin_C /. z1) * (sin_C /. z2))) ; hence cos_C /. (z1 - z2) = ((cos_C /. z1) * (cos_C /. z2)) + ((sin_C /. z1) * (sin_C /. z2)) ; ::_thesis: verum end; theorem Th8: :: SIN_COS3:8 for z being Element of COMPLEX holds ((cosh_C /. z) * (cosh_C /. z)) - ((sinh_C /. z) * (sinh_C /. z)) = 1 proof let z be Element of COMPLEX ; ::_thesis: ((cosh_C /. z) * (cosh_C /. z)) - ((sinh_C /. z) * (sinh_C /. z)) = 1 set e1 = exp z; set e2 = exp (- z); ((cosh_C /. z) * (cosh_C /. z)) - ((sinh_C /. z) * (sinh_C /. z)) = ((cosh_C /. z) * (cosh_C /. z)) - ((((exp z) - (exp (- z))) / 2) * (sinh_C /. z)) by Def3 .= ((cosh_C /. z) * (cosh_C /. z)) - ((((exp z) - (exp (- z))) / 2) * (((exp z) - (exp (- z))) / 2)) by Def3 .= ((((exp z) + (exp (- z))) / 2) * (cosh_C /. z)) - ((((exp z) - (exp (- z))) * ((exp z) - (exp (- z)))) / (2 * 2)) by Def4 .= ((((exp z) + (exp (- z))) / 2) * (((exp z) + (exp (- z))) / 2)) - ((((exp z) - (exp (- z))) * ((exp z) - (exp (- z)))) / (2 * 2)) by Def4 .= ((((exp z) * (exp (- z))) + ((exp z) * (exp (- z)))) + (((exp z) * (exp (- z))) + ((exp z) * (exp (- z))))) / (2 * 2) .= ((1 + ((exp z) * (exp (- z)))) + (((exp z) * (exp (- z))) + ((exp z) * (exp (- z))))) / (2 * 2) by Lm3 .= ((1 + 1) + (((exp z) * (exp (- z))) + ((exp z) * (exp (- z))))) / (2 * 2) by Lm3 .= ((1 + 1) + (1 + ((exp z) * (exp (- z))))) / (2 * 2) by Lm3 .= (2 + 2) / (2 * 2) by Lm3 .= 1 ; hence ((cosh_C /. z) * (cosh_C /. z)) - ((sinh_C /. z) * (sinh_C /. z)) = 1 ; ::_thesis: verum end; theorem Th9: :: SIN_COS3:9 for z being Element of COMPLEX holds - (sinh_C /. z) = sinh_C /. (- z) proof let z be Element of COMPLEX ; ::_thesis: - (sinh_C /. z) = sinh_C /. (- z) sinh_C /. (- z) = ((exp (- z)) - (exp (- (- z)))) / 2 by Def3 .= - (((exp z) - (exp (- z))) / 2) ; hence - (sinh_C /. z) = sinh_C /. (- z) by Def3; ::_thesis: verum end; theorem Th10: :: SIN_COS3:10 for z being Element of COMPLEX holds cosh_C /. z = cosh_C /. (- z) proof let z be Element of COMPLEX ; ::_thesis: cosh_C /. z = cosh_C /. (- z) cosh_C /. (- z) = ((exp (- z)) + (exp (- (- z)))) / 2 by Def4 .= ((exp (- z)) + (exp z)) / 2 ; hence cosh_C /. z = cosh_C /. (- z) by Def4; ::_thesis: verum end; theorem Th11: :: SIN_COS3:11 for z1, z2 being Element of COMPLEX holds sinh_C /. (z1 + z2) = ((sinh_C /. z1) * (cosh_C /. z2)) + ((cosh_C /. z1) * (sinh_C /. z2)) proof let z1, z2 be Element of COMPLEX ; ::_thesis: sinh_C /. (z1 + z2) = ((sinh_C /. z1) * (cosh_C /. z2)) + ((cosh_C /. z1) * (sinh_C /. z2)) set e1 = exp z1; set e2 = exp (- z1); set e3 = exp z2; set e4 = exp (- z2); ((sinh_C /. z1) * (cosh_C /. z2)) + ((cosh_C /. z1) * (sinh_C /. z2)) = ((((exp z1) - (exp (- z1))) / 2) * (cosh_C /. z2)) + ((cosh_C /. z1) * (sinh_C /. z2)) by Def3 .= ((((exp z1) - (exp (- z1))) / 2) * (cosh_C /. z2)) + ((cosh_C /. z1) * (((exp z2) - (exp (- z2))) / 2)) by Def3 .= ((((exp z1) - (exp (- z1))) / 2) * (cosh_C /. z2)) + ((((exp z1) + (exp (- z1))) / 2) * (((exp z2) - (exp (- z2))) / 2)) by Def4 .= ((((exp z1) - (exp (- z1))) / 2) * (((exp z2) + (exp (- z2))) / 2)) + ((((exp z1) + (exp (- z1))) / 2) * (((exp z2) - (exp (- z2))) / 2)) by Def4 .= ((((exp z1) * (exp z2)) + ((exp z1) * (exp z2))) - (((exp (- z1)) * (exp (- z2))) + ((exp (- z1)) * (exp (- z2))))) / 4 .= ((((Re ((exp z1) * (exp z2))) + (Re ((exp z1) * (exp z2)))) + (((Im ((exp z1) * (exp z2))) + (Im ((exp z1) * (exp z2)))) * )) - (((exp (- z1)) * (exp (- z2))) + ((exp (- z1)) * (exp (- z2))))) / 4 by COMPLEX1:def_5 .= (((2 * (Re ((exp z1) * (exp z2)))) + ((2 * (Im ((exp z1) * (exp z2)))) * )) - (((exp (- z1)) * (exp (- z2))) + ((exp (- z1)) * (exp (- z2))))) / 4 .= (((Re (2 * ((exp z1) * (exp z2)))) + ((2 * (Im ((exp z1) * (exp z2)))) * )) - (((exp (- z1)) * (exp (- z2))) + ((exp (- z1)) * (exp (- z2))))) / 4 by COMSEQ_3:17 .= (((Re (2 * ((exp z1) * (exp z2)))) + ((Im (2 * ((exp z1) * (exp z2)))) * )) - (((exp (- z1)) * (exp (- z2))) + ((exp (- z1)) * (exp (- z2))))) / 4 by COMSEQ_3:17 .= ((2 * ((exp z1) * (exp z2))) - (((exp (- z1)) * (exp (- z2))) + ((exp (- z1)) * (exp (- z2))))) / 4 by COMPLEX1:13 .= ((2 * ((exp z1) * (exp z2))) - (((Re ((exp (- z1)) * (exp (- z2)))) + (Re ((exp (- z1)) * (exp (- z2))))) + (((Im ((exp (- z1)) * (exp (- z2)))) + (Im ((exp (- z1)) * (exp (- z2))))) * ))) / 4 by COMPLEX1:def_5 .= ((2 * ((exp z1) * (exp z2))) - ((2 * (Re ((exp (- z1)) * (exp (- z2))))) + ((2 * (Im ((exp (- z1)) * (exp (- z2))))) * ))) / 4 .= ((2 * ((exp z1) * (exp z2))) - ((Re (2 * ((exp (- z1)) * (exp (- z2))))) + ((2 * (Im ((exp (- z1)) * (exp (- z2))))) * ))) / 4 by COMSEQ_3:17 .= ((2 * ((exp z1) * (exp z2))) - ((Re (2 * ((exp (- z1)) * (exp (- z2))))) + ((Im (2 * ((exp (- z1)) * (exp (- z2))))) * ))) / 4 by COMSEQ_3:17 .= ((2 * ((exp z1) * (exp z2))) - (2 * ((exp (- z1)) * (exp (- z2))))) / 4 by COMPLEX1:13 .= (((exp z1) * (exp z2)) / 2) - ((2 * ((exp (- z1)) * (exp (- z2)))) / (2 * 2)) .= ((exp (z1 + z2)) / 2) - (((exp (- z1)) * (exp (- z2))) / 2) by SIN_COS:23 .= ((exp (z1 + z2)) / 2) - ((exp ((- z1) + (- z2))) / 2) by SIN_COS:23 .= ((exp (z1 + z2)) - (exp (- (z1 + z2)))) / 2 ; hence sinh_C /. (z1 + z2) = ((sinh_C /. z1) * (cosh_C /. z2)) + ((cosh_C /. z1) * (sinh_C /. z2)) by Def3; ::_thesis: verum end; theorem Th12: :: SIN_COS3:12 for z1, z2 being Element of COMPLEX holds sinh_C /. (z1 - z2) = ((sinh_C /. z1) * (cosh_C /. z2)) - ((cosh_C /. z1) * (sinh_C /. z2)) proof let z1, z2 be Element of COMPLEX ; ::_thesis: sinh_C /. (z1 - z2) = ((sinh_C /. z1) * (cosh_C /. z2)) - ((cosh_C /. z1) * (sinh_C /. z2)) sinh_C /. (z1 - z2) = sinh_C /. (z1 + (- z2)) .= ((sinh_C /. z1) * (cosh_C /. (- z2))) + ((cosh_C /. z1) * (sinh_C /. (- z2))) by Th11 .= ((sinh_C /. z1) * (cosh_C /. z2)) + ((cosh_C /. z1) * (sinh_C /. (- z2))) by Th10 .= ((sinh_C /. z1) * (cosh_C /. z2)) + ((cosh_C /. z1) * (- (sinh_C /. z2))) by Th9 .= ((sinh_C /. z1) * (cosh_C /. z2)) + (- ((cosh_C /. z1) * (sinh_C /. z2))) ; hence sinh_C /. (z1 - z2) = ((sinh_C /. z1) * (cosh_C /. z2)) - ((cosh_C /. z1) * (sinh_C /. z2)) ; ::_thesis: verum end; theorem Th13: :: SIN_COS3:13 for z1, z2 being Element of COMPLEX holds cosh_C /. (z1 - z2) = ((cosh_C /. z1) * (cosh_C /. z2)) - ((sinh_C /. z1) * (sinh_C /. z2)) proof let z1, z2 be Element of COMPLEX ; ::_thesis: cosh_C /. (z1 - z2) = ((cosh_C /. z1) * (cosh_C /. z2)) - ((sinh_C /. z1) * (sinh_C /. z2)) set e1 = exp z1; set e2 = exp (- z1); set e3 = exp z2; set e4 = exp (- z2); ((cosh_C /. z1) * (cosh_C /. z2)) - ((sinh_C /. z1) * (sinh_C /. z2)) = ((((exp z1) + (exp (- z1))) / 2) * (cosh_C /. z2)) - ((sinh_C /. z1) * (sinh_C /. z2)) by Def4 .= ((((exp z1) + (exp (- z1))) / 2) * (((exp z2) + (exp (- z2))) / 2)) - ((sinh_C /. z1) * (sinh_C /. z2)) by Def4 .= ((((exp z1) + (exp (- z1))) * ((exp z2) + (exp (- z2)))) / (2 * 2)) - ((((exp z1) - (exp (- z1))) / 2) * (sinh_C /. z2)) by Def3 .= ((((exp z1) + (exp (- z1))) * ((exp z2) + (exp (- z2)))) / (2 * 2)) - ((((exp z1) - (exp (- z1))) / 2) * (((exp z2) - (exp (- z2))) / 2)) by Def3 .= ((((exp (- z1)) * (exp z2)) + ((exp (- z1)) * (exp z2))) + ((((exp z1) * (exp (- z2))) + ((exp (- z1)) * (exp (- z2)))) + (((exp z1) * (exp (- z2))) - ((exp (- z1)) * (exp (- z2)))))) / (2 * 2) .= ((((Re ((exp (- z1)) * (exp z2))) + (Re ((exp (- z1)) * (exp z2)))) + (((Im ((exp (- z1)) * (exp z2))) + (Im ((exp (- z1)) * (exp z2)))) * )) + (((exp z1) * (exp (- z2))) + ((exp z1) * (exp (- z2))))) / (2 * 2) by COMPLEX1:def_5 .= (((2 * (Re ((exp (- z1)) * (exp z2)))) + ((2 * (Im ((exp (- z1)) * (exp z2)))) * )) + (((exp z1) * (exp (- z2))) + ((exp z1) * (exp (- z2))))) / (2 * 2) .= (((Re (2 * ((exp (- z1)) * (exp z2)))) + ((2 * (Im ((exp (- z1)) * (exp z2)))) * )) + (((exp z1) * (exp (- z2))) + ((exp z1) * (exp (- z2))))) / (2 * 2) by COMSEQ_3:17 .= (((Re (2 * ((exp (- z1)) * (exp z2)))) + ((Im (2 * ((exp (- z1)) * (exp z2)))) * )) + (((exp z1) * (exp (- z2))) + ((exp z1) * (exp (- z2))))) / (2 * 2) by COMSEQ_3:17 .= ((2 * ((exp (- z1)) * (exp z2))) + (((exp z1) * (exp (- z2))) + ((exp z1) * (exp (- z2))))) / (2 * 2) by COMPLEX1:13 .= ((2 * ((exp (- z1)) * (exp z2))) + (((Re ((exp z1) * (exp (- z2)))) + (Re ((exp z1) * (exp (- z2))))) + (((Im ((exp z1) * (exp (- z2)))) + (Im ((exp z1) * (exp (- z2))))) * ))) / (2 * 2) by COMPLEX1:def_5 .= ((2 * ((exp (- z1)) * (exp z2))) + ((2 * (Re ((exp z1) * (exp (- z2))))) + ((2 * (Im ((exp z1) * (exp (- z2))))) * ))) / (2 * 2) .= ((2 * ((exp (- z1)) * (exp z2))) + ((Re (2 * ((exp z1) * (exp (- z2))))) + ((2 * (Im ((exp z1) * (exp (- z2))))) * ))) / (2 * 2) by COMSEQ_3:17 .= ((2 * ((exp (- z1)) * (exp z2))) + ((Re (2 * ((exp z1) * (exp (- z2))))) + ((Im (2 * ((exp z1) * (exp (- z2))))) * ))) / (2 * 2) by COMSEQ_3:17 .= ((2 * ((exp (- z1)) * (exp z2))) + (2 * ((exp z1) * (exp (- z2))))) / (2 * 2) by COMPLEX1:13 .= (((exp z1) * (exp (- z2))) / 2) + ((2 * ((exp (- z1)) * (exp z2))) / (2 * 2)) .= ((exp (z1 + (- z2))) / 2) + (((exp (- z1)) * (exp z2)) / 2) by SIN_COS:23 .= ((exp (z1 - z2)) / 2) + ((exp ((- z1) + z2)) / 2) by SIN_COS:23 .= ((exp (z1 - z2)) + (exp (- (z1 - z2)))) / 2 ; hence cosh_C /. (z1 - z2) = ((cosh_C /. z1) * (cosh_C /. z2)) - ((sinh_C /. z1) * (sinh_C /. z2)) by Def4; ::_thesis: verum end; theorem Th14: :: SIN_COS3:14 for z1, z2 being Element of COMPLEX holds cosh_C /. (z1 + z2) = ((cosh_C /. z1) * (cosh_C /. z2)) + ((sinh_C /. z1) * (sinh_C /. z2)) proof let z1, z2 be Element of COMPLEX ; ::_thesis: cosh_C /. (z1 + z2) = ((cosh_C /. z1) * (cosh_C /. z2)) + ((sinh_C /. z1) * (sinh_C /. z2)) cosh_C /. (z1 + z2) = cosh_C /. (z1 - (- z2)) .= ((cosh_C /. z1) * (cosh_C /. (- z2))) - ((sinh_C /. z1) * (sinh_C /. (- z2))) by Th13 .= ((cosh_C /. z1) * (cosh_C /. z2)) - ((sinh_C /. z1) * (sinh_C /. (- z2))) by Th10 .= ((cosh_C /. z1) * (cosh_C /. z2)) - ((sinh_C /. z1) * (- (sinh_C /. z2))) by Th9 .= ((cosh_C /. z1) * (cosh_C /. z2)) - (- ((sinh_C /. z1) * (sinh_C /. z2))) ; hence cosh_C /. (z1 + z2) = ((cosh_C /. z1) * (cosh_C /. z2)) + ((sinh_C /. z1) * (sinh_C /. z2)) ; ::_thesis: verum end; theorem Th15: :: SIN_COS3:15 for z being complex number holds sin_C /. ( * z) = * (sinh_C /. z) proof let z be complex number ; ::_thesis: sin_C /. ( * z) = * (sinh_C /. z) reconsider z = z as Element of COMPLEX by XCMPLX_0:def_2; sin_C /. ( * z) = ((exp (( * ) * z)) - (exp (- ( * ( * z))))) / ( * 2) by Def1 .= * (((exp z) - (exp (- z))) / 2) ; then sin_C /. ( * z) = * (sinh_C /. z) by Def3; hence sin_C /. ( * z) = * (sinh_C /. z) ; ::_thesis: verum end; theorem Th16: :: SIN_COS3:16 for z being complex number holds cos_C /. ( * z) = cosh_C /. z proof let z be complex number ; ::_thesis: cos_C /. ( * z) = cosh_C /. z reconsider z = z as Element of COMPLEX by XCMPLX_0:def_2; cos_C /. ( * z) = ((exp (( * ) * z)) + (exp (- ( * ( * z))))) / 2 by Def2 .= ((exp (- z)) + (exp z)) / 2 ; then cos_C /. ( * z) = cosh_C /. z by Def4; hence cos_C /. ( * z) = cosh_C /. z ; ::_thesis: verum end; theorem Th17: :: SIN_COS3:17 for z being complex number holds sinh_C /. ( * z) = * (sin_C /. z) proof let z be complex number ; ::_thesis: sinh_C /. ( * z) = * (sin_C /. z) reconsider z = z as Element of COMPLEX by XCMPLX_0:def_2; sinh_C /. ( * z) = ((exp ( * z)) - (exp (- ( * z)))) / 2 by Def3 .= * (((exp ( * z)) - (exp (- ( * z)))) / ( * 2)) ; then sinh_C /. ( * z) = * (sin_C /. z) by Def1; hence sinh_C /. ( * z) = * (sin_C /. z) ; ::_thesis: verum end; theorem Th18: :: SIN_COS3:18 for z being complex number holds cosh_C /. ( * z) = cos_C /. z proof let z be complex number ; ::_thesis: cosh_C /. ( * z) = cos_C /. z reconsider z = z as Element of COMPLEX by XCMPLX_0:def_2; cosh_C /. ( * z) = ((exp ( * z)) + (exp (- ( * z)))) / 2 by Def4; then cosh_C /. ( * z) = cos_C /. z by Def2; hence cosh_C /. ( * z) = cos_C /. z ; ::_thesis: verum end; Lm4: for x, y being Element of REAL holds exp (x + (y * )) = (exp_R x) * ((cos y) + ((sin y) * )) proof let x, y be Element of REAL ; ::_thesis: exp (x + (y * )) = (exp_R x) * ((cos y) + ((sin y) * )) exp (x + (y * )) = (exp x) * (exp (y * )) by SIN_COS:23 .= (exp_R x) * (exp (y * )) by SIN_COS:49 .= (exp_R x) * ((cos y) + ((sin y) * )) by SIN_COS:25 ; hence exp (x + (y * )) = (exp_R x) * ((cos y) + ((sin y) * )) ; ::_thesis: verum end; theorem Th19: :: SIN_COS3:19 for x, y being Element of REAL holds exp (x + (y * )) = ((exp_R . x) * (cos . y)) + (((exp_R . x) * (sin . y)) * ) proof let x, y be Element of REAL ; ::_thesis: exp (x + (y * )) = ((exp_R . x) * (cos . y)) + (((exp_R . x) * (sin . y)) * ) exp (x + (y * )) = (exp_R x) * ((cos y) + ((sin y) * )) by Lm4 .= (((exp_R x) * (cos y)) - (0 * (sin y))) + ((((exp_R x) * (sin y)) + ((cos y) * 0)) * ) .= ((exp_R x) * (cos . y)) + (((exp_R x) * (sin y)) * ) by SIN_COS:def_19 .= ((exp_R . x) * (cos . y)) + (((exp_R x) * (sin y)) * ) by SIN_COS:def_23 .= ((exp_R . x) * (cos . y)) + (((exp_R . x) * (sin y)) * ) by SIN_COS:def_23 ; hence exp (x + (y * )) = ((exp_R . x) * (cos . y)) + (((exp_R . x) * (sin . y)) * ) by SIN_COS:def_17; ::_thesis: verum end; theorem :: SIN_COS3:20 exp 0c = 1 by SIN_COS:49, SIN_COS:51; theorem Th21: :: SIN_COS3:21 sin_C /. 0c = 0 proof sin_C /. 0c = ((exp 0c) - (exp (- ( * 0c)))) / ( * 2) by Def1 .= 0c / ( * 2) ; hence sin_C /. 0c = 0 ; ::_thesis: verum end; theorem :: SIN_COS3:22 sinh_C /. 0c = 0 proof sinh_C /. 0c = ((exp 0c) - (exp (- 0c))) / 2 by Def3 .= 0c / 2 ; hence sinh_C /. 0c = 0 ; ::_thesis: verum end; theorem Th23: :: SIN_COS3:23 cos_C /. 0c = 1 proof cos_C /. 0c = ((exp 0c) + (exp (- ( * 0c)))) / 2 by Def2 .= 1 by SIN_COS:49, SIN_COS:51 ; hence cos_C /. 0c = 1 ; ::_thesis: verum end; theorem :: SIN_COS3:24 cosh_C /. 0c = 1 proof cosh_C /. 0c = ((exp 0c) + (exp (- 0c))) / 2 by Def4 .= 1 by SIN_COS:49, SIN_COS:51 ; hence cosh_C /. 0c = 1 ; ::_thesis: verum end; theorem :: SIN_COS3:25 for z being Element of COMPLEX holds exp z = (cosh_C /. z) + (sinh_C /. z) proof let z be Element of COMPLEX ; ::_thesis: exp z = (cosh_C /. z) + (sinh_C /. z) (cosh_C /. z) + (sinh_C /. z) = (((exp z) + (exp (- z))) / 2) + (sinh_C /. z) by Def4 .= (((exp z) + (exp (- z))) / 2) + (((exp z) - (exp (- z))) / 2) by Def3 .= ((exp z) + (((exp (- z)) + (exp z)) - (exp (- z)))) / 2 .= (((Re (exp z)) + (Re (exp z))) + (((Im (exp z)) + (Im (exp z))) * )) / 2 by COMPLEX1:def_5 .= ((2 * (Re (exp z))) + ((2 * (Im (exp z))) * )) / 2 .= ((Re (2 * (exp z))) + ((2 * (Im (exp z))) * )) / 2 by COMSEQ_3:17 .= ((Re (2 * (exp z))) + ((Im (2 * (exp z))) * )) / 2 by COMSEQ_3:17 .= (2 * (exp z)) / 2 by COMPLEX1:13 .= (exp z) * 1 ; hence exp z = (cosh_C /. z) + (sinh_C /. z) ; ::_thesis: verum end; theorem :: SIN_COS3:26 for z being Element of COMPLEX holds exp (- z) = (cosh_C /. z) - (sinh_C /. z) proof let z be Element of COMPLEX ; ::_thesis: exp (- z) = (cosh_C /. z) - (sinh_C /. z) (cosh_C /. z) - (sinh_C /. z) = (((exp z) + (exp (- z))) / 2) - (sinh_C /. z) by Def4 .= (((exp z) + (exp (- z))) / 2) - (((exp z) - (exp (- z))) / 2) by Def3 .= ((exp (- z)) + (exp (- z))) / 2 .= (((Re (exp (- z))) + (Re (exp (- z)))) + (((Im (exp (- z))) + (Im (exp (- z)))) * )) / 2 by COMPLEX1:def_5 .= ((2 * (Re (exp (- z)))) + ((2 * (Im (exp (- z)))) * )) / 2 .= ((Re (2 * (exp (- z)))) + ((2 * (Im (exp (- z)))) * )) / 2 by COMSEQ_3:17 .= ((Re (2 * (exp (- z)))) + ((Im (2 * (exp (- z)))) * )) / 2 by COMSEQ_3:17 .= (2 * (exp (- z))) / 2 by COMPLEX1:13 .= (exp (- z)) * 1 ; hence exp (- z) = (cosh_C /. z) - (sinh_C /. z) ; ::_thesis: verum end; theorem :: SIN_COS3:27 for z being Element of COMPLEX holds exp (z + ((2 * PI) * )) = exp z proof let z be Element of COMPLEX ; ::_thesis: exp (z + ((2 * PI) * )) = exp z z + ((2 * PI) * ) = ((Re z) + ((Im z) * )) + (((2 * PI) + (0 * )) * ) by COMPLEX1:13 .= ((Re z) + 0) + (((Im z) + (2 * PI)) * ) ; then exp (z + ((2 * PI) * )) = ((exp_R . (Re z)) * (cos . ((Im z) + ((2 * PI) * 1)))) + (((exp_R . (Re z)) * (sin . ((Im z) + (2 * PI)))) * ) by Th19 .= ((exp_R . (Re z)) * (cos . (Im z))) + (((exp_R . (Re z)) * (sin . ((Im z) + ((2 * PI) * 1)))) * ) by SIN_COS2:11 .= ((exp_R . (Re z)) * (cos . (Im z))) + (((exp_R . (Re z)) * (sin . (Im z))) * ) by SIN_COS2:10 .= exp ((Re z) + ((Im z) * )) by Th19 ; hence exp (z + ((2 * PI) * )) = exp z by COMPLEX1:13; ::_thesis: verum end; theorem Th28: :: SIN_COS3:28 for n being Element of NAT holds exp (((2 * PI) * n) * ) = 1 proof let n be Element of NAT ; ::_thesis: exp (((2 * PI) * n) * ) = 1 thus exp (((2 * PI) * n) * ) = (cos (0 + ((2 * PI) * n))) + ((sin (0 + ((2 * PI) * n))) * ) by SIN_COS:25 .= (cos . (0 + ((2 * PI) * n))) + ((sin (0 + ((2 * PI) * n))) * ) by SIN_COS:def_19 .= (cos . (0 + ((2 * PI) * n))) + ((sin . (0 + ((2 * PI) * n))) * ) by SIN_COS:def_17 .= (cos . (0 + ((2 * PI) * n))) + ((sin . 0) * ) by SIN_COS2:10 .= 1 by SIN_COS:30, SIN_COS2:11 ; ::_thesis: verum end; theorem Th29: :: SIN_COS3:29 for n being Element of NAT holds exp ((- ((2 * PI) * n)) * ) = 1 proof let n be Element of NAT ; ::_thesis: exp ((- ((2 * PI) * n)) * ) = 1 thus exp ((- ((2 * PI) * n)) * ) = (cos (- ((2 * PI) * n))) + ((sin (- ((2 * PI) * n))) * ) by SIN_COS:25 .= (cos ((2 * PI) * n)) + ((sin (- ((2 * PI) * n))) * ) by SIN_COS:31 .= (cos (0 + ((2 * PI) * n))) + ((- (sin ((2 * PI) * n))) * ) by SIN_COS:31 .= (cos . (0 + ((2 * PI) * n))) + (- ((sin (0 + ((2 * PI) * n))) * )) by SIN_COS:def_19 .= (cos . (0 + ((2 * PI) * n))) + (- ((sin . (0 + ((2 * PI) * n))) * )) by SIN_COS:def_17 .= (cos . (0 + ((2 * PI) * n))) + (- ((sin . 0) * )) by SIN_COS2:10 .= 1 by SIN_COS:30, SIN_COS2:11 ; ::_thesis: verum end; theorem :: SIN_COS3:30 for n being Element of NAT holds exp ((((2 * n) + 1) * PI) * ) = - 1 proof let n be Element of NAT ; ::_thesis: exp ((((2 * n) + 1) * PI) * ) = - 1 exp ((((2 * n) + 1) * PI) * ) = (cos (((PI * 2) * n) + PI)) + ((sin ((PI * (2 * n)) + (1 * PI))) * ) by SIN_COS:25 .= (cos . (((PI * 2) * n) + PI)) + ((sin (((PI * 2) * n) + PI)) * ) by SIN_COS:def_19 .= (cos . (((PI * 2) * n) + PI)) + ((sin . (((PI * 2) * n) + PI)) * ) by SIN_COS:def_17 .= (cos . PI) + ((sin . (((PI * 2) * n) + PI)) * ) by SIN_COS2:11 .= (- 1) + ((sin . PI) * ) by SIN_COS:76, SIN_COS2:10 ; hence exp ((((2 * n) + 1) * PI) * ) = - 1 by SIN_COS:76; ::_thesis: verum end; theorem :: SIN_COS3:31 for n being Element of NAT holds exp ((- (((2 * n) + 1) * PI)) * ) = - 1 proof let n be Element of NAT ; ::_thesis: exp ((- (((2 * n) + 1) * PI)) * ) = - 1 exp ((- (((2 * n) + 1) * PI)) * ) = (cos (- (((2 * n) + 1) * PI))) + ((sin (- (((2 * n) + 1) * PI))) * ) by SIN_COS:25 .= (cos (((2 * n) + 1) * PI)) + ((sin (- (((2 * n) + 1) * PI))) * ) by SIN_COS:31 .= (cos (((PI * 2) * n) + PI)) + ((- (sin ((PI * (2 * n)) + PI))) * ) by SIN_COS:31 .= (cos . (((PI * 2) * n) + PI)) + (- ((sin (((PI * 2) * n) + PI)) * )) by SIN_COS:def_19 .= (cos . (((PI * 2) * n) + PI)) + (- ((sin . (((PI * 2) * n) + PI)) * )) by SIN_COS:def_17 .= (cos . PI) + (- ((sin . (((PI * 2) * n) + PI)) * )) by SIN_COS2:11 .= (- 1) + (- ((sin . PI) * )) by SIN_COS:76, SIN_COS2:10 ; hence exp ((- (((2 * n) + 1) * PI)) * ) = - 1 by SIN_COS:76; ::_thesis: verum end; theorem :: SIN_COS3:32 for n being Element of NAT holds exp ((((2 * n) + (1 / 2)) * PI) * ) = proof let n be Element of NAT ; ::_thesis: exp ((((2 * n) + (1 / 2)) * PI) * ) = exp ((((2 * n) + (1 / 2)) * PI) * ) = (cos (((PI * 2) * n) + ((1 / 2) * PI))) + ((sin ((PI * (2 * n)) + ((1 / 2) * PI))) * ) by SIN_COS:25 .= (cos . (((PI * 2) * n) + ((1 / 2) * PI))) + ((sin (((PI * 2) * n) + ((1 / 2) * PI))) * ) by SIN_COS:def_19 .= (cos . (((PI * 2) * n) + ((1 / 2) * PI))) + ((sin . (((PI * 2) * n) + ((1 / 2) * PI))) * ) by SIN_COS:def_17 .= (cos . ((1 / 2) * PI)) + ((sin . (((PI * 2) * n) + ((1 / 2) * PI))) * ) by SIN_COS2:11 .= (sin . (PI / 2)) * by SIN_COS:76, SIN_COS2:10 ; hence exp ((((2 * n) + (1 / 2)) * PI) * ) = by SIN_COS:76; ::_thesis: verum end; theorem :: SIN_COS3:33 for n being Element of NAT holds exp ((- (((2 * n) + (1 / 2)) * PI)) * ) = - (1 * ) proof let n be Element of NAT ; ::_thesis: exp ((- (((2 * n) + (1 / 2)) * PI)) * ) = - (1 * ) exp ((- (((2 * n) + (1 / 2)) * PI)) * ) = (cos (- (((2 * n) + (1 / 2)) * PI))) + ((sin (- (((2 * n) + (1 / 2)) * PI))) * ) by SIN_COS:25 .= (cos (((2 * n) + (1 / 2)) * PI)) + ((sin (- (((2 * n) + (1 / 2)) * PI))) * ) by SIN_COS:31 .= (cos (((PI * 2) * n) + ((1 / 2) * PI))) + ((- (sin ((PI * (2 * n)) + ((1 / 2) * PI)))) * ) by SIN_COS:31 .= (cos . (((PI * 2) * n) + ((1 / 2) * PI))) + (- ((sin (((PI * 2) * n) + ((1 / 2) * PI))) * )) by SIN_COS:def_19 .= (cos . (((PI * 2) * n) + ((1 / 2) * PI))) + (- ((sin . (((PI * 2) * n) + ((1 / 2) * PI))) * )) by SIN_COS:def_17 .= (cos . ((1 / 2) * PI)) + ((- (sin . (((PI * 2) * n) + ((1 / 2) * PI)))) * ) by SIN_COS2:11 .= (- (sin . (PI / 2))) * by SIN_COS:76, SIN_COS2:10 ; hence exp ((- (((2 * n) + (1 / 2)) * PI)) * ) = - (1 * ) by SIN_COS:76; ::_thesis: verum end; theorem :: SIN_COS3:34 for z being Element of COMPLEX for n being Element of NAT holds sin_C /. (z + ((2 * n) * PI)) = sin_C /. z proof let z be Element of COMPLEX ; ::_thesis: for n being Element of NAT holds sin_C /. (z + ((2 * n) * PI)) = sin_C /. z let n be Element of NAT ; ::_thesis: sin_C /. (z + ((2 * n) * PI)) = sin_C /. z sin_C /. (z + ((2 * n) * PI)) = ((exp (( * z) + ( * ((2 * n) * PI)))) - (exp (- ( * (z + ((2 * n) * PI)))))) / (2 * ) by Def1 .= (((exp ( * z)) * (exp (((2 * PI) * n) * ))) - (exp (- ( * (z + ((2 * n) * PI)))))) / (2 * ) by SIN_COS:23 .= (((exp ( * z)) * 1) - (exp (- ( * (z + ((2 * n) * PI)))))) / (2 * ) by Th28 .= ((exp ( * z)) - (exp (((- ) * z) + ((- ) * ((2 * n) * PI))))) / (2 * ) .= ((exp ( * z)) - ((exp ((- ) * z)) * (exp ((- ((2 * PI) * n)) * )))) / (2 * ) by SIN_COS:23 .= ((exp ( * z)) - ((exp ((- ) * z)) * 1)) / (2 * ) by Th29 .= ((exp ( * z)) - (exp (- ( * z)))) / (2 * ) ; hence sin_C /. (z + ((2 * n) * PI)) = sin_C /. z by Def1; ::_thesis: verum end; theorem :: SIN_COS3:35 for z being Element of COMPLEX for n being Element of NAT holds cos_C /. (z + ((2 * n) * PI)) = cos_C /. z proof let z be Element of COMPLEX ; ::_thesis: for n being Element of NAT holds cos_C /. (z + ((2 * n) * PI)) = cos_C /. z let n be Element of NAT ; ::_thesis: cos_C /. (z + ((2 * n) * PI)) = cos_C /. z cos_C /. (z + ((2 * n) * PI)) = ((exp (( * z) + ( * ((2 * n) * PI)))) + (exp (- ( * (z + ((2 * n) * PI)))))) / 2 by Def2 .= (((exp ( * z)) * (exp (((2 * PI) * n) * ))) + (exp (- ( * (z + ((2 * n) * PI)))))) / 2 by SIN_COS:23 .= (((exp ( * z)) * 1) + (exp (- ( * (z + ((2 * n) * PI)))))) / 2 by Th28 .= ((exp ( * z)) + (exp (((- ) * z) + ((- ) * ((2 * n) * PI))))) / 2 .= ((exp ( * z)) + ((exp ((- ) * z)) * (exp ((- ((2 * PI) * n)) * )))) / 2 by SIN_COS:23 .= (((exp ( * z)) * 1) + ((exp (- ( * z))) * 1)) / 2 by Th29 .= ((exp ( * z)) + (exp (- ( * z)))) / 2 ; hence cos_C /. (z + ((2 * n) * PI)) = cos_C /. z by Def2; ::_thesis: verum end; theorem Th36: :: SIN_COS3:36 for z being complex number holds exp ( * z) = (cos_C /. z) + ( * (sin_C /. z)) proof let z be complex number ; ::_thesis: exp ( * z) = (cos_C /. z) + ( * (sin_C /. z)) reconsider z = z as Element of COMPLEX by XCMPLX_0:def_2; (cos_C /. z) + ( * (sin_C /. z)) = (((exp ( * z)) + (exp (- ( * z)))) / 2) + ( * (sin_C /. z)) by Def2 .= (((exp ( * z)) + (exp (- ( * z)))) / 2) + ( * (((exp ( * z)) - (exp (- ( * z)))) / (2 * ))) by Def1 .= ((exp ( * z)) + (((exp (- ( * z))) + (exp ( * z))) - (exp (- ( * z))))) / 2 .= (((Re (exp ( * z))) + (Re (exp ( * z)))) + (((Im (exp ( * z))) + (Im (exp ( * z)))) * )) / 2 by COMPLEX1:def_5 .= ((2 * (Re (exp ( * z)))) + ((2 * (Im (exp ( * z)))) * )) / 2 .= ((Re (2 * (exp ( * z)))) + ((2 * (Im (exp ( * z)))) * )) / 2 by COMSEQ_3:17 .= ((Re (2 * (exp ( * z)))) + ((Im (2 * (exp ( * z)))) * )) / 2 by COMSEQ_3:17 .= (2 * (exp ( * z))) / 2 by COMPLEX1:13 ; hence exp ( * z) = (cos_C /. z) + ( * (sin_C /. z)) ; ::_thesis: verum end; theorem Th37: :: SIN_COS3:37 for z being complex number holds exp (- ( * z)) = (cos_C /. z) - ( * (sin_C /. z)) proof let z be complex number ; ::_thesis: exp (- ( * z)) = (cos_C /. z) - ( * (sin_C /. z)) reconsider z = z as Element of COMPLEX by XCMPLX_0:def_2; (cos_C /. z) - ( * (sin_C /. z)) = (((exp ( * z)) + (exp (- ( * z)))) / 2) - ( * (sin_C /. z)) by Def2 .= (((exp ( * z)) + (exp (- ( * z)))) / 2) - ( * (((exp ( * z)) - (exp (- ( * z)))) / (2 * ))) by Def1 .= ((exp (- ( * z))) + (exp (- ( * z)))) / 2 .= (((Re (exp (- ( * z)))) + (Re (exp (- ( * z))))) + (((Im (exp (- ( * z)))) + (Im (exp (- ( * z))))) * )) / 2 by COMPLEX1:def_5 .= ((2 * (Re (exp (- ( * z))))) + ((2 * (Im (exp (- ( * z))))) * )) / 2 .= ((Re (2 * (exp (- ( * z))))) + ((2 * (Im (exp (- ( * z))))) * )) / 2 by COMSEQ_3:17 .= ((Re (2 * (exp (- ( * z))))) + ((Im (2 * (exp (- ( * z))))) * )) / 2 by COMSEQ_3:17 .= (2 * (exp (- ( * z)))) / 2 by COMPLEX1:13 ; hence exp (- ( * z)) = (cos_C /. z) - ( * (sin_C /. z)) ; ::_thesis: verum end; theorem Th38: :: SIN_COS3:38 for x being Element of REAL holds sin_C /. x = sin . x proof let x be Element of REAL ; ::_thesis: sin_C /. x = sin . x x in REAL ; then reconsider z = x as Element of COMPLEX by NUMBERS:11; sin_C /. x = sin_C /. z .= ((exp ((- 0) + (x * ))) - (exp (- ( * x)))) / (2 * ) by Def1 .= ((((exp_R . 0) * (cos . x)) + (((exp_R . 0) * (sin . x)) * )) - (exp (- (x * )))) / (2 * ) by Th19 .= ((((exp_R 0) * (cos . x)) + (((exp_R . 0) * (sin . x)) * )) - (exp (- (x * )))) / (2 * ) by SIN_COS:def_23 .= ((((exp_R 0) * (cos . x)) + (((exp_R 0) * (sin . x)) * )) - (exp (- (x * )))) / (2 * ) by SIN_COS:def_23 .= (((cos . x) + ((sin . x) * )) - (exp (0 + ((- x) * )))) / (2 * ) by SIN_COS:51 .= (((cos . x) + ((sin . x) * )) - (((exp_R . 0) * (cos . (- x))) + (((exp_R . 0) * (sin . (- x))) * ))) / (2 * ) by Th19 .= (((cos . x) + ((sin . x) * )) - (((exp_R 0) * (cos . (- x))) + (((exp_R . 0) * (sin . (- x))) * ))) / (2 * ) by SIN_COS:def_23 .= (((cos . x) + ((sin . x) * )) - ((1 * (cos . (- x))) + ((1 * (sin . (- x))) * ))) / (2 * ) by SIN_COS:51, SIN_COS:def_23 .= (((cos . x) + ((sin . x) * )) - ((cos . (- x)) + ((- (sin . x)) * ))) / (2 * ) by SIN_COS:30 .= (((cos . x) + ((sin . x) * )) - ((cos . x) + ((- (sin . x)) * ))) / (2 * ) by SIN_COS:30 .= sin . x ; hence sin_C /. x = sin . x ; ::_thesis: verum end; theorem Th39: :: SIN_COS3:39 for x being Element of REAL holds cos_C /. x = cos . x proof let x be Element of REAL ; ::_thesis: cos_C /. x = cos . x x in REAL ; then reconsider z = x as Element of COMPLEX by NUMBERS:11; cos_C /. x = cos_C /. z .= ((exp (0 + ( * x))) + (exp (- ( * x)))) / 2 by Def2 .= ((((exp_R . 0) * (cos . x)) + (((exp_R . 0) * (sin . x)) * )) + (exp (- ( * x)))) / 2 by Th19 .= ((((exp_R 0) * (cos . x)) + (((exp_R . 0) * (sin . x)) * )) + (exp (- ( * x)))) / 2 by SIN_COS:def_23 .= (((1 * (cos . x)) + ((1 * (sin . x)) * )) + (exp (- ( * x)))) / 2 by SIN_COS:51, SIN_COS:def_23 .= (((cos . x) + ((sin . x) * )) + (exp (0 + ((- x) * )))) / 2 .= (((cos . x) + ((sin . x) * )) + (((exp_R . 0) * (cos . (- x))) + (((exp_R . 0) * (sin . (- x))) * ))) / 2 by Th19 .= (((cos . x) + ((sin . x) * )) + (((exp_R 0) * (cos . (- x))) + (((exp_R . 0) * (sin . (- x))) * ))) / 2 by SIN_COS:def_23 .= (((cos . x) + ((sin . x) * )) + ((1 * (cos . (- x))) + ((1 * (sin . (- x))) * ))) / 2 by SIN_COS:51, SIN_COS:def_23 .= (((cos . x) + ((sin . x) * )) + ((1 * (cos . x)) + ((1 * (sin . (- x))) * ))) / 2 by SIN_COS:30 .= (((cos . x) + ((sin . x) * )) + ((cos . x) + ((- (sin . x)) * ))) / 2 by SIN_COS:30 .= cos . x ; hence cos_C /. x = cos . x ; ::_thesis: verum end; theorem Th40: :: SIN_COS3:40 for x being Element of REAL holds sinh_C /. x = sinh . x proof let x be Element of REAL ; ::_thesis: sinh_C /. x = sinh . x A1: (sinh . x) * 2 = 2 * (((exp_R . x) - (exp_R . (- x))) / 2) by SIN_COS2:def_1 .= ((exp_R . x) - (exp_R . (- x))) / (2 / 2) ; x in REAL ; then reconsider z = x as Element of COMPLEX by NUMBERS:11; sinh_C /. x = sinh_C /. z .= ((exp (x + (0 * ))) - (exp (- z))) / 2 by Def3 .= ((((exp_R . x) * 1) + (((exp_R . x) * 0) * )) - (exp (- z))) / 2 by Th19, SIN_COS:30 .= ((exp_R . x) - (exp ((- x) + (0 * )))) / 2 .= ((exp_R . x) - (((exp_R . (- x)) * 1) + (((exp_R . (- x)) * 0) * ))) / 2 by Th19, SIN_COS:30 .= ((sinh . x) * 2) / 2 by A1 ; hence sinh_C /. x = sinh . x ; ::_thesis: verum end; theorem Th41: :: SIN_COS3:41 for x being Element of REAL holds cosh_C /. x = cosh . x proof let x be Element of REAL ; ::_thesis: cosh_C /. x = cosh . x A1: (cosh . x) * 2 = 2 * (((exp_R . x) + (exp_R . (- x))) / 2) by SIN_COS2:def_3 .= ((exp_R . x) + (exp_R . (- x))) / (2 / 2) ; x in REAL ; then reconsider z = x as Element of COMPLEX by NUMBERS:11; cosh_C /. x = cosh_C /. z .= ((exp (x + (0 * ))) + (exp (- z))) / 2 by Def4 .= ((((exp_R . x) * 1) + (((exp_R . x) * 0) * )) + (exp (- z))) / 2 by Th19, SIN_COS:30 .= ((exp_R . x) + (exp ((- x) + (0 * )))) / 2 .= ((exp_R . x) + (((exp_R . (- x)) * 1) + (((exp_R . (- x)) * 0) * ))) / 2 by Th19, SIN_COS:30 .= ((cosh . x) * 2) / 2 by A1 ; hence cosh_C /. x = cosh . x ; ::_thesis: verum end; theorem Th42: :: SIN_COS3:42 for x, y being Element of REAL holds sin_C /. (x + (y * )) = ((sin . x) * (cosh . y)) + (((cos . x) * (sinh . y)) * ) proof let x, y be Element of REAL ; ::_thesis: sin_C /. (x + (y * )) = ((sin . x) * (cosh . y)) + (((cos . x) * (sinh . y)) * ) sin_C /. (x + (y * )) = ((sin_C /. x) * (cos_C /. (y * ))) + ((cos_C /. x) * (sin_C /. (y * ))) by Th4 .= ((sin_C /. x) * (cosh_C /. y)) + ((cos_C /. x) * (sin_C /. (y * ))) by Th16 .= ((sin_C /. x) * (cosh_C /. y)) + ((cos_C /. x) * ((sinh_C /. y) * )) by Th15 .= ((sin . x) * (cosh_C /. y)) + ((cos_C /. x) * ( * (sinh_C /. y))) by Th38 .= ((sin . x) * (cosh_C /. y)) + ((cos . x) * ( * (sinh_C /. y))) by Th39 .= ((sin . x) * (cosh_C /. y)) + ((cos . x) * ( * (sinh . y))) by Th40 .= (((sin . x) * (cosh . y)) + (0 * )) + (0 + (((cos . x) * (sinh . y)) * )) by Th41 ; hence sin_C /. (x + (y * )) = ((sin . x) * (cosh . y)) + (((cos . x) * (sinh . y)) * ) ; ::_thesis: verum end; theorem Th43: :: SIN_COS3:43 for x, y being Element of REAL holds sin_C /. (x + ((- y) * )) = ((sin . x) * (cosh . y)) + ((- ((cos . x) * (sinh . y))) * ) proof let x, y be Element of REAL ; ::_thesis: sin_C /. (x + ((- y) * )) = ((sin . x) * (cosh . y)) + ((- ((cos . x) * (sinh . y))) * ) sin_C /. (x + ((- y) * )) = ((sin . x) * (cosh . (- y))) + (((cos . x) * (sinh . (- y))) * ) by Th42 .= ((sin . x) * (cosh . y)) + (((cos . x) * (sinh . (- y))) * ) by SIN_COS2:19 .= ((sin . x) * (cosh . y)) + (((cos . x) * (- (sinh . y))) * ) by SIN_COS2:19 ; hence sin_C /. (x + ((- y) * )) = ((sin . x) * (cosh . y)) + ((- ((cos . x) * (sinh . y))) * ) ; ::_thesis: verum end; theorem Th44: :: SIN_COS3:44 for x, y being Element of REAL holds cos_C /. (x + (y * )) = ((cos . x) * (cosh . y)) + ((- ((sin . x) * (sinh . y))) * ) proof let x, y be Element of REAL ; ::_thesis: cos_C /. (x + (y * )) = ((cos . x) * (cosh . y)) + ((- ((sin . x) * (sinh . y))) * ) cos_C /. (x + (y * )) = ((cos_C /. x) * (cos_C /. ( * y))) - ((sin_C /. x) * (sin_C /. ( * y))) by Th6 .= ((cos_C /. x) * (cos_C /. ( * y))) - ((sin_C /. x) * ((sinh_C /. y) * )) by Th15 .= ((cos_C /. x) * (cosh_C /. y)) - ((sin_C /. x) * ((sinh_C /. y) * )) by Th16 .= ((cos_C /. x) * (cosh_C /. y)) - ((sin . x) * ((sinh_C /. y) * )) by Th38 .= ((cos . x) * (cosh_C /. y)) - ((sin . x) * ((sinh_C /. y) * )) by Th39 .= ((cos . x) * (cosh_C /. y)) - ((sin . x) * ((sinh . y) * )) by Th40 .= ((cos . x) * (cosh . y)) - (((sin . x) * (sinh . y)) * ) by Th41 .= ((cos . x) * (cosh . y)) + ((- ((sin . x) * (sinh . y))) * ) ; hence cos_C /. (x + (y * )) = ((cos . x) * (cosh . y)) + ((- ((sin . x) * (sinh . y))) * ) ; ::_thesis: verum end; theorem Th45: :: SIN_COS3:45 for x, y being Element of REAL holds cos_C /. (x + ((- y) * )) = ((cos . x) * (cosh . y)) + (((sin . x) * (sinh . y)) * ) proof let x, y be Element of REAL ; ::_thesis: cos_C /. (x + ((- y) * )) = ((cos . x) * (cosh . y)) + (((sin . x) * (sinh . y)) * ) cos_C /. (x + ((- y) * )) = ((cos . x) * (cosh . (- y))) + ((- ((sin . x) * (sinh . (- y)))) * ) by Th44 .= ((cos . x) * (cosh . y)) + (- (((sin . x) * (sinh . (- y))) * )) by SIN_COS2:19 .= ((cos . x) * (cosh . y)) + (- (((sin . x) * (- (sinh . y))) * )) by SIN_COS2:19 .= ((cos . x) * (cosh . y)) + (- (- (((sin . x) * (sinh . y)) * ))) ; hence cos_C /. (x + ((- y) * )) = ((cos . x) * (cosh . y)) + (((sin . x) * (sinh . y)) * ) ; ::_thesis: verum end; theorem Th46: :: SIN_COS3:46 for x, y being Element of REAL holds sinh_C /. (x + (y * )) = ((sinh . x) * (cos . y)) + (((cosh . x) * (sin . y)) * ) proof let x, y be Element of REAL ; ::_thesis: sinh_C /. (x + (y * )) = ((sinh . x) * (cos . y)) + (((cosh . x) * (sin . y)) * ) sinh_C /. (x + (y * )) = sinh_C /. ((y + ((- x) * )) * ) .= * (sin_C /. (y + ((- x) * ))) by Th17 .= * (((sin . y) * (cosh . x)) + ((- ((cos . y) * (sinh . x))) * )) by Th43 .= (- (- ((sinh . x) * (cos . y)))) + (((cosh . x) * (sin . y)) * ) ; hence sinh_C /. (x + (y * )) = ((sinh . x) * (cos . y)) + (((cosh . x) * (sin . y)) * ) ; ::_thesis: verum end; theorem Th47: :: SIN_COS3:47 for x, y being Element of REAL holds sinh_C /. (x + ((- y) * )) = ((sinh . x) * (cos . y)) + ((- ((cosh . x) * (sin . y))) * ) proof let x, y be Element of REAL ; ::_thesis: sinh_C /. (x + ((- y) * )) = ((sinh . x) * (cos . y)) + ((- ((cosh . x) * (sin . y))) * ) sinh_C /. (x + ((- y) * )) = ((sinh . x) * (cos . (- y))) + (((cosh . x) * (sin . (- y))) * ) by Th46 .= ((sinh . x) * (cos . y)) + (((cosh . x) * (sin . (- y))) * ) by SIN_COS:30 .= ((sinh . x) * (cos . y)) + (((cosh . x) * (- (sin . y))) * ) by SIN_COS:30 ; hence sinh_C /. (x + ((- y) * )) = ((sinh . x) * (cos . y)) + ((- ((cosh . x) * (sin . y))) * ) ; ::_thesis: verum end; theorem Th48: :: SIN_COS3:48 for x, y being Element of REAL holds cosh_C /. (x + (y * )) = ((cosh . x) * (cos . y)) + (((sinh . x) * (sin . y)) * ) proof let x, y be Element of REAL ; ::_thesis: cosh_C /. (x + (y * )) = ((cosh . x) * (cos . y)) + (((sinh . x) * (sin . y)) * ) cosh_C /. ( * (y + ((- x) * ))) = cos_C /. (y + ((- x) * )) by Th18; hence cosh_C /. (x + (y * )) = ((cosh . x) * (cos . y)) + (((sinh . x) * (sin . y)) * ) by Th45; ::_thesis: verum end; theorem Th49: :: SIN_COS3:49 for x, y being Element of REAL holds cosh_C /. (x + ((- y) * )) = ((cosh . x) * (cos . y)) + ((- ((sinh . x) * (sin . y))) * ) proof let x, y be Element of REAL ; ::_thesis: cosh_C /. (x + ((- y) * )) = ((cosh . x) * (cos . y)) + ((- ((sinh . x) * (sin . y))) * ) cosh_C /. (x + ((- y) * )) = ((cosh . x) * (cos . (- y))) + (((sinh . x) * (sin . (- y))) * ) by Th48 .= ((cosh . x) * (cos . y)) + (((sinh . x) * (sin . (- y))) * ) by SIN_COS:30 .= ((cosh . x) * (cos . y)) + (((sinh . x) * (- (sin . y))) * ) by SIN_COS:30 ; hence cosh_C /. (x + ((- y) * )) = ((cosh . x) * (cos . y)) + ((- ((sinh . x) * (sin . y))) * ) ; ::_thesis: verum end; theorem Th50: :: SIN_COS3:50 for n being Element of NAT for z being Element of COMPLEX holds ((cos_C /. z) + ( * (sin_C /. z))) #N n = (cos_C /. (n * z)) + ( * (sin_C /. (n * z))) proof defpred S1[ Element of NAT ] means for z being Element of COMPLEX holds ((cos_C /. z) + ( * (sin_C /. z))) #N $1 = (cos_C /. ($1 * z)) + ( * (sin_C /. ($1 * z))); A1: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A2: for z being Element of COMPLEX holds ((cos_C /. z) + ( * (sin_C /. z))) #N n = (cos_C /. (n * z)) + ( * (sin_C /. (n * z))) ; ::_thesis: S1[n + 1] for z being Element of COMPLEX holds ((cos_C /. z) + ( * (sin_C /. z))) #N (n + 1) = (cos_C /. ((n + 1) * z)) + ( * (sin_C /. ((n + 1) * z))) proof let z be Element of COMPLEX ; ::_thesis: ((cos_C /. z) + ( * (sin_C /. z))) #N (n + 1) = (cos_C /. ((n + 1) * z)) + ( * (sin_C /. ((n + 1) * z))) set cn = cos_C /. (n * z); set sn = sin_C /. (n * z); set c1 = cos_C /. z; set s1 = sin_C /. z; A3: ((cos_C /. z) + ( * (sin_C /. z))) #N (n + 1) = (((cos_C /. z) + ( * (sin_C /. z))) GeoSeq) . (n + 1) by COMSEQ_3:def_2 .= ((((cos_C /. z) + ( * (sin_C /. z))) GeoSeq) . n) * ((cos_C /. z) + ( * (sin_C /. z))) by COMSEQ_3:def_1 .= (((cos_C /. z) + ( * (sin_C /. z))) #N n) * ((cos_C /. z) + ( * (sin_C /. z))) by COMSEQ_3:def_2 .= ((cos_C /. (n * z)) + ( * (sin_C /. (n * z)))) * ((cos_C /. z) + ( * (sin_C /. z))) by A2 .= (((cos_C /. (n * z)) * (cos_C /. z)) + (( * (sin_C /. (n * z))) * (cos_C /. z))) + ((( * (cos_C /. (n * z))) * (sin_C /. z)) + (- ((sin_C /. (n * z)) * (sin_C /. z)))) ; (cos_C /. ((n + 1) * z)) + ( * (sin_C /. ((n + 1) * z))) = (cos_C /. ((n * z) + (1 * z))) + ( * (((sin_C /. (n * z)) * (cos_C /. (1 * z))) + ((cos_C /. (n * z)) * (sin_C /. (1 * z))))) by Th4 .= (((cos_C /. (n * z)) * (cos_C /. z)) - ((sin_C /. (n * z)) * (sin_C /. z))) + ( * (((sin_C /. (n * z)) * (cos_C /. z)) + ((cos_C /. (n * z)) * (sin_C /. z)))) by Th6 .= ((cos_C /. (n * z)) * (cos_C /. z)) + ((( * (sin_C /. (n * z))) * (cos_C /. z)) + ((( * (cos_C /. (n * z))) * (sin_C /. z)) + (- ((sin_C /. (n * z)) * (sin_C /. z))))) ; hence ((cos_C /. z) + ( * (sin_C /. z))) #N (n + 1) = (cos_C /. ((n + 1) * z)) + ( * (sin_C /. ((n + 1) * z))) by A3; ::_thesis: verum end; hence S1[n + 1] ; ::_thesis: verum end; A4: S1[ 0 ] by Th21, Th23, COMPLEX1:def_4, COMSEQ_3:11; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A1); hence for n being Element of NAT for z being Element of COMPLEX holds ((cos_C /. z) + ( * (sin_C /. z))) #N n = (cos_C /. (n * z)) + ( * (sin_C /. (n * z))) ; ::_thesis: verum end; theorem Th51: :: SIN_COS3:51 for n being Element of NAT for z being Element of COMPLEX holds ((cos_C /. z) - ( * (sin_C /. z))) #N n = (cos_C /. (n * z)) - ( * (sin_C /. (n * z))) proof let n be Element of NAT ; ::_thesis: for z being Element of COMPLEX holds ((cos_C /. z) - ( * (sin_C /. z))) #N n = (cos_C /. (n * z)) - ( * (sin_C /. (n * z))) let z be Element of COMPLEX ; ::_thesis: ((cos_C /. z) - ( * (sin_C /. z))) #N n = (cos_C /. (n * z)) - ( * (sin_C /. (n * z))) ((cos_C /. z) - ( * (sin_C /. z))) #N n = ((cos_C /. z) + ( * (- (sin_C /. z)))) #N n .= ((cos_C /. z) + ( * (sin_C /. (- z)))) #N n by Th2 .= ((cos_C /. (- z)) + ( * (sin_C /. (- z)))) #N n by Th3 .= (cos_C /. (- (n * z))) + ( * (sin_C /. (n * (- z)))) by Th50 .= (cos_C /. (n * z)) + ( * (sin_C /. (- (n * z)))) by Th3 .= (cos_C /. (n * z)) + ( * (- (sin_C /. (n * z)))) by Th2 .= (cos_C /. (n * z)) + (- ( * (sin_C /. (n * z)))) ; hence ((cos_C /. z) - ( * (sin_C /. z))) #N n = (cos_C /. (n * z)) - ( * (sin_C /. (n * z))) ; ::_thesis: verum end; theorem :: SIN_COS3:52 for n being Element of NAT for z being Element of COMPLEX holds exp (( * n) * z) = ((cos_C /. z) + ( * (sin_C /. z))) #N n proof let n be Element of NAT ; ::_thesis: for z being Element of COMPLEX holds exp (( * n) * z) = ((cos_C /. z) + ( * (sin_C /. z))) #N n let z be Element of COMPLEX ; ::_thesis: exp (( * n) * z) = ((cos_C /. z) + ( * (sin_C /. z))) #N n exp (( * n) * z) = exp ( * (n * z)) .= (cos_C /. (n * z)) + ( * (sin_C /. (n * z))) by Th36 ; hence exp (( * n) * z) = ((cos_C /. z) + ( * (sin_C /. z))) #N n by Th50; ::_thesis: verum end; theorem :: SIN_COS3:53 for n being Element of NAT for z being Element of COMPLEX holds exp (- (( * n) * z)) = ((cos_C /. z) - ( * (sin_C /. z))) #N n proof let n be Element of NAT ; ::_thesis: for z being Element of COMPLEX holds exp (- (( * n) * z)) = ((cos_C /. z) - ( * (sin_C /. z))) #N n let z be Element of COMPLEX ; ::_thesis: exp (- (( * n) * z)) = ((cos_C /. z) - ( * (sin_C /. z))) #N n exp (- (( * n) * z)) = exp (- ( * (n * z))) .= (cos_C /. (n * z)) - ( * (sin_C /. (n * z))) by Th37 ; hence exp (- (( * n) * z)) = ((cos_C /. z) - ( * (sin_C /. z))) #N n by Th51; ::_thesis: verum end; theorem :: SIN_COS3:54 for x, y being Element of REAL holds (((1 + ((- 1) * )) / 2) * (sinh_C /. (x + (y * )))) + (((1 + ) / 2) * (sinh_C /. (x + ((- y) * )))) = ((sinh . x) * (cos . y)) + ((cosh . x) * (sin . y)) proof let x, y be Element of REAL ; ::_thesis: (((1 + ((- 1) * )) / 2) * (sinh_C /. (x + (y * )))) + (((1 + ) / 2) * (sinh_C /. (x + ((- y) * )))) = ((sinh . x) * (cos . y)) + ((cosh . x) * (sin . y)) set shx = sinh . x; set cy = cos . y; set chx = cosh . x; set sy = sin . y; (((1 + ((- 1) * )) / 2) * (sinh_C /. (x + (y * )))) + (((1 + ) / 2) * (sinh_C /. (x + ((- y) * )))) = (((1 + ((- 1) * )) / 2) * (((sinh . x) * (cos . y)) + (((cosh . x) * (sin . y)) * ))) + (((1 + ) / 2) * (sinh_C /. (x + ((- y) * )))) by Th46 .= (((1 + ((- 1) * )) / 2) * (((sinh . x) * (cos . y)) + (((cosh . x) * (sin . y)) * ))) + (((1 + ) / 2) * (((sinh . x) * (cos . y)) + ((- ((cosh . x) * (sin . y))) * ))) by Th47 .= (2 * ((((sinh . x) * (cos . y)) + ((cosh . x) * (sin . y))) + (0 * ))) / 2 ; hence (((1 + ((- 1) * )) / 2) * (sinh_C /. (x + (y * )))) + (((1 + ) / 2) * (sinh_C /. (x + ((- y) * )))) = ((sinh . x) * (cos . y)) + ((cosh . x) * (sin . y)) ; ::_thesis: verum end; theorem :: SIN_COS3:55 for x, y being Element of REAL holds (((1 + ((- 1) * )) / 2) * (cosh_C /. (x + (y * )))) + (((1 + ) / 2) * (cosh_C /. (x + ((- y) * )))) = ((sinh . x) * (sin . y)) + ((cosh . x) * (cos . y)) proof let x, y be Element of REAL ; ::_thesis: (((1 + ((- 1) * )) / 2) * (cosh_C /. (x + (y * )))) + (((1 + ) / 2) * (cosh_C /. (x + ((- y) * )))) = ((sinh . x) * (sin . y)) + ((cosh . x) * (cos . y)) set shx = sinh . x; set cy = cos . y; set chx = cosh . x; set sy = sin . y; (((1 + ((- 1) * )) / 2) * (cosh_C /. (x + (y * )))) + (((1 + ) / 2) * (cosh_C /. (x + ((- y) * )))) = (((1 + ((- 1) * )) / 2) * (((cosh . x) * (cos . y)) + (((sinh . x) * (sin . y)) * ))) + (((1 + ) / 2) * (cosh_C /. (x + ((- y) * )))) by Th48 .= (((1 + ((- 1) * )) * (((cosh . x) * (cos . y)) + (((sinh . x) * (sin . y)) * ))) / 2) + (((1 + ) / 2) * (((cosh . x) * (cos . y)) + ((- ((sinh . x) * (sin . y))) * ))) by Th49 .= (2 * ((((cosh . x) * (cos . y)) + ((sinh . x) * (sin . y))) + (0 * ))) / 2 ; hence (((1 + ((- 1) * )) / 2) * (cosh_C /. (x + (y * )))) + (((1 + ) / 2) * (cosh_C /. (x + ((- y) * )))) = ((sinh . x) * (sin . y)) + ((cosh . x) * (cos . y)) ; ::_thesis: verum end; theorem :: SIN_COS3:56 for z being Element of COMPLEX holds (sinh_C /. z) * (sinh_C /. z) = ((cosh_C /. (2 * z)) - 1) / 2 proof let z be Element of COMPLEX ; ::_thesis: (sinh_C /. z) * (sinh_C /. z) = ((cosh_C /. (2 * z)) - 1) / 2 set e1 = exp z; set e2 = exp (- z); (sinh_C /. z) * (sinh_C /. z) = (((exp z) - (exp (- z))) / 2) * (sinh_C /. z) by Def3 .= (((exp z) - (exp (- z))) / 2) * (((exp z) - (exp (- z))) / 2) by Def3 .= (((((exp z) * (exp z)) + ((exp (- z)) * (exp (- z)))) - (2 * ((exp z) * (exp (- z))))) / 2) / 2 .= (((((exp z) * (exp z)) + ((exp (- z)) * (exp (- z)))) - (2 * 1)) / 2) / 2 by Lm3 .= ((((exp (z + z)) + ((exp (- z)) * (exp (- z)))) - 2) / 2) / 2 by SIN_COS:23 .= ((((exp (2 * z)) + (exp ((- z) + (- z)))) - 2) / 2) / 2 by SIN_COS:23 .= ((((exp (2 * z)) + (exp (- (2 * z)))) / 2) - 1) / 2 ; hence (sinh_C /. z) * (sinh_C /. z) = ((cosh_C /. (2 * z)) - 1) / 2 by Lm2; ::_thesis: verum end; theorem Th57: :: SIN_COS3:57 for z being Element of COMPLEX holds (cosh_C /. z) * (cosh_C /. z) = ((cosh_C /. (2 * z)) + 1) / 2 proof let z be Element of COMPLEX ; ::_thesis: (cosh_C /. z) * (cosh_C /. z) = ((cosh_C /. (2 * z)) + 1) / 2 set e1 = exp z; set e2 = exp (- z); (cosh_C /. z) * (cosh_C /. z) = (((exp z) + (exp (- z))) / 2) * (cosh_C /. z) by Def4 .= (((exp z) + (exp (- z))) / 2) * (((exp z) + (exp (- z))) / 2) by Def4 .= (((((exp z) * (exp z)) + ((exp (- z)) * (exp (- z)))) + (2 * ((exp z) * (exp (- z))))) / 2) / 2 .= (((((exp z) * (exp z)) + ((exp (- z)) * (exp (- z)))) + (2 * 1)) / 2) / 2 by Lm3 .= ((((exp (z + z)) + ((exp (- z)) * (exp (- z)))) + 2) / 2) / 2 by SIN_COS:23 .= ((((exp (2 * z)) + (exp ((- z) + (- z)))) + 2) / 2) / 2 by SIN_COS:23 .= ((((exp (2 * z)) + (exp (- (2 * z)))) / 2) + 1) / 2 ; hence (cosh_C /. z) * (cosh_C /. z) = ((cosh_C /. (2 * z)) + 1) / 2 by Lm2; ::_thesis: verum end; theorem Th58: :: SIN_COS3:58 for z being Element of COMPLEX holds ( sinh_C /. (2 * z) = (2 * (sinh_C /. z)) * (cosh_C /. z) & cosh_C /. (2 * z) = ((2 * (cosh_C /. z)) * (cosh_C /. z)) - 1 ) proof let z be Element of COMPLEX ; ::_thesis: ( sinh_C /. (2 * z) = (2 * (sinh_C /. z)) * (cosh_C /. z) & cosh_C /. (2 * z) = ((2 * (cosh_C /. z)) * (cosh_C /. z)) - 1 ) set e1 = exp z; set e2 = exp (- z); A1: ((2 * (cosh_C /. z)) * (cosh_C /. z)) - 1 = (2 * ((cosh_C /. z) * (cosh_C /. z))) - 1 .= (2 * (((cosh_C /. (2 * z)) + 1) / 2)) - 1 by Th57 .= ((cosh_C /. (2 * z)) + 1) - 1 ; (2 * (sinh_C /. z)) * (cosh_C /. z) = 2 * ((sinh_C /. z) * (cosh_C /. z)) .= 2 * ((sinh_C /. z) * (((exp z) + (exp (- z))) / 2)) by Def4 .= 2 * ((((exp z) - (exp (- z))) / 2) * (((exp z) + (exp (- z))) / 2)) by Def3 .= (((exp z) * (exp z)) - ((exp (- z)) * (exp (- z)))) / 2 .= ((exp (z + z)) - ((exp (- z)) * (exp (- z)))) / 2 by SIN_COS:23 .= ((exp (2 * z)) - (exp ((- z) + (- z)))) / 2 by SIN_COS:23 .= ((exp (2 * z)) - (exp (- (2 * z)))) / 2 .= sinh_C /. (2 * z) by Lm1 ; hence ( sinh_C /. (2 * z) = (2 * (sinh_C /. z)) * (cosh_C /. z) & cosh_C /. (2 * z) = ((2 * (cosh_C /. z)) * (cosh_C /. z)) - 1 ) by A1; ::_thesis: verum end; theorem Th59: :: SIN_COS3:59 for z1, z2 being Element of COMPLEX holds ( ((sinh_C /. z1) * (sinh_C /. z1)) - ((sinh_C /. z2) * (sinh_C /. z2)) = (sinh_C /. (z1 + z2)) * (sinh_C /. (z1 - z2)) & ((cosh_C /. z1) * (cosh_C /. z1)) - ((cosh_C /. z2) * (cosh_C /. z2)) = (sinh_C /. (z1 + z2)) * (sinh_C /. (z1 - z2)) & ((sinh_C /. z1) * (sinh_C /. z1)) - ((sinh_C /. z2) * (sinh_C /. z2)) = ((cosh_C /. z1) * (cosh_C /. z1)) - ((cosh_C /. z2) * (cosh_C /. z2)) ) proof let z1, z2 be Element of COMPLEX ; ::_thesis: ( ((sinh_C /. z1) * (sinh_C /. z1)) - ((sinh_C /. z2) * (sinh_C /. z2)) = (sinh_C /. (z1 + z2)) * (sinh_C /. (z1 - z2)) & ((cosh_C /. z1) * (cosh_C /. z1)) - ((cosh_C /. z2) * (cosh_C /. z2)) = (sinh_C /. (z1 + z2)) * (sinh_C /. (z1 - z2)) & ((sinh_C /. z1) * (sinh_C /. z1)) - ((sinh_C /. z2) * (sinh_C /. z2)) = ((cosh_C /. z1) * (cosh_C /. z1)) - ((cosh_C /. z2) * (cosh_C /. z2)) ) set s1 = sinh_C /. z1; set s2 = sinh_C /. z2; set c1 = cosh_C /. z1; set c2 = cosh_C /. z2; A1: (sinh_C /. (z1 + z2)) * (sinh_C /. (z1 - z2)) = (((sinh_C /. z1) * (cosh_C /. z2)) + ((cosh_C /. z1) * (sinh_C /. z2))) * (sinh_C /. (z1 - z2)) by Th11 .= (((sinh_C /. z1) * (cosh_C /. z2)) + ((cosh_C /. z1) * (sinh_C /. z2))) * (((sinh_C /. z1) * (cosh_C /. z2)) - ((cosh_C /. z1) * (sinh_C /. z2))) by Th12 .= (((sinh_C /. z1) * (sinh_C /. z1)) * ((cosh_C /. z2) * (cosh_C /. z2))) - (((sinh_C /. z2) * ((cosh_C /. z1) * (cosh_C /. z1))) * (sinh_C /. z2)) ; then A2: (sinh_C /. (z1 + z2)) * (sinh_C /. (z1 - z2)) = (((- (((cosh_C /. z1) * (cosh_C /. z1)) - ((sinh_C /. z1) * (sinh_C /. z1)))) * ((cosh_C /. z2) * (cosh_C /. z2))) + (((cosh_C /. z1) * (cosh_C /. z1)) * ((cosh_C /. z2) * (cosh_C /. z2)))) - (((sinh_C /. z2) * (sinh_C /. z2)) * ((cosh_C /. z1) * (cosh_C /. z1))) .= (((- 1) * ((cosh_C /. z2) * (cosh_C /. z2))) + (((cosh_C /. z1) * (cosh_C /. z1)) * ((cosh_C /. z2) * (cosh_C /. z2)))) - (((sinh_C /. z2) * (sinh_C /. z2)) * ((cosh_C /. z1) * (cosh_C /. z1))) by Th8 .= ((- 1) * ((cosh_C /. z2) * (cosh_C /. z2))) + (((cosh_C /. z1) * (cosh_C /. z1)) * (((cosh_C /. z2) * (cosh_C /. z2)) - ((sinh_C /. z2) * (sinh_C /. z2)))) .= ((- 1) * ((cosh_C /. z2) * (cosh_C /. z2))) + (((cosh_C /. z1) * (cosh_C /. z1)) * 1) by Th8 .= (- ((cosh_C /. z2) * (cosh_C /. z2))) + ((cosh_C /. z1) * (cosh_C /. z1)) ; (sinh_C /. (z1 + z2)) * (sinh_C /. (z1 - z2)) = ((((sinh_C /. z1) * (sinh_C /. z1)) * (((cosh_C /. z2) * (cosh_C /. z2)) - ((sinh_C /. z2) * (sinh_C /. z2)))) + (((sinh_C /. z1) * (sinh_C /. z1)) * ((sinh_C /. z2) * (sinh_C /. z2)))) - (((sinh_C /. z2) * (sinh_C /. z2)) * ((cosh_C /. z1) * (cosh_C /. z1))) by A1 .= ((((sinh_C /. z1) * (sinh_C /. z1)) * 1) + (((sinh_C /. z1) * (sinh_C /. z1)) * ((sinh_C /. z2) * (sinh_C /. z2)))) - (((sinh_C /. z2) * (sinh_C /. z2)) * ((cosh_C /. z1) * (cosh_C /. z1))) by Th8 .= (((sinh_C /. z1) * (sinh_C /. z1)) * 1) + (((sinh_C /. z2) * (sinh_C /. z2)) * (- (((cosh_C /. z1) * (cosh_C /. z1)) - ((sinh_C /. z1) * (sinh_C /. z1))))) .= (((sinh_C /. z1) * (sinh_C /. z1)) * 1) + (((sinh_C /. z2) * (sinh_C /. z2)) * (- 1)) by Th8 .= (((sinh_C /. z1) * (sinh_C /. z1)) * 1) - ((sinh_C /. z2) * (sinh_C /. z2)) ; hence ( ((sinh_C /. z1) * (sinh_C /. z1)) - ((sinh_C /. z2) * (sinh_C /. z2)) = (sinh_C /. (z1 + z2)) * (sinh_C /. (z1 - z2)) & ((cosh_C /. z1) * (cosh_C /. z1)) - ((cosh_C /. z2) * (cosh_C /. z2)) = (sinh_C /. (z1 + z2)) * (sinh_C /. (z1 - z2)) & ((sinh_C /. z1) * (sinh_C /. z1)) - ((sinh_C /. z2) * (sinh_C /. z2)) = ((cosh_C /. z1) * (cosh_C /. z1)) - ((cosh_C /. z2) * (cosh_C /. z2)) ) by A2; ::_thesis: verum end; theorem Th60: :: SIN_COS3:60 for z1, z2 being Element of COMPLEX holds ( (cosh_C /. (z1 + z2)) * (cosh_C /. (z1 - z2)) = ((sinh_C /. z1) * (sinh_C /. z1)) + ((cosh_C /. z2) * (cosh_C /. z2)) & (cosh_C /. (z1 + z2)) * (cosh_C /. (z1 - z2)) = ((cosh_C /. z1) * (cosh_C /. z1)) + ((sinh_C /. z2) * (sinh_C /. z2)) & ((sinh_C /. z1) * (sinh_C /. z1)) + ((cosh_C /. z2) * (cosh_C /. z2)) = ((cosh_C /. z1) * (cosh_C /. z1)) + ((sinh_C /. z2) * (sinh_C /. z2)) ) proof let z1, z2 be Element of COMPLEX ; ::_thesis: ( (cosh_C /. (z1 + z2)) * (cosh_C /. (z1 - z2)) = ((sinh_C /. z1) * (sinh_C /. z1)) + ((cosh_C /. z2) * (cosh_C /. z2)) & (cosh_C /. (z1 + z2)) * (cosh_C /. (z1 - z2)) = ((cosh_C /. z1) * (cosh_C /. z1)) + ((sinh_C /. z2) * (sinh_C /. z2)) & ((sinh_C /. z1) * (sinh_C /. z1)) + ((cosh_C /. z2) * (cosh_C /. z2)) = ((cosh_C /. z1) * (cosh_C /. z1)) + ((sinh_C /. z2) * (sinh_C /. z2)) ) set s1 = sinh_C /. z1; set s2 = sinh_C /. z2; set c1 = cosh_C /. z1; set c2 = cosh_C /. z2; A1: (cosh_C /. (z1 + z2)) * (cosh_C /. (z1 - z2)) = (((cosh_C /. z1) * (cosh_C /. z2)) + ((sinh_C /. z1) * (sinh_C /. z2))) * (cosh_C /. (z1 - z2)) by Th14 .= (((cosh_C /. z1) * (cosh_C /. z2)) + ((sinh_C /. z1) * (sinh_C /. z2))) * (((cosh_C /. z1) * (cosh_C /. z2)) - ((sinh_C /. z1) * (sinh_C /. z2))) by Th13 .= ((((cosh_C /. z1) * (cosh_C /. z1)) * (cosh_C /. z2)) * (cosh_C /. z2)) - ((((sinh_C /. z1) * (sinh_C /. z1)) * (sinh_C /. z2)) * (sinh_C /. z2)) ; then A2: (cosh_C /. (z1 + z2)) * (cosh_C /. (z1 - z2)) = (((cosh_C /. z1) * (cosh_C /. z1)) * (((cosh_C /. z2) * (cosh_C /. z2)) - ((sinh_C /. z2) * (sinh_C /. z2)))) + ((((cosh_C /. z1) * (cosh_C /. z1)) - ((sinh_C /. z1) * (sinh_C /. z1))) * ((sinh_C /. z2) * (sinh_C /. z2))) .= (((cosh_C /. z1) * (cosh_C /. z1)) * 1) + ((((cosh_C /. z1) * (cosh_C /. z1)) - ((sinh_C /. z1) * (sinh_C /. z1))) * ((sinh_C /. z2) * (sinh_C /. z2))) by Th8 .= ((cosh_C /. z1) * (cosh_C /. z1)) + (1 * ((sinh_C /. z2) * (sinh_C /. z2))) by Th8 ; (cosh_C /. (z1 + z2)) * (cosh_C /. (z1 - z2)) = ((((cosh_C /. z1) * (cosh_C /. z1)) - ((sinh_C /. z1) * (sinh_C /. z1))) * ((cosh_C /. z2) * (cosh_C /. z2))) + (((sinh_C /. z1) * (sinh_C /. z1)) * (((cosh_C /. z2) * (cosh_C /. z2)) - ((sinh_C /. z2) * (sinh_C /. z2)))) by A1 .= (1 * ((cosh_C /. z2) * (cosh_C /. z2))) + (((sinh_C /. z1) * (sinh_C /. z1)) * (((cosh_C /. z2) * (cosh_C /. z2)) - ((sinh_C /. z2) * (sinh_C /. z2)))) by Th8 .= ((cosh_C /. z2) * (cosh_C /. z2)) + (((sinh_C /. z1) * (sinh_C /. z1)) * 1) by Th8 ; hence ( (cosh_C /. (z1 + z2)) * (cosh_C /. (z1 - z2)) = ((sinh_C /. z1) * (sinh_C /. z1)) + ((cosh_C /. z2) * (cosh_C /. z2)) & (cosh_C /. (z1 + z2)) * (cosh_C /. (z1 - z2)) = ((cosh_C /. z1) * (cosh_C /. z1)) + ((sinh_C /. z2) * (sinh_C /. z2)) & ((sinh_C /. z1) * (sinh_C /. z1)) + ((cosh_C /. z2) * (cosh_C /. z2)) = ((cosh_C /. z1) * (cosh_C /. z1)) + ((sinh_C /. z2) * (sinh_C /. z2)) ) by A2; ::_thesis: verum end; theorem :: SIN_COS3:61 for z1, z2 being Element of COMPLEX holds ( (sinh_C /. (2 * z1)) + (sinh_C /. (2 * z2)) = (2 * (sinh_C /. (z1 + z2))) * (cosh_C /. (z1 - z2)) & (sinh_C /. (2 * z1)) - (sinh_C /. (2 * z2)) = (2 * (sinh_C /. (z1 - z2))) * (cosh_C /. (z1 + z2)) ) proof let z1, z2 be Element of COMPLEX ; ::_thesis: ( (sinh_C /. (2 * z1)) + (sinh_C /. (2 * z2)) = (2 * (sinh_C /. (z1 + z2))) * (cosh_C /. (z1 - z2)) & (sinh_C /. (2 * z1)) - (sinh_C /. (2 * z2)) = (2 * (sinh_C /. (z1 - z2))) * (cosh_C /. (z1 + z2)) ) set c1 = cosh_C /. z1; set c2 = cosh_C /. z2; set s1 = sinh_C /. z1; set s2 = sinh_C /. z2; A1: (2 * (sinh_C /. (z1 - z2))) * (cosh_C /. (z1 + z2)) = (2 * (((sinh_C /. z1) * (cosh_C /. z2)) - ((cosh_C /. z1) * (sinh_C /. z2)))) * (cosh_C /. (z1 + z2)) by Th12 .= (2 * (((sinh_C /. z1) * (cosh_C /. z2)) - ((cosh_C /. z1) * (sinh_C /. z2)))) * (((cosh_C /. z1) * (cosh_C /. z2)) + ((sinh_C /. z1) * (sinh_C /. z2))) by Th14 .= 2 * ((((sinh_C /. z1) * (cosh_C /. z1)) * (((cosh_C /. z2) * (cosh_C /. z2)) - ((sinh_C /. z2) * (sinh_C /. z2)))) - ((((sinh_C /. z2) * (cosh_C /. z2)) * ((cosh_C /. z1) * (cosh_C /. z1))) - (((sinh_C /. z2) * (cosh_C /. z2)) * ((sinh_C /. z1) * (sinh_C /. z1))))) .= 2 * ((((sinh_C /. z1) * (cosh_C /. z1)) * 1) - (((sinh_C /. z2) * (cosh_C /. z2)) * (((cosh_C /. z1) * (cosh_C /. z1)) - ((sinh_C /. z1) * (sinh_C /. z1))))) by Th8 .= 2 * ((((sinh_C /. z1) * (cosh_C /. z1)) * 1) - (((sinh_C /. z2) * (cosh_C /. z2)) * 1)) by Th8 .= ((2 * (sinh_C /. z1)) * (cosh_C /. z1)) - (2 * ((sinh_C /. z2) * (cosh_C /. z2))) .= (sinh_C /. (2 * z1)) - ((2 * (sinh_C /. z2)) * (cosh_C /. z2)) by Th58 ; (2 * (sinh_C /. (z1 + z2))) * (cosh_C /. (z1 - z2)) = (2 * (((sinh_C /. z1) * (cosh_C /. z2)) + ((cosh_C /. z1) * (sinh_C /. z2)))) * (cosh_C /. (z1 - z2)) by Th11 .= (2 * (((sinh_C /. z1) * (cosh_C /. z2)) + ((cosh_C /. z1) * (sinh_C /. z2)))) * (((cosh_C /. z1) * (cosh_C /. z2)) - ((sinh_C /. z1) * (sinh_C /. z2))) by Th13 .= 2 * (((((cosh_C /. z2) * (cosh_C /. z2)) - ((sinh_C /. z2) * (sinh_C /. z2))) * ((cosh_C /. z1) * (sinh_C /. z1))) + ((((cosh_C /. z1) * (cosh_C /. z1)) * ((sinh_C /. z2) * (cosh_C /. z2))) - (((sinh_C /. z1) * (sinh_C /. z1)) * ((cosh_C /. z2) * (sinh_C /. z2))))) .= 2 * ((1 * ((cosh_C /. z1) * (sinh_C /. z1))) + ((((cosh_C /. z1) * (cosh_C /. z1)) - ((sinh_C /. z1) * (sinh_C /. z1))) * ((cosh_C /. z2) * (sinh_C /. z2)))) by Th8 .= 2 * ((1 * ((cosh_C /. z1) * (sinh_C /. z1))) + (1 * ((cosh_C /. z2) * (sinh_C /. z2)))) by Th8 .= ((2 * (sinh_C /. z1)) * (cosh_C /. z1)) + (2 * ((cosh_C /. z2) * (sinh_C /. z2))) .= (sinh_C /. (2 * z1)) + ((2 * (sinh_C /. z2)) * (cosh_C /. z2)) by Th58 .= (sinh_C /. (2 * z1)) + (sinh_C /. (2 * z2)) by Th58 ; hence ( (sinh_C /. (2 * z1)) + (sinh_C /. (2 * z2)) = (2 * (sinh_C /. (z1 + z2))) * (cosh_C /. (z1 - z2)) & (sinh_C /. (2 * z1)) - (sinh_C /. (2 * z2)) = (2 * (sinh_C /. (z1 - z2))) * (cosh_C /. (z1 + z2)) ) by A1, Th58; ::_thesis: verum end; Lm5: for z1 being Element of COMPLEX holds (sinh_C /. z1) * (sinh_C /. z1) = ((cosh_C /. z1) * (cosh_C /. z1)) - 1 proof let z1 be Element of COMPLEX ; ::_thesis: (sinh_C /. z1) * (sinh_C /. z1) = ((cosh_C /. z1) * (cosh_C /. z1)) - 1 ((cosh_C /. z1) * (cosh_C /. z1)) - 1 = ((cosh_C /. z1) * (cosh_C /. z1)) - (((cosh_C /. z1) * (cosh_C /. z1)) - ((sinh_C /. z1) * (sinh_C /. z1))) by Th8 .= (((sinh_C /. z1) * (sinh_C /. z1)) + ((cosh_C /. z1) * (cosh_C /. z1))) - ((cosh_C /. z1) * (cosh_C /. z1)) ; hence (sinh_C /. z1) * (sinh_C /. z1) = ((cosh_C /. z1) * (cosh_C /. z1)) - 1 ; ::_thesis: verum end; theorem :: SIN_COS3:62 for z1, z2 being Element of COMPLEX holds ( (cosh_C /. (2 * z1)) + (cosh_C /. (2 * z2)) = (2 * (cosh_C /. (z1 + z2))) * (cosh_C /. (z1 - z2)) & (cosh_C /. (2 * z1)) - (cosh_C /. (2 * z2)) = (2 * (sinh_C /. (z1 + z2))) * (sinh_C /. (z1 - z2)) ) proof let z1, z2 be Element of COMPLEX ; ::_thesis: ( (cosh_C /. (2 * z1)) + (cosh_C /. (2 * z2)) = (2 * (cosh_C /. (z1 + z2))) * (cosh_C /. (z1 - z2)) & (cosh_C /. (2 * z1)) - (cosh_C /. (2 * z2)) = (2 * (sinh_C /. (z1 + z2))) * (sinh_C /. (z1 - z2)) ) A1: (2 * (sinh_C /. (z1 + z2))) * (sinh_C /. (z1 - z2)) = 2 * ((sinh_C /. (z1 + z2)) * (sinh_C /. (z1 - z2))) .= 2 * (((cosh_C /. z1) * (cosh_C /. z1)) - ((cosh_C /. z2) * (cosh_C /. z2))) by Th59 .= ((((2 * (cosh_C /. z1)) * (cosh_C /. z1)) - 1) + 1) - (2 * ((cosh_C /. z2) * (cosh_C /. z2))) .= ((cosh_C /. (2 * z1)) + 1) - (2 * ((cosh_C /. z2) * (cosh_C /. z2))) by Th58 .= (cosh_C /. (2 * z1)) - (((2 * (cosh_C /. z2)) * (cosh_C /. z2)) - 1) ; (2 * (cosh_C /. (z1 + z2))) * (cosh_C /. (z1 - z2)) = 2 * ((cosh_C /. (z1 + z2)) * (cosh_C /. (z1 - z2))) .= 2 * (((sinh_C /. z1) * (sinh_C /. z1)) + ((cosh_C /. z2) * (cosh_C /. z2))) by Th60 .= 2 * ((((cosh_C /. z1) * (cosh_C /. z1)) - 1) + ((cosh_C /. z2) * (cosh_C /. z2))) by Lm5 .= (((2 * (cosh_C /. z1)) * (cosh_C /. z1)) - 1) + (((2 * (cosh_C /. z2)) * (cosh_C /. z2)) - 1) .= (cosh_C /. (2 * z1)) + (((2 * (cosh_C /. z2)) * (cosh_C /. z2)) - 1) by Th58 .= (cosh_C /. (2 * z1)) + (cosh_C /. (2 * z2)) by Th58 ; hence ( (cosh_C /. (2 * z1)) + (cosh_C /. (2 * z2)) = (2 * (cosh_C /. (z1 + z2))) * (cosh_C /. (z1 - z2)) & (cosh_C /. (2 * z1)) - (cosh_C /. (2 * z2)) = (2 * (sinh_C /. (z1 + z2))) * (sinh_C /. (z1 - z2)) ) by A1, Th58; ::_thesis: verum end;