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