Powers

Symbol: Pow —

{a}^{b}

— Power

The following table lists conditions such that Pow(a, b) is defined in Fungrim.

Domain	Codomain
Numbers
$a \in \mathbb{C} \setminus 0 \,\mathbin{\operatorname{and}}\, b \in \mathbb{C}$	${a}^{b} \in \mathbb{C}$
$a \in \mathbb{C} \,\mathbin{\operatorname{and}}\, b \in \left\{0\right\}$	${a}^{b} \in \left\{1\right\}$
Infinities
$a \in \left\{\infty, -\infty, {\tilde \infty}\right\} \,\mathbin{\operatorname{and}}\, b \in \{-1, -2, \ldots\}$	${a}^{b} \in \left\{0\right\}$
General domains
$a \in R \,\mathbin{\operatorname{and}}\, R \in \operatorname{Rings} \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}_{\ge 0}$	${a}^{b} \in R$
$a \in K \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, K \in \operatorname{Fields} \,\mathbin{\operatorname{and}}\, \mathbb{Q} \subseteq K \,\mathbin{\operatorname{and}}\, b \in \mathbb{Z}$	${a}^{b} \in R$

Table data:

\left(P, Q\right)

such that

\left(P\right) \implies \left(Q\right)

Definitions:

Fungrim symbol	Notation	Short description
`Pow`	${a}^{b}$	Power
`CC`	$\mathbb{C}$	Complex numbers
`Infinity`	$\infty$	Positive infinity
`UnsignedInfinity`	${\tilde \infty}$	Unsigned infinity
`ZZLessEqual`	$\mathbb{Z}_{\le n}$	Integers less than or equal to n
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n
`QQ`	$\mathbb{Q}$	Rational numbers
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("ef9f8a"),
    SymbolDefinition(Pow, Pow(a, b), "Power"),
    Description(""),
    Description("The following table lists conditions such that", SourceForm(Pow(a, b)), "is defined in Fungrim."),
    Table(TableRelation(Tuple(P, Q), Implies(P, Q)), TableHeadings(Description("Domain"), Description("Codomain")), List(TableSection("Numbers"), Tuple(And(Element(a, SetMinus(CC, 0)), Element(b, CC)), Element(Pow(a, b), CC)), Tuple(And(Element(a, CC), Element(b, Set(0))), Element(Pow(a, b), Set(1))), TableSection("Infinities"), Tuple(And(Element(a, Set(Infinity, Neg(Infinity), UnsignedInfinity)), Element(b, ZZLessEqual(-1))), Element(Pow(a, b), Set(0))), TableSection("General domains"), Tuple(And(Element(a, R), Element(R, Rings), Element(b, ZZGreaterEqual(0))), Element(Pow(a, b), R)), Tuple(And(Element(a, SetMinus(K, Set(0))), Element(K, Fields), SubsetEqual(QQ, K), Element(b, ZZ)), Element(Pow(a, b), R)))))

d316bc

{0}^{0} = 1

TeX:

{0}^{0} = 1

Definitions:

Fungrim symbol	Notation	Short description
`Pow`	${a}^{b}$	Power

Source code for this entry:

Entry(ID("d316bc"),
    Formula(Equal(Pow(0, 0), 1)))

310f36

{z}^{0} = 1

Assumptions:

z \in \mathbb{C}

z \in R \,\mathbin{\operatorname{and}}\, R \in \operatorname{Rings} \,\mathbin{\operatorname{and}}\, \mathbb{Z} \subseteq R

TeX:

{z}^{0} = 1

z \in \mathbb{C}

Definitions:

Fungrim symbol	Notation	Short description
`Pow`	${a}^{b}$	Power
`CC`	$\mathbb{C}$	Complex numbers
`ZZ`	$\mathbb{Z}$	Integers

Source code for this entry:

Entry(ID("310f36"),
    Formula(Equal(Pow(z, 0), 1)),
    Variables(z),
    Assumptions(Element(z, CC)),
    And(Element(z, R), Element(R, Rings), SubsetEqual(ZZ, R)))

a249f6

{z}^{1} = z

Assumptions:

z \in \mathbb{C}

z \in R \,\mathbin{\operatorname{and}}\, R \in \operatorname{Rings}

TeX:

{z}^{1} = z

