Assumptions:
TeX:
\left|x + y i\right| = \sqrt{{x}^{2} + {y}^{2}}
x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R}Definitions:
| Fungrim symbol | Notation | Short description |
|---|---|---|
| Abs | Absolute value | |
| ConstI | Imaginary unit | |
| Sqrt | Principal square root | |
| Pow | Power | |
| RR | Real numbers |
Source code for this entry:
Entry(ID("4f0049"),
Formula(Equal(Abs(Add(x, Mul(y, ConstI))), Sqrt(Add(Pow(x, 2), Pow(y, 2))))),
Variables(x, y),
Assumptions(And(Element(x, RR), Element(y, RR))))