environ
vocabularies HIDDEN, SUBSET_1, NUMBERS, FUNCT_1, ORDINAL2, XCMPLX_0, RELAT_1, ARYTM_1, ARYTM_3, PARTFUN1, COMPLEX1, SIN_COS, CARD_1, SIN_COS2, PREPOWER, SIN_COS3, FUNCT_7, REAL_1, NEWTON, NAT_1;
notations HIDDEN, SUBSET_1, FUNCT_1, ORDINAL1, NUMBERS, XCMPLX_0, COMPLEX1, XREAL_0, REAL_1, NAT_1, PARTFUN1, FUNCT_2, COMSEQ_3, SIN_COS, SIN_COS2;
definitions FUNCT_2;
theorems COMPLEX1, SIN_COS, SIN_COS2, COMSEQ_3, XCMPLX_0, NUMBERS, XREAL_0;
schemes NAT_1, FUNCT_2;
registrations NUMBERS, XCMPLX_0, MEMBERED, RELSET_1, XREAL_0, SIN_COS, VALUED_0, CFUNCT_1;
constructors HIDDEN, FUNCT_4, ARYTM_0, REAL_1, NAT_1, BINOP_2, PARTFUN1, COMSEQ_3, SIN_COS, SIN_COS2, RVSUM_1, XXREAL_0, FCONT_1;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities ;
expansions ;
Lm1:
for z being Complex holds sinh_C /. z = ((exp z) - (exp (- z))) / 2
by Def3;
Lm2:
for z being Complex holds cosh_C /. z = ((exp z) + (exp (- z))) / 2
by Def4;
Lm3:
for z being Complex holds (exp z) * (exp (- z)) = 1
Lm4:
for x, y being Real holds exp (x + (y * <i>)) = (exp_R x) * ((cos y) + ((sin y) * <i>))
Lm5:
for z1 being Complex holds (sinh_C /. z1) * (sinh_C /. z1) = ((cosh_C /. z1) * (cosh_C /. z1)) - 1