z \in \mathbb{C}

Definitions:

Fungrim symbol	Notation	Short description
`Pow`	${a}^{b}$	Power
`CC`	$\mathbb{C}$	Complex numbers

Source code for this entry:

Entry(ID("a249f6"),
    Formula(Equal(Pow(z, 1), z)),
    Variables(z),
    Assumptions(Element(z, CC)),
    And(Element(z, R), Element(R, Rings)))

6c2b31

{z}^{n + 1} = {z}^{n} z

Assumptions:

z \in \mathbb{C} \,\mathbin{\operatorname{and}}\, n \in \mathbb{Z}_{\ge 0}

Alternative assumptions:

z \in R \,\mathbin{\operatorname{and}}\, R \in \operatorname{Rings} \,\mathbin{\operatorname{and}}\, n \in \mathbb{Z}_{\ge 0}

TeX:

{z}^{n + 1} = {z}^{n} z

z \in \mathbb{C} \,\mathbin{\operatorname{and}}\, n \in \mathbb{Z}_{\ge 0}

z \in R \,\mathbin{\operatorname{and}}\, R \in \operatorname{Rings} \,\mathbin{\operatorname{and}}\, n \in \mathbb{Z}_{\ge 0}

Definitions:

Fungrim symbol	Notation	Short description
`Pow`	${a}^{b}$	Power
`CC`	$\mathbb{C}$	Complex numbers
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("6c2b31"),
    Formula(Mul(Equal(Pow(z, Add(n, 1)), Pow(z, n)), z)),
    Variables(z, n),
    Assumptions(And(Element(z, CC), Element(n, ZZGreaterEqual(0))), And(Element(z, R), Element(R, Rings), Element(n, ZZGreaterEqual(0)))))

c53d94

{z}^{-1} = \frac{1}{z}

Assumptions:

z \in \mathbb{C}

Alternative assumptions:

z \in K \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, K \in \operatorname{Fields} \,\mathbin{\operatorname{and}}\, \mathbb{Q} \subseteq K

TeX:

{z}^{-1} = \frac{1}{z}

z \in \mathbb{C}

z \in K \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, K \in \operatorname{Fields} \,\mathbin{\operatorname{and}}\, \mathbb{Q} \subseteq K

Definitions:

Fungrim symbol	Notation	Short description
`Pow`	${a}^{b}$	Power
`CC`	$\mathbb{C}$	Complex numbers
`QQ`	$\mathbb{Q}$	Rational numbers

Source code for this entry:

Entry(ID("c53d94"),
    Formula(Equal(Pow(z, -1), Div(1, z))),
    Variables(z),
    Assumptions(Element(z, CC), And(Element(z, SetMinus(K, Set(0))), Element(K, Fields), SubsetEqual(QQ, K))))

4d6416

{a}^{b} = \exp\!\left(b \log\!\left(a\right)\right)

Assumptions:

a \in \mathbb{C} \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, b \in \mathbb{C}

TeX:

{a}^{b} = \exp\!\left(b \log\!\left(a\right)\right)

a \in \mathbb{C} \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, b \in \mathbb{C}

Definitions:

Fungrim symbol	Notation	Short description
`Pow`	${a}^{b}$	Power
`Exp`	${e}^{z}$	Exponential function
`Log`	$\log\!\left(z\right)$	Natural logarithm
`CC`	$\mathbb{C}$	Complex numbers

Source code for this entry:

Entry(ID("4d6416"),
    Formula(Equal(Pow(a, b), Exp(Mul(b, Log(a))))),
    Variables(a, b),
    Assumptions(And(Element(a, SetMinus(CC, Set(0))), Element(b, CC))))

634687

{z}^{1 / 2} = \sqrt{z}

Assumptions:

z \in \mathbb{C}

TeX:

{z}^{1 / 2} = \sqrt{z}

z \in \mathbb{C}

Definitions:

Fungrim symbol	Notation	Short description
`Pow`	${a}^{b}$	Power
`Sqrt`	$\sqrt{z}$	Principal square root
`CC`	$\mathbb{C}$	Complex numbers

Source code for this entry:

Entry(ID("634687"),
    Formula(Equal(Pow(z, Div(1, 2)), Sqrt(z))),
    Variables(z),
    Assumptions(Element(z, CC)))

