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))))