Assumptions:
TeX:
\operatorname{Im}\!\left(\sin\!\left(x + i y\right)\right) = \cos(x) \sinh(y)
x \in \mathbb{R} \;\mathbin{\operatorname{and}}\; y \in \mathbb{R}Definitions:
| Fungrim symbol | Notation | Short description |
|---|---|---|
| Im | Imaginary part | |
| Sin | Sine | |
| ConstI | Imaginary unit | |
| Cos | Cosine | |
| RR | Real numbers |
Source code for this entry:
Entry(ID("037a6e"),
Formula(Equal(Im(Sin(Add(x, Mul(ConstI, y)))), Mul(Cos(x), Sinh(y)))),
Variables(x, y),
Assumptions(And(Element(x, RR), Element(y, RR))))