2e0d99

{z}^{-1 / 2} = \frac{1}{\sqrt{z}}

Assumptions:

z \in \mathbb{C} \setminus \left\{0\right\}

TeX:

{z}^{-1 / 2} = \frac{1}{\sqrt{z}}

z \in \mathbb{C} \setminus \left\{0\right\}

Definitions:

Fungrim symbol	Notation	Short description
`Pow`	${a}^{b}$	Power
`Sqrt`	$\sqrt{z}$	Principal square root
`CC`	$\mathbb{C}$	Complex numbers

Source code for this entry:

Entry(ID("2e0d99"),
    Formula(Equal(Pow(z, Neg(Div(1, 2))), Div(1, Sqrt(z)))),
    Variables(z),
    Assumptions(Element(z, SetMinus(CC, Set(0)))))

0aac97

{\left(a + b i\right)}^{c + d i} = {M}^{c} {e}^{-d \theta} \left(\cos\!\left(c \theta + d \log\!\left(M\right)\right) + i \sin\!\left(c \theta + d \log\!\left(M\right)\right)\right)\; \text{ where } M = \left|a + b i\right|,\,\theta = \arg\!\left(a + b i\right)

Assumptions:

a \in \mathbb{R} \,\mathbin{\operatorname{and}}\, b \in \mathbb{R} \,\mathbin{\operatorname{and}}\, c \in \mathbb{R} \,\mathbin{\operatorname{and}}\, d \in \mathbb{R} \,\mathbin{\operatorname{and}}\, a + b i \ne 0

TeX:

{\left(a + b i\right)}^{c + d i} = {M}^{c} {e}^{-d \theta} \left(\cos\!\left(c \theta + d \log\!\left(M\right)\right) + i \sin\!\left(c \theta + d \log\!\left(M\right)\right)\right)\; \text{ where } M = \left|a + b i\right|,\,\theta = \arg\!\left(a + b i\right)

a \in \mathbb{R} \,\mathbin{\operatorname{and}}\, b \in \mathbb{R} \,\mathbin{\operatorname{and}}\, c \in \mathbb{R} \,\mathbin{\operatorname{and}}\, d \in \mathbb{R} \,\mathbin{\operatorname{and}}\, a + b i \ne 0

Definitions:

Fungrim symbol	Notation	Short description
`Pow`	${a}^{b}$	Power
`ConstI`	$i$	Imaginary unit
`Exp`	${e}^{z}$	Exponential function
`Log`	$\log\!\left(z\right)$	Natural logarithm
`Sin`	$\sin\!\left(z\right)$	Sine
`Abs`	$\left\|z\right\|$	Absolute value
`Arg`	$\arg\!\left(z\right)$	Complex argument
`RR`	$\mathbb{R}$	Real numbers

Source code for this entry:

Entry(ID("0aac97"),
    Formula(Equal(Pow(Add(a, Mul(b, ConstI)), Add(c, Mul(d, ConstI))), Where(Mul(Mul(Pow(M, c), Exp(Neg(Mul(d, theta)))), Add(Cos(Add(Mul(c, theta), Mul(d, Log(M)))), Mul(ConstI, Sin(Add(Mul(c, theta), Mul(d, Log(M))))))), Equal(M, Abs(Add(a, Mul(b, ConstI)))), Equal(theta, Arg(Add(a, Mul(b, ConstI))))))),
    Variables(a, b, c, d),
    Assumptions(And(Element(a, RR), Element(b, RR), Element(c, RR), Element(d, RR), Unequal(Add(a, Mul(b, ConstI)), 0))))

bc4d0a

\left|{\left(a + b i\right)}^{c + d i}\right| = {M}^{c} {e}^{-d \theta}\; \text{ where } M = \left|a + b i\right|,\,\theta = \arg\!\left(a + b i\right)

Assumptions:

a \in \mathbb{R} \,\mathbin{\operatorname{and}}\, b \in \mathbb{R} \,\mathbin{\operatorname{and}}\, c \in \mathbb{R} \,\mathbin{\operatorname{and}}\, d \in \mathbb{R} \,\mathbin{\operatorname{and}}\, a + b i \ne 0

TeX:

