Fungrim home page

Fungrim entry: 4f0049

x+yi=x2+y2\left|x + y i\right| = \sqrt{{x}^{2} + {y}^{2}}
Assumptions:xRandyRx \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R}
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
Absz\left|z\right| Absolute value
ConstIii Imaginary unit
Sqrtz\sqrt{z} Principal square root
Powab{a}^{b} Power
RRR\mathbb{R} 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))))

Topics using this entry

Copyright (C) Fredrik Johansson and contributors. Fungrim is provided under the MIT license. The source code is on GitHub.

2019-09-19 20:12:49.583742 UTC