\left|{\left(a + b i\right)}^{c + d i}\right| = {M}^{c} {e}^{-d \theta}\; \text{ where } M = \left|a + b i\right|,\,\theta = \arg\!\left(a + b i\right)

a \in \mathbb{R} \,\mathbin{\operatorname{and}}\, b \in \mathbb{R} \,\mathbin{\operatorname{and}}\, c \in \mathbb{R} \,\mathbin{\operatorname{and}}\, d \in \mathbb{R} \,\mathbin{\operatorname{and}}\, a + b i \ne 0

Definitions:

Fungrim symbol	Notation	Short description
`Abs`	$\left\|z\right\|$	Absolute value
`Pow`	${a}^{b}$	Power
`ConstI`	$i$	Imaginary unit
`Exp`	${e}^{z}$	Exponential function
`Arg`	$\arg\!\left(z\right)$	Complex argument
`RR`	$\mathbb{R}$	Real numbers

Source code for this entry:

Entry(ID("bc4d0a"),
    Formula(Equal(Abs(Pow(Add(a, Mul(b, ConstI)), Add(c, Mul(d, ConstI)))), Where(Mul(Pow(M, c), Exp(Neg(Mul(d, theta)))), Equal(M, Abs(Add(a, Mul(b, ConstI)))), Equal(theta, Arg(Add(a, Mul(b, ConstI))))))),
    Variables(a, b, c, d),
    Assumptions(And(Element(a, RR), Element(b, RR), Element(c, RR), Element(d, RR), Unequal(Add(a, Mul(b, ConstI)), 0))))

caf8cf

\operatorname{Re}\!\left({\left(a + b i\right)}^{c + d i}\right) = {M}^{c} {e}^{-d \theta} \cos\!\left(c \theta + d \log\!\left(M\right)\right)\; \text{ where } M = \left|a + b i\right|,\,\theta = \arg\!\left(a + b i\right)

Assumptions:

a \in \mathbb{R} \,\mathbin{\operatorname{and}}\, b \in \mathbb{R} \,\mathbin{\operatorname{and}}\, c \in \mathbb{R} \,\mathbin{\operatorname{and}}\, d \in \mathbb{R} \,\mathbin{\operatorname{and}}\, a + b i \ne 0

TeX:

\operatorname{Re}\!\left({\left(a + b i\right)}^{c + d i}\right) = {M}^{c} {e}^{-d \theta} \cos\!\left(c \theta + d \log\!\left(M\right)\right)\; \text{ where } M = \left|a + b i\right|,\,\theta = \arg\!\left(a + b i\right)

a \in \mathbb{R} \,\mathbin{\operatorname{and}}\, b \in \mathbb{R} \,\mathbin{\operatorname{and}}\, c \in \mathbb{R} \,\mathbin{\operatorname{and}}\, d \in \mathbb{R} \,\mathbin{\operatorname{and}}\, a + b i \ne 0

Definitions:

Fungrim symbol	Notation	Short description
`Re`	$\operatorname{Re}\!\left(z\right)$	Real part
`Pow`	${a}^{b}$	Power
`ConstI`	$i$	Imaginary unit
`Exp`	${e}^{z}$	Exponential function
`Log`	$\log\!\left(z\right)$	Natural logarithm
`Abs`	$\left\|z\right\|$	Absolute value
`Arg`	$\arg\!\left(z\right)$	Complex argument
`RR`	$\mathbb{R}$	Real numbers

Source code for this entry:

Entry(ID("caf8cf"),
    Formula(Equal(Re(Pow(Add(a, Mul(b, ConstI)), Add(c, Mul(d, ConstI)))), Where(Mul(Mul(Pow(M, c), Exp(Neg(Mul(d, theta)))), Cos(Add(Mul(c, theta), Mul(d, Log(M))))), Equal(M, Abs(Add(a, Mul(b, ConstI)))), Equal(theta, Arg(Add(a, Mul(b, ConstI))))))),
    Variables(a, b, c, d),
    Assumptions(And(Element(a, RR), Element(b, RR), Element(c, RR), Element(d, RR), Unequal(Add(a, Mul(b, ConstI)), 0))))

18873d

\operatorname{Im}\!\left({\left(a + b i\right)}^{c + d i}\right) = {M}^{c} {e}^{-d \theta} \sin\!\left(c \theta + d \log\!\left(M\right)\right)\; \text{ where } M = \left|a + b i\right|,\,\theta = \arg\!\left(a + b i\right)

Assumptions:

a \in \mathbb{R} \,\mathbin{\operatorname{and}}\, b \in \mathbb{R} \,\mathbin{\operatorname{and}}\, c \in \mathbb{R} \,\mathbin{\operatorname{and}}\, d \in \mathbb{R} \,\mathbin{\operatorname{and}}\, a + b i \ne 0

TeX:

\operatorname{Im}\!\left({\left(a + b i\right)}^{c + d i}\right) = {M}^{c} {e}^{-d \theta} \sin\!\left(c \theta + d \log\!\left(M\right)\right)\; \text{ where } M = \left|a + b i\right|,\,\theta = \arg\!\left(a + b i\right)

a \in \mathbb{R} \,\mathbin{\operatorname{and}}\, b \in \mathbb{R} \,\mathbin{\operatorname{and}}\, c \in \mathbb{R} \,\mathbin{\operatorname{and}}\, d \in \mathbb{R} \,\mathbin{\operatorname{and}}\, a + b i \ne 0

Definitions:

Fungrim symbol	Notation	Short description
`Im`	$\operatorname{Im}\!\left(z\right)$	Imaginary part
`Pow`	${a}^{b}$	Power
`ConstI`	$i$	Imaginary unit
`Exp`	${e}^{z}$	Exponential function
`Sin`	$\sin\!\left(z\right)$	Sine
`Log`	$\log\!\left(z\right)$	Natural logarithm
`Abs`	$\left\|z\right\|$	Absolute value
`Arg`	$\arg\!\left(z\right)$	Complex argument
`RR`	$\mathbb{R}$	Real numbers

Source code for this entry:

Entry(ID("18873d"),
    Formula(Equal(Im(Pow(Add(a, Mul(b, ConstI)), Add(c, Mul(d, ConstI)))), Where(Mul(Mul(Pow(M, c), Exp(Neg(Mul(d, theta)))), Sin(Add(Mul(c, theta), Mul(d, Log(M))))), Equal(M, Abs(Add(a, Mul(b, ConstI)))), Equal(theta, Arg(Add(a, Mul(b, ConstI))))))),
    Variables(a, b, c, d),
    Assumptions(And(Element(a, RR), Element(b, RR), Element(c, RR), Element(d, RR), Unequal(Add(a, Mul(b, ConstI)), 0))))

2090c3

{\left(x y\right)}^{a} = {x}^{a} {y}^{a} \exp\!\left(2 \pi i a \left\lfloor \frac{\pi - \arg\!\left(x\right) - \arg\!\left(y\right)}{2 \pi} \right\rfloor\right)

Assumptions:

x \in \mathbb{C} \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, y \in \mathbb{C} \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, a \in \mathbb{C}

TeX:

{\left(x y\right)}^{a} = {x}^{a} {y}^{a} \exp\!\left(2 \pi i a \left\lfloor \frac{\pi - \arg\!\left(x\right) - \arg\!\left(y\right)}{2 \pi} \right\rfloor\right)

x \in \mathbb{C} \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, y \in \mathbb{C} \setminus \left\{0\right\} \,\mathbin{\operatorname{and}}\, a \in \mathbb{C}

Definitions:

Fungrim symbol	Notation	Short description
`Pow`	${a}^{b}$	Power
`Exp`	${e}^{z}$	Exponential function
`ConstPi`	$\pi$	The constant pi (3.14...)
`ConstI`	$i$	Imaginary unit
`Arg`	$\arg\!\left(z\right)$	Complex argument
`CC`	$\mathbb{C}$	Complex numbers

Source code for this entry:

Entry(ID("2090c3"),
    Formula(Equal(Pow(Mul(x, y), a), Mul(Mul(Pow(x, a), Pow(y, a)), Exp(Mul(Mul(Mul(Mul(2, ConstPi), ConstI), a), Floor(Div(Sub(Sub(ConstPi, Arg(x)), Arg(y)), Mul(2, ConstPi)))))))),
    Variables(x, y, a),
    Assumptions(And(Element(x, SetMinus(CC, Set(0))), Element(y, SetMinus(CC, Set(0))), Element(a, CC))))

Integer exponents

Elementary functions

Complex parts

Expansion